Foundation Primitive Recognition Calculus Frscomplex Amplitude Normalized Iff Di

The normalization bridge

In quantum mechanics, a state's total probability must sum to one, a condition called normalization. For a finite set of alternatives, this means the sum of the squared magnitudes of the complex amplitudes equals 1. The declaration normalized_iff_display establishes an exact equivalence: a state expressed in the framework's finite-description notation is normalized in that notation if and only if its display as ordinary complex numbers is normalized in the usual sense.

The framework's notation, called F_RS[i], represents a complex number by two real-valued expressions from a restricted carrier field, rather than by arbitrary complex numbers. The declaration proves that this representation is faithful for normalization: the native Born weight, computed as the sum of squares of the real and imaginary parts, matches the standard complex Born weight after display. This is a theorem in the machine-checked library of formal theorems, meaning the equivalence is verified by the kernel's rules of inference, not by informal argument.

The practical consequence is that normalization, a global constraint on a quantum state, can be checked entirely within the finite-description notation. The theorem also shows that the real and imaginary parts of any displayed value remain inside the carrier field, and that the displayed norm equals the native sum of Born weights. These facts together mean the finite notation does not lose or distort the probabilistic content of a state when it is translated to the ambient complex numbers.

What the declaration does not claim is that every complex amplitude can be expressed in the finite notation, nor that the notation defines a new probability rule. The Born rule itself, the sum of squared magnitudes, is taken as the definition of weight, not derived here. The theorem also does not address infinite-dimensional systems; it concerns finite amplitude vectors only, where the index set is a finite range of natural numbers.

theorem normalized_iff_display {N : ℕ} (ψ : FRSIAmp N) :
    Normalized ψ ↔ DeltaAmplitude.ComplexNormalized (displayAmp ψ) := by
  unfold Normalized DeltaAmplitude.ComplexNormalized
  rw [display_normSq_eq]

/-- The displayed complex Born weight agrees with the native F_RS[i] formula. -/
theorem display_bornWeight_eq {N : ℕ} (ψ : FRSIAmp N) (i : Fin (N + 1)) :
    DeltaAmplitude.complexBornWeight (displayAmp ψ) i = bornWeight ψ i := by
  rfl

/-- Every displayed real part remains in the real RS carrier field. -/
theorem eval_re_mem (z : FRSIExpr) : (eval z).re ∈ MinimalField.rsField := by
  simpa [eval] using FRSCarrier.eval_mem z.re

What this page does not claim

Every complex amplitude can be expressed in the finite F_RS[i] notation. The Born rule is derived here; it is used as the definition of weight. The theorem covers infinite-dimensional systems.

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