born_rule_normalized

formal source

 194    - br.prob γ = if γ ∈ br.paths then PathWeight γ / br.Z else 0
 195
 196    These are the default definitions in BornRule. -/
 197theorem born_rule_normalized (br : BornRule) (hZ : br.Z ≠ 0)
 198    (h_Z_def : br.Z = br.paths.foldl (fun acc γ => acc + PathWeight γ) 0)
 199    (h_prob_def : ∀ γ, br.prob γ = if γ ∈ br.paths then PathWeight γ / br.Z else 0) :
 200    br.paths.foldl (fun acc γ => acc + br.prob γ) 0 = 1 := by
 201  -- Key insight: each prob γ = PathWeight γ / Z for γ ∈ paths
 202  -- Sum of (PathWeight γ / Z) = (Sum of PathWeight γ) / Z = Z / Z = 1
 203  have h_sum_prob : br.paths.foldl (fun acc γ => acc + br.prob γ) 0 =
 204                    (br.paths.map (fun γ => br.prob γ)).sum := foldl_add_eq_sum br.paths br.prob
 205  -- The map of prob equals the map of (PathWeight / Z) for paths in the list
 206  have h_maps : br.paths.map (fun γ => br.prob γ) = br.paths.map (fun γ => PathWeight γ / br.Z) := by
 207    apply List.map_congr_left
 208    intro γ hγ
 209    rw [h_prob_def γ, if_pos hγ]
 210  rw [h_sum_prob, h_maps, List.sum_map_div' br.paths PathWeight br.Z hZ]
 211  -- Now: (br.paths.map PathWeight).sum / br.Z = 1
 212  -- This is Z / Z = 1 since Z = (map PathWeight).sum
 213  have h_Z_eq : br.Z = (br.paths.map PathWeight).sum := by
 214    rw [h_Z_def, foldl_add_eq_sum]
 215  rw [← h_Z_eq]
 216  field_simp
 217
 218/-! ## Collapse as Cost Threshold -/
 219
 220/-- **COLLAPSE THRESHOLD**: C = 1 is the recognition cost threshold for definiteness.
 221
 222    When the accumulated recognition cost C ≥ 1:
 223    - Superposition collapses to definite state
 224    - No measurement postulate needed
 225    - Built into dynamics, not added as axiom -/
 226def collapse_threshold : ℝ := 1
 227