Pith. sign in
module module high

IndisputableMonolith.Cosmology.BaryogenesisTrajectoryFromPhiLadder

show as:
view Lean formalization →

The module formalizes the growth of baryon asymmetry η_B along the phi-ladder, with η_B increasing by exactly φ at each temperature rung. Cosmologists working in Recognition Science would cite these definitions when tracing the discrete evolution of the asymmetry from the imported constants. The module consists of a set of definitions and supporting objects built directly on the RS time quantum.

claim$\eta_B$ grows by exactly $\phi$ per temperature rung on the $\phi$-ladder.

background

The module sits in the cosmology domain and imports the fundamental RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants. Its doc-comment encodes the central claim that η_B grows by exactly φ per temperature rung. Sibling definitions introduce etaB (the asymmetry at a rung), etaB_ratio (the growth factor), etaB_at_gap45, BViolationChannel (the violation mechanism), bViolationChannel_count, BaryogenesisCert, and baryogenesisCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the baryogenesis trajectory that connects the phi-ladder to the asymmetry parameter in the Recognition framework. It directly encodes the growth law from its doc-comment and supports BaryogenesisCert within the same module. No external downstream uses are recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)