Foundation Primitive Recognition Calculus Prcminimal Field Subfield Closure Coun

The countable field

A subfield of the real numbers generated by a countable set is countable. This is the load-bearing closure fact: adjoining countably many reals to the rationals never escapes countability. It is the field-level analogue of delta_algebraic_closure_stays_countable, lifted from algebraic generators to arbitrary (including transcendental) generators.

The theorem, named subfield_closure_countable_of_countable, states that if a set s of real numbers is countable, then the subfield it generates is also countable. The proof uses cardinal arithmetic: the cardinality of the closure is at most the maximum of the cardinality of the generators and aleph-null, which is countable. A corollary for finite generating sets, subfield_closure_countable_of_finite, covers the case the Recognition Science constants need.

In Recognition Science, the framework defines a minimal field rsField generated by the named constants: the golden ratio φ, π, Euler's number e, and the fine-structure weight α⁻¹. The theorem rsField_countable proves this field is countable. The field contains every integer power of φ, the eight-tick output 8, the spatial dimension 3, and every rung of the mass ladder when the yardstick is in the field. rsField_extend_stays_countable shows that adjoining any further countable family of constants keeps the field countable.

The field is a proper subset of the real numbers, since it is countable while the continuum is not. The theorem rs_physics_below_continuum packages this: the entire Recognition-Science scaffold lives in a countable field, not in the uncountable real line. This means the framework's working machinery, the φ-ladder and the chain's integer outputs, is countable-field content.

What the theorem does not claim: it does not say the field is the real numbers, nor that it contains every real number. It does not claim that the constants are the only elements, nor that the field is minimal in any sense beyond being generated by the named set. It does not assert that the field is algebraically closed or that it contains all real algebraic numbers. The theorem is a cardinality statement, not a structural characterization of the field.

/-- A subfield of `ℝ` generated by a countable set is countable.

This is the load-bearing closure fact: adjoining countably many reals to the
rationals never escapes countability. It is the field-level analogue of
`delta_algebraic_closure_stays_countable`, lifted from algebraic generators to
arbitrary (including transcendental) generators. -/
theorem subfield_closure_countable_of_countable {s : Set ℝ} (hs : s.Countable) :
    (Subfield.closure s : Set ℝ).Countable := by
  have hs' : Cardinal.mk s ≤ ℵ₀ :=
    Cardinal.mk_le_aleph0_iff.mpr (Set.countable_coe_iff.mpr hs)
  have hcard : Cardinal.mk (Subfield.closure s) ≤ ℵ₀ :=
    (Subfield.cardinalMk_closure_le_max s).trans (max_le hs' le_rfl)
  have hcount : Countable (Subfield.closure s) := Cardinal.mk_le_aleph0_iff.mp hcard
  exact Set.countable_coe_iff.mp hcount

/-- The RS constant field is countable. -/
theorem rsField_countable : (rsField : Set ℝ).Countable :=
  subfield_closure_countable_of_finite rsConstants_finite

/-- The RS constant field is a *proper* subset of ℝ: it is countable, while the
continuum is not. The continuum is therefore not the home of RS physics. -/
theorem rsField_proper : (rsField : Set ℝ) ≠ Set.univ := by
  intro h
  have huniv : (Set.univ : Set ℝ).Countable := h ▸ rsField_countable
  exact Cardinal.not_countable_real huniv

/-- **Item 1 headline.** Every named Recognition-Science constant value lives in
one countable subfield of ℝ that is strictly below the continuum. The arbitrary
content of the framework's codomain is therefore at most countable; the
uncountable real line is not required as the home of the constants. -/
theorem rs_physics_below_continuum :
    (rsField : Set ℝ).Countable
      ∧ Real.goldenRatio ∈ rsField
      ∧ Real.pi ∈ rsField
      ∧ Real.exp 1 ∈ rsField
      ∧ alphaInv ∈ rsField
      ∧ (rsField : Set ℝ) ≠ Set.univ :=
  ⟨rsField_countable, rsField_mem_phi, rsField_mem_pi, rsField_mem_e,
    rsField_mem_alphaInv, rsField_proper⟩

What this page does not claim

The theorem does not claim the field is the real numbers or contains every real number. The theorem does not claim the field is algebraically closed or contains all real algebraic numbers. The theorem does not claim the constants are the only elements of the field.

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/PRCMinimalField.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: