IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSComplexAmplitude
Defines finite-description complex scalars over the Recognition Science carrier field: each amplitude has real and imaginary parts that are F_RS expressions. Supplies evaluation maps, a display amplitude, and the Born weight (squared modulus) with nonnegativity. Downstream native analysis and Hilbert-display modules import this layer to treat complex amplitudes without leaving the finite RS language.
claimAn element of $F_{RS}[i]$ is a pair of $F_{RS}$ expressions $(a,b)$ interpreted as the complex scalar $a+bi$. Evaluation sends such a pair to $\mathbb{C}$; the display amplitude and Born weight are $|z|^2 = (\mathrm{Re}\,z)^2+(\mathrm{Im}\,z)^2$, proved nonnegative.
background
Recognition Science keeps amplitudes inside a finite-description carrier $F_{RS}$ rather than raw $\mathbb{C}$. The sibling carrier module supplies that language; the delta-amplitude module supplies the real scalar amplitude calculus that this file complexifies.
This module adjoins a formal imaginary unit by pairing two $F_{RS}$ expressions. The resulting type is a finite-description complex scalar: real and imaginary parts remain RS expressions, so every subsequent identity stays checkable in the same formal language.
Notation in the file: expression pairs, componentwise evaluation to reals, a display map into ordinary complex amplitudes, and the Born weight as squared modulus. These are the primitives needed before native analysis or Hilbert-space display completion.
proof idea
This is a definition module. It introduces the complex expression type, evaluation of real and imaginary parts, membership lemmas for those parts in the carrier, the display amplitude, and the Born weight. The nontrivial content is algebraic: Born weight equals the squared complex modulus of the display amplitude, and that weight is nonnegative. No deep analytic argument lives here; proofs are direct from the real/imaginary decomposition and nonnegativity of squares.
why it matters in Recognition Science
Complex amplitudes are the bridge from real RS cost calculus to Born-rule weights and Hilbert-space display. Delta-native analysis and strong-closure modules import this file to reason about complex delta amplitudes inside $F_{RS}[i]$. Hilbert display completion uses the same display amplitude and Born weight to connect finite RS expressions to the completed inner-product picture.
In the broader framework this sits under Primitive Recognition Calculus: it does not force $J$, $\varphi$, or dimension, but it makes the amplitude side of recognition formally complex while preserving finite describability. Without it, downstream native and Hilbert layers would have to reinvent the $F_{RS}[i]$ carrier ad hoc.
scope and limits
- Does not define the real carrier $F_{RS}$ itself; that lives in the carrier module.
- Does not prove completeness or Hilbert-space axioms; only display and Born weight.
- Does not derive Born's rule from recognition postulates; only defines $|z|^2$.
- Does not address forcing-chain landmarks (J-uniqueness, $\varphi$, eight-tick, $D=3$).
- Does not supply analytic estimates; those belong to native-analysis importers.
used by (3)
depends on (2)
declarations in this module (15)
-
structure
FRSIExpr -
def
eval -
theorem
eval_re -
theorem
eval_im -
theorem
eval_re_mem -
theorem
eval_im_mem -
abbrev
FRSIAmp -
def
displayAmp -
def
bornWeight -
theorem
display_bornWeight_eq -
theorem
display_normSq_eq -
theorem
bornWeight_nonneg -
def
Normalized -
theorem
normalized_iff_display -
theorem
frsi_amplitude_headline