`QuantumState`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.QuantumLedger
domain: Foundation
line: 145 · 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 145.

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

 142/-! ## Quantum Superposition -/
 143
 144/-- A quantum state is a superposition over ledger configurations. -/
 145structure QuantumState (n : ℕ) where
 146  /-- The possible ledger configurations -/
 147  configurations : Fin n → Ledger
 148  /-- Complex amplitudes -/
 149  amplitudes : Fin n → ℂ
 150  /-- Normalization: |ψ|² = 1 -/
 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

papers checked against this theorem

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