Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSCarrier

show as:
view Lean formalization →

Defines the F_RS carrier: finite field expressions built from rationals and the RS constant inventory (phi, pi, e, alpha inverse). Evaluation lands in the reals, and the image set is countable and proper. Downstream native-analysis and complex-amplitude modules import this syntax as the ambient term language for delta and amplitude constructions.

claimLet $F_{RS}$ be the set of finite terms generated from $\mathbb{Q}$ and the constant inventory $\{\varphi,\pi,e,\alpha^{-1}\}$ under the field operations $+,-,\cdot,/$. Evaluation $[[\cdot]]:F_{RS}\to\mathbb{R}$ is well-defined on the carrier; the image $\mathrm{carrierValues}\subset\mathbb{R}$ is countable and a proper subset of $\mathbb{R}$.

background

Primitive Recognition Calculus needs a precise ambient field of scalars before native delta analysis or complex amplitudes. This module supplies that language: an inductive expression type whose leaves are rationals or named RS constants, closed under the four field operations.

The constant inventory is the RS-native set used throughout the foundation: the golden ratio $\varphi$ (T6 fixed point), $\pi$, $e$, and the fine-structure inverse $\alpha^{-1}$ (targeted to the RS band near $137.03$). Upstream modules supply the minimal field interface and the real embedding of delta quantities; this file only builds the term syntax and its evaluation.

Sibling facts record that every rational, and each inventory constant, is a term; evaluation stays inside the intended real carrier; and the set of values is countable yet not all of $\mathbb{R}$.

proof idea

This is a definition module, not a theorem chain. The core object is an inductive expression datatype for finite field terms. Evaluation is defined by recursion on that datatype. Membership, subset, countability, and properness of the value set are short structural lemmas (induction on terms, countable union of countable sets, and an explicit real outside the image).

why it matters in Recognition Science

Every later native-analysis step needs a fixed, countable term language so that identities about delta and amplitudes are statements about concrete expressions rather than arbitrary reals. Downstream importers are DeltaNativeAnalysis, DeltaNativeStrongClosure, and FRSComplexAmplitude: they treat this carrier as the syntax of scalars on which native closure and complex-amplitude constructions are stated.

In the broader RS stack the carrier is the bookkeeping layer beneath the forcing chain and the Recognition Composition Law: constants such as $\varphi$ and $\alpha^{-1}$ appear as leaves, not as free real parameters. Without a proper countable carrier, countability and definability arguments used in native strong closure would not type-check.

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 (14)