HitsBalancedPhase

formal source

  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