Foundation Primitive Recognition Calculus Generable Real Gen Field Countable

The countable field

The real numbers are vast: there are uncountably many of them, more than can ever be listed or described one by one. Yet most mathematical work proceeds from a small set of named constants, such as π or e, and builds new numbers by the familiar field operations: addition, multiplication, subtraction, and division. The question is how much of the real line such a process can reach. The answer, proved in the machine-checked library of formal theorems, is that the reachable set is always countable: no matter which countable family of starting constants you choose, the numbers you can generate from them by finitely many field operations form only a countable collection.

This result, called genField_countable in the library, is a theorem about the generable reals, the subfield of ℝ generated by a given countable family of constants. The proof is short and structural: the starting family is countable, and the collection of all finite expressions built from a countable set is itself countable, so the closure under field operations remains countable. The theorem holds for any countable constant family, with no further assumptions on the constants themselves. A companion theorem, genField_proper, draws the immediate consequence: the generable reals are a proper subset of ℝ, since the whole real line is uncountable while the generable field is not.

The framework's library goes one step further with a theorem named display_exceeds_generation. It shows that for any countable constant family, there exists a real number that is the value of a Delta-real protocol, meaning it can be displayed or approximated through the analysis interface, yet is not generable from the constants. This establishes a precise sense in which display exceeds generation: the protocol value map reaches the full continuum, while the ontology, the countable generable field, is strictly smaller. The gap consists exactly of those reals that exist only as display, never as finite generation.

The generable field is not a bare set but a genuine operational carrier. Another theorem, genField_is_operational_carrier, packages the closure properties: it contains all rationals and all named constants, and is closed under addition, multiplication, negation, and inversion. This means the field supports real arithmetic internally, so it can serve as the working domain for the framework's recognition calculus without smuggling in uncountable ontology through the analysis interface. The countability theorem is the guard that keeps the ontology countable and the display honest.

/-- 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⟩

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

What this page does not claim

The theorem does not identify which specific reals are nongenerable, only that at least one exists for any countable family. The theorem does not claim the generable field contains all reals that appear in any physical theory, only those finitely generated from the chosen constants. The theorem does not imply that uncountable sets are unusable in the framework, only that they are not part of the finite generation ontology.

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: