baryogenesisTrajectoryCert
plain-language theorem explainer
baryogenesisTrajectoryCert assembles the complete certificate for the baryon-to-photon ratio trajectory η_B(N) under the phi-ladder dynamics. Cosmologists citing Recognition Science predictions for the baryon asymmetry would use this to confirm the geometric decay from GUT-scale unity to the observed φ^{-44} after exactly 44 e-folds. The definition is a direct structure construction that wires in the six supporting lemmas for positivity, initial value, ratio per step, monotonicity, adjacent equality, and present value.
Claim. A certificate for the baryon-to-photon ratio trajectory states that the function η_B : ℕ → ℝ satisfies ∀N, 0 < η_B(N), η_B(0) = 1, η_B(N+1) = η_B(N) ⋅ φ^{-1}, η_B(N+1) < η_B(N), η_B(N+1)/η_B(N) = φ^{-1}, and η_B(44) = φ^{-44}.
background
The module develops the dynamic trajectory of the baryon-to-photon ratio η_B on the phi-ladder, building on the equilibrium identity η_B ⋅ Θ_crit = φ from the matter-consciousness duality. Here η_B(N) = φ^{-N} for recognition e-fold count N, starting at η_B(0)=1 at the GUT epoch and reaching η_B(44)=φ^{-44} today. The phi-ladder refers to the discrete steps governed by the self-similar fixed point φ from the forcing chain T6.
proof idea
The definition constructs the BaryogenesisTrajectoryCert record by assigning each field to the corresponding theorem: eta_pos to etaBAt_pos, initial_unity to etaBAt_zero, one_step_ratio to etaBAt_succ_ratio, strictly_decreasing to etaBAt_strictly_decreasing, adjacent_ratio_eq_inv_phi to etaBAt_adjacent_ratio, and present_value to etaBAt_44. Each supporting theorem unfolds etaBAt and applies zpow arithmetic or positivity of phi.
why it matters
This certificate certifies the full dynamic content of the baryogenesis trajectory predicted by the matter-consciousness duality theorem. It realizes the structural prediction that every e-fold drops log-η_B by log φ, with the 44-rung gap setting the inflation e-fold count N_e=44. In the Recognition framework it anchors the cosmology module to the phi-ladder and the constants derived from T5-T8, providing the explicit trajectory η_B(N) = exp(-N log φ) for use in further calculations of cosmic evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.