Pith. sign in
module module low

IndisputableMonolith.Physics.MatterAntimatterAsymmetryFromRS

show as:
view Lean formalization →

Packages the Recognition Science account of cosmological baryon asymmetry: an enumerated asymmetry mechanism and a certificate that the RS ledger yields a net matter excess. Cosmologists linking Sakharov-type conditions to the phi-ladder would cite it. The module is definitional, with a small certificate witness rather than a deep derivation.

claimThe module introduces an enumeration of asymmetry mechanisms and a certificate asserting that Recognition Science produces a nonzero matter--antimatter imbalance, consistent in sign with the observed baryon asymmetry of the universe.

background

Standard cosmology requires a primordial excess of matter over antimatter to match the observed baryon-to-photon ratio. The usual checklist is the Sakharov conditions: baryon-number violation, C and CP violation, and a departure from thermal equilibrium.

Recognition Science reframes that excess as a ledger imbalance on the phi-ladder rather than an ad hoc CP phase. The module sits in the Physics domain and imports only Mathlib and Constants (where the RS time quantum is fixed as $\tau_0 = 1$ tick). Sibling names indicate an enumerated mechanism type, a count of those mechanisms, and a certificate structure with a concrete witness instance.

No deep dynamical derivation is exposed at module level; the packaging is the certificate that RS supplies a directed matter excess.

proof idea

This is a definition and certificate module, not a multi-step proof development. It declares an asymmetry-mechanism enumeration, records how many mechanisms are listed, defines a certificate type for matter--antimatter asymmetry from RS, and supplies one concrete certificate instance. Argument structure is witness packaging rather than tactic-heavy derivation.

why it matters in Recognition Science

Gives Physics a named home for the RS baryon-asymmetry claim so downstream cosmology or ledger results can point at a single certificate rather than an informal narrative. No downstream consumers are wired yet in the graph, so the module is presently a leaf packaging unit. It touches the broader RS program of deriving observed cosmological imbalances from the same forcing chain (phi fixed point, eight-tick octave, $D=3$) that fixes the constants, without importing those landmarks directly here.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)