Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSComplexAmplitude

show as:
view Lean formalization →

Defines finite-description complex scalars over the Recognition Science carrier field: real and imaginary parts are both F_RS expressions. Introduces evaluation into C, display amplitudes, and Born weights with nonnegativity. Downstream native-analysis and Hilbert-display modules import this layer. The content is definitional scaffolding plus elementary algebraic identities, not a deep existence proof.

claimA complex scalar in $F_{RS}[i]$ is a pair of $F_{RS}$ expressions $(a,b)$ interpreted as $a+bi$. Evaluation maps such expressions to $\mathbb{C}$; the display amplitude and Born weight $|z|^2$ are defined on this type, with $|z|^2\ge 0$ and agreement between display and native norm-squared forms.

background

Recognition Science builds amplitudes on a finite-description carrier $F_{RS}$ rather than bare $\mathbb{C}$. The carrier module supplies the real scalar expressions; the delta-amplitude layer supplies the real amplitude calculus that this module complexifies.

This module packages a complex scalar as two $F_{RS}$ expressions (real and imaginary parts). Evaluation sends those expressions into ordinary complex numbers. Display amplitude and Born weight are then defined so that probability weights stay nonnegative and match the squared modulus of the evaluated complex value.

The setting is the Primitive Recognition Calculus foundation: keep every intermediate object finitely describable before any completion or Hilbert-space display step.

proof idea

This is primarily a definition module. It introduces the complex expression type, evaluation maps for real and imaginary parts (with membership lemmas), display amplitude, and Born weight. The short theorems are algebraic: Born weight equals the display norm-squared, equals the squared complex modulus after evaluation, and is nonnegative. No deep analytic argument lives here; identities follow from the real carrier and standard complex arithmetic.

why it matters in Recognition Science

Complex amplitudes are the bridge from real $F_{RS}$ calculus to Born-rule weights and Hilbert-style display. Downstream modules DeltaNativeAnalysis and DeltaNativeStrongClosure import this layer to analyze native delta amplitudes over complex scalars. HilbertDisplayCompletion uses it when completing display data toward a Hilbert picture.

In the broader RS chain, this sits under Primitive Recognition Calculus: finite carriers first, continuum displays later. It does not itself force $J$, $\varphi$, the eight-tick octave, or $D=3$; it supplies the complex scalar language those analytic closures need once the real carrier is fixed.

scope and limits

used by (3)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)