V_cb
plain-language theorem explainer
V_cb defines the real number for the CKM charm-to-bottom element as the geometric prediction V_cb_pred. Researchers computing quark mixing from phi-ladder rung differences cite it when constructing s23 or the Jarlskog invariant. The implementation is a direct one-line alias to the upstream geometric definition.
Claim. $V_{cb} := V_{cb, pred}$ where $V_{cb, pred}$ equals the real cast of the edge-dual ratio, which is the inverse of twice the cube edge count.
background
The CKM module derives mixing angles from rung differences on the phi-ladder between up and down quark generations at positions 0, 11 and 17. Angles satisfy θ_ij ~ φ^{-Δτ/2} and the Jarlskog invariant emerges as a forced dimensionless output from residue asymmetry, with all elements grounded in geometric proofs from MixingDerivation.lean. V_cb is the 2-3 generation transition element. Upstream, V_cb_pred is defined as the real number V_cb_geom, and the doc-comment states that V_cb is the inverse of twice the total edge count (1/24).
proof idea
This definition is a one-line wrapper that directly aliases V_cb to V_cb_pred from the CKMGeometry module.
why it matters
V_cb supplies the value used in torsion_differences, which fixes the rung spacings 11, 6 and 17, and in jarlskog_witness_pos. It realizes the geometric prediction inside the T11Cert structure, where V_cb_geom = 1/(2 * cube_edges 3) and the match to experiment is certified. In the Recognition Science framework it anchors CKM phenomenology to the eight-tick octave and the phi-ladder, closing the step from rung differences to observable mixing parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.