boxComplement

formal source

  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. -/