path_action_single

formal source

 134lemma path_action_nil : PathAction [] = 0 := rfl
 135
 136/-- Single-element path has cost J. -/
 137lemma path_action_single (c : Config) : PathAction [c] = J c.value := rfl
 138
 139/-- **PATH WEIGHT**: The exponential weight of a path.
 140
 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) :