Gravity Seven Gaps Zq Phase Structure Opposite Phase Pair Strict

The cancellation lemma

The declaration opposite_phase_pair_strict is a proved lemma about adding two complex numbers. If you take a positive real mass m, multiply it by a phase e^{iθ} (a unit-length arrow in the complex plane), and add to it the same mass m multiplied by the opposite phase e^{i(θ+π)}, the two terms cancel exactly. The theorem states the modulus of their sum is strictly less than the sum of their moduli. The strictness is the point: the triangle inequality usually allows equality, but here the opposite phases force a smaller result.

In the Recognition Science framework, this lemma is a tool inside a larger structure called the quotient-first path sum, a discrete record of events where each event carries a weight. The framework's library shows that when two events have equal mass and phases that differ by π, their paired contributions vanish. This exact cancellation is what makes a later bound strictly better than the crude triangle inequality, which would only say the sum is at most the total mass. The lemma is pure finite-sum arithmetic; it does not depend on any limit or any physical assumption.

What the lemma does not claim is just as important as what it establishes. It does not establish that such opposite-phase pairs exist in general; the pairing hypothesis is stated explicitly and discharged only in one concrete witness at a fixed complexity cap. It does not establish the continuum limit of the phased path sum, which remains open. It does not establish regulator removal. The cancellation mechanism is supplied by the hypothesis, not derived from deeper principles.

/-- **THEOREM (two-term exact cancellation).**  Equal masses at phases
`θ` and `θ + π` cancel exactly. -/
theorem opposite_phase_pair_cancels (m θ : ℝ) :
    (m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))
      + (m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ)) = 0 := by
  rw [opposite_phase_exp, mul_neg, add_neg_cancel]

/-- **THEOREM (two-term strict improvement).**  For positive mass the
paired two-term sum is STRICTLY below its triangle bound. -/
theorem opposite_phase_pair_strict (m θ : ℝ) (hm : 0 < m) :
    ‖(m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))
        + (m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ))‖
      < ‖(m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))‖
        + ‖(m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ))‖ := by
  rw [opposite_phase_pair_cancels, norm_zero]
  have h1 : ‖(m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))‖ = m := by
    rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos hm,
      Complex.norm_exp_I_mul_ofReal, mul_one]
  have h2 : ‖(m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ))‖
      = m := by
    rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos hm,
      Complex.norm_exp_I_mul_ofReal, mul_one]
  rw [h1, h2]
  linarith

/-- **HEADLINE (non-vacuous quantitative cancellation witness).**  The
explicit phase model at `B = 2` beats the triangle bound by EXACTLY the
paired mass 2: `‖Zq‖ <= totalClassMass 2 - 2`.  This discharges the
pairing hypotheses of the general theorems in one concrete instance. -/
theorem phased_Zq_pairing_witness :
    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ ≤ totalClassMass 2 - 2 := by
  have hb := Zq_pairing_bound 2 (phasedWeight witnessPhaseModel)
    (fun q => le_of_eq (phasedWeight_norm witnessPhaseModel q))
    witnessPaired witnessPairing witnessPairing_injOn witnessPairing_disj
    witnessPairing_cancel
  rw [witnessPaired_mass] at hb
  exact hb

What this page does not claim

The lemma does not establish that opposite-phase pairs exist for every phase model or every complexity cap. The lemma does not establish the continuum limit or regulator removal. The phase model itself is a definitional choice, not a derived consequence.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/ZqPhaseStructure.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: