sum_filter_eq_sum_all
plain-language theorem explainer
The lemma shows that for any complex function on a finite index set the sum of squared moduli over non-zero entries equals the sum over the full set. Quantum theorists deriving the Born rule from Recognition Science ledger commitments cite it when confirming that zero-amplitude branches add nothing to total weight. The proof splits the universal sum with Finset.sum_filter_add_sum_filter_not after proving the zero part vanishes via sum_eq_zero and simp.
Claim. For any natural number $n$ and map $f : [n] → ℂ$, the sum of $|f(i)|^2$ over those $i$ with $f(i) ≠ 0$ equals the sum of $|f(i)|^2$ over all $i ∈ [n]$.
background
The module derives the measurement postulate from ledger commitment in Recognition Science. Superposition corresponds to an uncommitted ledger entry whose branches carry recognition weights given by squared amplitudes; measurement forces commitment and selects one branch with probability proportional to its J-cost weight. The helper lemma is used inside the same file to pass from the full amplitude vector to the filtered list of non-zero LedgerBranch entries. Upstream, the map operation on Measurement structures preserves window, protocol and uncertainty data while the via structure in MassToLight supplies recognition-weighted assembly rules that later constrain the same J-cost weighting.
proof idea
The tactic proof first invokes Finset.sum_eq_zero on the zero-filtered sum, using simp to discharge the membership condition and obtain zero. It then applies Finset.sum_filter_add_sum_filter_not to the universal set with predicate f i ≠ 0, rewrites the resulting not_not, and closes with linarith on the two summands.
why it matters
The lemma closes a normalization step required by filter_map_weight_sum, which asserts that the summed weights of the filtered LedgerBranch list equal one. In the Recognition Science chain this supports the claim that measurement selects branches with probability |ψ_i|^2, matching the J-cost weighting that appears in the phi-ladder mass formula and the eight-tick octave. It therefore supplies a concrete algebraic bridge between the abstract ledger commitment described in the module doc and the concrete Born-rule probabilities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.