N_sph
plain-language theorem explainer
Defines the sphaleron active-window length as N_sph = φ^8 real cycles of the eight-tick clock. Cosmology proofs that build the first-order washout factor (1−δ)^N_sph cite this constant. The body is a one-line power of the golden ratio, matching one full octave on the RS ladder.
Claim. Let $\varphi$ be the golden ratio. Define the sphaleron cycle count $N_{\mathrm{sph}} := \varphi^{8} \in \mathbb{R}$.
background
The module treats the first subleading correction to the RS baryon asymmetry $\eta_B = \varphi^{-44}$. Leading order overshoots the Planck 2018 CMB value by about 4.5%; with no free parameters, the gap must come from dynamics rather than fitting.
During the electroweak phase transition, sphalerons remain active for a finite window. Recognition Science measures that window in units of the eight-tick octave (forcing step T7). Each cycle the recognition operator applies one defect-reduction step at the natural washout rate $\delta = \varphi^{-8}$.
$N_{\mathrm{sph}}$ is the dimensionless count of those cycles. Setting it to $\varphi^8$ (one full octave on the $\varphi$-ladder) makes the net washout $(1-\delta)^{N_{\mathrm{sph}}}$ and yields the corrected prediction $\eta_B^{(1)} = \varphi^{-44}(1-\varphi^{-8})$.
proof idea
Pure definition: unfold to $\varphi$ raised to the natural number 8. No lemmas are invoked at the definition site. Downstream positivity and comparison proofs apply pow_pos phi_pos and one_lt_zpow₀ one_lt_phi after unfolding.
why it matters
Anchors the 8-tick washout mechanism that halves the $\eta_B$ gap to CMB data. Downstream results use it directly: N_sph_pos and N_sph_gt_one establish $0 < N_{\mathrm{sph}}$ and $N_{\mathrm{sph}} > 1$; correction_term_rung identifies the first-order piece $\varphi^{-44}\cdot\varphi^{-8} = \varphi^{-52}$; eta_B_leading_pos sits in the same correction block.
Framework landmarks: T7 eight-tick octave and the $\varphi$-ladder mass/rung calculus. The module marks the washout picture as hypothesis, with explicit falsifiers on the $\eta_B$ windows $[5.5,7.5]\times 10^{-10}$ (leading) and $[6.0,6.5]\times 10^{-10}$ (corrected).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.