theorem
proved
vcb_derived
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.MixingDerivation on GitHub at line 56.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
Structure -
of -
is -
of -
from -
is -
of -
is -
of -
parity -
is -
and -
V_ub -
V_cb_geom -
V_cb_pred -
edge_dual_ratio -
fine_structure_leakage -
half -
half -
constant -
V_ub -
half -
vacuum -
overlap
used by
formal source
53 - Edge-Dual Coupling: The second generation (s, c) occupies the faces, while the
54 third generation (b, t) occupies the vertices. The transition $|V_{cb}|$
55 represents the dual mapping from a face-center to a vertex via a single edge. -/
56theorem vcb_derived :
57 V_cb_pred = edge_dual_ratio := by
58 unfold V_cb_pred V_cb_geom edge_dual_ratio
59 norm_num
60
61/-- **THEOREM: V_ub from Fine Structure Leakage**
62 The CKM element $|V_{ub}|$ is exactly half the fine-structure constant.
63 - α: Fine structure coupling.
64 - 1/2: Leakage between non-adjacent vertices across a cube diagonal (fine_structure_leakage).
65 - Geometric Origin: The first and third generations are separated by the maximum
66 diameter of the cube (√3 units). The recognition overlap is mediated by the
67 vacuum polarization term α, with a 1/2 factor from the parity split. -/
68theorem vub_derived :
69 V_ub_pred = fine_structure_leakage := by
70 unfold V_ub_pred fine_structure_leakage
71 rfl
72
73/-- **Geometric Interpretation**:
74 - 12 edges in a cube.
75 - Each edge has 2 vertices.
76 - Total coverage space = 24 (vertex_edge_slots).
77 - V_cb represents the single-edge contribution. -/
78theorem vcb_geometric_origin :
79 V_cb_pred = 1 / vertex_edge_slots := by
80 -- 1/24 = 1/(2 * 12) = 1/vertex_edge_slots
81 -- Reduce both sides to 1/24 using the proven slot count.
82 have hslots : (vertex_edge_slots : ℝ) = 24 := by
83 -- vertex_edge_slots = 24 as a Nat; cast to ℝ.
84 have h := vertex_edge_slots_eq_24
85 norm_cast at h
86 -- Now `V_cb_pred` is `1/24` (as a real), so both sides match.