list_map_sum_eq_finset_sum
plain-language theorem explainer
The lemma equates the sum of a real-valued function over the list of elements in a finite set of indices with the direct sum over that finite set. Researchers deriving the Born rule from ledger commitment in Recognition Science cite it when converting between list-based amplitude maps and set sums in quantum state weights. The term proof reduces the equality by rewriting the finset sum as a multiset sum and matching list representations via coefficient coercions.
Claim. For any natural number $n$, finite subset $s$ of indices in $0$ to $n-1$, and function $f$ from those indices to reals, the sum of $f$ over the listed elements of $s$ equals the sum of $f$ over the set $s$.
background
The module derives the measurement postulate from Recognition Science ledger structure: superposition corresponds to uncommitted ledger entries, measurement to commitment, and probabilities to J-cost weights with the Born rule emerging as $P$ proportional to amplitude squared. This lemma supplies a basic summation identity used when filtering non-zero amplitudes in quantum states represented via Fin n indices and LedgerBranch weights. Upstream structures calibrate the J function (from PhiForcingDerived and DAlembert.LedgerFactorization) and enforce discrete tiers (from NucleosynthesisTiers and SpectralEmergence) that underpin the normalization condition invoked downstream.
proof idea
Term-mode proof: rewrite the finset sum as a multiset sum, equate the list to the multiset's list representation by reflexivity, then apply multiset sum and map coercions to obtain the desired equality.
why it matters
It supplies the summation identity required by the downstream theorem filter_map_weight_sum, which establishes that the total weight of non-zero branches equals 1 under state normalization. This technical step supports the QF-001 derivation of collapse from ledger balancing without external postulates, linking to the eight-tick octave and phi-ladder constants in the broader forcing chain. No open scaffolding remains here; the result closes a conversion gap between list and set representations in amplitude calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.