cp_source_positive
plain-language theorem explainer
The structural Jarlskog invariant is strictly positive, supplying the CP-violation source required by Sakharov. Cosmology and baryogenesis arguments cite it as the RS-native J_CP > 0 fact. The proof is a one-line alias of the JarlskogInvariant positivity theorem (matter-over-antimatter convention).
Claim. The structural Jarlskog invariant $J_{\mathrm{struct}} = A^2 \lambda^6 \sin\delta$ (Wolfenstein $A$, $\lambda$, and CP phase $\delta$ all RS-derived) satisfies $J_{\mathrm{struct}} > 0$.
background
The module reconstructs Sakharov's three baryogenesis conditions on the RS ledger. Condition 2 is C/CP violation. In the Standard Model this is measured by the Jarlskog invariant $J_{CP}$; the module imports the RS structural form
$J_{\mathrm{struct}} = A^2 \lambda^6 \sin\delta$
from JarlskogInvariant, where $A$ and $\lambda$ are Wolfenstein parameters fixed by RS structure and $\delta$ is the CP phase from the chiral Gray-code Berry cycle.
Upstream, jarlskog_positive already proves $J_{\mathrm{struct}} > 0$ under the convention that matter dominates antimatter, by unfolding the product and checking each factor (positive $A$, positive $\lambda$, and $\sin\delta > 0$). This declaration simply re-exports that fact under the cosmology module's name for the CP source.
proof idea
One-line term proof: the claim is definitionally identical to jarlskog_positive, so the proof is just that theorem applied as a term. No local unfolding or arithmetic is repeated here; all positivity work (structural $A > 0$, $\lambda > 0$, and $\sin\delta > 0$) lives upstream in JarlskogInvariant.
why it matters
Sakharov condition 2 demands CP violation. The module doc states this is proved via the Berry phase of the chiral Gray-code cycle giving $\delta_{CKM} \neq 0$, hence $J_{CP} > 0$. This theorem is the local handle on that fact inside SakharovFromLedger.
It is consumed by the permits structure and sits beside siblings that package the full Sakharov bundle (SakharovConditions, sakharov_from_RS, baryogenesis_possible, cp_asymmetry_nonzero). Condition 1 (B violation via sphaleron-like 8-tick multi-axis windings) is treated separately; condition 3 (departure from equilibrium) remains an explicit underived hypothesis. The result therefore closes only the CP leg of the ledger story, not the full baryogenesis derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.