pith. machine review for the scientific record. sign in
def definition def or abbrev

outcomeCost

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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) -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.