Foundation Primitive Recognition Calculus Generable Real Const Mem

The named constants

In mathematics, a field is a number system where addition, subtraction, multiplication, and division by nonzero numbers all work and stay inside the system. The rationals are a field; the reals are a field. Given any collection of starting numbers, there is a smallest field containing them: take the rationals, throw in the starting numbers, and close under the four operations. The theorem const_mem states the simplest possible fact about this construction: every one of the starting numbers is indeed inside the field it generates. If the starting numbers are a countable family, the resulting field is countable, meaning its members can be listed in an infinite sequence.

The framework's library, a machine-checked collection of formal theorems, defines the generable reals relative to a countable family of named constants: the subfield of the real numbers generated by those constants. Equivalently, it is everything obtainable from the constants and the rationals by finitely many field operations. The theorem const_mem proves, for any constant family and any index, that the constant belongs to this field. The proof is immediate from the definition: a field generated by a set must contain every element of that set. The same library also proves that every rational is generable, that the generable reals are countable, and that they form a proper subset of the reals, since countability rules out the whole continuum.

In Recognition Science, this construction carries a specific role. The framework models a discrete record of events, a ledger, and asks which real numbers can be produced as finite objects. The generable field is the ontology: the numbers that exist as finite generation. A separate theorem, display_exceeds_generation, shows that some reals can be displayed by a protocol yet are not generable, so the analysis interface cannot smuggle in uncountable ontology. The theorem const_mem is the entry point: it guarantees that every named constant is a legitimate finite object within the framework's ontology.

The theorem does not claim that the named constants are distinct, that they are independent, or that they exhaust the generable reals. It does not say anything about what the constants are, only that each one, whatever its value, is in the field it generates. It also does not claim that the generable field equals the reals; the companion theorem genField_proper proves the opposite. The practical consequence is that the framework's constants, whatever they are, are always available as building blocks for further finite constructions.

/-- Every named constant is generable. -/
theorem const_mem (κ : ℕ → ℝ) (n : ℕ) : κ n ∈ genField κ :=
  Subfield.subset_closure ⟨n, rfl⟩

/-- The generable reals are countable: only countably many finite descriptions
exist. -/
theorem genField_countable (κ : ℕ → ℝ) : (genField κ : Set ℝ).Countable :=
  MinimalField.subfield_closure_countable_of_countable (Set.countable_range κ)

/-- The generable reals are a proper subset of ℝ: countability rules out the whole
continuum. -/
theorem genField_proper (κ : ℕ → ℝ) : (genField κ : Set ℝ) ≠ Set.univ := by
  intro h
  exact Cardinal.not_countable_real (h ▸ genField_countable κ)

What this page does not claim

The named constants are distinct or independent of one another. The generable field exhausts the real numbers. The theorem identifies what the named constants are or what values they take.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/GenerableReal.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: