etaBAt_adjacent_ratio
plain-language theorem explainer
The theorem shows that the baryon-to-photon ratio η_B decreases by exactly the factor φ^{-1} between consecutive recognition e-folds. Cosmologists using the Recognition Science framework cite it when confirming the geometric decay of η_B from GUT-scale unity to the present epoch. The proof rewrites the left-hand side via the successor ratio lemma then clears the denominator with positivity and field simplification.
Claim. For every natural number $N$, the ratio satisfies $$η_B(N+1)/η_B(N)=φ^{-1}.$$
background
The module treats baryogenesis as a dynamic trajectory on the phi-ladder. It defines η_B(N) as the value of the baryon-to-photon ratio at recognition e-fold N since the GUT epoch, with the explicit form η_B(N) := φ^{-N}. The upstream successor ratio lemma states that η_B(N+1) equals η_B(N) multiplied by φ^{-1}. The module_doc fixes the present-epoch value at φ^{-44} via the equilibrium identity η_B · Θ_crit = φ and notes that the 44-rung gap matches the inflation e-fold count.
proof idea
The term proof first rewrites the ratio using the successor ratio lemma etaBAt_succ_ratio. It then obtains a positivity hypothesis from etaBAt_pos and applies field_simp to cancel the common nonzero factor in the denominator.
why it matters
This supplies the adjacent-ratio property required by the downstream baryogenesisTrajectoryCert definition, which collects positivity, initial unity, one-step ratio, strict decrease, and the φ^{-1} ratio into a single certificate. It directly encodes the module claim that each e-fold drops log-η_B by exactly log φ, aligning with the eight-tick octave and D=3 spatial structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.