cp_violation_small
plain-language theorem explainer
The theorem shows that the Jarlskog invariant measuring CP violation in the CKM matrix is positive but bounded above by 10^{-4}. Particle physicists examining quark flavor mixing and CP violation in extensions of the Standard Model would cite this when matching Recognition Science outputs to data. The proof is a one-line wrapper that unfolds the invariant definition and applies numerical normalization to confirm both sides of the conjunction.
Claim. The Jarlskog invariant $J$ of the CKM matrix satisfies $0 < J < 10^{-4}$.
background
In the Recognition Science treatment of the Standard Model, the CKM matrix is obtained from φ-quantized mixing angles that arise from the eight-tick phase structure. The module derives the nine complex entries from golden-ratio geometry, producing the observed hierarchy of magnitudes and a single physical phase responsible for CP violation. Upstream, SpectralEmergence supplies the three-generation structure and the SU(3)×SU(2)×U(1) gauge content, while PhiForcingDerived encodes the J-cost that quantizes the angles.
proof idea
The proof unfolds the definition of the Jarlskog invariant, splits the conjunction with constructor, and discharges both inequalities by norm_num.
why it matters
The result confirms that Recognition Science reproduces the small but nonzero CP violation observed in the quark sector, consistent with the φ-forcing chain and the eight-tick octave that sets the phase quantization. It supports the paper proposition on CKM matrix elements from golden-ratio geometry. No downstream theorems are listed, leaving the explicit numerical prediction of the invariant for later closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.