V_cb_match
plain-language theorem explainer
The declaration proves that the geometrically predicted CKM matrix element |V_cb| equals 1/24 and lies within one sigma of the experimental measurement 0.04182 with uncertainty 0.00085. Flavor physicists and phenomenologists studying quark mixing would reference this as evidence that the CKM parameters emerge from cubic ledger geometry rather than being free inputs. The proof reduces to unfolding the rational definitions via simp and confirming the inequality with norm_num.
Claim. $|1/24 - 0.04182| < 0.00085$
background
The CKMGeometry module derives the Cabibbo-Kobayashi-Maskawa matrix elements from the geometry of the cubic ledger and the fine-structure constant. For the element V_cb corresponding to the theta_23 mixing angle, the model predicts exactly 1/24 from the inverse of twice the total edge count on the lattice. The experimental comparison uses the observed central value 0.04182 and uncertainty 0.00085, which are treated as fixed inputs for this verification. This result is independent of alpha, unlike the predictions for V_ub and V_us.
proof idea
The proof is a direct term-mode verification. It applies simp to unfold V_cb_pred (defined as V_cb_geom), V_cb_exp, V_cb_err, and the edge_dual_ratio auxiliary, then uses norm_num to evaluate the absolute difference and confirm it is strictly less than the error bound.
why it matters
This theorem completes the T11 verification for V_cb within the CKMGeometry module, feeding directly into the scorecard row_V_cb and the T11 certificate t11_V_cb_verified. It demonstrates that the edge-dual coupling on the cubic lattice yields a rational prediction matching observation to high precision, supporting the broader claim that CKM parameters are geometrically determined. In the Recognition Science framework, this aligns with the derivation of spatial dimensions and self-similar structures from the forcing chain, here applied to flavor mixing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.