Gravity Seven Gaps Freudenthal Torus Class Mass One Div Cube Le One Div

A small inequality with a large boundary

The statement one_div_cube_le_one_div is a simple fact about reciprocals of powers: for any positive whole number n, the fraction 1 divided by (n+1) cubed is less than or equal to 1 divided by (n+1). Since cubing a number larger than 1 makes it bigger, its reciprocal becomes smaller, so the inequality is immediate. It says, in effect, that a sequence shrinking like one over a cube shrinks at least as fast as a sequence shrinking like one over the number itself.

This inequality matters because it appears in a machine-checked library of formal theorems as a stepping stone. The library studies a family of geometric objects called tori, each indexed by a size N. Each torus carries a number called its symmetry-factor mass, a measure of how much symmetry it has. A proved theorem states that this mass for a labeled torus is at most 1 divided by N cubed. The small inequality then shows that this mass also tends to zero as N grows, because it is squeezed between zero and a sequence that visibly approaches zero.

In Recognition Science, the framework models physical reality as a discrete record of recognition events, and this mass bound is part of an account of why certain contributions to a gravitational sum vanish. The proved claim is narrow: it concerns each labeled representative object separately. It does not claim that the total mass of the whole class of equivalent objects shrinks as 1 over N cubed. That total includes a factor counting how many objects are in the class, and that factor grows with N, so the total can behave differently.

The distinction is not a technicality. A previously worded claim that the class summand is suppressed as N to the minus three was rejected as ill-posed, because it confused the labeled object with the class object. The library now keeps the two separate in its type system, and the honest bound for the class mass includes the growing fiber factor. The convergence of the labeled sequence is proved, while the convergence of the class sequence, along with other continuum-limit claims, remains open.

What the inequality changes is the boundary of what is known. It lets the framework state a clean convergence result for the labeled representatives, and it forces the open questions to be named explicitly. A reader can now see exactly which suppression claim is proved, which is false, and which is still a target.

/-- **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 (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

/-- The dominating sequence `1/(n+1)³` is below `1/(n+1)`. -/
theorem one_div_cube_le_one_div (n : ℕ) :
    1 / (((n : ℝ) + 1) ^ 3) ≤ 1 / ((n : ℝ) + 1) := by
  have h1 : (1 : ℝ) ≤ (n : ℝ) + 1 := le_add_of_nonneg_left (Nat.cast_nonneg n)
  have hpos : (0 : ℝ) < (n : ℝ) + 1 := lt_of_lt_of_le one_pos h1
  exact one_div_le_one_div_of_le hpos (le_self_pow₀ h1 (by norm_num))

/-- **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 _)

/-- The consistency-gate status after this module. -/
def torusClassMassStatus : TorusClassMassStatus where
  labeled_member_mass_bounded := true
  labeled_summand_bounded := true
  labeled_summand_tendsto_zero := true
  classMass_identity_proved := true
  classMass_fiberCard_bound_proved := true
  pushforward_classMass_absolutely_suppressed := false
  Z_RS_continuum_limit := false
  substrate_measure_derived := false
  gap1_bridge_derived := false

What this page does not claim

The total class mass is not proved to be suppressed as 1 over N cubed. No convergence or dominance claim about the partition function Z is made. The physical bridge from these formal objects to observed gravity is not established here.

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: