vcb_geometric_origin

formal source

  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.
  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. -/
  93noncomputable def pmns_weight (dτ : ℤ) : ℝ :=
  94  Real.exp (- (dτ : ℝ) * J_bit)
  95
  96theorem pmns_weight_eq_phi_pow (dτ : ℤ) :
  97    pmns_weight dτ = phi ^ (-dτ : ℤ) := by
  98  -- Algebraic identity: exp(-dτ * ln(φ)) = φ^(-dτ)
  99  unfold pmns_weight
 100  -- simp turns RHS into inverse form via `zpow_neg`
 101  simp [J_bit]
 102  have hphi_pos : 0 < phi := phi_pos
 103  -- exp(-x) = (exp x)⁻¹
 104  rw [Real.exp_neg]
 105  have hexp : Real.exp (↑dτ * Real.log phi) = phi ^ (dτ : ℝ) := by
 106    calc
 107      Real.exp (↑dτ * Real.log phi)
 108          = Real.exp (Real.log phi * (dτ : ℝ)) := by simpa [mul_comm]