cabibbo_correction_eq
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.