t11_V_cb_verified
plain-language theorem explainer
The T11 certificate for the CKM element V_cb records that its geometric value equals exactly 1/24 from cube edge geometry and that this value lies within experimental uncertainty of the measured PDG datum. Quark mixing studies would cite the result when testing whether ledger geometry fixes the Cabibbo-Kobayashi-Maskawa parameters. The declaration is a direct packaging of the two component theorems into the required certificate structure.
Claim. The T11 certificate asserts that the geometric value of the CKM matrix element satisfies $V_{cb} = 1/24$ and that the absolute difference between the predicted and experimental values obeys $|V_{cb}^{pred} - V_{cb}^{exp}| < V_{cb}^{err}$.
background
The CKMGeometry module derives the three CKM matrix elements from cubic ledger geometry together with the fine-structure constant. T11Cert is the structure that packages the two required properties for the V_cb component: geometric_origin requires V_cb_geom to equal 1 over twice the cube edge count in three dimensions, while matches_pdg requires the absolute difference between prediction and experiment to lie inside the stated uncertainty.
proof idea
The definition constructs a T11Cert instance by direct field assignment, supplying the geometric equality from the V_cb_from_cube_edges theorem and the numerical match from the V_cb_match theorem.
why it matters
This definition closes the exact verification for the V_cb term in the T11 hypothesis of the CKM matrix geometry. The module states that 1/24 is now proven as an exact rational, completing one of the three geometric predictions for the mixing angles. It sits downstream of the edge-dual ratio and cube-edges lemmas and supplies the verified certificate for any later use of the full T11 statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.