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 and Born weights that sum to one when normalized. Supplies the amplitude layer sitting above delta-probability in the primitive recognition calculus. Downstream native-analysis and FRS complex-amplitude modules import it as the carrier type for Born-rule bookkeeping. Mostly definitions plus elementary nonnegativity and normalization lemmas.

claimA real amplitude is a vector $A \in \mathbb{R}^{N+1}$. Its squared norm is $\|A\|^2 = \sum_i A_i^2$, and the Born weight of index $i$ is $w_i = A_i^2$. The vector is normalized when $\sum_i w_i = 1$. Complex amplitudes $C \in \mathbb{C}^{N+1}$ use $w_i = |C_i|^2$. Norm-preserving maps send normalized amplitudes to normalized amplitudes.

background

In the primitive recognition calculus, discrete configurations live on a finite index set $\mathrm{Fin}(N+1)$. The upstream DeltaProbability module treats probability weights on that set. This module lifts those weights to an amplitude layer: a real vector whose coordinate squares recover the Born weights.

The squared-norm functional $\mathrm{normSq}$ and the per-coordinate $\mathrm{bornWeight}$ are the basic observables. A predicate $\mathrm{Normalized}$ asserts that the Born weights sum to one. Parallel complex amplitudes and a complex Born weight are introduced for the FRS (finite recognition state) complex path.

The local setting is foundational bookkeeping only: no dynamics, no J-cost, and no forcing-chain step. The types are the carrier data for later native-analysis and objecthood registry work.

proof idea

This is primarily a definition module. Core objects (real amplitude, complex amplitude, squared norm, Born weight, normalized predicate, norm-preserving maps) are introduced by direct defs. Supporting lemmas are elementary: nonnegativity of squared norms and Born weights by sum-of-squares, the identity that Born weights of a normalized vector sum to one, and the fact that a norm-preserving map sends normalized vectors to normalized vectors. A headline lemma packages the real-amplitude story for downstream citation. No deep tactic proof is required beyond Mathlib arithmetic on finite sums.

why it matters in Recognition Science

Amplitudes are the bridge from bare delta-probability weights to a Born-rule layer inside Recognition Science. Downstream, DeltaNativeAnalysis and DeltaNativeStrongClosure import this module to reason about native delta structure with amplitude data; FRSComplexAmplitude extends the complex carrier; ObjecthoodRegistry consumes the normalized amplitude interface when registering discrete objects.

In the broader framework the Born weight $w_i = A_i^2$ is the discrete counterpart of the measurement rule that later meets the phi-ladder mass formula and eight-tick bookkeeping. The module itself does not force phi, D=3, or the RCL; it only standardizes the finite-dimensional amplitude type those arguments will use.

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)