English
There is no minimal solution with an odd a and positive c under the Fermat42 framework; any would yield a contradiction.
Русский
Не существует минимального решения с нечетным a и положительным c в рамках Фермат42; любое такое решение ведет к противоречию.
LaTeX
$$$\forall a,b,c \; (\text{Fermat42.Minimal } a\, b\, c \,\wedge\; a \equiv 1 \pmod 2 \wedge c > 0) \rightarrow \text{False}$$$
Lean4
theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0 < c) : False := by
-- Use the fact that a ^ 2, b ^ 2, c form a pythagorean triple to obtain m and n such that
-- a ^ 2 = m ^ 2 - n ^ 2, b ^ 2 = 2 * m * n and c = m ^ 2 + n ^ 2
-- first the formula:
have ht : PythagoreanTriple (a ^ 2) (b ^ 2) c :=
by
delta PythagoreanTriple
linear_combination
h.1.2.2
-- coprime requirement:
have h2 : Int.gcd (a ^ 2) (b ^ 2) = 1 := Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal h).pow
have ha22 : a ^ 2 % 2 = 1 := by
rw [sq, Int.mul_emod, ha2]
decide
obtain ⟨m, n, ht1, ht2, ht3, ht4, ht5, ht6⟩ := ht.coprime_classification' h2 ha22 hc
have htt : PythagoreanTriple a n m := by
delta PythagoreanTriple
linear_combination ht1
have h3 : Int.gcd a n = 1 := by
apply Int.isCoprime_iff_gcd_eq_one.mp
apply @IsCoprime.of_mul_left_left _ _ _ a
rw [← sq, ht1, (by ring : m ^ 2 - n ^ 2 = m ^ 2 + -n * n)]
exact
(Int.isCoprime_iff_gcd_eq_one.mpr ht4).pow_left.add_mul_right_left
(-n)
-- m is positive because b is non-zero and b ^ 2 = 2 * m * n and we already have 0 ≤ m.
have hb20 : b ^ 2 ≠ 0 := mt pow_eq_zero h.1.2.1
have h4 : 0 < m := by
apply lt_of_le_of_ne ht6
rintro rfl
omega
obtain ⟨r, s, _, htt2, htt3, htt4, htt5, htt6⟩ := htt.coprime_classification' h3 ha2 h4
have hcp : Int.gcd m (r * s) = 1 := by
rw [htt3]
exact
Int.isCoprime_iff_gcd_eq_one.mp
(Int.isCoprime_of_sq_sum' (Int.isCoprime_iff_gcd_eq_one.mpr htt4))
-- b is even because b ^ 2 = 2 * m * n.
have hb2 : 2 ∣ b := by
apply @Int.Prime.dvd_pow' _ 2 _ Nat.prime_two
rw [ht2, mul_assoc]
exact dvd_mul_right 2 (m * n)
obtain ⟨b', hb2'⟩ := hb2
have hs : b' ^ 2 = m * (r * s) := by
apply (mul_right_inj' (by simp : (4 : ℤ) ≠ 0)).mp
linear_combination (-b - 2 * b') * hb2' + ht2 + 2 * m * htt2
have hrsz : r * s ≠ 0 := by grind
have h2b0 : b' ≠ 0 := by grind
obtain ⟨i, hi⟩ := Int.sq_of_gcd_eq_one hcp hs.symm
have hi' : ¬m = -i ^ 2 := by
by_contra h1
have hit : -i ^ 2 ≤ 0 := neg_nonpos.mpr (sq_nonneg i)
rw [← h1] at hit
apply absurd h4 (not_lt.mpr hit)
replace hi : m = i ^ 2 := Or.resolve_right hi hi'
rw [mul_comm] at hs
rw [Int.gcd_comm] at hcp
obtain ⟨d, hd⟩ := Int.sq_of_gcd_eq_one hcp hs.symm
have hd' : ¬r * s = -d ^ 2 := by
by_contra h1
rw [h1] at hs
have h2 : b' ^ 2 ≤ 0 := by
rw [hs, (by ring : -d ^ 2 * m = -(d ^ 2 * m))]
exact neg_nonpos.mpr ((mul_nonneg_iff_of_pos_right h4).mpr (sq_nonneg d))
have h2' : 0 ≤ b' ^ 2 := by apply sq_nonneg b'
exact absurd (lt_of_le_of_ne h2' (Ne.symm (pow_ne_zero _ h2b0))) (not_lt.mpr h2)
replace hd : r * s = d ^ 2 := Or.resolve_right hd hd'
obtain ⟨j, hj⟩ := Int.sq_of_gcd_eq_one htt4 hd
have hj0 : j ≠ 0 := by grind
rw [mul_comm] at hd
rw [Int.gcd_comm] at htt4
obtain ⟨k, hk⟩ := Int.sq_of_gcd_eq_one htt4 hd
have hk0 : k ≠ 0 := by grind
have hj2 : r ^ 2 = j ^ 4 := by grind
have hk2 : s ^ 2 = k ^ 4 := by
grind
-- from m = r ^ 2 + s ^ 2 we now get a new solution to a ^ 4 + b ^ 4 = c ^ 2:
have hh : i ^ 2 = j ^ 4 + k ^ 4 := by grind
have hn : n ≠ 0 := by
grind
-- and it has a smaller c: from c = m ^ 2 + n ^ 2 we see that m is smaller than c, and i ^ 2 = m.
have hic : Int.natAbs i < Int.natAbs c := by
apply Int.ofNat_lt.mp
rw [← Int.eq_natAbs_of_nonneg (le_of_lt hc)]
apply lt_of_le_of_lt (Int.natAbs_le_self_sq i)
rw [← hi, ht3]
apply lt_of_le_of_lt (Int.le_self_sq m)
exact lt_add_of_pos_right (m ^ 2) (sq_pos_of_ne_zero hn)
have hic' : Int.natAbs c ≤ Int.natAbs i := by
apply h.2 j k i
exact ⟨hj0, hk0, hh.symm⟩
apply absurd (not_le_of_gt hic) (not_not.mpr hic')
