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

The mass bound

The declaration two_le_totalClassMass_two is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states, in plain terms, that the number called totalClassMass (a sum of weights assigned to certain geometric classes) is at least 2 when the complexity cap B is set to 2. The proof is a finite arithmetic check: the library shows that the total mass at cap 2 is at least 2, so the quantity totalClassMass 2 - 2 is nonnegative.

Why does this matter? A companion theorem in the same module proves that, under a specific pairing hypothesis, the modulus of a certain phased sum is bounded by totalClassMass 2 - 2. That bound is only meaningful if the subtracted 2 does not push the result below zero. The theorem two_le_totalClassMass_two supplies exactly that guarantee: it ensures the improved bound is nonnegative, so the cancellation result is not vacuous. The library also exhibits a concrete witness: a phase model where the empty complex and the one-point complex have equal mass and opposite phases, so the paired contributions cancel exactly.

It is important to be precise about what this theorem does not claim. It does not prove that the continuum limit of the phased sum exists; that limit remains an open target. It does not prove that regulator removal works for any phase, only that at a fixed cap a specific pairing cancels. It does not assert that such pairings exist for every phase model or every cap. The theorem is a finite structural statement, not a statement about the infinite limit.

/-- **THEOREM (non-vacuity of the improved bound).**  The total class mass
at cap 2 is at least 2 (the two distinct unit-mass witness classes alone
contribute 2), so `totalClassMass 2 - 2` is nonnegative and the improved
bound is meaningful. -/
theorem two_le_totalClassMass_two : (2 : ℝ) ≤ totalClassMass 2 := by
  have hsum : ∑ q ∈ ({emptyClass, pointClass} : Finset (TriangulationClass 2)),
      mu (Quotient.out q) = 2 := by
    rw [Finset.sum_insert (by
        rw [Finset.mem_singleton]
        exact emptyClass_ne_pointClass),
      Finset.sum_singleton, mu_out_emptyClass, mu_out_pointClass]
    norm_num
  calc (2 : ℝ)
      = ∑ q ∈ ({emptyClass, pointClass} : Finset (TriangulationClass 2)),
          mu (Quotient.out q) := hsum.symm
    _ ≤ ∑ q : TriangulationClass 2, mu (Quotient.out q) :=
        Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _)
          (fun q _ _ => (mu_pos _).le)
    _ = totalClassMass 2 := rfl

/-- **HEADLINE (single-theorem chain).**  The full advertised chain in one
kernel statement: the witness `Zq` is bounded by `totalClassMass 2 - 2`,
that improved bound is strictly below the triangle bound, and it is
nonnegative. -/
theorem phased_Zq_witness_chain :
    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ ≤ totalClassMass 2 - 2 ∧
    totalClassMass 2 - 2 < totalClassMass 2 ∧
    (0 : ℝ) ≤ totalClassMass 2 - 2 :=
  ⟨phased_Zq_pairing_witness, by linarith,
    by linarith [two_le_totalClassMass_two]⟩

What this page does not claim

The continuum limit of the phased sum is not proved to exist. Regulator removal is not proved for any phase. Pairing cancellations are not claimed to exist for every phase model or every cap.

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: