QuantumState
plain-language theorem explainer
A quantum state in Recognition Science is a normalized superposition of ledger configurations, each carrying a J-cost. Researchers deriving the Born rule from cost minimization would cite this structure when linking ledger conservation to quantum amplitudes. The declaration is a direct structure definition that encodes configurations, complex amplitudes, and the unit-norm condition without invoking lemmas.
Claim. A quantum state over $n$ configurations consists of a map from indices in Fin $n$ to ledger configurations together with complex amplitudes $a_i$ satisfying $sum_i |a_i|^2 = 1$.
background
In the Quantum Ledger module a ledger is a list of entries whose balance equals the sum of log-ratios, enforcing conservation under the Recognition Composition Law. Quantum states are defined as superpositions over these ledgers, with the normalization condition taken directly from the unit-norm axiom on amplitudes. Upstream results include the Normalization class (cost vanishes at ratio 1) and the PhiForcingDerived and LedgerFactorization structures that calibrate the J-cost functional used in downstream expected-cost calculations.
proof idea
The declaration is a structure definition that directly encodes the superposition of ledger configurations with complex amplitudes and enforces normalization via the sum of squared norms equaling one. No lemmas are applied; it serves as the foundational type for subsequent definitions such as probability and expectedCost.
why it matters
This structure supplies the type on which the Born rule is derived from J-cost minimization rather than postulated. It is used by born_rule_jcost_connection (which equates expected cost to a probability-weighted sum of totalCost values) and by expectedCost itself. The definition realizes the module claim that quantum states are ledger superpositions, connecting to the eight-tick octave and the J-uniqueness property in the forcing chain. It closes the interface between classical ledger balance and quantum superposition without addressing dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.