V_cb_exp
plain-language theorem explainer
Experimental input for the CKM mixing verification enters through the constant 0.04182, which records the measured magnitude of the matrix element connecting charm and bottom quarks. Ledger-geometry derivations cite this value to test the edge-dual coupling prediction of exactly 1/24 against laboratory data. The declaration is a bare numerical assignment taken from external measurements.
Claim. The observed magnitude of the CKM matrix element $|V_{cb}|$ equals 0.04182.
background
The CKMGeometry module derives the three CKM magnitudes from cubic ledger couplings and the fine-structure constant. For $|V_{cb}|$ the module isolates an edge-dual coupling on the cube that produces the exact rational 1/24. The experimental central value is supplied here so that the match test can be performed inside the T11 certificate and the element scorecard.
proof idea
The declaration is a one-line definition that directly assigns the numerical constant 0.04182 drawn from particle data compilations.
why it matters
This definition supplies the benchmark used by T11Cert and V_cb_match to confirm that the geometric prediction 1/24 lies inside the reported uncertainty. It closes the verification loop for the edge-dual coupling inside the T11 hypothesis that all CKM elements follow from alpha and the phi-ladder. The parent structures CKMElementScoreCardCert and row_V_cb both invoke it to certify the match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.