def
definition
s23_w
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 61.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
71 -- s12 * s23 * s13 = V_us * V_cb * V_ub
72 -- This matches the terms in jarlskog_pred up to radiative corrections.
73 unfold V_us_pred V_cb_pred V_ub_pred
74 unfold edge_dual_ratio fine_structure_leakage torsion_overlap
75 -- The witness is positive because each component is positive.
76 have h_us : 0 < V_us_pred := by
77 -- V_us_pred = torsion_overlap - cabibbo_radiative_correction
78 unfold V_us_pred torsion_overlap cabibbo_radiative_correction
79 have h1 := phi_inv3_lower_bound
80 have h2 := alpha_upper_bound
81 -- phi^-3 > 0.236, alpha < 0.00731
82 -- 1.5 * alpha < 1.5 * 0.00731 = 0.010965
83 -- US > 0.236 - 0.010965 = 0.225035 > 0
84 linarith
85 have h_cb : 0 < V_cb_pred := by unfold V_cb_pred; norm_num
86 have h_ub : 0 < V_ub_pred := by unfold V_ub_pred fine_structure_leakage; exact div_pos Constants.alpha_pos (by norm_num)
87 exact mul_pos (mul_pos h_us h_cb) h_ub
88
89end Physics
90end IndisputableMonolith