IndisputableMonolith.NumberTheory.Erdos_C7_Closure

   1import Mathlib
   2
   3/-!
   4# Erdős-Straus c = 7 Gate Closures
   5
   6For `n ≡ 1 mod 4`, the gate `c = 7` closes the residue classes
   7`n mod 7 ∈ {0, 3, 5, 6}` via explicit Egyptian-fraction formulas.
   8
   9These formulas extend the c = 3 closure layer.  Together with c = 11
  10and higher gates, the residual class for Erdős-Straus shrinks rapidly,
  11but never to zero in any fixed bound.
  12
  13The four parametric closures below collapse to the identity
  14
  15```text
  164/n = (n + 7) / (n · x) = 4/n   [since x = (n + 7)/4]
  17```
  18
  19with the remaining factors absorbed by the corresponding modular
  20divisor `n + 1`, `n + 2`, `2n + 1`, or `n` itself.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace NumberTheory
  25namespace Erdos_C7_Closure
  26
  27/-! ## Case `n ≡ 6 mod 7` (and `n ≡ 1 mod 4`)
  28
  29CRT residue: `n = 28j + 13`.  Choose `c = 7`, `x = 7j + 5`,
  30`n + 1 = 14(2j + 1)`.  Concrete trapped instance: `j = 15`, `n = 433`.
  31-/
  32
  33theorem erdos_straus_six_mod_seven (j : ℕ) :
  34    (4 : ℚ) / (28 * (j : ℚ) + 13)
  35      = 1 / (7 * (j : ℚ) + 5)
  36        + 1 / (2 * (7 * (j : ℚ) + 5) * (2 * (j : ℚ) + 1))
  37        + 1 / (2 * (28 * (j : ℚ) + 13) * (7 * (j : ℚ) + 5)
  38                 * (2 * (j : ℚ) + 1)) := by
  39  have h1 : (7 * (j : ℚ) + 5) > 0 := by positivity
  40  have h2 : (2 * (j : ℚ) + 1) > 0 := by positivity
  41  have h3 : (28 * (j : ℚ) + 13) > 0 := by positivity
  42  have h1' : (7 * (j : ℚ) + 5) ≠ 0 := ne_of_gt h1
  43  have h2' : (2 * (j : ℚ) + 1) ≠ 0 := ne_of_gt h2
  44  have h3' : (28 * (j : ℚ) + 13) ≠ 0 := ne_of_gt h3
  45  field_simp
  46  ring
  47
  48/-! ## Case `n ≡ 0 mod 7` (and `n ≡ 1 mod 24`)
  49
  50CRT residue: `n = 168j + 49 = 7(24j + 7)`.  Then `x = 14(3j + 1)`,
  51and `y = z = 2N/7 = 28(24j+7)(3j+1)`.  Concrete instance: `j = 0`,
  52`n = 49 = 7^2`.
  53-/
  54
  55theorem erdos_straus_zero_mod_seven (j : ℕ) :
  56    (4 : ℚ) / (168 * (j : ℚ) + 49)
  57      = 1 / (14 * (3 * (j : ℚ) + 1))
  58        + 1 / (28 * (24 * (j : ℚ) + 7) * (3 * (j : ℚ) + 1))
  59        + 1 / (28 * (24 * (j : ℚ) + 7) * (3 * (j : ℚ) + 1)) := by
  60  have h1 : (3 * (j : ℚ) + 1) > 0 := by positivity
  61  have h2 : (24 * (j : ℚ) + 7) > 0 := by positivity
  62  have h3 : (168 * (j : ℚ) + 49) > 0 := by positivity
  63  have h1' : (3 * (j : ℚ) + 1) ≠ 0 := ne_of_gt h1
  64  have h2' : (24 * (j : ℚ) + 7) ≠ 0 := ne_of_gt h2
  65  have h3' : (168 * (j : ℚ) + 49) ≠ 0 := ne_of_gt h3
  66  field_simp
  67  ring
  68
  69/-! ## Case `n ≡ 5 mod 7` (and `n ≡ 1 mod 24`)
  70
  71CRT residue: `n = 168m + 145`.  Then `x = 2(21m + 19)`,
  72`n + 2 = 21(8m + 7)`.  Concrete trapped instance: `m = 1`, `n = 313`.
  73-/
  74
  75theorem erdos_straus_five_mod_seven (m : ℕ) :
  76    (4 : ℚ) / (168 * (m : ℚ) + 145)
  77      = 1 / (2 * (21 * (m : ℚ) + 19))
  78        + 1 / (6 * (21 * (m : ℚ) + 19) * (8 * (m : ℚ) + 7))
  79        + 1 / ((168 * (m : ℚ) + 145) * 3 * (21 * (m : ℚ) + 19)
  80                 * (8 * (m : ℚ) + 7)) := by
  81  have h1 : (21 * (m : ℚ) + 19) > 0 := by positivity
  82  have h2 : (8 * (m : ℚ) + 7) > 0 := by positivity
  83  have h3 : (168 * (m : ℚ) + 145) > 0 := by positivity
  84  have h1' : (21 * (m : ℚ) + 19) ≠ 0 := ne_of_gt h1
  85  have h2' : (8 * (m : ℚ) + 7) ≠ 0 := ne_of_gt h2
  86  have h3' : (168 * (m : ℚ) + 145) ≠ 0 := ne_of_gt h3
  87  field_simp
  88  ring
  89
  90/-! ## Case `n ≡ 3 mod 7` (and `n ≡ 1 mod 24`)
  91
  92CRT residue: `n = 168m + 73`.  Then `x = 2(21m + 10)`,
  93`2n + 1 = 21(16m + 7)`.  Concrete trapped instance: `m = 0`, `n = 73`.
  94-/
  95
  96theorem erdos_straus_three_mod_seven (m : ℕ) :
  97    (4 : ℚ) / (168 * (m : ℚ) + 73)
  98      = 1 / (2 * (21 * (m : ℚ) + 10))
  99        + 1 / (3 * (21 * (m : ℚ) + 10) * (16 * (m : ℚ) + 7))
 100        + 1 / ((168 * (m : ℚ) + 73) * 6 * (21 * (m : ℚ) + 10)
 101                 * (16 * (m : ℚ) + 7)) := by
 102  have h1 : (21 * (m : ℚ) + 10) > 0 := by positivity
 103  have h2 : (16 * (m : ℚ) + 7) > 0 := by positivity
 104  have h3 : (168 * (m : ℚ) + 73) > 0 := by positivity
 105  have h1' : (21 * (m : ℚ) + 10) ≠ 0 := ne_of_gt h1
 106  have h2' : (16 * (m : ℚ) + 7) ≠ 0 := ne_of_gt h2
 107  have h3' : (168 * (m : ℚ) + 73) ≠ 0 := ne_of_gt h3
 108  field_simp
 109  ring
 110
 111end Erdos_C7_Closure
 112end NumberTheory
 113end IndisputableMonolith
 114