etaBAt_zero
plain-language theorem explainer
The theorem establishes that the baryon asymmetry parameter equals unity at recognition e-fold zero, the GUT-scale starting point on the phi-ladder. Cosmologists using the Recognition Science trajectory model cite this as the fixed initial condition before integer e-fold decrements begin. The proof is a direct one-line wrapper that unfolds the etaBAt definition and simplifies the resulting power to 1.
Claim. Let η_B(N) denote the baryon-to-photon ratio at recognition e-fold N after the GUT epoch, given by η_B(N) = φ^{-N}. Then η_B(0) = 1.
background
The BaryogenesisTrajectory module defines the dynamic descent of the baryon asymmetry η_B from its GUT-scale value through successive recognition e-folds. The upstream definition etaBAt N := phi ^ (-N) supplies the explicit power-law form, where phi is the self-similar fixed point fixed by the Recognition Science forcing chain. The module doc states that this produces the trajectory η_B(N) = exp(-N · log φ), with the 44-rung gap from rung 0 to the present fixing both the current ratio φ^{-44} and the inflation e-fold count.
proof idea
The proof is a one-line wrapper that unfolds the definition of etaBAt at argument 0 and applies simplification to reduce phi^0 to 1.
why it matters
This result supplies the initial_unity field required by the baryogenesisTrajectoryCert certificate, which assembles the full set of trajectory properties including positivity, strict decrease, and the exact 1/φ ratio per step. It anchors the model to the GUT-scale unity value stated in the module doc, consistent with the phi-ladder and the 44-step descent to the present epoch. The certificate in turn supports the matter-consciousness duality theorem that fixes the observed ratio at φ^{-44}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.