pith. sign in
module module moderate

IndisputableMonolith.Cosmology.MatterAntimatter

show as:
view Lean formalization →

The Cosmology.MatterAntimatter module collects definitions and lemmas for the baryon-to-photon ratio η and associated asymmetry parameters within Recognition Science. Cosmologists examining baryogenesis and Sakharov conditions in RS-native units would cite these objects. The module is a pure collection of declarations with no embedded proofs.

claimThe baryon-to-photon ratio is the quantity $\eta = n_B / n_\gamma$, together with the observed value $\eta_{observed}$, the baryon asymmetry $\eta_B$, the ratio $\eta_{matterAntimatterRatio}$, the Sakharov conditions, the CP-violation parameter $\epsilon_{CP}$, and the dilution factor.

background

This module sits in the cosmology domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants together with Mathlib structures. It introduces the baryon-to-photon ratio $\eta$ as the central observable for matter-antimatter asymmetry. Sibling declarations define $\eta_{observed}$, $\eta_B$, $\eta_{is_small}$, the SakharovCondition, allConditionsNeeded, cpTransformTick, cp_not_symmetry, $\epsilon_{CP}$, dilutionFactor, and eta_from_epsilon.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the $\eta$ interface and Sakharov conditions used by downstream cosmology results on asymmetry generation. It fills the chain step that links the RS time quantum to the observed baryon-to-photon ratio without external baryogenesis mechanisms.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (25)