etaBAt_strictly_decreasing
plain-language theorem explainer
The declaration establishes that the baryon-to-photon ratio η_B decreases strictly with each recognition e-fold N. Cosmologists working within the Recognition Science framework would cite it to confirm the monotonic decay from GUT-scale unity to the present value φ^{-44}. The proof proceeds by rewriting the successor via the exact ratio lemma, invoking positivity, and applying the inequality φ^{-1} < 1 derived from φ > 1.5.
Claim. For every natural number $N$, the baryon-to-photon ratio satisfies $η_B(N+1) < η_B(N)$, where $η_B(N) := φ^{-N}$.
background
In the BaryogenesisTrajectory module the function etaBAt assigns to each recognition e-fold count N the value φ to the power of minus N, representing the baryon-to-photon ratio after N e-folds since the GUT epoch. The module states that η_B falls from its GUT-scale unity value through the electroweak transition by integer φ-step decrements per recognition e-fold, yielding the trajectory η_B(N) = exp(-N · log φ). This result relies on the positivity of etaBAt at every N and the exact one-step ratio etaBAt(N+1) = etaBAt(N) * φ^{-1}, together with the bound φ > 1.5 from Constants.
proof idea
The proof rewrites etaBAt(N+1) using the successor ratio theorem to obtain etaBAt(N) * φ^{-1}. It then invokes etaBAt_pos to obtain strict positivity of etaBAt(N), derives φ^{-1} < 1 from φ > 1.5 via linarith and inv_lt_one_of_one_lt₀, and concludes the inequality by multiplying the strict inequality φ^{-1} < 1 on the left by the positive etaBAt(N).
why it matters
This theorem supplies the strictly_decreasing field in the baryogenesisTrajectoryCert definition, which bundles the key properties of the η_B trajectory. It directly supports the dynamic content of the Recognition Science cosmology module, where every e-fold drops log-η_B by exactly log φ, consistent with the phi-ladder structure. The result closes the monotonicity requirement for the certificate that links the GUT-scale initial value to the present φ^{-44} prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.