etaB_pos
plain-language theorem explainer
The declaration proves that the baryon asymmetry parameter η_B(k) stays strictly positive for every natural number k on the φ-ladder trajectory. Cosmologists using Recognition Science models cite it to confirm the asymmetry builds monotonically from GUT to electroweak scales without sign reversal. The proof is a direct term-mode reduction that unfolds the ratio definition and invokes positivity of powers and division.
Claim. For every natural number $k$, $0 < φ^k / φ^{44}$.
background
The module models baryogenesis as a φ-ladder on the temperature axis with T_k = T_GUT · φ^{-k} and η_B(T_k) = φ^{k-44}. The definition etaB(k) := phi^k / phi^44 encodes this exact expression, so positivity of etaB follows from the base properties of φ. Upstream results supply the etaB definition itself, a parallel positivity theorem from the baryon asymmetry module, and configDim values that fix the terminal rung at 44 for the electroweak scale.
proof idea
The term proof unfolds etaB to the explicit ratio of powers, then applies div_pos to the pair of pow_pos applications on phi_pos at exponents k and 44.
why it matters
This theorem supplies the positivity clause required by baryogenesisCert and baryonAsymmetryCert, closing the dynamic trajectory claim that η_B grows by exactly φ per rung. It aligns with the Recognition Science forcing chain at the point where the eight-tick octave and D = 3 spatial dimensions determine the rung spacing, and it supports the predicted late-time value φ^{-44} ≈ 6 × 10^{-10}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.