V_cb_real
plain-language theorem explainer
V_cb_real casts the rational 1 over the edge-dual count of an RSBridge into a real for embedding in mixing-angle triples. CKM phenomenology groups working inside Recognition Science ledger geometry cite it when converting the exact 1/24 result into real arithmetic for downstream matrix assembly. The definition is a direct cast from V_cb_from_bridge.
Claim. Let $B$ be an RSBridge over ledger $L$. Then $V_{cb}(B) := 1/B. edgeDual$ cast to type $ℝ$, where edgeDual defaults to 24.
background
RSBridge augments a basic Bridge with geometric fields: edgeDual (default edgeDualCount = 24 for the cube dual), alphaExponent, and phiProj (default -3). V_cb_from_bridge returns the exact rational 1/B.edgeDual, encoding second-to-third generation mixing as the inverse of dual edge count. The module RecogSpec.RSBridge derives all three CKM angles from ledger geometry (V_ub = α/2, V_cb = 1/24, V_us via φ-ladder) rather than free parameters, consistent with the eight-tick octave and D = 3.
proof idea
One-line wrapper that casts the rational output of V_cb_from_bridge B to type ℝ.
why it matters
Supplies the real V_cb to mixingFromCycles, which assembles the full CkmMixingAngles triple. It completes the geometric derivation of the CKM matrix inside the Recognition framework, replacing arbitrary parameters with counts from the dual structure. The construction aligns with T7 (eight-tick octave) via the factor 24 = 2^3 × 3 and feeds the alpha band and phi-ladder results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.