Encyclopedia Gravity Gravity Seven Gaps Freudenthal Torus Class Mass Mu Torus Class Member Le

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Freudenthal Torus Class Mass Mu Torus Class Member Le

A machine-checked theorem bounds the symmetry weight of each labeled torus member by 1/N³, while carefully not claiming the same for the whole class.

Verify this page

The labeled mass bound

In the Recognition Science framework's study of gravity, a central object is the torus class, a collection of related discrete structures indexed by a natural number N. Each structure in this class has a symmetry-factor mass, a real number that measures how much its internal symmetries contribute to its weight in a larger calculation. The declaration mu_torusClassMember_le is a proved theorem: for every labeled member K of the torus class, this symmetry-factor mass is at most 1/N³.

The proof is short and rests on two previously established facts. First, the mass is a class function, meaning that any two structures equivalent under relabeling have the same mass. Second, the canonical torus itself has mass bounded by 1/N³. The theorem combines these to conclude that every member of the class inherits the bound. A companion result extends this to the summand: for any unit-modulus complex number z, the product μ(K)·z has modulus at most 1/N³.

The theorem is careful about what it does not say. The pushforward class mass, which is the mass of the entire class as a single object, equals the fiber cardinality times the symmetry factor of the canonical torus. The fiber cardinality grows with N, so the class mass is not absolutely bounded by 1/N³. The theorem explicitly forbids claiming that the pushforward class mass is suppressed by N⁻³; that claim is false in general.

In Recognition Science, this distinction matters for the consistency of the framework's gravitational derivations. The labeled bound supports the convergence of individual representative sequences, while the class mass remains honest about its growing fiber factor. The theorem also leaves open several larger targets, including the continuum limit of the partition function and the derivation of the substrate measure, both flagged as not yet established.

THEOREM mu_torusClassMember_le · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean
mu_torusClassMember_le · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean:70 
/-- **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 norm_freudenthal_labeledSummand_le · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean
norm_freudenthal_labeledSummand_le · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean:83 
/-- **THEOREM (labeled summand bound; class-API restatement of
`unnormalized_torus_weight_suppressed`).**  For any labeled member `K` of
the torus class and any unit-modulus value `z`, the single labeled
summand `μ(K)·z` has modulus at most `N⁻³`.  LABELED / CLASS DISTINCTION:
this bounds ONE labeled summand; the pushforward CLASS mass is
`|fiber|·μ` and is NOT bounded by `N⁻³` here. -/
theorem norm_freudenthal_labeledSummand_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))
    (z : ℂ) (hz : ‖z‖ ≤ 1) :
    ‖(mu K : ℂ) * z‖ ≤ 1 / ((N : ℝ) ^ 3) := by
  rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (mu_pos K)]
  calc mu K * ‖z‖
      ≤ mu K * 1 := mul_le_mul_of_nonneg_left hz (le_of_lt (mu_pos K))
    _ = mu K := mul_one _
    _ ≤ 1 / ((N : ℝ) ^ 3) := mu_torusClassMember_le N K hK
THEOREM torus_classMass_eq_fiberCard_mul_mu · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean
torus_classMass_eq_fiberCard_mul_mu · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean:103 
/-- **THEOREM (class mass, identity form).**  The pushforward class mass
of the torus class is the labeled fiber cardinality times the symmetry
factor of the canonical torus:
`classMass(⟦T_N⟧) = |fiber(⟦T_N⟧)| · μ(T_N)`. -/
theorem torus_classMass_eq_fiberCard_mul_mu (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)) : ℝ) *
        mu (freudenthalBoundedComplex N) := by
  rw [classMass_eq_fiberCard_mul_mu]
  congr 1
  exact mu_congr (equivalent_of_mk_eq (Quotient.out_eq _))
THEOREM torusClassMassStatus_flags · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean
torusClassMassStatus_flags · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean:203 
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

The pushforward class mass is not suppressed by N⁻³; the fiber cardinality grows with N. No convergence or continuum-limit claim about the partition function Z is made here. The substrate measure and the gap-1 bridge remain open targets, not derived results.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND