outcomeCost
plain-language theorem explainer
outcomeCost assigns to each basis outcome i of a normalized quantum state ψ the value -log(|ψ_i|^2) when the amplitude is nonzero and zero otherwise. Researchers deriving the Born rule from ledger commitment in Recognition Science cite this definition to link amplitude magnitudes to information costs. The definition is a direct conditional that returns the negative logarithm of the squared modulus or the zero fallback.
Claim. For a normalized quantum state ψ in dimension n and index i, the outcome cost equals -log(|ψ_i|^2) if ψ_i ≠ 0 and equals 0 otherwise.
background
The module derives the measurement postulate from Recognition Science ledger structure. A quantum state is a structure carrying amplitudes from Fin n to complex numbers together with the normalization condition that the sum of squared moduli equals one. Outcome cost implements the recognition cost of a measurement outcome by applying the negative logarithm to the squared amplitude, which is the probability extracted by the upstream probability definition.
proof idea
The definition is a direct case split on whether the amplitude at i is nonzero. When the amplitude is nonzero it returns the negative real logarithm of the squared modulus; otherwise it returns zero. No lemmas are applied beyond the built-in real logarithm and complex norm.
why it matters
outcomeCost supplies the cost function required by the downstream cost_probability_relation theorem, which proves that measurement probability equals exp(-outcome cost). It fills the explicit cost step in the QF-001 derivation of the Born rule from ledger commitment, where lower J-cost branches receive higher probability. The construction rests on the J-cost supplied by ObserverForcing and the multiplicative recognizer cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.