ComplexAmp
plain-language theorem explainer
Finite complex amplitude vectors on N+1 alternatives are maps from {0,...,N} into the complex numbers. Anyone building Born weights, normalization, or finite unitary evolution in the primitive recognition calculus cites this type. The declaration is a one-line type abbreviation with no proof content.
Claim. For each natural number $N$, a complex amplitude vector of size $N+1$ is a function $\psi:\{0,1,\ldots,N\}\to\mathbb{C}$.
background
The DeltaAmplitude module sets up finite amplitude calculus for the primitive recognition layer: discrete alternatives indexed by Fin (N+1), with both real and complex variants. The real sibling is a map into ℝ; this abbreviation is the complex counterpart used when phases matter.
In ordinary quantum mechanics an amplitude is a vector in a Hilbert space, and probabilities are squared moduli. Here the same idea is finitized: N+1 slots, each carrying a complex value. Downstream definitions extract the Born weight of slot i as re²+im² and the total squared norm as the sum of those weights.
Upstream, related notions of amplitude appear in the double-slit model (sum of two complex path phases) and various norms (GoldenInt field norm, L² action norm). Those are separate constructions; this type is the local carrier for the finite complex Born package.
proof idea
Pure type abbreviation: ComplexAmp N is definitionally Fin (N+1) → ℂ. No lemmas, no tactics, no proof obligations. Unfolding is definitional equality.
why it matters
This type is the carrier for the finite complex Born rule and finite unitary evolution in the primitive recognition calculus. Downstream it is used by complex Born weight (per-slot |z|²), nonnegativity of those weights, the squared-norm sum, the ComplexNormalized predicate (total squared norm equals one), ComplexNormPreserving maps (native finite stand-in for unitary evolution), and the theorem that norm-preserving maps send normalized vectors to normalized vectors.
In the Recognition Science stack this is scaffolding for discrete recognition alternatives before continuum Hilbert-space structure is recovered. It sits beside the real amplitude path and feeds any argument that needs complex phases on a finite set of outcomes. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those enter only if later modules connect amplitudes to J-cost or the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.