  67
  68/-- A rational closure witness for a gate `c`: the data needed by
  69`repr_of_gate_divisor_pair`. -/
  70def GateClosureWitness (n c : ℕ) : Prop :=
  71  ∃ x N d q : ℚ,
  72    (n : ℚ) ≠ 0 ∧
  73    x ≠ 0 ∧
  74    (c : ℚ) ≠ 0 ∧
  75    N = (n : ℚ) * x ∧
  76    x = ((n : ℚ) + (c : ℚ)) / 4 ∧
  77    d * q = N ∧
  78    (N + d) / (c : ℚ) ≠ 0 ∧
  79    (N + N * q) / (c : ℚ) ≠ 0
  80
  81/-- The RCL divisor-pair bridge: a gate closure witness gives a rational
  82Erdős-Straus representation. -/
  83theorem gate_closure_witness_gives_repr {n c : ℕ}
  84    (h : GateClosureWitness n c) :
  85    HasRationalErdosStrausRepr (n : ℚ) := by
  86  rcases h with ⟨x, N, d, q, hn, hx, hc, hN, hxdef, hdq, hy, hz⟩
  87  exact repr_of_gate_divisor_pair
  88    (n := (n : ℚ)) (x := x) (c := (c : ℚ)) (N := N) (d := d) (q := q)
  89    hn hx hc hN hxdef hdq hy hz
  90
  91/-- A direct balanced-pair phase support witness in the square budget `N^2`.
  92This is the exact finite-quotient condition:
  93
  94* `x` is the first denominator, so `N = n*x` and `c = 4*x - n`;
  95* `d*e = N^2`;
  96* both defects land in phase `-N mod c`, expressed as divisibility of
  97  `N+d` and `N+e`.
  98
  99The positivity fields keep the rational denominators nonzero. -/
 100def BalancedPairPhaseSupport (n c : ℕ) : Prop :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.