cabibbo_correction
plain-language theorem explainer
The Cabibbo radiative correction equals (3/2) times the fine-structure constant. Physicists deriving PMNS mixing angles from cube topology cite this when inserting the quark-sector correction into angle predictions. The definition is a direct cast-and-multiply of the precomputed rational coefficient by alpha.
Claim. The Cabibbo radiative correction is given by $ (3/2) alpha $, where $alpha$ is the fine-structure constant.
background
The module derives the integer coefficients (6, 10, 3/2) that appear in PMNS mixing-angle formulas from the topology of a 3-cube. The coefficient 3/2 is obtained as faces divided by 4, reflecting vertex-edge duality in the quark sector under face-diagonal torsion. Alpha is imported as the fine-structure constant from Constants.Alpha.
proof idea
One-line definition that casts the rational cabibbo_coefficient (3/2) to real and multiplies by alpha.
why it matters
This supplies the explicit radiative term used by cabibbo_correction_geometric and cabibbo_matches to confirm agreement with MixingGeometry. It completes the cube-topology derivation of the Cabibbo coefficient, tying the quark-sector correction to the 3D voxel ledger and the eight-tick octave. The parent theorems verify that the 3/2 factor is forced by the same geometry that produces the atmospheric and solar corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.