CKMPhenomenology
plain-language theorem explainer
CKMPhenomenology packages a positive real number that approximates the Jarlskog invariant for use in CKM mixing derivations. Zero-parameter model builders cite it to supply experimental inputs when invoking the inevitability theorem. The declaration is introduced as a bare structure definition carrying three fields and no computational body.
Claim. A record consisting of a real number $j>0$ such that $j$ approximates the Jarlskog invariant $J=Im(V_{ud}V_{cb}V_{ub}^*V_{cd}^*)$.
background
The CKM module derives mixing angles from rung differences on the phi-ladder with generation labels tau_g=0,11,17, producing theta_ij ~ phi^{-Delta tau/2} and the Jarlskog invariant from residue asymmetry. The structure supplies the required phenomenological value for J, documented in Assumptions.md, to connect the derivation to the Inevitability Theorem. That theorem states any zero-parameter alternative framework deriving observables must match RS cost and selection or violate a necessity gate.
proof idea
This is a structure definition that collects a real value, its positivity proof, and an approximation to the jarlskog definition. No lemmas or tactics are applied; the declaration serves only as a data carrier for downstream summaries.
why it matters
It provides the phenomenological interface inside the CKM module, which derives the mixing matrix from the phi-ladder without adjustable parameters. The structure feeds jarlskog_summary and jarlskog_summary_of_facts, linking directly to the inevitability theorem. This supports the framework claim that CKM phenomenology emerges as a forced dimensionless output consistent with J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.