vub_derived
plain-language theorem explainer
The declaration establishes that the CKM matrix element |V_ub| equals half the fine-structure constant alpha. Researchers deriving quark mixing from cubic geometry in the Recognition framework would cite this equality. The proof is a one-line wrapper that unfolds the two definitions and applies reflexivity.
Claim. The predicted CKM element satisfies $|V_{ub}| = V_{ub, pred} = $ fine-structure leakage, where fine-structure leakage is defined as $alpha / 2$ and $alpha$ is the fine-structure constant.
background
Module Physics.MixingDerivation formalizes geometric derivation of CKM and PMNS elements from the cubic ledger structure. Edge-dual coupling is set by overlap of 8-tick windows, and topological ratios fix |V_cb| = 1/24 from vertex-edge incidence while |V_ub| arises from leakage across the cube diagonal. fine_structure_leakage is the parity-split term Constants.alpha / 2 that mediates coupling between non-adjacent generations 1 and 3. vertex_edge_slots counts the 24 incidences in a 3-cube. V_ub_pred is introduced as the alias for this leakage term. Upstream results supply the Standard-Model CKM definition of V_cb and the geometric predicate V_ub_pred.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of V_ub_pred and fine_structure_leakage, then applies reflexivity to obtain the equality.
why it matters
The result supplies the vub_leakage field required by the mixing_verified theorem and is invoked directly by row_vub_eq_leakage in the CKM element scorecard. It realizes the paper proposition that |V_ub| = alpha/2 from the cubic ledger, consistent with the eight-tick octave and D = 3 spatial dimensions. The geometric interpretation notes that the first and third generations are separated by the cube diameter, with the 1/2 factor arising from the parity split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.