cabibbo_coefficient
plain-language theorem explainer
The definition assigns the rational 3/2 to the Cabibbo coefficient for PMNS radiative corrections. Researchers working on geometric derivations of mixing angles cite this value when assembling the full set of integer prefactors. It is introduced as the direct ratio of six cube faces to four vertex-edge slots in the 3D ledger.
Claim. The Cabibbo coefficient is defined to be the rational number $3/2$.
background
The module derives integer coefficients appearing in PMNS mixing-angle predictions from the topology of a 3-cube. Atmospheric mixing uses the six faces directly, solar mixing subtracts an active pair from the twelve edges to obtain ten, and the Cabibbo sector uses the six faces divided by four vertex-edge slots. The module states that all three integers are forced by the cube topology of the 3D voxel ledger rather than chosen by hand.
proof idea
This is a direct definition that sets the coefficient to the rational 3/2. Downstream theorems such as cabibbo_coefficient_from_geometry recover the same value by unfolding cube_faces and applying norm_num.
why it matters
It supplies the prefactor for the Cabibbo term (3/2)α that enters the CKM sector. The theorems cabibbo_correction_eq and cabibbo_matches apply it to obtain equality with MixingGeometry.cabibbo_radiative_correction. The structure CorrectionDerivationCert records cabibbo_coefficient = (cube_faces 3 : ℚ) / 4 together with the atmospheric and solar cases, certifying that the integers 6, 10, 3/2 are forced by the same 3D cubic ledger that yields D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.