Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.GenerableReal

show as:
view Lean formalization →

Defines the generable reals: the subfield of ℝ obtained from a countable family of named constants κ together with the rationals by finitely many field operations. Supplies countability, properness, and membership lemmas for rationals and the named constants. Downstream native-analysis and objecthood modules cite this carrier as the operational scalar field of Primitive Recognition Calculus.

claimFor a countable family of named constants $\kappa$, the generable field $\mathrm{Gen}(\kappa)\subset\mathbb{R}$ is the subfield generated by $\kappa\cup\mathbb{Q}$. Equivalently, it is the set of all reals obtainable from the constants and rationals by finitely many additions, multiplications, and inversions.

background

Primitive Recognition Calculus works with a minimal operational scalar field rather than the full continuum. The present module isolates that carrier: fix a countable list of named constants $\kappa$ (imported from the PRC minimal-field and $\Delta$-real layers), and form the smallest subfield of $\mathbb{R}$ containing $\kappa$ and $\mathbb{Q}$.

Every element is therefore a finite rational expression in the named constants. The construction is the standard field adjunction $\mathbb{Q}(\kappa)$, written here as a concrete subset of $\mathbb{R}$ so that later modules can compare generable scalars against display values and native $\Delta$-quantities without leaving the real line.

Sibling facts record that the generable field is countable, properly smaller than $\mathbb{R}$ once $\kappa$ is countable, contains every rational and every constant from $\kappa$, and serves as the operational carrier for subsequent PRC analysis.

proof idea

Definition module. The main object is the subfield generated by a countable constant family; surrounding lemmas are standard field-adjunction and countability arguments (countable union of finite expressions, closure under the field operations, properness via cardinality). No deep analytic content lives here; the module only packages the carrier and its elementary membership and size facts for import.

why it matters in Recognition Science

Gives the scalar universe in which Primitive Recognition Calculus performs native arithmetic. DeltaNativeAnalysis and DeltaNativeStrongClosure import it to reason about $\Delta$-quantities inside a countable operational field rather than full $\mathbb{R}$. ObjecthoodRegistry uses the same carrier when registering which scalars count as generable objects.

In the broader Recognition stack this is foundation plumbing: once the forcing chain has fixed the cost $J$ and the self-similar scale $\phi$, concrete computations still need a precise subfield of reals closed under the field operations and generated by the named constants of the theory. GenerableReal is that subfield. It does not itself force $\phi$, the eight-tick period, or $D=3$; it only supplies the ambient arithmetic those later results compute inside.

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