def
definition
V_ub
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.CKM on GitHub at line 33.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
30-- Grounded CKM elements from geometric predictions
31noncomputable def V_us : ℝ := V_us_pred
32noncomputable def V_cb : ℝ := V_cb_pred
33noncomputable def V_ub : ℝ := V_ub_pred
34
35-- Derived diagonal elements (approximate unitarity)
36noncomputable def V_ud : ℝ := Real.sqrt (1 - V_us^2)
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