Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMinimalField

show as:
view Lean formalization →

Establishes that any subfield of the reals generated by a countable set remains countable, then builds the minimal Recognition Science field as the subfield generated by a finite list of RS constants (including φ, π, e, and α⁻¹). Anyone working on FRS carriers or generable reals cites this. The countability argument is the field-level lift of algebraic-closure countability to arbitrary generators.

claimAny subfield of $\mathbb{R}$ generated by a countable set is countable. In particular, if $S\subset\mathbb{R}$ is the finite set of Recognition Science constants (including $\varphi$, $\pi$, $e$, and $\alpha^{-1}$), then the subfield $\mathbb{Q}(S)\subset\mathbb{R}$ is countable and contains $\varphi$, $\pi$, and $e$.

background

Primitive Recognition Calculus needs a concrete scalar field inside $\mathbb{R}$ that holds every constant the forcing chain and mass ladder use, yet stays small enough for enumeration and certificate arguments. The natural candidate is the subfield generated over $\mathbb{Q}$ by those constants.

The load-bearing fact is field-theoretic: adjoining countably many reals (algebraic or transcendental) to $\mathbb{Q}$ never leaves the countable realm. This is the direct analogue of the algebraic-closure countability lemma, extended past algebraic generators. Once that closure theorem is in hand, a finite seed set of RS constants yields a countable ambient field.

The module names that seed set (rsConstants) and its generated subfield (rsField), and records the elementary membership facts for $\varphi$, $\pi$, and $e$.

proof idea

Two layers. First, a general countability theorem: the subfield generated by a countable (resp. finite) subset of $\mathbb{R}$ is countable, proved by enumerating field expressions (rational functions in finitely many generators at each stage) and taking a countable union. Second, a definitional layer: a finite list of RS constants is packaged, shown finite hence countable, and the generated subfield is declared; membership of $\varphi$, $\pi$, and $e$ is immediate from the generators. No deep analysis is required beyond the closure enumeration.

why it matters in Recognition Science

This module is the scalar substrate for the rest of Primitive Recognition Calculus. Downstream importers include FRSCarrier (the carrier for forced recognition structures), GenerableReal (reals reachable by RS generation), PRCExpLogField (exp/log structure over the same scalars), PRCChainBridge (linking the forcing chain into the field), and PRCShrunkCertificate (compact certificates that rely on countability). Without a countable ambient field containing $\varphi$, $\pi$, and the fine-structure constants, enumeration and certificate arguments later in the stack have nowhere to live. The construction sits under the Foundation layer that feeds T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$) once those constants are interpreted inside $\mathbb{R}$.

scope and limits

used by (5)

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

declarations in this module (22)