Foundation Primitive Recognition Calculus Delta Amplitude Delta Amplitude Headli

The finite amplitude headline

In quantum mechanics, an amplitude is a number attached to a possible outcome, and the probability of that outcome is the square of the amplitude's size. The declaration delta_amplitude_headline takes this idea and makes it precise for a finite list of alternatives: it proves, in one packaged theorem, that these squared sizes are never negative, that they add up to exactly one when the amplitudes are normalized, and that any transformation preserving the total squared size also preserves normalization.

The statement works with a finite amplitude vector, a list of real numbers indexed from 0 to N. The first part says each entry's square is nonnegative, an obvious fact that nevertheless anchors the whole probability interpretation. The second part is the Born rule in miniature: if the sum of squares is 1, then the sum of the individual squared entries is also 1, so they behave like probabilities. The third part is a conservation law: a linear map that keeps the total squared size unchanged will send a normalized vector to another normalized vector, the finite analogue of unitary evolution in quantum theory.

The theorem is proved in the machine-checked library of formal theorems, meaning every step is verified by a computer kernel, not taken on faith. It is a THEOREM in the framework's tagging system: it derives its three conclusions from the definitions alone, with no extra assumptions. The complex version, delta_complex_amplitude_headline, extends the same three facts to amplitudes with complex numbers, where the squared size uses the sum of the squares of the real and imaginary parts.

What the headline does not claim is just as important. It does not introduce any new physics; it packages standard finite-dimensional quantum probability into a single formal result. It does not say anything about infinite-dimensional Hilbert spaces, which the framework calls the display completion, the place where the finite structure is later extended. It does not assert that this finite layer is the whole story of quantum mechanics, only that it is a self-contained starting point.

The consequence for a reader is practical: the three rules that make quantum probability work, nonnegativity, normalization, and conservation under evolution, hold already at the finite level, before any limit or completion. This is what the declaration establishes, and it is the foundation on which the framework's later claims about recognition and cost are built.

/-- **Delta-native amplitude headline.** Finite amplitude data has nonnegative
Born weights; normalized finite amplitudes yield total probability one; and
norm-preserving finite transformations preserve normalization. -/
theorem delta_amplitude_headline (N : ℕ) :
    (∀ ψ : Amp N, ∀ i : Fin (N + 1), 0 ≤ bornWeight ψ i)
      ∧ (∀ ψ : Amp N, Normalized ψ →
          Finset.univ.sum (fun i : Fin (N + 1) => bornWeight ψ i) = 1)
      ∧ (∀ U : Amp N → Amp N, NormPreserving U →
          ∀ ψ : Amp N, Normalized ψ → Normalized (U ψ)) :=
  ⟨bornWeight_nonneg, fun _ hψ => born_weights_sum_one hψ,
    fun _ hU _ hψ => normalized_of_normPreserving hU hψ⟩

/-- **Complex finite-amplitude headline.** Complex amplitudes already have a
native finite layer: Born weights are nonnegative, normalized finite complex
amplitudes sum to one, and norm-preserving finite complex transformations
preserve normalization. Hilbert space remains the display completion. -/
theorem delta_complex_amplitude_headline (N : ℕ) :
    (∀ ψ : ComplexAmp N, ∀ i : Fin (N + 1), 0 ≤ complexBornWeight ψ i)
      ∧ (∀ ψ : ComplexAmp N, ComplexNormalized ψ →
          Finset.univ.sum (fun i : Fin (N + 1) => complexBornWeight ψ i) = 1)
      ∧ (∀ U : ComplexAmp N → ComplexAmp N, ComplexNormPreserving U →
          ∀ ψ : ComplexAmp N, ComplexNormalized ψ → ComplexNormalized (U ψ)) :=
  ⟨complexBornWeight_nonneg, fun _ hψ => complex_born_weights_sum_one hψ,
    fun _ hU _ hψ => complex_normalized_of_normPreserving hU hψ⟩

What this page does not claim

The theorem does not introduce new physics beyond standard finite-dimensional quantum probability. The theorem does not address infinite-dimensional Hilbert spaces or the display completion. The theorem does not claim that the finite layer is 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/DeltaAmplitude.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: