Gravity Seven Gaps Zq Phase Structure Phased Zq Beats Triangle Witness

The phase pairing witness

In quantum gravity, one often needs to sum over many possible discrete geometries, such as triangulations of space. A central difficulty is that the sum can grow too quickly, and a standard bound, the triangle inequality, is too crude to show that the sum converges. The declaration phased_Zq_beats_triangle_witness proves a small but concrete example where this crude bound is beaten: by assigning an oscillatory phase to each geometry, two terms cancel exactly, and the total sum's magnitude is strictly less than the sum of the magnitudes of its parts.

The setting is a sum over equivalence classes of bounded triangulations, where each class is weighted by a measure and a phase. The phase is a real number attached to each class, and the weight is the complex exponential of that phase, so each weight has unit modulus. The witness uses two specific classes: the empty complex and the one-point complex, each with unit measure. It assigns phase zero to the empty class and phase π to the one-point class. Because exp(iπ) = -1, the two contributions are exactly opposite, and they cancel in the sum.

The theorem proves that the magnitude of the phased sum at complexity cap 2 is strictly less than the total mass, which is the sum of the measures of all classes. The bound improves from totalClassMass to totalClassMass - 2, and the proof chain shows this improved bound is nonnegative. This is a structure theorem at a fixed complexity cap, not a statement about the infinite limit. The continuum limit, where the cap goes to infinity, remains an open problem, as does the removal of a regulator at any oscillatory phase.

The pairing hypothesis is explicit: an injection from a subfamily of classes to classes outside it, whose measured summands are exactly opposite. The witness discharges this hypothesis concretely for the two classes at cap 2, showing the hypothesis is satisfiable, not vacuous. The general pairing theorems are finite-sum arithmetic under this exact-opposite hypothesis; the cancellation mechanism itself is not derived here but supplied by the hypothesis and discharged in this one instance.

In Recognition Science, this result is part of a larger program to understand the phase structure of gravitational path sums. The framework's machine-checked library of formal theorems records this as a proved theorem, with no unproved axioms beyond the standard trio. The result shows that phase cancellation is a viable mechanism for improving bounds, but it does not prove that such pairings exist for every phase model or every cap, nor does it establish any limit.

/-- **HEADLINE (strict improvement, witnessed).**  The phased `Zq` of the
explicit witness model is STRICTLY below the triangle bound.  Genuine
cancellation, not an inequality-shuffling tautology: the bound drop is
the exact paired mass. -/
theorem phased_Zq_beats_triangle_witness :
    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ < totalClassMass 2 :=
  Zq_pairing_beats_triangle 2 (phasedWeight witnessPhaseModel)
    (fun q => le_of_eq (phasedWeight_norm witnessPhaseModel q))
    witnessPaired witnessPairing witnessPairing_injOn witnessPairing_disj
    witnessPairing_cancel ⟨emptyClass, Finset.mem_singleton_self _⟩

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

/-- The representative symmetry factor of the empty-complex class is 1. -/
theorem mu_out_emptyClass : mu (Quotient.out emptyClass) = 1 := by
  rw [mu_out_eq_of_mk_eq (K := emptyComplex 2) emptyClass rfl]
  exact MeasureInvarianceNoGo.mu_emptyComplex 2

/-- The representative symmetry factor of the one-point class is 1. -/
theorem mu_out_pointClass : mu (Quotient.out pointClass) = 1 := by
  rw [mu_out_eq_of_mk_eq (K := onePointComplex) pointClass rfl]
  exact mu_onePointComplex

What this page does not claim

The continuum limit of the phased Zq is not proved. Regulator removal at any oscillatory phase is not derived. The existence of pairings for every phase model or every cap is not claimed. The cancellation mechanism itself is not derived; it is supplied by the pairing hypothesis.

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: