Pith. sign in
module module high

IndisputableMonolith.Cosmology.PhiRungLadder

show as:
view Lean formalization →

Defines the cosmological φ-rung ladder centered on the baryon asymmetry address −44. Supplies the numerical rung values, inverse, and factorization identities that place η_B on the ladder and relate it to e-fold and eleven-times arithmetic. Cosmology and gravity tracks cite it whenever a structural scale φ^(−44) is needed. Content is mostly definitions plus short algebraic equalities and a certificate bundle.

claimThe module fixes the baryon-asymmetry rung at $-44$ on the $\varphi$-ladder: $\eta_B$ is identified with a pure power of $\varphi$ at that address, with companion values for the inverse and the balance $\eta_B \cdot \varphi^{45} = \varphi$. It also records the arithmetic factorizations for the e-fold count $N_e$ and the eleven-times table used to reach that rung, packaged as a ladder certificate.

background

Recognition Science places dimensionless cosmological ratios on a discrete $\varphi$-ladder whose rungs are integer powers of the golden ratio fixed by the self-similar point of the J-cost (forcing chain T5–T6). Masses and abundances take the schematic form yardstick $\cdot \varphi^{(\mathrm{rung}-8+\mathrm{gap})}$; pure ratios such as the baryon asymmetry $\eta_B$ sit at a single rung address.

The upstream module BaryonAsymmetryExact already proves that $\eta_B$ occupies rung $-44$ and that the power balance $\eta_B \times \varphi^{45} = \varphi$ holds as a formal theorem. The present module extracts the ladder data those proofs rely on: the rung value, its inverse, the factorization of the baryon rung, and the elementary $N_e$ and eleven-times arithmetic that locate $-44$ without free parameters.

Constants are RS-native ($c=1$, $\hbar=\varphi^{-5}$, etc.). The ladder is therefore a pure combinatorial address book, not a new dynamical postulate.

proof idea

Definition-heavy module with short algebraic lemmas rather than a single deep proof. Rung and inverse values are closed-form constants; equality lemmas discharge by rfl or direct rewriting against the upstream exact baryon-asymmetry theorems. Factorization statements for the baryon rung and for $N_e$ are multiplicative identities on integer powers of $\varphi$. The eleven-times table is a finite arithmetic lookup used to reach address $-44$. A certificate structure bundles these facts so downstream modules can import one object instead of re-proving the ladder arithmetic.

why it matters in Recognition Science

Rung $-44$ and the scale $\varphi^{-44}$ recur across the cosmology/gravity bridge. Downstream, Dark-Energy $w(z)$ structural form and Vacuum Horizon Forcing import the ladder when vacuum or horizon rungs must match the same discrete address book. On the gravity side, the PTA stochastic-background discriminator explicitly uses the rung-44 positive scale $\varphi^{-44}$ as the RS signature against a zero inflation baseline; QG channel rung derivation and observable signal models read channel powers from these addresses; Strong-Field structural tests and the zero-free-parameters ledger likewise depend on a single shared ladder.

Without this module each track would re-encode the baryon rung and the $N_e$/eleven-times arithmetic, risking inconsistent addresses. It is the thin shared spine that keeps Track 4 (cosmology) and Tracks 6.B–6.C / D5 (gravity, QG falsifiers) on the same $\varphi$-ladder.

scope and limits

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)