jarlskog_summary
plain-language theorem explainer
The declaration defines a proposition asserting positivity of the Jarlskog invariant together with its numerical match to supplied phenomenological data. A physicist modeling CKM mixing angles from the phi-ladder would cite it to record that the CP-violating measure emerges as a forced dimensionless output. The definition is a direct conjunction packaging the two record fields from the CKMPhenomenology structure.
Claim. Let $J$ be the Jarlskog invariant. Given a record $f$ of phenomenological facts whose field $j$ satisfies $j>0$ and $J$ approximates $j$, the summary asserts $J>0$ and $J$ approximates the value in $f$.
background
The module derives the CKM matrix from rung differences on the phi-ladder between up and down quark generations at tau_g = 0, 11, 17. Mixing angles satisfy theta_ij ~ phi^{-Delta tau / 2} and the Jarlskog invariant J = Im(V_ud V_cb V_ub^* V_cd^*) appears as a forced dimensionless quantity with no free parameters. CKMPhenomenology is the structure that packages the experimental anchor: a real j_value together with the two assertions j_value > 0 and jarlskog approximates j_value. The upstream jarlskog definition supplies the left-hand side of the approximation as jarlskog_pred.
proof idea
The definition is a one-line wrapper that returns the conjunction jarlskog > 0 and jarlskog approximates facts.j_value. It directly references the two fields of the CKMPhenomenology record and the jarlskog constant defined earlier in the same module.
why it matters
This definition supplies the target proposition for the downstream lemma jarlskog_summary_of_facts, which constructs an instance from the record fields. It records the dimensionless inevitability of the Jarlskog invariant once the phi-ladder geometry is granted, closing the link between the geometric proofs in MixingDerivation and the phenomenological summary. The step sits inside the broader derivation of CP violation from rung asymmetry on the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.