Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcexp Log Field Rs Operations Below C
ARTICLE 2 claims 2 theorems
Foundation Primitive Recognition Calculus Prcexp Log Field Rs Operations Below C
The constants of Recognition Science live in a small, countable field, not spread across the whole real number line.
A countable home for constants
The real number line is vast and uncountable. Most of its points are unreachable by any finite recipe. Recognition Science asks a sharper question: where do its own constants actually live? The answer, proved in the framework's machine-checked library of formal theorems, is a single countable subfield of the reals, a set no larger than the integers, which already contains every constant the framework derives.
This field is built in stages. It starts with two seeds: π and the golden ratio φ. At each stage, the construction takes every number already present, applies the exponential and the natural logarithm to each, and then closes the result under addition, subtraction, multiplication, and division. Repeating this forever produces a field T. The framework proves T is countable, closed under exp and log, contains π, φ, Euler's number e, and the inverse fine-structure constant α⁻¹, and is still a proper subset of the reals.
The declaration rs_operations_below_continuum packages exactly this result. It states that there exists a countable subfield K of the reals such that K is closed under exp and log, contains π, φ, e, and α⁻¹, and is not the whole real line. The construction of every Recognition Science constant can be performed entirely inside K. The uncountable continuum is removed from the framework's operations, not just from its outputs.
What this does not claim is just as important. It does not say the framework has tamed the continuum or made the reals countable. The real line remains uncountable; K is merely a small island within it. It does not claim that α⁻¹ is derived from first principles inside K, only that the constant, once defined, is an element of K. And it does not say the framework's operations are computable in the sense of a Turing machine, only that they stay inside a countable field.
THEOREM rs_operations_below_continuum · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCExpLogField.lean
/-- **Item 1, deep half.** There is a single countable subfield `T` of ℝ that is
closed under exactly the operations the RS constants are built from (field
operations, `exp`, `log`), already contains the seeds π and φ, and contains the
derived constants `e` and `α⁻¹`. The construction of every RS constant can be
performed entirely inside this countable field; the uncountable real line is not
required as the workspace, only (at most) as the ambient in which the standard
`exp`/`log` happen to be defined. The continuum is removed from the framework's
operations, not just its outputs. -/
theorem rs_operations_below_continuum :
∃ K : Subfield ℝ,
(K : Set ℝ).Countable
∧ (∀ x ∈ K, Real.exp x ∈ K)
∧ (∀ x ∈ K, Real.log x ∈ K)
∧ Real.pi ∈ K
∧ Real.goldenRatio ∈ K
∧ Real.exp 1 ∈ K
∧ MinimalField.alphaInv ∈ K
∧ (K : Set ℝ) ≠ Set.univ :=
⟨T, T_countable, fun _ hx => T_exp_closed hx, fun _ hx => T_log_closed hx,
pi_mem_T, phi_mem_T, e_mem_T, alphaInv_mem_T, T_proper⟩
THEOREM T_countable · T_exp_closed · T_log_closed · pi_mem_T · phi_mem_T · e_mem_T · alphaInv_mem_T · T_proper · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCExpLogField.lean
/-- `T` is countable: a countable union of countable stages. -/
theorem T_countable : (T : Set ℝ).Countable := by
rw [T_coe]
exact Set.countable_iUnion S_countable
/-- `T` is closed under `exp`. -/
theorem T_exp_closed {x : ℝ} (hx : x ∈ T) : Real.exp x ∈ T := by
rw [mem_T_iff] at hx ⊢
obtain ⟨n, hn⟩ := hx
refine ⟨n + 1, ?_⟩
have : Real.exp x ∈ Sstep (S n) :=
Subfield.subset_closure (Or.inl (Or.inr ⟨x, hn, rfl⟩))
exact this
/-- `T` is closed under `log`. -/
theorem T_log_closed {x : ℝ} (hx : x ∈ T) : Real.log x ∈ T := by
rw [mem_T_iff] at hx ⊢
obtain ⟨n, hn⟩ := hx
refine ⟨n + 1, ?_⟩
have : Real.log x ∈ Sstep (S n) :=
Subfield.subset_closure (Or.inr ⟨x, hn, rfl⟩)
exact this
theorem pi_mem_T : Real.pi ∈ T :=
mem_T_iff.mpr ⟨0, Subfield.subset_closure (Set.mem_insert _ _)⟩
theorem phi_mem_T : Real.goldenRatio ∈ T :=
mem_T_iff.mpr ⟨0, Subfield.subset_closure (Set.mem_insert_of_mem _ rfl)⟩
/-- Euler's number is `exp 1`, and `1 ∈ T`, so `e ∈ T` by exp-closure. -/
theorem e_mem_T : Real.exp 1 ∈ T := T_exp_closed (one_mem T)
/-- **The payoff: α⁻¹ is built entirely inside `T`.** Every operation in
`α⁻¹ = 44·π·exp(−w₈·ln φ/(44·π))` (field operations, one `log`, one `exp`) lands in
`T`, so the constant is a `T`-element produced without leaving the countable
field. -/
theorem alphaInv_mem_T : MinimalField.alphaInv ∈ T := by
have hpi : Real.pi ∈ T := pi_mem_T
have hphi : Real.goldenRatio ∈ T := phi_mem_T
have h44 : (44 : ℝ) ∈ T := by exact_mod_cast (natCast_mem T 44)
have hw8 : MinimalField.w8 ∈ T := by
unfold MinimalField.w8
exact_mod_cast (natCast_mem T 4)
have hlogphi : Real.log Real.goldenRatio ∈ T := T_log_closed hphi
have harg :
-(MinimalField.w8) * Real.log Real.goldenRatio / (44 * Real.pi) ∈ T :=
div_mem (mul_mem (neg_mem hw8) hlogphi) (mul_mem h44 hpi)
have hexp :
Real.exp (-(MinimalField.w8) * Real.log Real.goldenRatio / (44 * Real.pi)) ∈ T :=
T_exp_closed harg
unfold MinimalField.alphaInv
exact mul_mem (mul_mem h44 hpi) hexp
/-- `T` is a proper subset of ℝ: it is countable, the continuum is not. -/
theorem T_proper : (T : Set ℝ) ≠ Set.univ := by
intro h
exact Cardinal.not_countable_real (h ▸ T_countable)
What this page does not claim
The framework does not make the real numbers countable. The declaration does not derive α⁻¹ from first principles inside T. The framework's operations are not claimed to be computable in the Turing machine sense.
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/PRCExpLogField.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:
- What does it mean for the framework's operations to be carried out inside a countable field?
- Which Recognition Science constants are not elements of the countable field T?
- Does the countable field T have a computable enumeration?
- How does the countable field T relate to the minimal field containing π and φ?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM rs_operations_below_continuum · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCExpLogField.lean
/-- **Item 1, deep half.** There is a single countable subfield `T` of ℝ that is closed under exactly the operations the RS constants are built from (field operations, `exp`, `log`), already contains the seeds π and φ, and contains the derived constants `e` and `α⁻¹`. The construction of every RS constant can be performed entirely inside this countable field; the uncountable real line is not required as the workspace, only (at most) as the ambient in which the standard `exp`/`log` happen to be defined. The continuum is removed from the framework's operations, not just its outputs. -/ theorem rs_operations_below_continuum : ∃ K : Subfield ℝ, (K : Set ℝ).Countable ∧ (∀ x ∈ K, Real.exp x ∈ K) ∧ (∀ x ∈ K, Real.log x ∈ K) ∧ Real.pi ∈ K ∧ Real.goldenRatio ∈ K ∧ Real.exp 1 ∈ K ∧ MinimalField.alphaInv ∈ K ∧ (K : Set ℝ) ≠ Set.univ := ⟨T, T_countable, fun _ hx => T_exp_closed hx, fun _ hx => T_log_closed hx, pi_mem_T, phi_mem_T, e_mem_T, alphaInv_mem_T, T_proper⟩The declaration rs_operations_below_continuum states that there exists a countable subfield K of the reals such that K is closed under exp and log, contains π, φ, e, and α⁻¹, and is not the whole real line. rs_operations_below_continuum · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCExpLogField.leanTHEOREM T_countable · T_exp_closed · T_log_closed · pi_mem_T · phi_mem_T · e_mem_T · alphaInv_mem_T · T_proper · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCExpLogField.lean
/-- `T` is countable: a countable union of countable stages. -/ theorem T_countable : (T : Set ℝ).Countable := by rw [T_coe] exact Set.countable_iUnion S_countable/-- `T` is closed under `exp`. -/ theorem T_exp_closed {x : ℝ} (hx : x ∈ T) : Real.exp x ∈ T := by rw [mem_T_iff] at hx ⊢ obtain ⟨n, hn⟩ := hx refine ⟨n + 1, ?_⟩ have : Real.exp x ∈ Sstep (S n) := Subfield.subset_closure (Or.inl (Or.inr ⟨x, hn, rfl⟩)) exact this/-- `T` is closed under `log`. -/ theorem T_log_closed {x : ℝ} (hx : x ∈ T) : Real.log x ∈ T := by rw [mem_T_iff] at hx ⊢ obtain ⟨n, hn⟩ := hx refine ⟨n + 1, ?_⟩ have : Real.log x ∈ Sstep (S n) := Subfield.subset_closure (Or.inr ⟨x, hn, rfl⟩) exact thistheorem pi_mem_T : Real.pi ∈ T := mem_T_iff.mpr ⟨0, Subfield.subset_closure (Set.mem_insert _ _)⟩theorem phi_mem_T : Real.goldenRatio ∈ T := mem_T_iff.mpr ⟨0, Subfield.subset_closure (Set.mem_insert_of_mem _ rfl)⟩/-- Euler's number is `exp 1`, and `1 ∈ T`, so `e ∈ T` by exp-closure. -/ theorem e_mem_T : Real.exp 1 ∈ T := T_exp_closed (one_mem T)/-- **The payoff: α⁻¹ is built entirely inside `T`.** Every operation in `α⁻¹ = 44·π·exp(−w₈·ln φ/(44·π))` (field operations, one `log`, one `exp`) lands in `T`, so the constant is a `T`-element produced without leaving the countable field. -/ theorem alphaInv_mem_T : MinimalField.alphaInv ∈ T := by have hpi : Real.pi ∈ T := pi_mem_T have hphi : Real.goldenRatio ∈ T := phi_mem_T have h44 : (44 : ℝ) ∈ T := by exact_mod_cast (natCast_mem T 44) have hw8 : MinimalField.w8 ∈ T := by unfold MinimalField.w8 exact_mod_cast (natCast_mem T 4) have hlogphi : Real.log Real.goldenRatio ∈ T := T_log_closed hphi have harg : -(MinimalField.w8) * Real.log Real.goldenRatio / (44 * Real.pi) ∈ T := div_mem (mul_mem (neg_mem hw8) hlogphi) (mul_mem h44 hpi) have hexp : Real.exp (-(MinimalField.w8) * Real.log Real.goldenRatio / (44 * Real.pi)) ∈ T := T_exp_closed harg unfold MinimalField.alphaInv exact mul_mem (mul_mem h44 hpi) hexp/-- `T` is a proper subset of ℝ: it is countable, the continuum is not. -/ theorem T_proper : (T : Set ℝ) ≠ Set.univ := by intro h exact Cardinal.not_countable_real (h ▸ T_countable)The field T is countable, closed under exp and log, contains π, φ, e, and α⁻¹, and is a proper subset of the reals. T_countable · T_exp_closed · T_log_closed · pi_mem_T · phi_mem_T · e_mem_T · alphaInv_mem_T · T_proper · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCExpLogField.lean