theorem
proved
tactic proof
born_rule_normalized
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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 -/