stateToLedger
plain-language theorem explainer
The definition converts a normalized quantum state in finite dimension n into an uncommitted ledger whose branches record only the non-zero amplitudes together with their Born weights. Workers formalizing the measurement problem inside Recognition Science cite it when treating superposition as a ledger that has not yet committed. The body directly assembles the branch list by filtering the support of the amplitude map and supplies the required normalization via an auxiliary sum lemma.
Claim. Let $n$ be a natural number and let $ψ$ be a normalized state whose amplitudes $ψ_i$ satisfy $∑_i |ψ_i|^2 = 1$. The map produces the uncommitted ledger whose branches are the triples $(i, ψ_i, |ψ_i|^2)$ for every basis index $i$ with $ψ_i ≠ 0$, together with the proof that the listed weights sum to one.
background
QuantumState is the structure whose field amplitudes : Fin n → Amplitude carries the complex coefficients and whose normalized field asserts that the sum of squared moduli equals one. UncommittedLedger is the structure whose branches field is a list of LedgerBranch records and whose normalized field asserts that the sum of the branch weights equals one. The surrounding module QF-001 frames the measurement problem as the transition from an uncommitted ledger (superposition) to a committed ledger (definite outcome) whose selection probabilities are given by the J-cost of each branch.
proof idea
The definition is a direct term-mode construction. It filters Finset.univ to the indices where the amplitude is nonzero, maps each such index to a LedgerBranch triple containing the index, the amplitude, and the squared modulus, and attaches the normalization proof supplied by the sibling lemma filter_map_weight_sum.
why it matters
The definition supplies the concrete translation between the QuantumState object and the UncommittedLedger object that the module uses to realize ledger commitment as the mechanism of wavefunction collapse. It therefore sits inside the QF-001 derivation of the measurement postulate from Recognition Science ledger structure and supplies the data structure on which the subsequent measurementProbability definition operates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.