DivisorExponentBox

formal source

  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