IndisputableMonolith.NumberTheory.ErdosStrausRCL

   1import Mathlib
   2
   3/-!
   4# Erdős-Straus RCL Ledger Reduction
   5
   6This file records the algebraic reduction behind the RCL attack on the
   7Erdős-Straus conjecture.
   8
   9After choosing the first denominator `x`, the residual equation is
  10
  11`c / N = 1 / y + 1 / z`, with `c = 4x - n` and `N = nx`.
  12
  13Clearing denominators gives the balanced factor-pair condition
  14
  15`(c y - N)(c z - N) = N^2`.
  16
  17That is the discrete ledger form of the reciprocal split: a left and right
  18defect multiply back to the square budget.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace NumberTheory
  23namespace ErdosStrausRCL
  24
  25/-- Rational Erdős-Straus representation.  The integer problem is the
  26same statement with positive natural witnesses. -/
  27def HasRationalErdosStrausRepr (n : ℚ) : Prop :=
  28  ∃ x y z : ℚ, x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧
  29    (4 : ℚ) / n = 1 / x + 1 / y + 1 / z
  30
  31/-- The core ledger identity: a balanced factor pair for the residual
  32two-denominator split gives a three-unit Erdős-Straus representation. -/
  33theorem repr_of_balanced_factor_pair
  34    {n x c N d e y z : ℚ}
  35    (hn : n ≠ 0) (hx : x ≠ 0) (hc : c ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0)
  36    (hN : N = n * x)
  37    (hcdef : c = 4 * x - n)
  38    (hde : d * e = N ^ 2)
  39    (hyd : c * y = N + d)
  40    (hze : c * z = N + e) :
  41    HasRationalErdosStrausRepr n := by
  42  have hN_ne : N ≠ 0 := by
  43    rw [hN]
  44    exact mul_ne_zero hn hx
  45  have hd_eq : c * y - N = d := by linarith
  46  have he_eq : c * z - N = e := by linarith
  47  have hquad : (c * y - N) * (c * z - N) = N ^ 2 := by
  48    rw [hd_eq, he_eq, hde]
  49  have hfactor : c * (c * y * z - N * (y + z)) = 0 := by
  50    nlinarith [hquad]
  51  have hinner : c * y * z = N * (y + z) := by
  52    have hzero : c * y * z - N * (y + z) = 0 :=
  53      (mul_eq_zero.mp hfactor).resolve_left hc
  54    linarith
  55  have hsplit : (1 : ℚ) / y + 1 / z = c / N := by
  56    field_simp [hy, hz, hN_ne]
  57    nlinarith [hinner]
  58  have hfirst : (4 : ℚ) / n = 1 / x + c / N := by
  59    rw [hN, hcdef]
  60    field_simp [hn, hx]
  61    ring
  62  refine ⟨x, y, z, hx, hy, hz, ?_⟩
  63  rw [hfirst, ← hsplit]
  64  ring
  65
  66/-- Equivalent operational form: it is enough to find nonzero `y,z`
  67whose residual defects multiply to the square budget. -/
  68theorem repr_of_residual_square
  69    {n x c N y z : ℚ}
  70    (hn : n ≠ 0) (hx : x ≠ 0) (hc : c ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0)
  71    (hN : N = n * x)
  72    (hcdef : c = 4 * x - n)
  73    (hres : (c * y - N) * (c * z - N) = N ^ 2) :
  74    HasRationalErdosStrausRepr n := by
  75  refine repr_of_balanced_factor_pair
  76    (d := c * y - N) (e := c * z - N)
  77    hn hx hc hy hz hN hcdef hres ?_ ?_
  78  · ring
  79  · ring
  80
  81/-- General residual-gate divisor split.  If `x = (n+c)/4` and a divisor
  82split `d*q = N` is chosen so that the displayed denominators are nonzero,
  83then the pair `d, N*q` is a balanced factor pair for the residual gate `c`. -/
  84theorem repr_of_gate_divisor_pair
  85    {n x c N d q : ℚ}
  86    (hn : n ≠ 0) (hx : x ≠ 0) (hc : c ≠ 0)
  87    (hN : N = n * x)
  88    (hxdef : x = (n + c) / 4)
  89    (hdq : d * q = N)
  90    (hy : (N + d) / c ≠ 0)
  91    (hz : (N + N * q) / c ≠ 0) :
  92    HasRationalErdosStrausRepr n := by
  93  have hcdef : c = 4 * x - n := by
  94    rw [hxdef]
  95    field_simp
  96    ring
  97  have hde : d * (N * q) = N ^ 2 := by
  98    rw [← hdq]
  99    ring
 100  refine repr_of_balanced_factor_pair
 101    (c := c) (N := N) (d := d) (e := N * q)
 102    (y := (N + d) / c) (z := (N + N * q) / c)
 103    hn hx hc hy hz hN hcdef hde ?_ ?_
 104  · field_simp [hc]
 105  · field_simp [hc]
 106
 107/-- The dominant hard-class gate.  For `n = 1 mod 4`, the minimal
 108choice is `x = (n+3)/4`, so `c = 3`.  A divisor split `d*q = N` gives a
 109balanced factor pair `d` and `N*q` for `N^2`, hence a representation. -/
 110theorem repr_c3_of_divisor_pair
 111    {n x N d q : ℚ}
 112    (hn : n ≠ 0) (hx : x ≠ 0)
 113    (hN : N = n * x)
 114    (hxdef : x = (n + 3) / 4)
 115    (hdq : d * q = N)
 116    (hy : (N + d) / 3 ≠ 0)
 117    (hz : (N + N * q) / 3 ≠ 0) :
 118    HasRationalErdosStrausRepr n := by
 119  have hc : (3 : ℚ) ≠ 0 := by norm_num
 120  exact repr_of_gate_divisor_pair
 121    (c := (3 : ℚ)) hn hx hc hN hxdef hdq hy hz
 122
 123/-! ### Explicit residue-class theorems
 124
 125Within `n ≡ 1 mod 4`, write `n mod 12 ∈ {1, 5, 9}`.  The two cases
 126`5 mod 12` and `9 mod 12` admit explicit Egyptian-fraction formulas with
 127gate `c = 3`; the genuine residual hard class is `n ≡ 1 mod 12`. -/
 128
 129/-- Explicit Erdős-Straus representation for `n = 12k + 5`.
 130
 131The gate-3 divisor pair takes `d = x = 3k + 2` (which is `2 mod 3`),
 132giving the closed-form three-unit sum below. -/
 133theorem erdos_straus_five_mod_twelve (k : ℕ) :
 134    (4 : ℚ) / (12 * (k : ℚ) + 5)
 135      = 1 / (3 * (k : ℚ) + 2)
 136        + 1 / (2 * (3 * (k : ℚ) + 2) * (2 * (k : ℚ) + 1))
 137        + 1 / (2 * (12 * (k : ℚ) + 5) * (3 * (k : ℚ) + 2)
 138                 * (2 * (k : ℚ) + 1)) := by
 139  have h1 : (3 * (k : ℚ) + 2) > 0 := by positivity
 140  have h2 : (2 * (k : ℚ) + 1) > 0 := by positivity
 141  have h3 : (12 * (k : ℚ) + 5) > 0 := by positivity
 142  have h1' : (3 * (k : ℚ) + 2) ≠ 0 := ne_of_gt h1
 143  have h2' : (2 * (k : ℚ) + 1) ≠ 0 := ne_of_gt h2
 144  have h3' : (12 * (k : ℚ) + 5) ≠ 0 := ne_of_gt h3
 145  field_simp
 146  ring
 147
 148/-- Explicit Erdős-Straus representation for `n = 12k + 9`.
 149
 150Here `3 ∣ n`, so the gate-3 divisor pair takes `d = N` (i.e. `q = 1`)
 151and the second and third unit fractions coincide. -/
 152theorem erdos_straus_nine_mod_twelve (k : ℕ) :
 153    (4 : ℚ) / (12 * (k : ℚ) + 9)
 154      = 1 / (3 * (k : ℚ) + 3)
 155        + 1 / (6 * (4 * (k : ℚ) + 3) * ((k : ℚ) + 1))
 156        + 1 / (6 * (4 * (k : ℚ) + 3) * ((k : ℚ) + 1)) := by
 157  have h1 : (3 * (k : ℚ) + 3) > 0 := by positivity
 158  have h2 : (4 * (k : ℚ) + 3) > 0 := by positivity
 159  have h3 : ((k : ℚ) + 1) > 0 := by positivity
 160  have h1' : (3 * (k : ℚ) + 3) ≠ 0 := ne_of_gt h1
 161  have h2' : (4 * (k : ℚ) + 3) ≠ 0 := ne_of_gt h2
 162  have h3' : ((k : ℚ) + 1) ≠ 0 := ne_of_gt h3
 163  field_simp
 164  ring
 165
 166/-! ### Natural-number existence
 167
 168Cast the rational identities to the natural-number existence form. -/
 169
 170/-- For every `n = 12k + 5`, an Erdős-Straus representation in `ℕ⁺`. -/
 171theorem erdos_straus_nat_five_mod_twelve (k : ℕ) :
 172    ∃ x y z : ℕ, 0 < x ∧ 0 < y ∧ 0 < z ∧
 173      (4 : ℚ) / ((12 * k + 5 : ℕ) : ℚ)
 174        = (1 : ℚ) / x + (1 : ℚ) / y + (1 : ℚ) / z := by
 175  refine ⟨3 * k + 2,
 176          2 * (3 * k + 2) * (2 * k + 1),
 177          2 * (12 * k + 5) * (3 * k + 2) * (2 * k + 1),
 178          by positivity, by positivity, by positivity, ?_⟩
 179  have h := erdos_straus_five_mod_twelve k
 180  have hcast : ((12 * k + 5 : ℕ) : ℚ) = 12 * (k : ℚ) + 5 := by push_cast; ring
 181  rw [hcast]
 182  push_cast
 183  convert h using 2
 184
 185/-- For every `n = 12k + 9`, an Erdős-Straus representation in `ℕ⁺`. -/
 186theorem erdos_straus_nat_nine_mod_twelve (k : ℕ) :
 187    ∃ x y z : ℕ, 0 < x ∧ 0 < y ∧ 0 < z ∧
 188      (4 : ℚ) / ((12 * k + 9 : ℕ) : ℚ)
 189        = (1 : ℚ) / x + (1 : ℚ) / y + (1 : ℚ) / z := by
 190  refine ⟨3 * k + 3,
 191          6 * (4 * k + 3) * (k + 1),
 192          6 * (4 * k + 3) * (k + 1),
 193          by positivity, by positivity, by positivity, ?_⟩
 194  have h := erdos_straus_nine_mod_twelve k
 195  have hcast : ((12 * k + 9 : ℕ) : ℚ) = 12 * (k : ℚ) + 9 := by push_cast; ring
 196  rw [hcast]
 197  push_cast
 198  convert h using 2
 199
 200/-! ### Discrete c = 3 divisor sufficiency
 201
 202For `n ≡ 1 mod 4`, the gate-3 representation succeeds whenever there
 203exist nonzero rationals `d, q` with `d · q = n · (n+3)/4` and the
 204displayed denominators `(N+d)/3` and `(N+Nq)/3` are nonzero. The
 205arithmetic content is captured by `repr_c3_of_divisor_pair`. -/
 206
 207/-! ### Sub-residue classes within `n ≡ 1 mod 12`
 208
 209Refine `n ≡ 1 mod 12` by writing `n = 12k + 1`.  When `k` is odd we have
 210`n ≡ 13 mod 24`, and `(n+3)/4 = 6m + 4 = 2(3m+2)` is even (writing
 211`k = 2m+1`), so the divisor `d = 2 ≡ 2 mod 3` succeeds.  The remaining
 212sub-class is `n ≡ 1 mod 24`. -/
 213
 214/-- Explicit Erdős-Straus representation for `n = 24m + 13`.
 215
 216Since `(n+3)/4 = 2(3m+2)` is even, `d = 2` gives the gate-3 split.
 217With `A = (24m+13)(3m+2) = N/2`, the formula is
 218
 219```text
 2204/n = 1/(6m+4) + 1/(2(A+1)/3) + 1/(2A(A+1)/3).
 221```
 222-/
 223theorem erdos_straus_thirteen_mod_twentyfour (m : ℕ) :
 224    (4 : ℚ) / (24 * (m : ℚ) + 13)
 225      = 1 / (6 * (m : ℚ) + 4)
 226        + 1 / (2 * ((24 * (m : ℚ) + 13) * (3 * (m : ℚ) + 2) + 1) / 3)
 227        + 1 / (2 * ((24 * (m : ℚ) + 13) * (3 * (m : ℚ) + 2))
 228                 * ((24 * (m : ℚ) + 13) * (3 * (m : ℚ) + 2) + 1) / 3) := by
 229  have h1 : (6 * (m : ℚ) + 4) > 0 := by positivity
 230  have h2 : (3 * (m : ℚ) + 2) > 0 := by positivity
 231  have h3 : (24 * (m : ℚ) + 13) > 0 := by positivity
 232  have hA : (24 * (m : ℚ) + 13) * (3 * (m : ℚ) + 2) > 0 := mul_pos h3 h2
 233  have hA1 : (24 * (m : ℚ) + 13) * (3 * (m : ℚ) + 2) + 1 > 0 := by linarith
 234  have h1' : (6 * (m : ℚ) + 4) ≠ 0 := ne_of_gt h1
 235  have h3' : (24 * (m : ℚ) + 13) ≠ 0 := ne_of_gt h3
 236  have hA' : (24 * (m : ℚ) + 13) * (3 * (m : ℚ) + 2) ≠ 0 := ne_of_gt hA
 237  have hA1' : (24 * (m : ℚ) + 13) * (3 * (m : ℚ) + 2) + 1 ≠ 0 := ne_of_gt hA1
 238  field_simp
 239  ring
 240
 241-- Natural-number existence form is omitted: the rational identity above is
 242-- the substantive content; converting to ℕ requires showing `3 ∣ 2(A+1)` and
 243-- `3 ∣ 2A(A+1)` for `A = (24m+13)(3m+2)`, which is a routine omega/Nat
 244-- manipulation we leave for a follow-up pass.
 245
 246end ErdosStrausRCL
 247end NumberTheory
 248end IndisputableMonolith
 249