theorem
proved
phi3_eq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder on GitHub at line 52.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
49noncomputable def cabibboPhi : ℝ := (phi ^ 3)⁻¹
50
51/-- φ³ = 2φ + 1. -/
52theorem phi3_eq : phi ^ 3 = 2 * phi + 1 := by nlinarith [phi_sq_eq]
53
54/-- 1/φ³ ∈ (0.225, 0.240) — contains PDG λ = 0.2247. -/
55theorem cabibbo_in_band :
56 (0.225 : ℝ) < cabibboPhi ∧ cabibboPhi < 0.240 := by
57 unfold cabibboPhi
58 rw [phi3_eq]
59 have h1 := phi_gt_onePointSixOne
60 have h2 := phi_lt_onePointSixTwo
61 constructor
62 · rw [lt_inv_comm₀ (by norm_num) (by linarith)]
63 linarith
64 · rw [inv_lt_comm₀ (by linarith) (by norm_num)]
65 linarith
66
67structure CKMLambdaCert where
68 wolfenstein_A : wolfensteinA = 9 / 11
69 A_in_pdg : |(wolfensteinA : ℝ) - 0.826| < 0.013
70 cabibbo_phi3 : phi ^ 3 = 2 * phi + 1
71 cabibbo_band : (0.225 : ℝ) < cabibboPhi ∧ cabibboPhi < 0.240
72
73noncomputable def ckmlambdaCert : CKMLambdaCert where
74 wolfenstein_A := wolfensteinA_val
75 A_in_pdg := wolfensteinA_in_pdg_band
76 cabibbo_phi3 := phi3_eq
77 cabibbo_band := cabibbo_in_band
78
79end IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder