eta_B_leading
plain-language theorem explainer
The leading-order baryon-to-photon ratio equals φ to the power −44. Cosmologists comparing the zero-parameter Recognition Science baseline to Planck CMB data cite this identity before applying washout corrections. The proof is pure definitional reflexivity: the named scale constant is already that power.
Claim. The leading-order baryon asymmetry scale equals $\varphi^{-44}$.
background
This module studies the first subleading correction to the baryon asymmetry $\eta_B$. Recognition Science places the leading prediction on the $\varphi$-ladder at rung $-44$, so $\eta_B=\varphi^{-44}\approx 6.376\times 10^{-10}$, about 4.5% above the Planck 2018 CMB central value.
Upstream, the constant eta_B_phi_scale is defined exactly as $\varphi^{-44}$. Here $\varphi$ is the self-similar fixed point forced at step T6 of the unified forcing chain; integer powers of $\varphi$ supply the discrete ladder for masses and cosmological ratios throughout RS.
The local setting is the proposed 8-tick sphaleron washout: over $N_{\mathrm{sph}}\approx\varphi^8$ active cycles the ledger multiplies by $(1-\varphi^{-8})$, yielding the corrected form $\eta_B^{(1)}=\varphi^{-44}(1-\varphi^{-8})$.
proof idea
One-line term proof by reflexivity (rfl). The left-hand side is the definition of the baryon-asymmetry $\varphi$-scale, whose body is already $\varphi^{-44}$, so the equality holds definitionally with no lemmas or rewriting.
why it matters
Fixes the clean leading term that the rest of the module multiplies by the first-order 8-tick washout factor $(1-\varphi^{-8})$. The module doc records the ~4.5% excess over Planck and treats the washout picture as a hypothesis with explicit falsifiers on the $\eta_B$ window. No downstream declarations currently depend on this identity in the graph; sibling results (positivity of the leading term, bounds on the correction factor) sit beside it. Framework landmarks: T6 ($\varphi$ forced) and T7 (eight-tick octave) supply the ladder rung and the washout period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.