etaBAt_zero
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.
claimLet η_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 in Recognition Science
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}.
scope and limits
- Does not derive the initial value 1 from more primitive axioms.
- Does not compute η_B at non-zero e-folds.
- Does not address continuous-time limits or non-integer steps.
- Does not incorporate deviations from the pure phi-ladder form.
formal statement (Lean)
41theorem etaBAt_zero : etaBAt 0 = 1 := by
proof body
Term-mode proof.
42 unfold etaBAt
43 simp
44
45/-- One e-fold cuts η_B by exactly 1/φ. -/