jarlskog_match
plain-language theorem explainer
The theorem shows that the Jarlskog invariant predicted by the geometric mixing model lies within 20 percent of the measured value 3.08 times 10 to the minus 5. Researchers in particle physics phenomenology would reference this when tracing CP violation to the underlying ledger geometry. The proof rewrites the expression using the fine structure constant and the inverse cube of phi, then encloses it between explicit numerical bounds derived from interval estimates on alpha and phi.
Claim. The absolute value of the difference between the predicted Jarlskog invariant $J = α φ^{-3}/48$ and $3.08 × 10^{-5}$ satisfies $|J - 3.08 × 10^{-5}| < 0.6 × 10^{-5}$.
background
In the mixing derivation module the CKM matrix elements arise from edge-dual coupling between generations in the cubic ledger, with the 8-tick octave enforcing unitarity. The Jarlskog invariant quantifies the CP-violating phase in this framework. The fine-structure constant alpha is defined as the reciprocal of its inverse, and phi denotes the golden ratio fixed point from the forcing chain. The module replaces numerical fits with topological proofs for ratios such as V_cb equal to 1 over 24 and V_ub equal to alpha over 2.
proof idea
The proof begins by confirming that the sine of the CP phase equals one. It then unfolds the definition of the predicted invariant and simplifies to obtain the closed form alpha times phi to the minus three over 48. Interval bounds on alpha and on phi inverse cubed are imported from the CKM geometry module. The absolute value inequality is expanded, and separate lower and upper bounds are established using nlinarith for the products and linarith for the final comparisons.
why it matters
This theorem supplies the Jarlskog row in the PMNS score card. It confirms the geometric origin of CP violation within the Recognition Science framework, connecting to the eight-tick octave and the alpha band. The result closes the verification loop for the mixing matrix derivation from the cubic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.