def
definition
radiativeCoeff
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogSpec.RSBridge on GitHub at line 53.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
50def cabibboProjection : ℤ := -3
51
52/-- The radiative correction coefficient -/
53def radiativeCoeff : ℚ := 3/2
54
55/-! ## RSBridge Structure -/
56
57/-- A bridge with geometric coupling structure for mixing angles.
58
59This extends the minimal `Bridge` with fields that determine the CKM matrix
60from geometric structure rather than arbitrary parameters.
61-/
62structure RSBridge (L : RSLedger) where
63 /-- The underlying bridge -/
64 toBridge : Bridge L.toLedger
65 /-- Edge count of dual structure (default: 24) -/
66 edgeDual : ℕ := edgeDualCount
67 /-- Fine structure exponent for V_ub -/
68 alphaExponent : ℝ
69 /-- Golden projection exponent for Cabibbo (default: -3) -/
70 phiProj : ℤ := cabibboProjection
71 /-- Radiative correction coefficient (default: 3/2) -/
72 radCoeff : ℚ := radiativeCoeff
73 /-- Loop order exponent for g-2 derivation (default: 5) -/
74 loopOrder : ℕ := 5
75
76/-! ## Mixing Angles from Bridge Structure -/
77
78variable {L : RSLedger}
79
80/-- V_cb from edge-dual geometry: 1/24
81
82This is EXACT — the mixing is the inverse of the dual edge count.
83-/