T11Cert
plain-language theorem explainer
T11Cert records that the CKM element V_cb equals exactly 1/24 from the edge count of the 3-cube and lies inside the PDG experimental band. A physicist deriving mixing angles from hypercube combinatorics or ledger geometry would cite the certificate to fix the theta_23 prediction. The structure is introduced by two direct field assertions, one algebraic identity and one numerical inequality, with no further proof steps required.
Claim. The T11 certificate asserts that the geometric CKM element satisfies $V_{cb}^{geom} = 1/(2 E_3) = 1/24$ where $E_3 = 3·2^{2}$ is the edge count of the 3-cube, and that the predicted real value obeys $|V_{cb}^{pred} - 0.04182| < 0.00085$.
background
The module derives CKM matrix elements from cubic ledger geometry. For the theta_23 angle, V_cb is the edge-dual coupling given by the inverse of twice the total edge count on the 3-cube. V_cb_geom is the rational 1/24 obtained as the edge dual ratio. V_cb_pred is its real embedding. The experimental anchors are the constants V_cb_exp = 0.04182 and V_cb_err = 0.00085. Upstream, cube_edges(d) is defined as d·2^(d-1), supplying the combinatorial count for dimension 3.
proof idea
The structure is defined by direct field assignment. The geometric_origin field is set to the equality V_cb_geom = 1/(2·cube_edges 3) using the upstream edge-count definition. The matches_pdg field is set to the absolute-difference inequality against the pre-declared experimental bounds. No tactics or lemmas are invoked beyond the field constructors.
why it matters
T11Cert supplies the verified rational anchor for V_cb inside the CKMGeometry module and is instantiated by the downstream definition t11_V_cb_verified. It realizes the T11 step of the CKM geometry hypothesis, where |V_cb| = 1/24 follows from D = 3 spatial dimensions and the cubic ledger. In the Recognition framework this closes the exact-rational part of the mixing-angle derivation, leaving only interval-arithmetic obligations for the alpha-dependent elements V_us and V_ub.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.