Foundation Primitive Recognition Calculus Valid Comparison Examples Hilbert Norm

The Hilbert display bridge

In quantum mechanics, a state is often described by a complex wavefunction, a list of numbers that encodes the likelihood of each possible outcome. The probability of a particular outcome is the square of that number's magnitude, a value known as the Born weight. Summing these weights over all possible outcomes gives the total probability, which must equal one for a valid physical state.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration, hilbertNormBridge, that establishes a precise rule for comparing two such quantum states. It defines a bridge that takes a native finite quantum state and displays it as its total probability, the sum of its Born weights. The framework then proves a theorem: two states are considered a valid comparison under this bridge exactly when their total probabilities are equal. In plain terms, the bridge says that two quantum states are equivalent for display purposes if they have the same overall probability mass, regardless of how that mass is distributed among the individual outcomes.

This result is one of three concrete examples the framework provides to illustrate its general doctrine of valid comparison. The other two examples work with real numbers and with finite probability events. In each case, the pattern is the same: a display function maps a native object to a real value, and the comparison is valid precisely when those displayed values match. The Hilbert bridge is the quantum-mechanical instance of this pattern.

What the declaration does not claim is just as important. It does not say that two states with equal total probability are physically identical, only that they display the same value. It does not establish that the Born rule itself is derived within the framework; the bridge takes the Born weight as given. And it does not extend to infinite-dimensional Hilbert spaces, since the declaration is explicitly finite, working with states indexed by a natural number N plus one.

/-- Finite Hilbert display bridge, re-exported at the valid-comparison example
layer. -/
noncomputable def hilbertNormBridge (N : ℕ) :
    ValidComparison.Bridge
      (FRSComplexAmplitude.FRSIAmp N)
      (HilbertDisplayCompletion.FiniteHilbertDisplay N)
      ℝ :=
  HilbertDisplayCompletion.normBridge N

theorem hilbert_display_valid_iff (N : ℕ)
    (ψ φ : FRSComplexAmplitude.FRSIAmp N) :
    ValidComparison.IsValidComparison (hilbertNormBridge N) ψ φ
      ↔ Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i)
        = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight φ i) :=
  ValidComparison.validComparison_iff_native (hilbertNormBridge N) ψ φ

/-- **Valid-comparison examples headline.** The doctrine has concrete bridges for
real display, finite probability display, and finite Hilbert display. -/
theorem valid_comparison_examples_headline :
    (∀ x y : DeltaReal.Protocol,
        ValidComparison.IsValidComparison realDisplayBridge x y ↔ x.value = y.value)
      ∧ (∀ (N : ℕ) (E F : DeltaProbability.Event N),
          ValidComparison.IsValidComparison (probabilityDisplayBridge N) E F
            ↔ DeltaProbability.prob E = DeltaProbability.prob F)
      ∧ (∀ (N : ℕ) (ψ φ : FRSComplexAmplitude.FRSIAmp N),
          ValidComparison.IsValidComparison (hilbertNormBridge N) ψ φ
            ↔ Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i)
              = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight φ i)) :=
  ⟨real_display_valid_iff, probability_display_valid_iff, hilbert_display_valid_iff⟩

What this page does not claim

It does not claim that equal total probability makes two quantum states physically identical. It does not claim that the Born rule is derived within the framework. It does not claim to apply to infinite-dimensional Hilbert spaces.

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/ValidComparisonExamples.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: