pith. sign in
module module low

IndisputableMonolith.Masses.Manifest

show as:
view Lean formalization →

Masses.Manifest declares the concrete realizations of particle masses on the phi-ladder within the Recognition Science framework. Physicists deriving mass spectra from the forcing chain would cite it for explicit assignments. This is a definition module containing no theorems or proofs.

claimThe module manifests masses via the formula $M = y_0 · ϕ^{r-8+g(Z)}$ on the phi-ladder, with yardstick $y_0$, rung $r$, and gap function $g(Z)$.

background

The module sits in the Masses domain and supplies the explicit mass objects used by the Recognition Science mass formula. It builds on the phi-ladder and the eight-tick octave (T7) together with D=3 from the upstream forcing chain. No new definitions of J-cost or defectDist appear here; those remain in the imported Mathlib and sibling modules.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete mass values that feed parent mass-spectrum calculations in the Recognition framework. It fills the final step of the T0-T8 chain by turning the abstract phi-ladder into manifest particle masses.

scope and limits

declarations in this module (2)