prob_nonneg

formal source

 155  Complex.normSq (ψ.amplitudes i)
 156
 157/-- Probabilities are non-negative. -/
 158theorem prob_nonneg {n : ℕ} (ψ : QuantumState n) (i : Fin n) :
 159    0 ≤ probability ψ i :=
 160  Complex.normSq_nonneg _
 161
 162/-- Probabilities sum to 1. -/
 163theorem prob_sum_one {n : ℕ} (ψ : QuantumState n) :
 164    (Finset.univ.sum fun i => probability ψ i) = 1 :=
 165  ψ.normalized
 166
 167/-! ## Born Rule from J-Cost Minimization -/
 168
 169/-- The expected J-cost of a quantum state. -/
 170noncomputable def expectedCost {n : ℕ} (ψ : QuantumState n) : ℝ :=
 171  Finset.univ.sum fun i => probability ψ i * totalCost (ψ.configurations i)
 172
 173/-- **BORN RULE INTERPRETATION**: The probability of a configuration is
 174    inversely related to its J-cost (cost-weighted selection).
 175
 176    In full RS, this is derived from the variational principle:
 177    The observed configuration minimizes expected J-cost subject to constraints.
 178
 179    Here we state the connection: lower J-cost configurations have higher probability
 180    in the cost-optimal distribution (analogous to Boltzmann: P ∝ exp(-βE)). -/
 181theorem born_rule_jcost_connection {n : ℕ} (ψ : QuantumState n) :
 182    -- The expected cost is a weighted average of configuration costs
 183    expectedCost ψ = Finset.univ.sum fun i => probability ψ i * totalCost (ψ.configurations i) :=
 184  rfl
 185
 186/-! ## 8-Tick Phase in Quantum Ledger -/
 187
 188/-- The phase factor for a ledger entry. -/