IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.ErdosStrausRotationHierarchy
   3
   4/-!
   5# Erdős-Straus Square-Budget Box Phase
   6
   7This module isolates the finite combinatorial part of the residual
   8Erdős-Straus proof.
   9
  10For a square budget `N^2`, a divisor exponent box is represented by a
  11complementary pair `(d,e)` with `d*e = N^2`.  This is equivalent to choosing
  12exponents `0 ≤ a_p ≤ 2 v_p(N)` in the prime factorization, but it avoids
  13unnecessary factorization API overhead in the finite closure lemma.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace ErdosStrausBoxPhase
  19
  20open ErdosStrausRotationHierarchy
  21
  22/-- A divisor exponent-box point for the square budget `N^2`, represented
  23by a divisor `d` and its complementary divisor `e`. -/
  24structure DivisorExponentBox (N : ℕ) where
  25  d : ℕ
  26  e : ℕ
  27  d_pos : 0 < d
  28  e_pos : 0 < e
  29  square_budget : d * e = N ^ 2
  30
  31/-- The divisor selected by a box point. -/
  32def boxDivisor {N : ℕ} (box : DivisorExponentBox N) : ℕ :=
  33  box.d
  34
  35/-- The complementary divisor selected by a box point. -/
  36def boxComplement {N : ℕ} (box : DivisorExponentBox N) : ℕ :=
  37  box.e
  38
  39theorem box_divisor_mul_complement {N : ℕ} (box : DivisorExponentBox N) :
  40    boxDivisor box * boxComplement box = N ^ 2 :=
  41  box.square_budget
  42
  43/-- A square-budget box hits the balanced residual phase for gate `c`.
  44
  45The conditions `c | N+d` and `c | N+e` say exactly that both reciprocal
  46defects land in phase `-N` modulo `c`. -/
  47def HitsBalancedPhase (n c : ℕ) : Prop :=
  48  ∃ x N : ℕ, ∃ box : DivisorExponentBox N,
  49    0 < n ∧ 0 < c ∧ 0 < x ∧ 0 < N ∧
  50    N = n * x ∧
  51    c = 4 * x - n ∧
  52    c ∣ N + boxDivisor box ∧
  53    c ∣ N + boxComplement box
  54
  55/-- The finite box-to-pair closure lemma.  A box phase hit is exactly the
  56balanced-pair support required by the RCL skeleton. -/
  57theorem box_phase_hit_gives_balanced_pair {n c : ℕ}
  58    (h : HitsBalancedPhase n c) :
  59    BalancedPairPhaseSupport n c := by
  60  rcases h with ⟨x, N, box, hn, hc, hx, hNpos, hN, hcdef, hdvd, hevd⟩
  61  refine ⟨x, N, boxDivisor box, boxComplement box,
  62    hn, hc, hx, hNpos, box.d_pos, box.e_pos, hN, hcdef, ?_, hdvd, hevd⟩
  63  exact box_divisor_mul_complement box
  64
  65/-- A box phase hit already gives a rational Erdős-Straus representation,
  66by composing the finite closure lemma with the RCL ledger theorem. -/
  67theorem box_phase_hit_gives_repr {n c : ℕ}
  68    (h : HitsBalancedPhase n c) :
  69    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
  70  balanced_pair_phase_support_gives_repr (box_phase_hit_gives_balanced_pair h)
  71
  72end ErdosStrausBoxPhase
  73end NumberTheory
  74end IndisputableMonolith
  75