Gravity Seven Gaps Zq Phase Structure Zq Pairing Beats Triangle

The pairing bound

The declaration Zq_pairing_beats_triangle is a proved theorem about a finite sum that arises in a model of gravity. The sum, written Zq, adds up contributions from a finite collection of geometric objects called triangulation classes. A basic inequality, the triangle inequality, says the size of the whole sum is at most the sum of the sizes of its parts. That bound is always true, but it can be loose. The theorem states a precise condition under which the bound is strictly improved: if two subfamilies of terms have exactly opposite values, so they cancel perfectly, then the size of the total sum is strictly less than the sum of all the individual sizes.

The condition is not assumed to hold everywhere. It is a hypothesis, an explicit injection that pairs a subfamily of classes with classes outside it whose contributions are exactly opposite. When such a pairing exists, the theorem proves the improved bound, and the improvement is strict whenever the paired family is nonempty. The proof is finite-sum arithmetic, and the cancellation mechanism itself is not derived; it is supplied by the hypothesis. The theorem also comes with a concrete witness at a fixed complexity cap, B = 2, where an explicit phase model assigns phase 0 to the empty class and phase π to the one-point class, and the two cancel exactly. That witness discharges the pairing hypothesis in one instance, so the theorem is not vacuous.

What the theorem does not claim is as important as what it proves. It is a structure theorem at a fixed complexity cap, not a statement about any limit. The continuum limit of this phased sum remains open, and the complexity cutoff is not a mesh refinement. The theorem does not prove regulator removal, and it does not show that pairings exist for every phase model or every cap. It also never equates this quotient-first object with the labeled path sum; the bridge between them carries a labeled fiber factor that nothing here bypasses. The result is a proved improvement of a bound under a stated hypothesis, with one concrete witness, and nothing more.

/-- **THEOREM (strictly better than the triangle inequality).**  Under the
pairing hypothesis with a NONEMPTY paired family, the phased `Zq` is
STRICTLY below the triangle bound `totalClassMass`. -/
theorem Zq_pairing_beats_triangle (B : ℕ) (wq : TriangulationClass B → ℂ)
    (hw : ∀ q, ‖wq q‖ ≤ 1)
    (s : Finset (TriangulationClass B))
    (j : TriangulationClass B → TriangulationClass B)
    (hinj : ∀ q ∈ s, ∀ q' ∈ s, j q = j q' → q = q')
    (hdisj : ∀ q ∈ s, j q ∉ s)
    (hcancel : ∀ q ∈ s,
      (mu (Quotient.out (j q)) : ℂ) * wq (j q)
        = -((mu (Quotient.out q) : ℂ) * wq q))
    (hne : s.Nonempty) :
    ‖Zq B wq‖ < totalClassMass B := by
  have hb := Zq_pairing_bound B wq hw s j hinj hdisj hcancel
  have hpos : 0 < ∑ q ∈ s ∪ s.image j, mu (Quotient.out q) := by
    obtain ⟨q0, hq0⟩ := hne
    exact Finset.sum_pos (fun q _ => mu_pos _)
      ⟨q0, Finset.mem_union_left _ hq0⟩
  linarith

/-- **THEOREM (strictly better than the triangle inequality).**  Under the
pairing hypothesis with a NONEMPTY paired family, the phased `Zq` is
STRICTLY below the triangle bound `totalClassMass`. -/
theorem Zq_pairing_beats_triangle (B : ℕ) (wq : TriangulationClass B → ℂ)
    (hw : ∀ q, ‖wq q‖ ≤ 1)
    (s : Finset (TriangulationClass B))
    (j : TriangulationClass B → TriangulationClass B)
    (hinj : ∀ q ∈ s, ∀ q' ∈ s, j q = j q' → q = q')
    (hdisj : ∀ q ∈ s, j q ∉ s)
    (hcancel : ∀ q ∈ s,
      (mu (Quotient.out (j q)) : ℂ) * wq (j q)
        = -((mu (Quotient.out q) : ℂ) * wq q))
    (hne : s.Nonempty) :
    ‖Zq B wq‖ < totalClassMass B := by
  have hb := Zq_pairing_bound B wq hw s j hinj hdisj hcancel
  have hpos : 0 < ∑ q ∈ s ∪ s.image j, mu (Quotient.out q) := by
    obtain ⟨q0, hq0⟩ := hne
    exact Finset.sum_pos (fun q _ => mu_pos _)
      ⟨q0, Finset.mem_union_left _ hq0⟩
  linarith

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

What this page does not claim

The theorem does not prove the continuum limit of the phased sum exists or has any value. The theorem does not derive a phase function from the substrate; the witness phase model is a definitional choice, not a derived result. The theorem does not show that the pairing hypothesis holds for every phase model or every complexity cap, only for the one concrete witness at B = 2.

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: