Encyclopedia Gravity Gravity Seven Gaps Freudenthal Torus Class Mass Torus Class Mass Status Flags

ARTICLE 5 claims 5 theorems

Gravity Seven Gaps Freudenthal Torus Class Mass Torus Class Mass Status Flags

A machine-checked flag list records which claims about torus mass are proved, which are false, and which remain open.

Verify this page

Status flags

The declaration torusClassMassStatus_flags is a single machine-checked list of nine true-or-false flags. It records, in one place, the exact state of a mathematical gate in the framework's library: five claims are proved, one claim is known to be false, and three targets remain open. The flags are forced by definition, with no unproved assumptions, so the list is a compact audit of what the framework does and does not know about this object.

The object in question is a torus, a shape like the surface of a donut, studied in a family indexed by a size N. The framework assigns each such torus a symmetry-factor mass, a number that counts how much a labeled representative contributes to a sum, divided by the size of its symmetry group. The proved flags say that for every labeled member of the torus class, this mass is at most 1/N³, and that the sequence of such masses tends to zero as N grows. These are statements about individual labeled representatives, not about the whole class.

The false flag is the important one. A previous wording claimed that the pushforward class mass, the total contribution of the whole class, is suppressed as N⁻³. That claim is false, because the class mass equals the number of labeled members times the symmetry-factor mass, and the number of labeled members grows with N. The framework's own library proves the honest bound: class mass is at most |fiber| / N³, where |fiber| is that growing count. The flag list records the false claim as false, preventing it from being reused.

Three flags remain red, meaning open targets: the continuum limit of a quantity called Z, the derivation of a substrate measure, and a bridge for gap one. None of these is claimed to be impossible; they are simply not yet derived. The declaration's value is that it separates what is proved from what is false from what is open, in a form a machine checks, so the framework's next step starts from an honest ledger.

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 tendsto_mu_freudenthal_zero · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean
tendsto_mu_freudenthal_zero · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean:141 
/-- **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 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 torus_classMass_le_fiberCard_div_cube · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean
torus_classMass_le_fiberCard_div_cube · IndisputableMonolith/Gravity/SevenGaps/FreudenthalTorusClassMass.lean:118 
/-- **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 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 absolutely N⁻³-suppressed; the fiber cardinality grows. No convergence or continuum-limit claim about Z is made. The three red flags are open targets, not impossibilities.

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