Foundation Primitive Recognition Calculus Hilbert Display Completion Display Nor

The norm bridge

In quantum mechanics, the squared norm of a state vector is the total probability, which must sum to 1. The Recognition Science framework represents physical states in its own native format, called F_RS[i] amplitudes, and also provides a way to display them as ordinary complex vectors in a finite Hilbert space. The theorem display_normSq_eq establishes that these two ways of computing the total probability always agree: the squared norm of the displayed vector equals the sum of the native Born weights over all alternatives. This is a bridge between the framework's internal language and the standard mathematical language of quantum theory.

The theorem is proved in the framework's machine-checked library of formal theorems. It is a statement about a finite number of alternatives, indexed from 0 to N. The proof is a direct equality, not an approximation or a limiting argument. The framework also proves that the individual Born weights, the probabilities for each alternative, are preserved by the display, and that a native state is normalized exactly when its displayed squared norm equals 1. These results together form a valid comparison protocol: two native states can be compared by their displayed norms without loss of information.

In Recognition Science, this theorem is part of a larger construction. The framework models physical reality as a ledger of recognition events, and it derives constants like the golden ratio and three spatial dimensions from a forced cost function. The Hilbert display is a tool for connecting that native calculus to conventional quantum mechanics. The theorem does not claim that the framework's native amplitudes are the same as standard quantum states; it claims only that a specific observable, the squared norm, is computed identically in both representations.

The theorem does not establish that the framework's amplitudes are physically real, that they obey the Schrödinger equation, or that the Hilbert space display is unique. It is a formal equality between two definitions, not a physical postulate. The framework's deeper claims about the origin of quantum mechanics remain separate from this bridge theorem, which is a technical result about how two formalisms can be made to agree on one observable.

/-- 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

What this page does not claim

The theorem does not claim that native F_RS[i] amplitudes are identical to standard quantum states. The theorem does not establish that the framework's amplitudes obey the Schrödinger equation. The theorem does not claim the Hilbert space display is the unique way to represent native amplitudes.

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: