eta_B_inv_val
plain-language theorem explainer
The inverse baryon asymmetry is the pure ladder value φ⁴⁴. Cosmologists and RS auditors matching η_B to the observed baryon-to-photon ratio cite this constant as the reciprocal of the rung-44 entry. It is a one-line definition: raise the golden-ratio fixed point to the integer power 44.
Claim. Define the reciprocal baryon asymmetry by $\eta_B^{-1} := \varphi^{44}$, where $\varphi$ is the self-similar fixed point of the Recognition ladder.
background
The module places the baryon asymmetry on the φ-ladder: the single integer rung 44 is assigned so that η_B = φ^{-44}. In RS-native units the golden ratio φ is forced as the unique self-similar fixed point (forcing step T6); every dimensionless abundance is then a pure power of φ, possibly corrected by an eight-tick or passive-mode factor.
The companion value on the same ladder is the direct asymmetry η_B itself (rung factor φ^{-44}). The present definition simply records the reciprocal power, so that arithmetic identities (factorizations through the 8-tick period and the passive-mode count) can be stated without repeated negative exponents.
Upstream constants supply φ and the integer rung infrastructure; the exact numerical match of η_B to observation is proved in the imported BaryonAsymmetryExact development.
proof idea
Pure definitional abbreviation. The body is the single term phi ^ (44 : ℤ); no lemmas or tactics are invoked. Noncomputable only because real exponentiation is noncomputable in the ambient library.
why it matters
Rung 44 is the module’s core cosmological entry: the table equates φ^{-44} with the baryon asymmetry η_B and marks that identification as a theorem. Recording the reciprocal φ^{44} lets later arithmetic lemmas (baryon rung factorization, N_e factorizations, eleven-times table) stay positive-exponent and readable.
In the broader framework this is the mass-formula style yardstick applied to a cosmological abundance rather than a particle mass: dimensionless ratios sit on the same φ-ladder forced by T5–T6. The eight-tick octave (T7) appears in the sibling factorization lemmas that decompose the exponent 44. No downstream consumers are wired yet; the definition exists so those arithmetic certificates can name a single symbol for 1/η_B.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.