IndisputableMonolith.Cosmology.BaryogenesisTrajectory
The module defines the baryon asymmetry η_B(N) at recognition e-folds N after the GUT epoch in the Recognition Science framework. Early-universe cosmologists would cite the functions and lemmas when tracking asymmetry evolution on the phi-ladder. It consists of a chain of definitions for etaBAt together with lemmas on sign, monotonicity and a final certification object.
claim$\eta_B(N)$ denotes the baryon-to-photon ratio at recognition e-fold $N$ since the GUT epoch, equipped with lemmas establishing $\eta_B(N)>0$ for finite $N$, $\eta_B(0)=0$, strict decrease, and the certificate object BaryogenesisTrajectoryCert.
background
The module imports the RS time quantum $\tau_0=1$ tick from Constants and operates in the cosmology domain. Recognition Science models cosmic evolution via e-folds counted in recognition ticks, with scaling governed by the self-similar fixed point $\phi$ and the J-cost function. The supplied doc-comment identifies the central object as the $\eta_B$ value at recognition e-fold $N$ since the GUT epoch.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the formal trajectory of baryon asymmetry required by Recognition Science cosmology. It feeds the BaryogenesisTrajectoryCert into downstream calculations of matter generation after the GUT scale. The chain of lemmas on positivity and decrease closes the discrete evolution model begun in the Constants import.
scope and limits
- Does not derive the initial condition at the GUT epoch from particle physics.
- Does not compute a numerical final value for observed $\eta_B$.
- Does not address post-recombination evolution of the asymmetry.
- Does not incorporate explicit RCL applications inside the trajectory.