pith. sign in
module module moderate

IndisputableMonolith.Cosmology.MatterAntimatter

show as:
view Lean formalization →

The Cosmology.MatterAntimatter module assembles definitions and relations for the baryon-to-photon ratio η together with Sakharov conditions and CP-violation factors that generate the observed matter-antimatter asymmetry. Researchers working on baryogenesis in Recognition Science cosmology would cite these objects. The module organizes the material as a set of sibling declarations rather than a single theorem.

claimThe baryon-to-photon ratio is the quantity $η$ with auxiliary objects $η_B$, $η_{observed}$, $ε_{CP}$, the Sakharov conditions, and the dilution factor that together quantify the small observed asymmetry $η ≈ 6×10^{-10}$.

background

The module imports the RS time quantum $τ_0 = 1$ tick from IndisputableMonolith.Constants and places the baryon-to-photon ratio η inside the cosmology domain. It introduces the observed value eta_observed, the asymmetry parameter eta_B, the smallness predicate eta_is_small, the matter-antimatter ratio, SakharovCondition, cpTransformTick, epsilon_CP, dilutionFactor, and eta_from_epsilon. The local setting is the Recognition Science derivation of physics from a single functional equation, here specialized to early-universe asymmetry generation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the η parameter and Sakharov conditions that feed into broader cosmology calculations of matter dominance. It addresses the smallness of the observed asymmetry as a key feature within the Recognition Science framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (25)