cabibbo_correction_eq
The equality establishes that the Cabibbo radiative correction equals three-halves times the fine-structure constant. Researchers deriving CKM and PMNS mixing angles from 3-cube topology would cite this result to fix the quark-sector coefficient. The term-mode proof reduces the claim to a numeric identity by unfolding the coefficient definition and applying normalization.
claimThe Cabibbo radiative correction equals $ (3/2) alpha $, where $ alpha $ is the fine-structure constant and the prefactor $ 3/2 $ is obtained as the ratio of the six faces of a 3-cube to four vertex-edge slots.
background
The PMNS Radiative Correction Derivation module obtains integer coefficients for mixing-angle corrections from the topology of the 3-cube. The Cabibbo coefficient is defined as the rational 3/2, interpreted as six faces divided by four vertex-edge slots under face-diagonal torsion. The fine-structure constant is imported as the definition alpha := 1/alphaInv from Constants.Alpha. The upstream phi-ladder lattice hypothesis supplies the Poisson-summation infrastructure for related analytic steps, although it is not invoked in this equality.
proof idea
The term proof unfolds cabibbo_correction (defined as cabibbo_coefficient times alpha) and cabibbo_coefficient (the constant 3/2), then applies norm_num to reduce the resulting rational multiple to an identity.
why it matters in Recognition Science
The theorem completes the geometric derivation of the 3/2 coefficient for the Cabibbo sector inside the cube-topology framework, feeding the PMNS predictions sin²θ₁₃ = φ⁻⁸, sin²θ₁₂ = φ⁻² − 10α and sin²θ₂₃ = ½ + 6α. It instantiates the D = 3 spatial dimensions and eight-tick octave closure of the Recognition Science chain by converting vertex-edge counts into the observed radiative adjustment. No downstream usage is recorded, leaving the result as a self-contained closure of the coefficient list.
scope and limits
- Does not derive the numerical value of alpha from first principles.
- Does not include higher-order radiative corrections beyond the leading term.
- Does not incorporate experimental mixing-angle data.
- Does not address neutrino mass terms or hierarchies.
formal statement (Lean)
138theorem cabibbo_correction_eq : cabibbo_correction = (3/2) * alpha := by
proof body
Term-mode proof.
139 unfold cabibbo_correction cabibbo_coefficient
140 norm_num
141
142/-! ## Verification Against MixingGeometry -/
143
144/-- Verify that our derived corrections match MixingGeometry definitions. -/