`step_charm_strange`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.MixingGeometry
domain: Physics
line: 83 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.MixingGeometry on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  80def step_bottom_charm : ℚ := 10 / 4
  81
  82/-- Step from Charm to Strange: 5.50 rungs. -/
  83def step_charm_strange : ℚ := 22 / 4
  84
  85/-- The radiative correction factor for the Cabibbo angle.
  86    Represented as 1.5 * alpha, derived from 6 faces / 4 vertex-edge weight. -/
  87noncomputable def cabibbo_radiative_correction : ℝ := (3/2) * Constants.alpha
  88
  89/-- **THEOREM: Cabibbo Scaling Forced**
  90    The Cabibbo scaling factor is forced by the torsion overlap and the
  91    face-mediated radiative corrections. -/
  92theorem cabibbo_scaling_forced :
  93    torsion_overlap - cabibbo_radiative_correction = phi ^ (-3 : ℤ) - (3/2) * Constants.alpha := by
  94  unfold torsion_overlap cabibbo_radiative_correction
  95  ring
  96
  97end MixingGeometry
  98end Physics
  99end IndisputableMonolith

papers checked against this theorem

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