born_rule_normalized
plain-language theorem explainer
The theorem shows that for any BornRule structure the probabilities defined by path weights sum exactly to 1 whenever the partition function Z is nonzero. Researchers deriving the Born rule from recognition costs rather than postulating it would cite this normalization step. The proof reduces the claim to an algebraic identity by equating foldl sums to explicit list sums, substituting the weight-over-Z definition, and applying field simplification.
Claim. Let $br$ be a BornRule whose paths form a nonempty list of configuration sequences, with partition function $Z = br.Z$ defined by $Z = br.paths.foldl (fun acc γ => acc + PathWeight γ) 0$ and probability function $P(γ) = PathWeight(γ)/Z$ whenever $γ$ belongs to the list (and 0 otherwise). Then the sum of $P(γ)$ over all $γ$ in $br.paths$ equals 1, provided $Z ≠ 0$.
background
BornRule is the structure that encodes the emergence of probabilities from path weights: $P[γ] = W[γ]/Σ W[γ']$ where the weight $W[γ] = exp(-PathAction γ)$ is supplied by the PathWeight definition. The module Actualization sits inside the Modal layer and treats actualization as the point at which accumulated recognition cost crosses a threshold, turning superpositions into definite outcomes without an extra measurement axiom. Upstream lemmas such as foldl_add_eq_sum (from list summation utilities) and sum_map_div' (from real division properties) supply the algebraic identities used to convert the foldl expression into an explicit sum.
proof idea
The tactic proof first rewrites the target foldl sum of probabilities as the ordinary list sum via foldl_add_eq_sum. It then applies map_congr_left together with the supplied h_prob_def to replace each probability entry by the corresponding PathWeight γ / br.Z. The resulting expression is reduced by sum_map_div' to (sum of PathWeights) / Z. A second application of foldl_add_eq_sum recovers that the sum of PathWeights equals br.Z, after which field_simp finishes the normalization.
why it matters
This normalization is the final algebraic step that lets the cost-derived weights become a probability measure, feeding directly into the Born-rule statements in Measurement.BornRule, BornRuleLight, and Quantum.Measurement.WavefunctionCollapse. It closes the loop from the ActualizationPrinciple (cost threshold C = 1 forces definiteness) to observable probabilities, confirming that the Born rule is not an independent postulate but a consequence of the J-cost ledger. The result sits at the interface between the Modal layer and the Measurement layer, removing the need for an extra normalization axiom in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.