PathWeight

formal source

 141    W[γ] = exp(-C[γ])
 142
 143    This is the fundamental quantity that gives rise to the Born rule. -/
 144noncomputable def PathWeight (path : List Config) : ℝ :=
 145  Real.exp (-PathAction path)
 146
 147/-- Path weight is always positive. -/
 148lemma path_weight_pos (path : List Config) : 0 < PathWeight path :=
 149  Real.exp_pos _
 150
 151/-- **BORN RULE EMERGENCE**: The probability of a path is proportional to its weight.
 152
 153    P[γ] = W[γ] / Σ_γ' W[γ']
 154
 155    This is not postulated—it emerges from the cost structure. -/
 156structure BornRule where
 157  /-- The paths being considered -/
 158  paths : List (List Config)
 159  /-- Non-empty path set -/
 160  nonempty : paths ≠ []
 161  /-- Total weight (partition function) -/
 162  Z : ℝ := paths.foldl (fun acc γ => acc + PathWeight γ) 0
 163  /-- Probability of a path -/
 164  prob (γ : List Config) : ℝ := if γ ∈ paths then PathWeight γ / Z else 0
 165
 166/-- Sum of (f x / c) over a list equals (sum of f x) / c. -/
 167lemma List.sum_map_div' {α : Type*} (l : List α) (f : α → ℝ) (c : ℝ) (hc : c ≠ 0) :
 168    (l.map (fun x => f x / c)).sum = (l.map f).sum / c := by
 169  induction l with
 170  | nil => simp
 171  | cons head tail ih =>
 172    simp only [List.map_cons, List.sum_cons, ih]
 173    field_simp
 174