IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.HilbertDisplayCompletion

   1/-
   2  PrimitiveRecognitionCalculus/HilbertDisplayCompletion.lean
   3
   4  Finite Hilbert space as display completion.
   5
   6  `FRSComplexAmplitude.lean` closes the native scalar-carrier gap: finite
   7  amplitudes can live over F_RS[i]. This module names the corresponding finite
   8  Hilbert display. The display carrier is an ambient complex vector
   9  `Fin (N+1) → ℂ`; the native carrier is an F_RS[i] amplitude; the bridge
  10  preserves coordinates, Born weights, normalization, and squared norm.
  11
  12  Infinite Hilbert space remains a completion/display target. The finite theorem
  13  here prevents the common mistake: importing ambient ℂ-Hilbert ontology before
  14  the finite F_RS[i] amplitude has been typed.
  15
  16  No project-local axioms. No sorry.
  17-/
  18
  19import Mathlib
  20import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSComplexAmplitude
  21import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison
  22
  23namespace IndisputableMonolith
  24namespace Foundation
  25namespace PrimitiveRecognitionCalculus
  26namespace HilbertDisplayCompletion
  27
  28/-- The finite Hilbert display carrier: an ambient complex vector on the finite
  29distinction alternatives. -/
  30abbrev FiniteHilbertDisplay (N : ℕ) := Fin (N + 1) → ℂ
  31
  32/-- Display an F_RS[i] amplitude as a finite Hilbert vector. -/
  33noncomputable def display {N : ℕ} (ψ : FRSComplexAmplitude.FRSIAmp N) : FiniteHilbertDisplay N :=
  34  FRSComplexAmplitude.displayAmp ψ
  35
  36/-- Squared norm on the finite Hilbert display. -/
  37noncomputable def normSq {N : ℕ} (v : FiniteHilbertDisplay N) : ℝ :=
  38  DeltaAmplitude.complexNormSq v
  39
  40/-- Born weight on the finite Hilbert display. -/
  41noncomputable def bornWeight {N : ℕ} (v : FiniteHilbertDisplay N) (i : Fin (N + 1)) : ℝ :=
  42  DeltaAmplitude.complexBornWeight v i
  43
  44/-- The Hilbert-display norm equals the native F_RS[i] finite norm. -/
  45theorem display_normSq_eq {N : ℕ} (ψ : FRSComplexAmplitude.FRSIAmp N) :
  46    normSq (display ψ)
  47      = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i) :=
  48  FRSComplexAmplitude.display_normSq_eq ψ
  49
  50/-- The Hilbert-display Born weight equals the native F_RS[i] Born weight. -/
  51theorem display_bornWeight_eq {N : ℕ} (ψ : FRSComplexAmplitude.FRSIAmp N) (i : Fin (N + 1)) :
  52    bornWeight (display ψ) i = FRSComplexAmplitude.bornWeight ψ i :=
  53  FRSComplexAmplitude.display_bornWeight_eq ψ i
  54
  55/-- Native F_RS[i] normalization is exactly display-Hilbert normalization. -/
  56theorem normalized_iff_display {N : ℕ} (ψ : FRSComplexAmplitude.FRSIAmp N) :
  57    FRSComplexAmplitude.Normalized ψ ↔ normSq (display ψ) = 1 := by
  58  rw [display_normSq_eq]
  59  rfl
  60
  61/-- The valid-comparison bridge from native F_RS[i] amplitudes to the finite
  62Hilbert display, using squared norm as the observable protocol. -/
  63noncomputable def normBridge (N : ℕ) :
  64    ValidComparison.Bridge (FRSComplexAmplitude.FRSIAmp N) (FiniteHilbertDisplay N) ℝ where
  65  display := display
  66  observeNative := fun ψ => Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i)
  67  observeDisplay := normSq
  68  commutes := by
  69    intro ψ
  70    exact display_normSq_eq ψ
  71
  72/-- **Finite Hilbert display headline.** Finite Hilbert space is a display of
  73native F_RS[i] finite amplitudes. The bridge preserves Born weights, squared
  74norm, and normalization, and comparison by norm is valid through the
  75native/display/observable bridge. -/
  76theorem finite_hilbert_display_headline (N : ℕ) :
  77    (∀ ψ : FRSComplexAmplitude.FRSIAmp N,
  78        normSq (display ψ)
  79          = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i))
  80      ∧ (∀ ψ : FRSComplexAmplitude.FRSIAmp N, ∀ i : Fin (N + 1),
  81          bornWeight (display ψ) i = FRSComplexAmplitude.bornWeight ψ i)
  82      ∧ (∀ ψ : FRSComplexAmplitude.FRSIAmp N,
  83          FRSComplexAmplitude.Normalized ψ ↔ normSq (display ψ) = 1)
  84      ∧ (∀ ψ φ : FRSComplexAmplitude.FRSIAmp N,
  85          ValidComparison.IsValidComparison (normBridge N) ψ φ
  86            ↔ Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i)
  87              = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight φ i)) :=
  88  ⟨display_normSq_eq, display_bornWeight_eq, normalized_iff_display,
  89    fun ψ φ => ValidComparison.validComparison_iff_native (normBridge N) ψ φ⟩
  90
  91end HilbertDisplayCompletion
  92end PrimitiveRecognitionCalculus
  93end Foundation
  94end IndisputableMonolith
  95