Gravity Seven Gaps Freudenthal Torus Class Mass

The torus class mass gate

In Recognition Science, physical structure emerges from a discrete record of events, and the cost of each recognition is forced by a proved theorem. This work concerns a particular object: the torus class, a set of bounded complexes that are all the same up to relabeling. The question is how much mass such a class carries. The answer turns on a distinction between counting one labeled representative and counting the whole class.

The classical mathematics here is about symmetry and counting. If you have a collection of objects and some are the same up to renaming, you can count them in two ways: count each labeled object separately, or count the equivalence classes. The proof establishes a bound for the first way. Every labeled member of the torus class has symmetry-factor mass at most 1/N³, where N is the size parameter. This is a symmetry factor, a weight that divides by the size of the automorphism group. The result is a theorem in the machine-checked library of formal theorems, with zero unproved assumptions.

The second way, the class mass, is more subtle. The pushforward class mass equals the labeled fiber cardinality times the symmetry factor of the canonical torus. The fiber cardinality is the number of labeled objects that map to the same class. This number grows with the class size. So the class mass is bounded by the fiber cardinality divided by N³, but that is not an absolute suppression. A naive claim that the class mass is at most 1/N³ is false in general, because the fiber grows. The proof explicitly forbids that claim.

The proof also establishes a convergence statement, but only for the labeled sequence. The sequence of symmetry-factor masses of the canonical torus representatives tends to zero as N grows. Likewise, any sequence of labeled summands, each a mass times a unit-modulus value, tends to zero. This is the honest gate: it holds for the labeled representatives, not for the pushforward class mass. The status ledger records which flags are true and which remain red. Three open targets stay red: the continuum limit of a partition function, the derived substrate measure, and the bridge to the first gap.

What this establishes is a precise boundary. The framework proves what it can prove, and it states plainly what it cannot. The labeled suppression is a theorem. The class mass has an identity and a bound, but no absolute suppression. The convergence is for labeled representatives only. This is the discipline that makes the framework's large claims credible: exact provenance, explicit limits, and no overstatement.

/-- **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 (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 (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 tendsto, measure form).**  The symmetry-factor mass
of the canonical torus LABELED representative tends to zero:
`μ(T_{N+1}) → 0`.  (Squeeze between `0` and `1/(N+1)³ ≤ 1/(N+1)`.) -/
theorem tendsto_mu_freudenthal_zero :
    Filter.Tendsto (fun n : ℕ => mu (freudenthalBoundedComplex (n + 1)))
      Filter.atTop (nhds 0) := by
  refine squeeze_zero (fun n => le_of_lt (mu_pos _)) (fun n => ?_)
    tendsto_one_div_add_atTop_nhds_zero_nat
  calc mu (freudenthalBoundedComplex (n + 1))
      ≤ 1 / (((n + 1 : ℕ) : ℝ) ^ 3) := mu_freudenthal_le_inv_cube (n + 1)
    _ = 1 / (((n : ℝ) + 1) ^ 3) := by rw [Nat.cast_add, Nat.cast_one]
    _ ≤ 1 / ((n : ℝ) + 1) := one_div_cube_le_one_div n

/-- **THEOREM (labeled tendsto, summand form; the honest T4 gate).**  The
labeled-representative summand sequence `μ(T_{N+1}) · z_N`, for ANY
sequence of unit-modulus values (e.g. `unitaryWeight` values of any
action), tends to `0`.  LABELED / CLASS DISTINCTION: this is the labeled
representative sequence; NO claim is made about the pushforward CLASS
mass sequence `|fiber|·μ`, whose fiber factor grows. -/
theorem tendsto_labeledSummand_zero (z : ℕ → ℂ) (hz : ∀ n, ‖z n‖ ≤ 1) :
    Filter.Tendsto
      (fun n : ℕ => (mu (freudenthalBoundedComplex (n + 1)) : ℂ) * z n)
      Filter.atTop (nhds 0) := by
  rw [tendsto_zero_iff_norm_tendsto_zero]
  refine squeeze_zero (fun n => norm_nonneg _) (fun n => ?_)
    tendsto_mu_freudenthal_zero
  rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (mu_pos _)]
  exact mul_le_of_le_one_right (le_of_lt (mu_pos _)) (hz n)

What this page does not claim

The pushforward class mass is absolutely suppressed as 1/N³; that claim is false because the fiber cardinality grows. Any convergence or continuum-limit statement about the partition function Z. The labeled convergence statements apply to the pushforward class mass.

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: