Foundation Primitive Recognition Calculus Generable Real Gen Field Is Operationa

The countable core

The real numbers are vast, and most of them are unreachable by any finite description. The declaration genField_is_operational_carrier proves that a much smaller set, the generable reals, still forms a complete arithmetic universe. Start with any countable list of named constants, say the values a theory cares about. Add every rational number. Then close under addition, multiplication, negation, and reciprocal. The result is the generable field: everything obtainable from those seeds by finitely many ordinary field operations.

The theorem states four properties together. Every rational is in the field. Every named constant is in the field. If two numbers are in the field, so are their sum and product. And every nonzero member has its negative and reciprocal inside. Together these mean the generable reals are a genuine operational carrier, a closed workspace where the basic arithmetic of recognition events never leaves the set. The field is also countable, since only countably many finite descriptions exist, and it is a proper subset of the reals: countability rules out the whole continuum.

In Recognition Science, this matters because the framework models reality as a ledger, a discrete record of recognition events. The generable field is the ontology: what can actually be generated and stored. The theorem guarantees that this ontology is not a bare set but a working arithmetic system, closed under every operation the ledger needs. The gap between the countable field and the full continuum is not a flaw; it is the guard against smuggling uncountable ontology in through the analysis interface. A companion result shows that some reals appear only as display values of protocols, never as finite generation, so the display exceeds the generation.

The declaration does not claim that every real number is generable, nor that the field contains any particular transcendental like pi or e unless they are named constants. It does not assert that the generable field is the only possible carrier, nor that it is the largest countable subfield. The theorem is structural: it establishes closure and countability, not uniqueness or maximality.

/-- The generable field is closed under the field operations and contains the
rationals and the named constants: it is a genuine operational carrier, not a bare
set. -/
theorem genField_is_operational_carrier (κ : ℕ → ℝ) :
    (∀ q : ℚ, (q : ℝ) ∈ genField κ)
      ∧ (∀ n : ℕ, κ n ∈ genField κ)
      ∧ (∀ a b : ℝ, a ∈ genField κ → b ∈ genField κ → a + b ∈ genField κ)
      ∧ (∀ a b : ℝ, a ∈ genField κ → b ∈ genField κ → a * b ∈ genField κ)
      ∧ (∀ a : ℝ, a ∈ genField κ → -a ∈ genField κ)
      ∧ (∀ a : ℝ, a ∈ genField κ → a⁻¹ ∈ genField κ)
      ∧ (genField κ : Set ℝ).Countable :=
  ⟨rat_mem κ, const_mem κ,
    fun _ _ ha hb => add_mem ha hb, fun _ _ ha hb => mul_mem ha hb,
    fun _ ha => neg_mem ha, fun _ ha => inv_mem ha, genField_countable κ⟩

/-- 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 κ)

/-- **Phase 2 headline: display exceeds generation.** For any countable constant
family, there is a real that is the value of a Delta-real protocol (so the
analysis display reaches it) yet is not generable. The protocol value map lands
onto the full continuum, while the ontology is the countable generable field; the
gap is exactly the reals that exist only as display, never as finite generation.
This is the guard against smuggling uncountable ontology in through the analysis
interface. -/
theorem display_exceeds_generation (κ : ℕ → ℝ) :
    ∃ r : ℝ, (∃ x : DeltaReal.Protocol, x.value = r) ∧ r ∉ genField κ := by
  obtain ⟨r, hr⟩ := (Set.ne_univ_iff_exists_notMem _).mp (genField_proper κ)
  exact ⟨r, DeltaReal.Protocol.value_surjective r, hr⟩

What this page does not claim

The generable field contains every real number or any particular transcendental unless it is a named constant. The generable field is the unique or maximal countable subfield of the reals. The theorem establishes that the ledger itself is countable, only that its arithmetic core is.

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: