etaBAt_succ_ratio
plain-language theorem explainer
etaBAt_succ_ratio establishes that each recognition e-fold multiplies the baryon-to-photon ratio by exactly φ^{-1}. Modelers of the GUT-to-present trajectory cite it to obtain the closed-form decay η_B(N) = φ^{-N}. The tactic proof unfolds the definition, invokes phi nonzero, rewrites the integer exponent via zpow_add, and casts the index.
Claim. For every natural number $N$, the baryon asymmetry at e-fold $N+1$ satisfies $η_B(N+1) = η_B(N) · φ^{-1}$, where $η_B(N) := φ^{-N}$.
background
The module treats the dynamic descent of the baryon-to-photon ratio on the phi-ladder. The upstream definition states that η_B(N) equals φ raised to the integer power -(N). The local setting fixes the present value at φ^{-44} via the 44-rung gap from GUT-scale unity, with each e-fold decrementing log η_B by exactly log φ. The lemma phi_ne_zero supplies the nonzero hypothesis required for exponent arithmetic.
proof idea
Unfold etaBAt to obtain φ^{-(N+1)}. Apply phi_ne_zero to license zpow_add₀. Rewrite the exponent -(N+1) as -N + (-1) by ring, then zpow_add yields the factor φ^{-1}. The final cast equates the natural-number index (N+1) with its integer counterpart.
why it matters
The result supplies the one_step_ratio field inside baryogenesisTrajectoryCert, which assembles positivity, initial unity at N=0, strict monotonicity, and adjacent ratios into a single certificate. It thereby completes the discrete step of the phi-ladder trajectory that matches the 44 e-fold inflation count. The construction rests on the self-similar fixed point φ forced in the T5-T6 segment of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.