Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.InflatonMass3_FromPhiLadder

show as:
view Lean formalization →

Module packaging the RS derivation of the cubed inflaton mass scale from the golden-ratio ladder and the J-cost. Cosmologists citing RS inflation thresholds use the certificate and the nonnegativity of the domain cost. The argument is definitional: a domain cost, a positive canonical threshold, and an inhabited certificate tying them to the phi-ladder mass formula.

claimIn RS-native units, a domain cost $C$ built from the $J$-cost is nonnegative, a canonical threshold $\theta>0$ is fixed, and an inhabited certificate asserts that the cubed inflaton mass scale is the phi-ladder value consistent with $C$ and $\theta$.

background

Recognition Science places particle and field masses on a discrete phi-ladder: mass equals a yardstick times $\phi$ raised to a rung offset by the eight-tick gap structure. Here the target is the cubed inflaton mass that sets the slow-roll energy scale in an RS cosmology module.

The cost layer supplies the unique $J$-cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law. Constants supply the RS tick $\tau_0$ and the golden ratio $\phi$. The module introduces a domain cost (a nonnegative functional built from $J$), equality lemmas for evaluation at canonical points, and a positive canonical threshold against which the inflaton scale is compared.

Local setting is pure Cosmology: no dynamics of the inflaton potential are proved here; only the mass-cubed identification and its certificate interface.

proof idea

Definition-and-certificate module rather than a deep proof stack. Domain cost is defined from the imported $J$-cost; nonnegativity and pointwise evaluation are short lemmas. The canonical threshold is a positive constant in RS units. InflatonMass3Cert packages the claim that the cubed inflaton mass matches the phi-ladder prediction at that threshold; cert and cert_inhabited discharge inhabitance so downstream cosmology can assume the certificate without reconstructing the ladder arithmetic.

why it matters in Recognition Science

Gives Cosmology a named, certificate-backed value for $m_\phi^3$ on the RS phi-ladder, so inflation and reheating estimates can cite a single inhabited object instead of re-deriving rung arithmetic. Sits downstream of Constants ($\phi$, $\tau_0$) and Cost ($J$-uniqueness, T5) and upstream of any slow-roll or power-spectrum modules that need a fixed inflaton scale. No external used_by edges are recorded yet; the module is a leaf certificate ready for those parents. Touches the mass-formula landmark (yardstick $\cdot\phi^{\mathrm{rung}-8+\mathrm{gap}}$) and the eight-tick octave only through the ladder offset, not through a new forcing step.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)