isDefinite
plain-language theorem explainer
A definition that marks a quantum state as definite precisely when exactly one basis amplitude is nonzero. Researchers deriving the measurement postulate from ledger commitment in Recognition Science would reference it to separate committed outcomes from superpositions. The definition is a direct abbreviation that applies the unique-existence quantifier to the amplitude map.
Claim. A quantum state $ψ$ in finite dimension $n$ is definite when there exists a unique index $i$ such that the amplitude of $ψ$ at $i$ is nonzero.
background
The module QF-001 models the measurement problem by identifying superposition with an uncommitted ledger entry and measurement with forced commitment to a single branch. QuantumState n is the structure whose amplitudes field maps each basis index in Fin n to an Amplitude value, subject to the normalization that the sum of squared moduli equals one. This representation lets multiple nonzero amplitudes stand for coexisting ledger branches before commitment occurs.
proof idea
The definition is a direct abbreviation that applies the unique-existence quantifier to the predicate that the amplitude at index i is nonzero.
why it matters
This definition supplies the precise predicate needed to distinguish committed ledger states from superpositions inside the Recognition Science account of wavefunction collapse. It directly supports the module's target of deriving the measurement postulate from ledger balancing and the associated Born-rule claim that outcome probabilities track squared amplitudes. The surrounding framework links the predicate to J-cost minimization and the eight-tick ledger structure, though the present declaration itself remains a pure type-level distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.