`probability`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.QuantumLedger
domain: Foundation
line: 154 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.QuantumLedger on GitHub at line 154.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 151  normalized : (Finset.univ.sum fun i => Complex.normSq (amplitudes i)) = 1
 152
 153/-- The probability of finding configuration i (Born rule). -/
 154noncomputable def probability {n : ℕ} (ψ : QuantumState n) (i : Fin n) : ℝ :=
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.