outcomeCost
plain-language theorem explainer
outcomeCost assigns to each possible measurement outcome i of a normalized quantum state ψ the value -log(|ψ_i|^2) (and zero for impossible outcomes). Workers deriving the Born rule from ledger commitment in Recognition Science would cite this definition when relating recognition cost to outcome probability. It is realized by a direct case split on whether the amplitude vanishes.
Claim. For a normalized quantum state ψ in an n-dimensional space and basis index i, the recognition cost of outcome i is defined to be -log(|ψ_i|^2) whenever ψ_i ≠ 0 and 0 otherwise.
background
QuantumState is the structure carrying a map from Fin n to complex amplitudes together with the normalization condition that the sum of squared moduli equals 1. The module works inside the QF-001 setting in which a superposition is an uncommitted ledger entry and measurement is ledger commitment; probabilities are then expected to arise from J-cost. Upstream, ObserverForcing.cost identifies the cost of any recognition event with its J-cost, while QuantumLedger.probability extracts the Born probability |ψ_i|^2 directly from the amplitude.
proof idea
The definition is a direct case distinction: when the amplitude at i is nonzero it returns the negative log of the squared modulus; otherwise it returns zero. No lemmas are invoked; the body simply unfolds the amplitude field of QuantumState and applies the real logarithm.
why it matters
outcomeCost supplies the concrete cost function required by the downstream cost_probability_relation theorem, which recovers P(i) = exp(-Cost(i)) and thereby the Born rule. It therefore occupies the precise step in the QF-001 derivation that converts ledger J-cost into measurement probabilities. The construction sits inside the larger Recognition Science program that obtains all quantum postulates from the single forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.