vcb_geometric_origin
plain-language theorem explainer
The declaration proves that the geometrically predicted CKM mixing element V_cb equals one over the vertex-edge slot count in the cubic ledger. Researchers deriving quark mixing angles from Recognition Science would cite this when replacing numerical fits with topological ratios. The short tactic proof first casts the slot count equality to reals then simplifies the geometric predicates for V_cb_pred and the edge dual ratio.
Claim. The predicted CKM matrix element satisfies $V_{cb}^{pred} = 1/24$, where the denominator is the total number of vertex-edge incidences obtained from twelve cube edges each incident to two vertices.
background
In the cubic ledger the twelve edges and eight vertices produce twenty-four vertex-edge incidences, which the module treats as the coverage space for single-edge contributions. The local setting is Phase 7.2, which derives CKM elements from edge-dual coupling between 8-tick generation windows and states that |V_cb| emerges as the ratio of one edge to the double-vertex total. Upstream results supply the slot-count lemma vertex_edge_slots_eq_24 together with the simplicial ledger identifications that convert combinatorial counts into real-valued ratios.
proof idea
The tactic proof opens with a have that invokes vertex_edge_slots_eq_24 and applies norm_cast to obtain the real equality 24. It then finishes with a single simp call that unfolds V_cb_pred, V_cb_geom and edge_dual_ratio while substituting the slot value, yielding immediate equality.
why it matters
This supplies the explicit geometric origin for the observed suppression of V_cb inside the CKM matrix, instantiating the topological ratio stated in the module doc-comment. It forms a leaf in the Phase 7.2 chain that replaces empirical inputs with proofs from the cubic structure and the eight-tick octave closure. No downstream theorems yet consume it, leaving the full unitarity argument for later declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.