`rho_bar_interval`

proved

show as: view math explainer →

module: IndisputableMonolith.StandardModel.CKMMatrix
domain: StandardModel
line: 250 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.CKMMatrix on GitHub at line 250.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 247
 248/-- ρ̄ is in the RS-predicted interval (0.10, 0.20).
 249    From unitarity triangle with δ = π/2: the real part ρ̄ ≈ 0.13. -/
 250theorem rho_bar_interval : (0.10 : ℝ) < wolfenstein_rho ∧ wolfenstein_rho < 0.20 := by
 251  unfold wolfenstein_rho; constructor <;> norm_num
 252
 253/-- The unitarity constraint ρ̄² + η̄² < 1 holds (required for V unitary). -/
 254theorem unitarity_triangle_valid :
 255    wolfenstein_rho^2 + wolfenstein_eta^2 < 1 := by
 256  unfold wolfenstein_rho wolfenstein_eta; norm_num
 257
 258/-! ## Experimental Verification -/
 259
 260/-- CKM elements are precisely measured:
 261
 262    | Element | Value | Error |
 263    |---------|-------|-------|
 264    | V_ud | 0.97373 | 0.00031 |
 265    | V_us | 0.2243 | 0.0008 |
 266    | V_ub | 0.00382 | 0.00020 |
 267    | V_cd | 0.221 | 0.004 |
 268    | V_cs | 0.975 | 0.006 |
 269    | V_cb | 0.0408 | 0.0014 |
 270    | V_td | 0.0080 | 0.0003 |
 271    | V_ts | 0.0388 | 0.0011 |
 272    | V_tb | 1.013 | 0.030 |
 273
 274    The hierarchy |V_ub| << |V_cb| << |V_us| is evident. -/
 275def experimentalValues : List (String × ℝ × ℝ) := [
 276  ("V_ud", 0.97373, 0.00031),
 277  ("V_us", 0.2243, 0.0008),
 278  ("V_ub", 0.00382, 0.0002),
 279  ("V_cb", 0.0408, 0.0014)
 280]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.