pith. sign in
module module high

IndisputableMonolith.Cosmology.BaryogenesisFromJCost

show as:
view Lean formalization →

The Cosmology.BaryogenesisFromJCost module defines the baryogenesis mechanism by tying matter-antimatter asymmetry to the J-cost function. It introduces BaryogenesisMechanism, equilibrium conditions, and asymmetry certificates. The module is purely definitional and imports its core objects from the Cost module.

claimEquilibrium holds when $J=0$, corresponding to matter-antimatter balance; baryogenesis arises when J-cost is positive, yielding the mechanism and its certificate.

background

Recognition Science derives all physics from one functional equation whose J-uniqueness is $J(x)=(x+x^{-1})/2-1$. This module lives in the cosmology domain and imports the Cost module that supplies the J-cost definitions and related lemmas. The supplied doc-comment fixes the convention that equilibrium equals matter-antimatter balance precisely when J vanishes.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies BaryogenesisMechanism and BaryogenesisCert that embed J-cost into cosmological asymmetry, feeding the larger Recognition framework that already fixes D=3, the eight-tick octave, and the alpha band.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)