cabibbo_correction_geometric
plain-language theorem explainer
The declaration equates the Cabibbo radiative correction coefficient of 3/2 to the matching value in the PMNS corrections module, with the factor arising from cubic ledger topology. Researchers deriving CKM parameters from geometric models would cite it to replace numerical fits with topological constraints. The proof is a one-line term wrapper that invokes symmetry on the established matching lemma.
Claim. The Cabibbo radiative correction coefficient equals the PMNS correction coefficient, both fixed at $3/2$ by the requirement of cubic topology in the ledger structure.
background
The module derives CKM and PMNS mixing elements from the cubic ledger using edge-dual coupling, where generation overlaps are set by 8-tick window alignments. Topological ratios fix values such as $|V_{cb}| = 1/24$ from single-edge versus double-vertex coverage and enforce unitarity through 8-tick closure. Upstream results on primitive distinction reduce seven axioms to four structural conditions plus definitional facts, while simplicial ledger theorems confirm algebraic tautologies without new axioms.
proof idea
The proof is a term-mode one-line wrapper. It applies the simpa tactic to the symmetric form of the cabibbo_matches lemma already proved in the PMNSCorrections module, confirming identity between the radiative correction and the geometric definition.
why it matters
This result identifies the 3/2 Cabibbo factor inside the Phase 7.2 geometric derivation, tying it to the same cubic symmetry that produces $|V_{cb}| = 1/24$ and the 8-tick octave closure. It advances the claim that mixing arises from ledger topology rather than free parameters, consistent with T7 and D = 3 landmarks. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.