Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.Baryogenesis3_FromJCost

show as:
view Lean formalization →

Module packaging a J-cost certificate for three-generation baryogenesis: a nonnegative domain cost, a positive canonical threshold, and an inhabited certificate record. Cosmologists working in the RS forcing chain would cite it when tying matter-antimatter asymmetry to the unique cost J. The argument is definitional plus elementary positivity and equality lemmas, not a deep existence proof.

claimDefine a domain cost $C$ built from the Recognition cost $J$, prove $C\ge 0$ and an evaluation identity, fix a positive canonical threshold $\theta>0$, and package these into an inhabited baryogenesis certificate (three-generation form).

background

Recognition Science forces a unique nonnegative cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) via the Recognition Composition Law and the T5 uniqueness step. Cosmology modules import that cost together with the RS constants (including the fundamental tick $\tau_0$) to express early-universe selection thresholds in cost units rather than ad hoc potentials.

This module sits in the cosmology layer and introduces a domain-level cost assembled from $J$, a canonical numerical threshold against which that cost is compared, and a small certificate record that bundles the positivity and threshold facts needed by three-generation baryogenesis arguments. No new dynamical field equations are stated here; the objects are pure cost-side scaffolding.

proof idea

Definition module with short supporting lemmas. The domain cost is defined from $J$; nonnegativity follows from the standard nonnegativity of $J$ on the positive reals. An evaluation identity records how the cost specializes at equality cases. The canonical threshold is a positive constant (positivity is a one-line arithmetic fact). The certificate record packages these pieces; inhabitation is by direct construction of the record fields.

why it matters in Recognition Science

Baryogenesis in RS is not driven by an external CP-violating Lagrangian term but by cost asymmetry measured in the unique $J$. This module supplies the cost-and-threshold certificate that later cosmology developments can import when closing a three-generation asymmetry claim. It does not itself appear in the T0-T8 forcing chain; it is an application layer that consumes T5 $J$-uniqueness and the Cost library. Downstream use is currently empty in the graph, so the module is a leaf certificate ready for a parent baryogenesis theorem rather than a proved link in the main chain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)