matter_balance_equilibrium
plain-language theorem explainer
The declaration establishes that the J-cost vanishes at unity, encoding exact matter-antimatter equilibrium in the early universe. Cosmologists modeling baryogenesis would cite it to satisfy the equilibrium clause of the Sakharov conditions within Recognition Science. The proof is a direct one-line application of the unit lemma for the J-cost function.
Claim. The J-cost function satisfies $J(1) = 0$, which encodes exact matter-antimatter balance.
background
The J-cost is defined as $J(x) = (x-1)^2/(2x)$, a measure of asymmetry between a configuration and its conjugate. In the Baryogenesis from J-Cost module this quantity translates the Sakharov conditions: baryon-number violation appears as sigma-export above threshold, CP violation as $J(r) neq J(r^*)$, and departure from equilibrium as $J(r) > 0$. The upstream Jcost_unit0 lemma records the base case $J(1) = 0$ by direct simplification of the definition.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module, which itself reduces the definition of J-cost at argument 1 to zero by simplification.
why it matters
This result supplies the equilibrium field inside the baryogenesisCert definition, which assembles five mechanisms, equilibrium, and positive asymmetry into a single certificate for A3 cosmology. It directly implements the module's translation of Sakharov non-equilibrium into positive J-cost and anchors the Recognition Science claim that the baryon-to-photon ratio arises from J-cost imbalances on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.