Gravity Seven Gaps Freudenthal Torus Class Mass Torus Class Mass Le Fiber Card D

The honest bound

A recognition ledger, a discrete record of events and their costs, assigns a number called mass to each object it tracks. In the framework's library, a machine-checked collection of formal theorems, one theorem governs the mass of an entire class of objects at once. The class is built from a torus, a shape like the surface of a doughnut, and the theorem is called torus_classMass_le_fiberCard_div_cube.

The theorem states that the class mass is at most the size of a certain fiber, a set of labeled representatives, divided by the cube of the size parameter N. In symbols: classMass(⟨T_N⟩) ≤ |fiber| / N³. The parameter N measures how finely the torus is subdivided. The fiber cardinality counts how many labeled objects collapse into the same class.

This bound is the honest version of a claim the framework's own panel rejected. The rejected claim said the class mass itself shrinks like 1/N³, an absolute suppression that would make large tori contribute almost nothing. That claim is false in general, because the fiber cardinality grows with N. The theorem here keeps the two objects separate: it bounds each labeled representative's own symmetry-factor mass by 1/N³, a per-object statement that is proved, and it bounds the class mass only by the fiber factor times that same 1/N³.

The theorem does not claim that the class mass tends to zero, nor that it is dominated by anything, nor that any continuum limit exists. Those targets remain open, marked RED in the framework's status ledger. The theorem's own status flag for absolute suppression is false, by definition, and its flags for the continuum limit, the substrate measure, and the gap bridge are all false as well.

What the theorem does establish is a precise, machine-checked relationship between two distinct objects that a careless wording had conflated. It shows exactly where the boundary lies between what is proved and what is not, and it names the growing fiber factor as the reason the dramatic suppression fails. That is a small but real piece of bookkeeping: it keeps the framework's claims honest about what its own formalism can and cannot force.

/-- **THEOREM (the honest class-mass bound).**
`classMass(⟦T_N⟧) ≤ |fiber(⟦T_N⟧)| / N³`.  The fiber cardinality is NOT
bounded here; in particular this does NOT yield the (killed) absolute
`N⁻³` suppression of the pushforward mass. -/
theorem torus_classMass_le_fiberCard_div_cube (N : ℕ) [NeZero N] :
    classMass (Quotient.mk (relabelSetoid (7 * N ^ 3))
        (freudenthalBoundedComplex N)) ≤
      (fiberCard (relabelSetoid (7 * N ^ 3))
          (Quotient.mk (relabelSetoid (7 * N ^ 3))
            (freudenthalBoundedComplex N)) : ℝ) / ((N : ℝ) ^ 3) := by
  rw [torus_classMass_eq_fiberCard_mul_mu, div_eq_mul_one_div]
  exact mul_le_mul_of_nonneg_left (mu_freudenthal_le_inv_cube N)
    (Nat.cast_nonneg _)

/-- **THEOREM (labeled, per-`1/|Aut|`).**  Every labeled member of the
torus class carries symmetry-factor mass at most `N⁻³`: μ is a class
function (`mu_congr`), and the translation embedding gives
`μ(T_N) ≤ 1/N³`.  This is a statement about EACH labeled representative,
not about the pushforward class mass. -/
theorem mu_torusClassMember_le (N : ℕ) [NeZero N]
    (K : BoundedComplex (7 * N ^ 3))
    (hK : Quotient.mk (relabelSetoid (7 * N ^ 3)) K =
      Quotient.mk (relabelSetoid (7 * N ^ 3)) (freudenthalBoundedComplex N)) :
    mu K ≤ 1 / ((N : ℝ) ^ 3) := by
  rw [mu_congr (equivalent_of_mk_eq hK)]
  exact mu_freudenthal_le_inv_cube N

theorem torusClassMassStatus_flags :
    torusClassMassStatus.labeled_member_mass_bounded = true ∧
    torusClassMassStatus.labeled_summand_bounded = true ∧
    torusClassMassStatus.labeled_summand_tendsto_zero = true ∧
    torusClassMassStatus.classMass_identity_proved = true ∧
    torusClassMassStatus.classMass_fiberCard_bound_proved = true ∧
    torusClassMassStatus.pushforward_classMass_absolutely_suppressed = false ∧
    torusClassMassStatus.Z_RS_continuum_limit = false ∧
    torusClassMassStatus.substrate_measure_derived = false ∧
    torusClassMassStatus.gap1_bridge_derived = false :=
  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩

What this page does not claim

This does not claim that the class mass is absolutely suppressed as 1/N³. This does not claim that the class mass sequence converges to zero. This does not claim that any continuum limit or dominance result about the partition function Z is proved.

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/FreudenthalTorusClassMass.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: