outcomeCost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that the costs normalize to a probability distribution.
- Does not treat infinite-dimensional or continuous spectra.
- Does not model the temporal dynamics of collapse.
- Does not incorporate environmental decoherence.
formal statement (Lean)
216noncomputable def outcomeCost {n : ℕ} (ψ : QuantumState n) (i : Fin n) : ℝ :=
proof body
Definition body.
217 if _h : ψ.amplitudes i ≠ 0 then
218 -(Real.log (‖ψ.amplitudes i‖^2)) -- Negative log probability = information cost
219 else
220 0 -- Infinite cost for impossible outcomes
221
222/-- **THEOREM (Cost-Probability Relation)**: Probability decreases with cost.
223 P(i) = exp(-Cost(i)) when properly normalized.
224
225 Proof: P(i) = |ψᵢ|², Cost(i) = -log(|ψᵢ|²)
226 exp(-Cost(i)) = exp(--log(|ψᵢ|²)) = exp(log(|ψᵢ|²)) = |ψᵢ|² = P(i) -/