Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude

show as:
view Lean formalization →

Defines finite real (and complex) amplitude vectors on Fin(N+1), with squared norm, Born weights, normalization, and norm-preserving maps. Anyone building discrete Born-rule calculus or the complex FRS amplitude layer cites this module. Content is definitional plus elementary nonnegativity and sum-to-one lemmas over the probability layer beneath it.

claimA real amplitude on $N+1$ outcomes is a map $a:\{0,\ldots,N\}\to\mathbb{R}$. Write $\|a\|_2^2=\sum_i a_i^2$ and Born weights $w_i=a_i^2/\|a\|_2^2$ (when $\|a\|_2\neq 0$). Normalization means $\|a\|_2^2=1$; a map is norm-preserving if it sends normalized amplitudes to normalized ones. Complex amplitudes and complex Born weights are defined in parallel.

background

Primitive Recognition Calculus works on a finite discrete outcome set Fin (N+1), matching ledger/tick structure used in the foundation. The upstream module DeltaProbability already treats probability mass on that set. This module lifts probabilities to amplitudes: real vectors whose squared components recover the Born rule.

Core objects introduced here are real amplitude vectors, their squared Euclidean norm, the associated Born weight vector, a Normalized predicate ($\sum a_i^2=1$), and NormPreserving maps. Parallel complex amplitude and complex Born-weight definitions prepare the phase-bearing layer without yet imposing dynamics.

The setting is pre-geometric and finite-dimensional: no continuum Hilbert space, no operator algebra. It is the discrete amplitude substrate that native analysis and objecthood registration will consume.

proof idea

This is a definition module, not a deep proof development. It declares real and complex amplitude types on Fin(N+1), defines squared norm and Born weight, and records elementary facts: nonnegativity of norm and weights, that Born weights of a nonzero (or normalized) vector sum to one, and that norm-preserving maps send normalized amplitudes to normalized amplitudes. Arguments are standard finite sums over Fin, building directly on the imported probability layer.

why it matters in Recognition Science

Sits between DeltaProbability and the native/complex amplitude stack. Downstream importers are DeltaNativeAnalysis and DeltaNativeStrongClosure (calculus and strong closure on delta amplitudes), FRSComplexAmplitude (complex/phase extension), and ObjecthoodRegistry (registration of amplitude-level objects). Without a clean Born-weight and normalization interface, those layers cannot state unit-norm evolution or probability readout in RS-native discrete form. The module does not itself touch the T0–T8 forcing chain, RCL, or mass ladder; it supplies the finite amplitude language those later stories need when they speak in Born-rule terms.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)