IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude

   1/-
   2  PrimitiveRecognitionCalculus/DeltaAmplitude.lean
   3
   4  Delta-native amplitude.
   5
   6  The native object is finite amplitude data, not an infinite-dimensional Hilbert
   7  space. A finite amplitude vector assigns a real amplitude to each finite
   8  distinction alternative. The squared norm is a finite sum, and normalization
   9  gives a finite probability distribution.
  10
  11  This first pass uses real amplitudes. The complex/Hilbert layer is explicitly a
  12  display completion to be added on top of this finite carrier.
  13  The second pass below adds finite complex amplitudes directly; the infinite
  14  Hilbert space is still only the display completion.
  15
  16  No project-local axioms. No sorry.
  17-/
  18
  19import Mathlib
  20import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability
  21
  22namespace IndisputableMonolith
  23namespace Foundation
  24namespace PrimitiveRecognitionCalculus
  25namespace DeltaAmplitude
  26
  27/-- A finite real amplitude vector on `Fin (N+1)`. -/
  28abbrev Amp (N : ℕ) := Fin (N + 1) → ℝ
  29
  30/-- A finite complex amplitude vector on `Fin (N+1)`. -/
  31abbrev ComplexAmp (N : ℕ) := Fin (N + 1) → ℂ
  32
  33/-- Squared norm of a finite amplitude vector. -/
  34noncomputable def normSq {N : ℕ} (ψ : Amp N) : ℝ :=
  35  Finset.univ.sum fun i : Fin (N + 1) => (ψ i)^2
  36
  37/-- Born weight of one finite alternative. -/
  38noncomputable def bornWeight {N : ℕ} (ψ : Amp N) (i : Fin (N + 1)) : ℝ :=
  39  (ψ i)^2
  40
  41/-- A finite amplitude is normalized when its squared norm is one. -/
  42def Normalized {N : ℕ} (ψ : Amp N) : Prop := normSq ψ = 1
  43
  44theorem bornWeight_nonneg {N : ℕ} (ψ : Amp N) (i : Fin (N + 1)) :
  45    0 ≤ bornWeight ψ i := by
  46  unfold bornWeight
  47  positivity
  48
  49theorem normSq_nonneg {N : ℕ} (ψ : Amp N) : 0 ≤ normSq ψ := by
  50  unfold normSq
  51  exact Finset.sum_nonneg (fun i _ => sq_nonneg (ψ i))
  52
  53/-- The Born weights of a normalized finite amplitude sum to one. -/
  54theorem born_weights_sum_one {N : ℕ} {ψ : Amp N} (hψ : Normalized ψ) :
  55    Finset.univ.sum (fun i : Fin (N + 1) => bornWeight ψ i) = 1 := by
  56  simpa [Normalized, normSq, bornWeight] using hψ
  57
  58/-- A finite linear map preserves norm exactly when it preserves `normSq`. This
  59is the finite native core of unitary evolution; Hilbert-space unitaries are the
  60display-completion version. -/
  61def NormPreserving {N : ℕ} (U : Amp N → Amp N) : Prop :=
  62  ∀ ψ : Amp N, normSq (U ψ) = normSq ψ
  63
  64theorem normalized_of_normPreserving {N : ℕ} {U : Amp N → Amp N}
  65    (hU : NormPreserving U) {ψ : Amp N} (hψ : Normalized ψ) : Normalized (U ψ) := by
  66  unfold Normalized
  67  rw [hU ψ, hψ]
  68
  69/-- **Delta-native amplitude headline.** Finite amplitude data has nonnegative
  70Born weights; normalized finite amplitudes yield total probability one; and
  71norm-preserving finite transformations preserve normalization. -/
  72theorem delta_amplitude_headline (N : ℕ) :
  73    (∀ ψ : Amp N, ∀ i : Fin (N + 1), 0 ≤ bornWeight ψ i)
  74      ∧ (∀ ψ : Amp N, Normalized ψ →
  75          Finset.univ.sum (fun i : Fin (N + 1) => bornWeight ψ i) = 1)
  76      ∧ (∀ U : Amp N → Amp N, NormPreserving U →
  77          ∀ ψ : Amp N, Normalized ψ → Normalized (U ψ)) :=
  78  ⟨bornWeight_nonneg, fun _ hψ => born_weights_sum_one hψ,
  79    fun _ hU _ hψ => normalized_of_normPreserving hU hψ⟩
  80
  81/-! ## Complex finite amplitudes -/
  82
  83/-- Complex Born weight `|z|² = re² + im²` for one finite alternative. -/
  84noncomputable def complexBornWeight {N : ℕ} (ψ : ComplexAmp N) (i : Fin (N + 1)) : ℝ :=
  85  (ψ i).re ^ 2 + (ψ i).im ^ 2
  86
  87/-- Squared norm of a finite complex amplitude vector. -/
  88noncomputable def complexNormSq {N : ℕ} (ψ : ComplexAmp N) : ℝ :=
  89  Finset.univ.sum fun i : Fin (N + 1) => complexBornWeight ψ i
  90
  91/-- A finite complex amplitude is normalized when its squared norm is one. -/
  92def ComplexNormalized {N : ℕ} (ψ : ComplexAmp N) : Prop := complexNormSq ψ = 1
  93
  94theorem complexBornWeight_nonneg {N : ℕ} (ψ : ComplexAmp N) (i : Fin (N + 1)) :
  95    0 ≤ complexBornWeight ψ i := by
  96  unfold complexBornWeight
  97  nlinarith [sq_nonneg (ψ i).re, sq_nonneg (ψ i).im]
  98
  99theorem complexNormSq_nonneg {N : ℕ} (ψ : ComplexAmp N) : 0 ≤ complexNormSq ψ := by
 100  unfold complexNormSq
 101  exact Finset.sum_nonneg (fun i _ => complexBornWeight_nonneg ψ i)
 102
 103theorem complex_born_weights_sum_one {N : ℕ} {ψ : ComplexAmp N} (hψ : ComplexNormalized ψ) :
 104    Finset.univ.sum (fun i : Fin (N + 1) => complexBornWeight ψ i) = 1 := by
 105  simpa [ComplexNormalized, complexNormSq] using hψ
 106
 107/-- Finite complex norm preservation, the native finite version of unitary
 108evolution. -/
 109def ComplexNormPreserving {N : ℕ} (U : ComplexAmp N → ComplexAmp N) : Prop :=
 110  ∀ ψ : ComplexAmp N, complexNormSq (U ψ) = complexNormSq ψ
 111
 112theorem complex_normalized_of_normPreserving {N : ℕ} {U : ComplexAmp N → ComplexAmp N}
 113    (hU : ComplexNormPreserving U) {ψ : ComplexAmp N} (hψ : ComplexNormalized ψ) :
 114    ComplexNormalized (U ψ) := by
 115  unfold ComplexNormalized
 116  rw [hU ψ, hψ]
 117
 118/-- **Complex finite-amplitude headline.** Complex amplitudes already have a
 119native finite layer: Born weights are nonnegative, normalized finite complex
 120amplitudes sum to one, and norm-preserving finite complex transformations
 121preserve normalization. Hilbert space remains the display completion. -/
 122theorem delta_complex_amplitude_headline (N : ℕ) :
 123    (∀ ψ : ComplexAmp N, ∀ i : Fin (N + 1), 0 ≤ complexBornWeight ψ i)
 124      ∧ (∀ ψ : ComplexAmp N, ComplexNormalized ψ →
 125          Finset.univ.sum (fun i : Fin (N + 1) => complexBornWeight ψ i) = 1)
 126      ∧ (∀ U : ComplexAmp N → ComplexAmp N, ComplexNormPreserving U →
 127          ∀ ψ : ComplexAmp N, ComplexNormalized ψ → ComplexNormalized (U ψ)) :=
 128  ⟨complexBornWeight_nonneg, fun _ hψ => complex_born_weights_sum_one hψ,
 129    fun _ hU _ hψ => complex_normalized_of_normPreserving hU hψ⟩
 130
 131end DeltaAmplitude
 132end PrimitiveRecognitionCalculus
 133end Foundation
 134end IndisputableMonolith
 135