IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSComplexAmplitude

   1/-
   2  PrimitiveRecognitionCalculus/FRSComplexAmplitude.lean
   3
   4  Finite amplitudes over F_RS[i].
   5
   6  `FRSCarrier.lean` gives the real finite-description carrier F_RS as an explicit
   7  expression language. `DeltaAmplitude.lean` gives finite real and complex
   8  amplitudes as native finite vectors, with the ambient complex vector space only
   9  as display.
  10
  11  This module closes the next interface gap: a complex amplitude does not need
  12  the full complex continuum as native scalar carrier. The native scalar is
  13  F_RS[i], represented by a pair of F_RS expressions `(a,b)` and displayed as
  14  `a + b i` in ℂ.
  15
  16  No project-local axioms. No sorry.
  17-/
  18
  19import Mathlib
  20import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSCarrier
  21import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude
  22
  23namespace IndisputableMonolith
  24namespace Foundation
  25namespace PrimitiveRecognitionCalculus
  26namespace FRSComplexAmplitude
  27
  28/-- A finite-description complex scalar in `F_RS[i]`: real and imaginary parts
  29are both `F_RS` expressions. -/
  30structure FRSIExpr where
  31  re : FRSCarrier.FRSExpr
  32  im : FRSCarrier.FRSExpr
  33  deriving DecidableEq, Repr
  34
  35/-- Display of an `F_RS[i]` expression into the ambient complex field. -/
  36noncomputable def eval : FRSIExpr → ℂ :=
  37  fun z => ⟨FRSCarrier.eval z.re, FRSCarrier.eval z.im⟩
  38
  39/-- Real part of the display is the F_RS real expression value. -/
  40theorem eval_re (z : FRSIExpr) : (eval z).re = FRSCarrier.eval z.re := rfl
  41
  42/-- Imaginary part of the display is the F_RS imaginary expression value. -/
  43theorem eval_im (z : FRSIExpr) : (eval z).im = FRSCarrier.eval z.im := rfl
  44
  45/-- Every displayed real part remains in the real RS carrier field. -/
  46theorem eval_re_mem (z : FRSIExpr) : (eval z).re ∈ MinimalField.rsField := by
  47  simpa [eval] using FRSCarrier.eval_mem z.re
  48
  49/-- Every displayed imaginary part remains in the real RS carrier field. -/
  50theorem eval_im_mem (z : FRSIExpr) : (eval z).im ∈ MinimalField.rsField := by
  51  simpa [eval] using FRSCarrier.eval_mem z.im
  52
  53/-- Finite amplitude vector over `F_RS[i]`. -/
  54abbrev FRSIAmp (N : ℕ) := Fin (N + 1) → FRSIExpr
  55
  56/-- Display an `F_RS[i]` finite amplitude as an ambient finite complex amplitude. -/
  57noncomputable def displayAmp {N : ℕ} (ψ : FRSIAmp N) : DeltaAmplitude.ComplexAmp N :=
  58  fun i => eval (ψ i)
  59
  60/-- Native Born weight computed from the two F_RS components. -/
  61noncomputable def bornWeight {N : ℕ} (ψ : FRSIAmp N) (i : Fin (N + 1)) : ℝ :=
  62  FRSCarrier.eval (ψ i).re ^ 2 + FRSCarrier.eval (ψ i).im ^ 2
  63
  64/-- The displayed complex Born weight agrees with the native F_RS[i] formula. -/
  65theorem display_bornWeight_eq {N : ℕ} (ψ : FRSIAmp N) (i : Fin (N + 1)) :
  66    DeltaAmplitude.complexBornWeight (displayAmp ψ) i = bornWeight ψ i := by
  67  rfl
  68
  69/-- The displayed complex norm agrees with the native finite F_RS[i] norm formula. -/
  70theorem display_normSq_eq {N : ℕ} (ψ : FRSIAmp N) :
  71    DeltaAmplitude.complexNormSq (displayAmp ψ)
  72      = Finset.univ.sum (fun i : Fin (N + 1) => bornWeight ψ i) := by
  73  rfl
  74
  75theorem bornWeight_nonneg {N : ℕ} (ψ : FRSIAmp N) (i : Fin (N + 1)) :
  76    0 ≤ bornWeight ψ i := by
  77  unfold bornWeight
  78  nlinarith [sq_nonneg (FRSCarrier.eval (ψ i).re), sq_nonneg (FRSCarrier.eval (ψ i).im)]
  79
  80/-- Normalization over `F_RS[i]` is exactly normalization of the ambient complex
  81display. -/
  82def Normalized {N : ℕ} (ψ : FRSIAmp N) : Prop :=
  83  Finset.univ.sum (fun i : Fin (N + 1) => bornWeight ψ i) = 1
  84
  85theorem normalized_iff_display {N : ℕ} (ψ : FRSIAmp N) :
  86    Normalized ψ ↔ DeltaAmplitude.ComplexNormalized (displayAmp ψ) := by
  87  unfold Normalized DeltaAmplitude.ComplexNormalized
  88  rw [display_normSq_eq]
  89
  90/-- **F_RS[i] finite amplitude headline.** Finite complex amplitudes can be
  91carried by the finite-description scalar carrier `F_RS[i]`; ambient ℂ is only the
  92display. The display preserves real/imaginary carrier membership, Born weights,
  93and normalization. -/
  94theorem frsi_amplitude_headline (N : ℕ) :
  95    (∀ ψ : FRSIAmp N, ∀ i : Fin (N + 1), 0 ≤ bornWeight ψ i)
  96      ∧ (∀ ψ : FRSIAmp N, DeltaAmplitude.complexNormSq (displayAmp ψ)
  97          = Finset.univ.sum (fun i : Fin (N + 1) => bornWeight ψ i))
  98      ∧ (∀ ψ : FRSIAmp N, Normalized ψ ↔ DeltaAmplitude.ComplexNormalized (displayAmp ψ))
  99      ∧ (∀ z : FRSIExpr, (eval z).re ∈ MinimalField.rsField ∧ (eval z).im ∈ MinimalField.rsField) :=
 100  ⟨bornWeight_nonneg, display_normSq_eq, normalized_iff_display,
 101    fun z => ⟨eval_re_mem z, eval_im_mem z⟩⟩
 102
 103end FRSComplexAmplitude
 104end PrimitiveRecognitionCalculus
 105end Foundation
 106end IndisputableMonolith
 107