def
definition
jarlskog
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CKM on GitHub at line 40.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
37noncomputable def V_cd : ℝ := - V_us
38
39-- Jarlskog invariant grounded in geometric prediction
40noncomputable def jarlskog : ℝ := jarlskog_pred
41
42/-- Phenomenological facts required by the CKM demo.
43 Documented in `docs/Assumptions.md`. -/
44structure CKMPhenomenology where
45 j_value : ℝ
46 j_positive : j_value > 0
47 j_matches_experiment : jarlskog ≈ j_value
48
49/-- Dimensionless inevitability when supplied with phenomenological data. -/
50def jarlskog_summary (facts : CKMPhenomenology) : Prop :=
51 jarlskog > 0 ∧ jarlskog ≈ facts.j_value
52
53lemma jarlskog_summary_of_facts (facts : CKMPhenomenology)
54 (hpos : jarlskog > 0 := facts.j_positive)
55 (hexp : jarlskog ≈ facts.j_value := facts.j_matches_experiment) :
56 jarlskog_summary facts :=
57 ⟨hpos, hexp⟩
58
59/- Auxiliary positive witness using φ-rung sines (keeps algebra simple). -/
60noncomputable def s12_w : ℝ := V_us
61noncomputable def s23_w : ℝ := V_cb
62noncomputable def s13_w : ℝ := V_ub
63
64noncomputable def jarlskog_witness : ℝ := s12_w * s23_w * s13_w
65
66/-- The witness is strictly positive (grounded in jarlskog_pos). -/
67theorem jarlskog_witness_pos : jarlskog_witness > 0 := by
68 have h := MixingDerivation.jarlskog_pos
69 unfold jarlskog_witness s12_w s23_w s13_w
70 -- jarlskog_pred = edge_dual_ratio * fine_structure_leakage * torsion_overlap * sin ckm_cp_phase