pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Cosmology.MatterAntimatter

show as:
view Lean formalization →

The module defines the baryon-to-photon ratio η and assembles the mathematical objects needed to express matter-antimatter asymmetry in Recognition Science cosmology. It collects the observed value, the baryonic contribution, the Sakharov conditions, and the CP-violation and dilution parameters that determine the final ratio. The module serves as the central repository for these quantities so that downstream cosmology statements can reference a single, consistent set of definitions.

claimThe baryon-to-photon ratio is denoted $η = n_B / n_γ$. The module also introduces the observed value $η_observed$, the baryon-specific ratio $η_B$, the Sakharov conditions, the CP-violation parameter $ε_{CP}$, the dilution factor, and the relation $η = f(ε_{CP}, dilution)$ that follows from them.

background

Recognition Science begins from the fundamental time quantum $τ_0 = 1$ tick supplied by the imported Constants module. The present module extends that foundation into cosmology by defining the baryon-to-photon ratio $η$ together with the minimal set of conditions required to generate a nonzero value from an initially symmetric state. All definitions sit inside the Recognition framework whose forcing chain already fixes the spatial dimension $D=3$ and the self-similar fixed point $φ$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the eta definitions and SakharovCondition objects that the cosmology domain relies upon. It directly implements the baryon-asymmetry interface required by the Recognition Science forcing chain after the constants module has fixed $τ_0$. No downstream theorems are recorded in the current graph, yet the declarations close the gap between the abstract J-cost and concrete cosmological observables.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (25)