asymmetry_positive_cost
plain-language theorem explainer
The theorem establishes that J-cost is strictly positive for any positive real r not equal to one, encoding the matter-antimatter asymmetry condition. Cosmologists modeling baryogenesis via Sakharov conditions would cite this when confirming non-equilibrium in the early universe. The proof is a direct one-line application of the core Jcost positivity lemma.
Claim. Let $r > 0$ with $r ≠ 1$. Then the J-cost satisfies $0 < J(r)$.
background
In the Baryogenesis from J-Cost module the matter-antimatter asymmetry is identified with positive J-cost when the ratio r differs from its conjugate. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x > 0 and x ≠ 1, proved by rewriting Jcost as a square over a positive denominator and applying positivity of squares. The module sets this positivity as the non-equilibrium Sakharov condition, with five mechanisms matching configDim D = 5 and the observed baryon-to-photon ratio η ≈ 6.1 × 10^{-10}.
proof idea
One-line wrapper that applies Jcost_pos_of_ne_one from the Cost module (and its duplicates in JcostCore and LocalCache).
why it matters
The result supplies the asymmetry field inside the baryogenesisCert definition, which bundles mechanism count, equilibrium, and asymmetry to certify the full mechanism. It directly implements the non-equilibrium clause of the Sakharov conditions listed in the module documentation and connects to the J-uniqueness step (T5) of the forcing chain where positive defects arise for r ≠ 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.