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

vcb_geometric_origin

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)

  78theorem vcb_geometric_origin :
  79    V_cb_pred = 1 / vertex_edge_slots := by

proof body

Tactic-mode proof.

  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.
  87  simp [CKMGeometry.V_cb_pred, CKMGeometry.V_cb_geom, edge_dual_ratio, hslots]
  88
  89/-! ## Neutrino Sector (PMNS) -/
  90
  91/-- The PMNS mixing weights follow the Born rule over the ladder steps.
  92    Weight W_ij = exp(-Δτ_ij * J_bit) = φ^-Δτ_ij. -/

depends on (14)

Lean names referenced from this declaration's body.