Foundation Primitive Recognition Calculus Prcminimal Field Rs Field Extend Stays

The countable field

A field is a number system closed under addition, subtraction, multiplication, and division. The rational numbers form the smallest such system. Start with any finite or countable set of real numbers, adjoin them to the rationals, and close under the four operations: the result is still countable. This is a theorem of standard mathematics, and the machine-checked library proves it in full generality.

Recognition Science names four constants as its starting set: the golden ratio φ, π, Euler's number e, and a fine-structure weight α⁻¹. These four generate a field, called the RS constant field. Because the starting set is finite, the field is countable: it has exactly as many elements as the natural numbers, not as many as the real line. The theorem rsField_extend_stays_countable sharpens this: adjoin any countable family of additional real constants, and the field remains countable. The construction never forces the framework to use the full continuum.

The payoff is structural. Every integer power of φ lies in the field, so the entire mass ladder of the framework is countable-field content. The outputs 8 and 3, the eight-tick cycle and the spatial dimension, are field elements. The field is a proper subset of the real numbers: countable, while the continuum is not. The framework's working machinery, in this account, lives below the continuum.

What the theorem does not claim is equally plain. It does not say the framework's physics is correct, or that the constants are derived rather than chosen. It does not say the real numbers are dispensable in general mathematics. It says only that the named constants and any countable extension of them generate a countable field, a fact about cardinality, not about physical truth.

/-- Adjoining any further countable family of constants keeps the field
countable. The construction never requires the continuum no matter how many
constants RS eventually names. -/
theorem rsField_extend_stays_countable {s : Set ℝ} (hs : s.Countable) :
    (Subfield.closure (rsConstants ∪ s) : Set ℝ).Countable :=
  subfield_closure_countable_of_countable (rsConstants_countable.union hs)

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

/-- Every integer power of φ lies in the field: the entire φ-ladder, the scaffold
of the RS mass law, is countable-field content, not continuum content. -/
theorem rsField_phi_zpow (n : ℤ) : Real.goldenRatio ^ n ∈ rsField :=
  zpow_mem rsField_mem_phi n

What this page does not claim

The theorem does not prove that the named constants are physically correct or derived rather than chosen. The theorem does not claim that the real numbers are dispensable in mathematics generally. The theorem does not assert that any specific uncountable set of constants is excluded from the framework.

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: