foldl_add_eq_sum
plain-language theorem explainer
The lemma equates left-fold accumulation of a real-valued function over a list to the direct sum of the mapped values. Modal actualization proofs cite it to convert foldl-based path weight totals into standard sums for Born rule normalization. The argument first generalizes to arbitrary initial accumulators, proves the identity by induction on the list, and specializes to the zero case.
Claim. For any list $l : List α$ and function $f : α → ℝ$, the left fold $l.foldl (λ acc x, acc + f x) 0$ equals the sum $(l.map f).sum$.
background
The Modal.Actualization module defines actualization via paths and weights, with BornRule using foldl to accumulate PathWeight values into the normalization constant Z. This helper equates that accumulation to the standard list sum, enabling direct algebraic manipulation in probability statements. The module imports Possibility and depends on list primitives; downstream born_rule_normalized invokes the equivalence under the explicit definitions br.Z = br.paths.foldl (fun acc γ => acc + PathWeight γ) 0 and br.prob γ = if γ ∈ br.paths then PathWeight γ / br.Z else 0.
proof idea
The proof first states and proves a generalized claim for arbitrary initial accumulator via induction on l. The nil case simplifies directly. The cons case rewrites foldl_cons and map_cons, applies the inductive hypothesis to the updated accumulator, and closes with the ring tactic. The original statement follows by specializing the general result to initial value 0 via simpa.
why it matters
This lemma directly supports born_rule_normalized, which establishes that probabilities sum to 1 for non-empty path sets. In the Recognition Science framework it supplies the summation identity required for modal actualization and the Born rule normalization step, consistent with path-weight conventions in the actualization principle. It touches the technical handling of list accumulations that appear in probability statements tied to the eight-tick octave and phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.