V_cb_approx
plain-language theorem explainer
The declaration confirms that one twenty-fourth lies strictly between 0.04 and 0.05. A physicist deriving CKM elements from Recognition Science geometry cites it to verify the numerical placement of the V_cb mixing angle obtained from cube dual edge counts. The proof is a one-line wrapper that splits the conjunction and normalizes the rational inequalities.
Claim. $ 1/24 > 0.04 $ and $ 1/24 < 0.05 $
background
RSBridge derives CKM mixing angles from ledger geometry rather than free parameters. The edge-dual coupling supplies the factor 24, identified as twice the twelve edges of the cube dual, so that V_cb equals 1/24. The module also records the companion approximations V_us ≈ φ^{-3} - (3/2)α and V_ub = α/2, all obtained from geometric counts and the φ-ladder projection.
proof idea
The proof is a one-line wrapper. Constructor splits the conjunction into two separate inequalities; norm_num then evaluates the rational arithmetic directly.
why it matters
The bound supplies a quick numeric sanity check for the geometric derivation of V_cb = 1/24 inside RSBridge. That derivation replaces arbitrary CKM parameters with counts from the cube dual and the φ-ladder, consistent with the framework's use of edge-dual couplings and eight-tick octave structure. The result closes a verification step before the full mixing-angle theorems are assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.