etaBAt_pos
plain-language theorem explainer
The declaration proves that the baryon asymmetry parameter etaBAt N exceeds zero for every natural number N of recognition e-folds since the GUT epoch. Cosmologists tracing the phi-ladder descent in baryogenesis models would cite it to confirm the asymmetry never changes sign. The proof is a one-line term wrapper that unfolds the definition and invokes positivity of powers of the positive constant phi.
Claim. For every natural number $N$, the baryon asymmetry at recognition e-fold $N$ satisfies $0 < phi^{-N}$.
background
The BaryogenesisTrajectory module defines the dynamic descent of the baryon-to-photon ratio on the phi-ladder. The function etaBAt maps each natural number N to phi raised to the power minus N, so that etaBAt N equals the value at the N-th recognition e-fold after the GUT epoch. The module states that this produces the trajectory eta_B(N) = exp(-N log phi), with the 44-rung gap from initial unity to the present value phi^{-44} matching the inflation e-fold count. Upstream, the definition etaBAt (N : ℕ) : ℝ := phi ^ (-(N : ℤ)) is supplied directly, while Constants provides the positivity hypothesis on phi.
proof idea
The proof is a one-line term-mode wrapper. It unfolds etaBAt to expose the power expression phi ^ (-(N : ℤ)) and applies the zpow_pos lemma using the positivity fact Constants.phi_pos.
why it matters
This result is collected inside the baryogenesisTrajectoryCert definition, which bundles positivity, initial unity at N=0, adjacent ratios equal to phi^{-1}, and strict decrease to certify the full trajectory. It supplies the required positivity for the dynamic content of the matter-consciousness duality theorem, ensuring the asymmetry parameter remains positive while descending the phi-ladder from GUT-scale unity to the present epoch, consistent with the forced phi fixed point and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.