filter_map_weight_sum
plain-language theorem explainer
The theorem establishes that the sum of recognition weights over non-zero amplitude branches of a finite-dimensional quantum state equals one after filtering and ledger mapping. Quantum information researchers deriving the Born rule from ledger commitment would cite it when constructing uncommitted ledgers. The proof is a short tactic sequence that rewrites the double map, identifies the composed weight function with squared norms, reduces via filter-sum lemmas, and invokes the state's normalization axiom.
Claim. Let $n$ be a natural number and let $ψ$ be a quantum state in dimension $n$ with amplitudes $a_i$. Let $S$ be the set of indices $i$ for which $a_i ≠ 0$. Then the sum of the recognition weights $|a_i|^2$ over $i ∈ S$ equals 1.
background
QuantumState is a structure consisting of a function from Fin n to Amplitude together with the normalization axiom that the sum of squared norms over all basis indices equals one. LedgerBranch is a structure packaging an outcome index, a complex amplitude, and a recognition weight that equals the squared norm of that amplitude by construction. The module treats superpositions as uncommitted ledger entries whose branches carry weights |amplitude|^2; measurement corresponds to ledger commitment that selects branches according to these weights. Upstream QuantumState definitions in QuantumLedger, NoCloning, and Unitarity all impose the same normalization condition on the sum of squared norms.
proof idea
The tactic proof introduces n and ψ, rewrites the nested List.map using List.map_map, proves that the composition LedgerBranch.weight ∘ (branch constructor) equals the squared-norm map, then applies the sibling lemmas list_map_sum_eq_finset_sum and sum_filter_eq_sum_all to collapse the filtered sum to the full sum, and finishes with the exact normalization field of ψ.
why it matters
The result supplies the weight-preservation step required by the downstream definition stateToLedger, which converts a quantum state into an uncommitted ledger. It therefore supports the module's ledger-commitment account of wavefunction collapse and the derivation of the Born rule from recognition weights. The lemma closes a necessary bookkeeping gap in showing that total probability mass remains unity after discarding zero-amplitude branches.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.