Gravity Seven Gaps Zq Phase Structure Zq Norm Le Total Class Mass

The bounded path sum

In quantum gravity, a path sum adds up contributions from many possible spacetime geometries. The Recognition Science framework writes such a sum over triangulations, which are shapes built from flat triangles glued together. The declaration Zq_norm_le_totalClassMass is a proved theorem about that sum: it says the size of the sum, measured as a complex number's modulus, can never exceed a quantity called totalClassMass. The total class mass is itself a sum, over all distinct triangulation classes at a fixed complexity cap, of a symmetry factor that counts how many labelings collapse to the same class. The theorem holds for any assignment of phases to the classes, as long as each phase has unit modulus, meaning it only rotates the contribution and never changes its magnitude.

The bound is sharp in a useful way. The theorem states, in symbols, that the modulus of the phased sum is at most the total class mass, and that this total is in turn at most the number of distinct triangulation classes. This is a finite statement: it applies only when the complexity cap, written B, is fixed, so the sum has finitely many terms. The proof is a direct application of the triangle inequality, which says the size of a sum is at most the sum of the sizes of its parts. Because each phase has size exactly one, each term's size is just its symmetry factor, and adding those factors gives the total class mass.

The theorem does not claim that the continuum limit exists, nor that the sum converges as the complexity cap grows without bound. Those questions remain open in the framework. It also does not claim that any particular phase choice is physically correct; the phase model itself is a definitional choice, not a derived result. What the theorem does establish is a necessary condition for any well-defined path sum: at every finite cap, the sum is bounded by a number that depends only on the symmetry structure of the triangulations, not on the phases. That makes it a stepping stone, not a destination. A reader can now see why phase cancellation matters: without it, the sum can only grow with the number of classes, and the bound is the best the triangle inequality can offer.

/-- **THEOREM (triangle bound for Zq).**  For any weight of modulus at
most 1, the quotient-first path sum is bounded by the total class mass. -/
theorem Zq_norm_le_totalClassMass (B : ℕ) (wq : TriangulationClass B → ℂ)
    (hw : ∀ q, ‖wq q‖ ≤ 1) :
    ‖Zq B wq‖ ≤ totalClassMass B := by
  show ‖∑ q : TriangulationClass B, (mu (Quotient.out q) : ℂ) * wq q‖ ≤ _
  calc ‖∑ q : TriangulationClass B, (mu (Quotient.out q) : ℂ) * wq q‖
      ≤ ∑ q : TriangulationClass B, ‖(mu (Quotient.out q) : ℂ) * wq q‖ :=
        norm_sum_le _ _
    _ ≤ ∑ q : TriangulationClass B, mu (Quotient.out q) := by
        refine Finset.sum_le_sum fun q _ => ?_
        rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
          abs_of_pos (mu_pos _)]
        exact mul_le_of_le_one_right (mu_pos _).le (hw q)
    _ = totalClassMass B := rfl

/-- **THEOREM (well-definedness of the phased Zq at fixed cap).**  For
every phase model, the phased quotient-first path sum has unit-modulus
weights and satisfies the proved finiteness bounds.  This is a structure
theorem at fixed complexity cap, NOT a continuum-limit statement. -/
theorem Zq_phased_wellDefined (B : ℕ) (P : PhaseModel B) :
    (∀ q, ‖phasedWeight P q‖ = 1) ∧
    ‖Zq B (phasedWeight P)‖ ≤ totalClassMass B ∧
    ‖Zq B (phasedWeight P)‖ ≤ (Fintype.card (TriangulationClass B) : ℝ) := by
  have hb := Zq_norm_le_totalClassMass B (phasedWeight P)
    (fun q => le_of_eq (phasedWeight_norm P q))
  exact ⟨phasedWeight_norm P, hb, le_trans hb (totalClassMass_le_card B)⟩

/-- The total class mass is bounded by the class count. -/
theorem totalClassMass_le_card (B : ℕ) :
    totalClassMass B ≤ (Fintype.card (TriangulationClass B) : ℝ) := by
  unfold totalClassMass
  calc ∑ q : TriangulationClass B, mu (Quotient.out q)
      ≤ ∑ _q : TriangulationClass B, (1 : ℝ) :=
        Finset.sum_le_sum fun q _ => mu_le_one _
    _ = (Fintype.card (TriangulationClass B) : ℝ) := by
        rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]

/-- **THEOREM (triangle bound for Zq).**  For any weight of modulus at
most 1, the quotient-first path sum is bounded by the total class mass. -/
theorem Zq_norm_le_totalClassMass (B : ℕ) (wq : TriangulationClass B → ℂ)
    (hw : ∀ q, ‖wq q‖ ≤ 1) :
    ‖Zq B wq‖ ≤ totalClassMass B := by
  show ‖∑ q : TriangulationClass B, (mu (Quotient.out q) : ℂ) * wq q‖ ≤ _
  calc ‖∑ q : TriangulationClass B, (mu (Quotient.out q) : ℂ) * wq q‖
      ≤ ∑ q : TriangulationClass B, ‖(mu (Quotient.out q) : ℂ) * wq q‖ :=
        norm_sum_le _ _
    _ ≤ ∑ q : TriangulationClass B, mu (Quotient.out q) := by
        refine Finset.sum_le_sum fun q _ => ?_
        rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
          abs_of_pos (mu_pos _)]
        exact mul_le_of_le_one_right (mu_pos _).le (hw q)
    _ = totalClassMass B := rfl

What this page does not claim

The continuum limit of the phased path sum exists or converges. Any particular phase model is physically correct or derived from first principles. The bound is strict for all phase choices; strictness requires additional cancellation hypotheses.

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: