Foundation Primitive Recognition Calculus Prcexp Log Field T Log Closed

The countable field

In mathematics, a field is a set of numbers closed under addition, subtraction, multiplication, and division by nonzero numbers. The rational numbers form a field; the real numbers form a larger one. Recognition Science (RS) works with a much smaller field, one that is countable, meaning its elements can be listed in an infinite sequence. The framework's library of formal theorems proves that this countable field contains every constant the framework uses, and that it is built from just two seeds: π and the golden ratio φ.

The construction starts with those two seeds and closes under field operations. Then, at each stage, it adjoins the exponential and logarithm of every number already present, and closes again. Repeating this process forever yields a field T. A theorem named T_log_closed proves that if a number lies in T, then its natural logarithm also lies in T. A companion theorem proves the same for the exponential function. Together they show that T is closed under both operations, so no step in building an RS constant ever leaves the field.

The payoff is that α⁻¹, the inverse fine-structure constant, lies in T. Its RS expression, 44·π·exp(−w₈·ln φ/(44·π)), uses only field operations, one logarithm, and one exponential, so it stays inside the countable field. This means the continuum of real numbers is not needed as a workspace for RS constants; it is only the ambient in which the standard functions happen to be defined. The theorem rs_operations_below_continuum packages this: there exists a countable subfield of ℝ containing π, φ, e, and α⁻¹, closed under exp and log, and not equal to the whole real line.

What T_log_closed does not claim is that the logarithm is defined on all of T in the usual sense. The theorem applies only to positive numbers, since the real logarithm is undefined at zero and negative numbers. It also does not claim that T is the smallest such field, only that one exists. Finally, it does not assert that α⁻¹ equals its measured value; the expression is an identification, not a derived coupling, and the exact value of α remains open.

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

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

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

What this page does not claim

The theorem does not claim that the logarithm is defined on all of T, only on positive elements. It does not claim that T is the smallest field with these properties. It does not claim that the expression for α⁻¹ equals its measured value.

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: