delta_lt_one
plain-language theorem explainer
The 8-tick washout rate δ = φ^{-8} is strictly less than one. Anyone assembling the first-order corrected baryon asymmetry η_B^{(1)} = φ^{-44}(1-δ) cites this to keep the correction factor positive. The argument rewrites the negative power as a reciprocal and invokes φ > 1 to obtain φ^8 > 1.
Claim. Let $\varphi$ be the golden ratio and let $\delta = \varphi^{-8}$ be the washout rate per 8-tick cycle. Then $\delta < 1$.
background
This module supplies the first subleading correction to the Recognition Science leading-order baryon asymmetry $\eta_B = \varphi^{-44}$. That bare prediction sits about 4.5% above the Planck 2018 CMB central value; with no free parameters the gap cannot be tuned, so the next term must come from dynamics already present in the framework.
The proposed source is 8-tick washout while sphalerons are active at the electroweak transition. Each 8-tick cycle the recognition operator reduces residual defect by a fixed factor whose natural RS rate is one rung, $\delta = \varphi^{-8}$. Over $N_{\mathrm{sph}}\approx\varphi^8$ cycles the net multiplicative correction is $(1-\delta)^{N_{\mathrm{sph}}}\approx 1-\delta$ at first order.
The only arithmetic prerequisite is $\varphi>1$, already proved from the closed form $(1+\sqrt{5})/2$ (and forced earlier by T6 self-similarity of the Recognition Composition Law). Positivity of $\varphi$ then makes every positive integer power of $\varphi$ strictly larger than 1.
proof idea
Unfold $\delta$ to $\varphi^{-8}$. Rewrite the negative integer power via $zpow_neg$ as the reciprocal $1/\varphi^8$. The comparison $\delta<1$ becomes $1/\varphi^8<1$. Because $\varphi^8>0$, division reverses to $1<\varphi^8$. Finish with the standard lemma that $a>1$ and $n>0$ imply $a^n>1$, feeding $1<\varphi$ and the trivial $0<8$.
why it matters
The immediate consumer is the positivity proof for the correction factor $1-\delta$: once $\delta<1$ is known, a one-line linear-arithmetic step yields $0<1-\delta$. That factor multiplies the leading $\varphi^{-44}$ prediction, cutting it from roughly $6.376\times10^{-10}$ to about $6.28\times10^{-10}$ and halving the tension with Planck.
The construction sits inside the eight-tick octave forced at T7 and uses the same $\varphi$-ladder rung counting that organises masses and the sphaleron active window $N_{\mathrm{sph}}\approx\varphi^8$. The broader washout story remains an explicit hypothesis: the module records falsifiers on the bands $[5.5,7.5]\times10^{-10}$ (leading order) and $[6.0,6.5]\times10^{-10}$ (first-order corrected).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.