`isDefinite`

definition

show as: view math explainer →

module: IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
domain: Quantum
line: 71 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse on GitHub at line 71.

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

formal source

  68  ∃ i j : Fin n, i ≠ j ∧ ψ.amplitudes i ≠ 0 ∧ ψ.amplitudes j ≠ 0
  69
  70/-- A definite state: exactly one basis state has non-zero amplitude. -/
  71def isDefinite {n : ℕ} (ψ : QuantumState n) : Prop :=
  72  ∃! i : Fin n, ψ.amplitudes i ≠ 0
  73
  74/-! ## Ledger Model of Quantum States -/
  75
  76/-- A ledger branch represents a potential measurement outcome. -/
  77structure LedgerBranch (n : ℕ) where
  78  /-- The basis state index. -/
  79  outcome : Fin n
  80  /-- The amplitude (complex). -/
  81  amplitude : Amplitude
  82  /-- Recognition weight (proportional to |amplitude|²). -/
  83  weight : ℝ
  84  /-- Weight equals squared norm. -/
  85  weight_eq : weight = ‖amplitude‖^2
  86
  87/-- An uncommitted ledger: a superposition of branches. -/
  88structure UncommittedLedger (n : ℕ) where
  89  /-- The branches (potential outcomes). -/
  90  branches : List (LedgerBranch n)
  91  /-- Weights sum to 1 (normalization). -/
  92  normalized : (branches.map LedgerBranch.weight).sum = 1
  93
  94/-- A committed ledger: exactly one branch selected. -/
  95structure CommittedLedger (n : ℕ) where
  96  /-- The selected outcome. -/
  97  outcome : Fin n
  98  /-- The final amplitude (phase factor). -/
  99  amplitude : Amplitude
 100  /-- The amplitude has unit norm (after normalization). -/
 101  unit_norm : ‖amplitude‖ = 1

papers checked against this theorem

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