pith. machine review for the scientific record. sign in
theorem proved term proof

vcb_derived

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  56theorem vcb_derived :
  57    V_cb_pred = edge_dual_ratio := by

proof body

Term-mode proof.

  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. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (25)

Lean names referenced from this declaration's body.