BaryogenesisTrajectoryCert
plain-language theorem explainer
The BaryogenesisTrajectoryCert structure certifies that the baryon-to-photon ratio follows the exact geometric sequence eta_B(N) = phi^{-N} from unity at the GUT epoch to phi^{-44} at the present epoch. Cosmologists using Recognition Science cite it when linking the 44-rung phi-ladder gap to the observed baryon asymmetry. The declaration is a plain structure that bundles six elementary properties of the exponential already established for etaBAt.
Claim. A structure asserting that the function eta_B(N) := phi^{-N} satisfies eta_B(N) > 0 for every natural number N, eta_B(0) = 1, eta_B(N+1) = eta_B(N) * phi^{-1}, eta_B(N+1) < eta_B(N), eta_B(N+1)/eta_B(N) = phi^{-1}, and eta_B(44) = phi^{-44}.
background
Recognition Science places the baryon-to-photon ratio on the phi-ladder. The upstream definition etaBAt(N) := phi^{-N} supplies the explicit closed form. The module adds the dynamic trajectory that descends from eta_B = 1 at rung 0 (GUT epoch) by exact multiplicative steps of phi^{-1} per recognition e-fold, reaching eta_B = phi^{-44} after 44 steps. The MODULE_DOC states that this 44-rung gap is the same gap-(consciousnessGap-1) that fixes the inflation e-fold count N_e = 44 and realizes the equilibrium identity eta_B * Theta_crit = phi from the matter-consciousness duality theorem.
proof idea
This is a structure definition that packages six already-proved lemmas for etaBAt: positivity (etaBAt_pos), initial value (etaBAt_zero), one-step ratio (etaBAt_succ_ratio), strict decrease (etaBAt_strictly_decreasing), adjacent ratio (etaBAt_adjacent_ratio), and the direct evaluation at N = 44. No tactics or reductions occur inside the structure itself; the downstream baryogenesisTrajectoryCert simply supplies the six fields by name.
why it matters
The certificate supplies the dynamic content that turns the static equilibrium eta_B = phi^{-44} into an explicit trajectory on the phi-ladder. It is consumed directly by baryogenesisTrajectoryCert. In the broader framework it closes the link between T6 (phi fixed point), T7 (eight-tick octave), T8 (D = 3), and the 44 e-fold count that matches the observed baryon asymmetry without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.