Foundation Primitive Recognition Calculus Hilbert Display Completion Norm Sq

The squared norm bridge

The squared norm is a standard measure of a vector's size, computed by summing the squares of its components. In quantum mechanics, this quantity carries physical meaning: for a wavefunction, the squared norm gives the total probability, and it must equal one for a properly normalized state. The declaration normSq defines this same concept for the finite Hilbert display, which is a complex vector space indexed by a finite set of distinction alternatives, essentially a list of complex numbers.

The framework's library of formal theorems proves that this new squared norm agrees exactly with the native norm already defined on the framework's own amplitudes. The theorem display_normSq_eq shows that for any amplitude, the squared norm of its display equals the sum of its native Born weights, which are the probabilities for each possible outcome. This means the two descriptions, native and displayed, assign the same total size to every state.

Two further theorems extend this agreement. The first, display_bornWeight_eq, proves that the probability assigned to each individual outcome is identical in both pictures. The second, normalized_iff_display, proves that a state is normalized in the native sense exactly when its displayed squared norm equals one. Together these establish that the finite Hilbert space is a faithful display of the native amplitudes: nothing is lost or distorted in translation.

In Recognition Science, this bridge matters because it makes the framework's objects usable with standard Hilbert space tools. The normBridge is a formal construction that carries native amplitudes into the display and shows that comparing two states by their total squared norm is a valid protocol, meaning the comparison gives the same answer whether done natively or through the display. The headline theorem finite_hilbert_display_headline packages all four agreements into one statement.

The declaration does not claim that the squared norm is the only observable, nor that it defines a physical measurement in the everyday sense. It establishes a mathematical equivalence between two formal descriptions. It also does not claim that the finite display space is infinite-dimensional or that it captures any dynamics or time evolution; it is a static carrier of amplitudes. Finally, it does not claim that the Born weight interpretation is derived from first principles; that interpretive step is a modeling choice within the framework.

/-- The Hilbert-display norm equals the native F_RS[i] finite norm. -/
theorem display_normSq_eq {N : ℕ} (ψ : FRSComplexAmplitude.FRSIAmp N) :
    normSq (display ψ)
      = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i) :=
  FRSComplexAmplitude.display_normSq_eq ψ

/-- The Hilbert-display Born weight equals the native F_RS[i] Born weight. -/
theorem display_bornWeight_eq {N : ℕ} (ψ : FRSComplexAmplitude.FRSIAmp N) (i : Fin (N + 1)) :
    bornWeight (display ψ) i = FRSComplexAmplitude.bornWeight ψ i :=
  FRSComplexAmplitude.display_bornWeight_eq ψ i

/-- Native F_RS[i] normalization is exactly display-Hilbert normalization. -/
theorem normalized_iff_display {N : ℕ} (ψ : FRSComplexAmplitude.FRSIAmp N) :
    FRSComplexAmplitude.Normalized ψ ↔ normSq (display ψ) = 1 := by
  rw [display_normSq_eq]
  rfl

/-- The valid-comparison bridge from native F_RS[i] amplitudes to the finite
Hilbert display, using squared norm as the observable protocol. -/
noncomputable def normBridge (N : ℕ) :
    ValidComparison.Bridge (FRSComplexAmplitude.FRSIAmp N) (FiniteHilbertDisplay N) ℝ where
  display := display
  observeNative := fun ψ => Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i)
  observeDisplay := normSq
  commutes := by
    intro ψ
    exact display_normSq_eq ψ

/-- **Finite Hilbert display headline.** Finite Hilbert space is a display of
native F_RS[i] finite amplitudes. The bridge preserves Born weights, squared
norm, and normalization, and comparison by norm is valid through the
native/display/observable bridge. -/
theorem finite_hilbert_display_headline (N : ℕ) :
    (∀ ψ : FRSComplexAmplitude.FRSIAmp N,
        normSq (display ψ)
          = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i))
      ∧ (∀ ψ : FRSComplexAmplitude.FRSIAmp N, ∀ i : Fin (N + 1),
          bornWeight (display ψ) i = FRSComplexAmplitude.bornWeight ψ i)
      ∧ (∀ ψ : FRSComplexAmplitude.FRSIAmp N,
          FRSComplexAmplitude.Normalized ψ ↔ normSq (display ψ) = 1)
      ∧ (∀ ψ φ : FRSComplexAmplitude.FRSIAmp N,
          ValidComparison.IsValidComparison (normBridge N) ψ φ
            ↔ Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i)
              = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight φ i)) :=
  ⟨display_normSq_eq, display_bornWeight_eq, normalized_iff_display,
    fun ψ φ => ValidComparison.validComparison_iff_native (normBridge N) ψ φ⟩

What this page does not claim

The squared norm is not claimed to be the only possible observable protocol. The declaration does not assert that the Born weight interpretation is derived from the framework's axioms. The finite Hilbert display is not claimed to capture dynamics or time evolution.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/HilbertDisplayCompletion.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: