Foundation Primitive Recognition Calculus Prcexp Log Field

The countable workspace

In Recognition Science (RS), the ledger, a discrete record of recognition events, is meant to be the only primitive. The framework addresses a basic question: where do its constants live? The answer is that they live in a countable subfield of the real numbers, not scattered across the entire uncountable real line.

The construction starts with two seeds: the real numbers π (pi) and φ (the golden ratio). From these, a chain of fields is built. At each stage, the current field is extended by adding the images of every element under the exponential function exp and the natural logarithm log, and then closing under field operations (addition, subtraction, multiplication, division). The union of all these stages is a field called T. The proofs show that T is countable, that it is closed under exp and log, and that it contains π, φ, and Euler's number e (since e = exp 1, and 1 is in every field).

The key result is that T also contains the inverse fine-structure constant α⁻¹. This is significant because α⁻¹ is not a simple rational or algebraic number; it is built from π, φ, and exponentials and logarithms. The theorem alphaInv_mem_T shows that every operation in its definition lands inside T. The central theorem, rs_operations_below_continuum, packages this all together: there exists a countable subfield of the reals that is closed under exp and log, contains the seeds and the derived constants e and α⁻¹, and is a proper subset of the real numbers.

In plain language, this means the framework's entire calculus, its recognition ledger and all derived constants, operates within a countable workspace. The uncountable real line is not needed as a workspace, only as the ambient space where the standard exp and log functions happen to be defined. This is a structural fact about the framework's parsimony: its operations do not require the full continuum. The result is a theorem, proved in a machine-checked library of formal theorems, and it establishes a boundary on where RS constants can be found.

/-- **The exp/log-closed RS field.** The union of the directed chain. -/
noncomputable def T : Subfield ℝ := ⨆ n, S n

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

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

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

This module does not derive the value of α⁻¹; it only shows that α⁻¹ lies inside the countable field T. This module does not claim that all real numbers are countable; it proves that T is a proper subset of the reals. This module does not establish that the framework's operations are computable, only that they can be performed within a countable 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/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: