N_sph_pos
plain-language theorem explainer
The sphaleron cycle count equals φ to the eighth and is strictly positive. Cosmology work on the first-order washout correction to the baryon asymmetry cites this before forming powers, logs, or the factor (1−δ) raised to that count. The proof is a one-line application of positivity of powers for a positive base.
Claim. $0 < N_{\mathrm{sph}}$, where $N_{\mathrm{sph}} = \varphi^{8}$ is the number of eight-tick cycles in the electroweak sphaleron-active window.
background
This module treats the first subleading correction to the RS baryon asymmetry η_B = φ^{-44}. The leading value sits about 4.5% above the Planck 2018 CMB central value; with no free parameters the gap must come from dynamics, not tuning.
The proposed mechanism is 8-tick washout during the electroweak phase transition. Sphalerons remain active for roughly N_sph cycles of the eight-tick octave. Each cycle the recognition operator reduces defect by a factor δ, so the net washout is (1−δ)^{N_sph}. The natural RS rate is δ = φ^{-8}, giving a correction factor near 0.985.
N_sph is defined as φ^8 (one full octave on the φ-ladder). The present lemma records that this real number is positive, which is the minimal arithmetic fact needed before any later inequality or interval statement about washout.
proof idea
One-line term proof. Apply Mathlib's pow_pos to the already-established fact that φ > 0, at natural exponent 8. Unfolding the definition N_sph := φ^8 finishes the goal.
why it matters
Positivity of the sphaleron cycle count is the first arithmetic gate in the higher-order η_B chain. Sibling lemmas (N_sph > 1, δ ∈ (0,1), and the correction factor lying in a concrete interval) all need a positive base and exponent before they can speak about washout magnitude.
In the broader RS picture this sits under the eight-tick octave (forcing step T7) and the φ-ladder mass/cosmology bookkeeping. The module itself is still hypothesis-level on the washout story: if precision data push η_B outside roughly [6.0, 6.5]×10^{-10} at high significance, the corrected prediction fails. The present lemma is pure arithmetic scaffolding for that testable claim, not the claim itself.
No downstream theorems currently depend on it in the graph; it is local infrastructure for the BaryonHigherOrder correction factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.