cabibbo_matches
plain-language theorem explainer
The theorem establishes equality between the Cabibbo correction coefficient and its counterpart from mixing geometry. Physicists deriving CKM matrix elements from the cubic ledger in Recognition Science would cite it to confirm the 3/2 factor originates in vertex-edge duality rather than free parameters. The proof is a one-line term wrapper that unfolds the two definitions, expands the coefficient, and applies norm_num to confirm numerical identity.
Claim. The Cabibbo correction coefficient equals the radiative correction from mixing geometry, where the former is defined as $(3/2)α$ via vertex-edge duality on the 3-cube.
background
The PMNS Radiative Correction Derivation module obtains the integer coefficients 6, 10, and 3/2 that appear in the predicted mixing angles sin²θ₁₃ = φ⁻⁸, sin²θ₁₂ = φ⁻² − 10α, and sin²θ₂₃ = ½ + 6α. These integers are forced by the topology of the 3D cubic ledger: a 3-cube possesses 6 faces, 12 edges, and 8 vertices, with the Cabibbo sector using the ratio of faces to vertex-edge slots to produce the factor 3/2. Upstream structures from LedgerFactorization and PhiForcingDerived supply the J-cost calibration and ledger factorization that underwrite the geometric counting.
proof idea
The term-mode proof unfolds cabibbo_correction and the mixing-geometry version, then unfolds the underlying cabibbo_coefficient definition, after which norm_num reduces both sides to the same numerical expression.
why it matters
It directly supports the parent theorem cabibbo_correction_geometric, which asserts that the Cabibbo radiative correction (3/2) is forced by cube topology and yields V_cb from ledger geometry. The result closes one link in the chain from the eight-tick octave and D = 3 to the observed CKM parameters, consistent with the Recognition Science derivation of constants inside the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.