jarlskog_pos
plain-language theorem explainer
The predicted Jarlskog invariant for the CKM matrix exceeds zero, confirming the sign required for CP violation. Physicists deriving quark mixing angles from ledger geometry cite this to anchor the phase term. The proof unfolds the product expression, substitutes sin(π/2) with one, and chains positivity of the edge ratio, fine-structure constant, and golden-ratio power via multiplication lemmas.
Claim. The Jarlskog invariant satisfies $J > 0$, where $J = (1/24) · (α/2) · φ^{-3} · sin(π/2)$ and sin(π/2) = 1.
background
The MixingDerivation module derives CKM and PMNS elements from edge-dual coupling of 8-tick windows in the cubic ledger, with topological ratios fixing |V_cb| = 1/24 from single-edge to double-vertex coverage and |V_ub| = α/2 from fine-structure leakage. The eight-tick closure enforces unitarity of the mixing matrix. Upstream results supply the fine-structure constant α := 1/α_inv, the structure of J-cost from PhiForcingDerived.of, and ledger factorization from DAlembert.LedgerFactorization.of.
proof idea
The tactic proof unfolds jarlskog_pred into its product, replaces sin(π/2) with 1 using Real.sin_pi_div_two, proves edge_dual_ratio > 0 by simp, α/2 > 0 via alpha_lower_bound and div_pos, and φ^{-3} > 0 via zpow_pos. It then forms successive products with mul_pos and finishes with simpa on the final inequality.
why it matters
This supplies the strict positivity required by jarlskog_witness_pos in the CKM module and row_jarlskog_pos in PMNSScoreCard. It completes the geometric sign requirement for the CP phase inside the Recognition framework, linking directly to the eight-tick octave and phi-ladder. No open scaffolding remains on this sign claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.