baryonRung
plain-language theorem explainer
The declaration fixes the baryon rung at 44 on the phi-ladder for the asymmetry calculation. Cosmologists using Recognition Science to predict η_B ≈ φ^{-44} would cite this constant when verifying the bound φ^{44} > 10^8. It is introduced as a direct definition with no further computation.
Claim. The rung for the baryon asymmetry on the phi-ladder is the natural number 44.
background
Recognition Science places physical parameters on a phi-ladder where quantities scale as φ raised to integer rungs. The baryon asymmetry η_B is predicted to be φ^{-44} in this framework, with the module documenting the RS prediction η_B ≈ φ^{-44} and the bound φ^{44} > 10^8. The local setting is the A3 Baryogenesis section, which derives the asymmetry from the phi-ladder without axioms or sorrys. This constant is shared with the Cosmic Microwave Background module, ensuring consistency across cosmology derivations.
proof idea
The declaration is a direct definition assigning the value 44 to the baryon rung.
why it matters
This supplies the rung value to BaryonAsymmetryCert, which requires rung : baryonRung = 44 along with positivity and smallness of η_B. It completes the chain step for baryon asymmetry in the phi-ladder, connecting to the self-similar fixed point phi and the exponential suppression consistent with observed cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.