frsi_amplitude_headline
plain-language theorem explainer
Finite complex amplitudes live natively on the finite-description carrier F_RS[i]; ambient ℂ is only a display map. The headline packages four facts: Born weights are nonnegative, display preserves the squared-norm sum, native normalization matches complex normalization, and real/imaginary evaluations stay in the RS scalar field. Anyone citing the Delta-native strong-closure certificate needs this bundle. The proof is a four-component term packaging prior lemmas.
Claim. For every $N \in \mathbb{N}$, writing $\mathrm{Amp}_{F_{RS}[i]}(N)$ for finite amplitude vectors with $N+1$ components over $F_{RS}[i]$: (i) every native Born weight is $\ge 0$; (ii) the squared complex norm of the ambient display equals the sum of those Born weights; (iii) native normalization (sum of Born weights $=1$) is equivalent to complex normalization of the display; (iv) for every $F_{RS}[i]$ scalar expression $z$, both $\mathrm{Re}(\mathrm{eval}\, z)$ and $\mathrm{Im}(\mathrm{eval}\, z)$ lie in the RS minimal scalar field.
background
This module equips the finite-description scalar carrier $F_{RS}[i]$ with complex amplitudes. An $F_{RS}[i]$ expression is a pair of real $F_{RS}$ expressions (real and imaginary parts). A finite amplitude of length $N+1$ is a map from $\mathrm{Fin}(N+1)$ into those expressions. The native Born weight at index $i$ is $\mathrm{eval}(\mathrm{re})^2 + \mathrm{eval}(\mathrm{im})^2$; the display map sends each component into ambient $\mathbb{C}$.
Upstream, DeltaAmplitude already defines real and complex finite amplitudes, their Born weights (squared components), squared norms as finite sums, and the corresponding normalization predicates. The present layer lifts those notions so that ambient $\mathbb{C}$ is only a forgetful display: carrier membership, Born weights, and normalization are computed natively on $F_{RS}[i]$ and shown to agree with the display.
Local normalization is defined exactly as the sum of native Born weights equaling one, and is intended to match complex normalization of the displayed vector.
proof idea
Term-mode packaging of four already-proved facts. The conjunction is assembled as a 4-tuple:
- Nonnegativity of native Born weights (
bornWeight_nonneg). - Equality of displayed complex squared-norm with the sum of native Born weights (
display_normSq_eq). - Equivalence of native and displayed normalization (
normalized_iff_display). - A lambda over $F_{RS}[i]$ expressions pairing
eval_re_memandeval_im_mem, which place real and imaginary evaluations in the RS minimal field.
No new algebra is done here; the headline is the certificate surface that downstream closure code can cite in one shot.
why it matters
This is the finite-amplitude headline for the $F_{RS}[i]$ carrier: it states that complex amplitudes needed by the recognition calculus need not leave the finite-description scalar field. Ambient $\mathbb{C}$ is display-only; Born structure and normalization survive the display.
Downstream, strongClosureCertificate in DeltaNativeStrongClosure consumes this bundle as part of the concrete certificate assembling the closed Delta-native theorem surface. That certificate ties together real-forgetful display, generable operational carriers, certified analytic protocols, and related transformers. Without the amplitude headline, the complex half of the Delta-native story would not sit on the same carrier footing as the real half.
In the broader Recognition Science stack this sits in Primitive Recognition Calculus foundation work that precedes the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$). It does not itself force constants or mass rungs; it secures the scalar/amplitude substrate those later steps assume can be carried finitely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.