Foundation Primitive Recognition Calculus Hilbert Display Completion Born Weight

Born weight

The Born rule is the oldest bridge between the mathematics of quantum states and what an experiment can count: if a system is in a state described by a complex number ψ on each alternative, the probability of seeing that alternative is the squared magnitude |ψ|². In Recognition Science, the declaration bornWeight performs exactly this operation on a finite Hilbert display, a vector of complex numbers indexed by a finite set of distinction alternatives. It takes a vector and an index and returns the real number |v(i)|², the same squared magnitude the Born rule prescribes.

The declaration is a definition, not a new physical law. Its content is that this displayed Born weight agrees with the native Born weight already defined on the framework's own amplitudes. Two theorems in the machine-checked library of formal theorems state this agreement: the displayed squared norm equals the sum of the native Born weights over all alternatives, and the displayed Born weight at any single index equals the native Born weight at that index. A further theorem says a native amplitude is normalized exactly when the displayed squared norm equals one. The headline theorem packages all three: comparison by squared norm through the display is a valid comparison protocol.

What bornWeight does not claim is larger than what it does. It does not introduce probabilities, measurements, or observers; it only names a function that maps a vector and an index to a squared magnitude. It does not assert that the squared magnitudes sum to one; that is a separate normalization condition, stated by a theorem about when a vector counts as normalized. It does not claim that the finite display is the whole of quantum mechanics; the display is a carrier for a finite set of alternatives, and the theorems here concern only the agreement between two ways of writing the same Born weight.

/-- Born weight on the finite Hilbert display. -/
noncomputable def bornWeight {N : ℕ} (v : FiniteHilbertDisplay N) (i : Fin (N + 1)) : ℝ :=
  DeltaAmplitude.complexBornWeight v i

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

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

bornWeight does not assert that squared magnitudes sum to one. bornWeight does not introduce probabilities, measurements, or observers. The finite display is not claimed to be the whole of quantum mechanics.

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: