Foundation Primitive Recognition Calculus Prcexp Log Field T Exp Closed

The countable field

The real numbers form an uncountable continuum, but the constants of Recognition Science live in a much smaller place. The framework's library of formal theorems builds a countable subfield of the reals, a set of numbers that can be listed one after another, and proves that every operation the framework's constants are built from stays inside it. This field, called T, is generated from just two seeds: the number π and the golden ratio φ. From those, the field operations of addition, subtraction, multiplication, and division, together with the exponential and logarithm functions, produce every constant the framework uses.

The central theorem T_exp_closed states that if a number lies in T, then its exponential also lies in T. The logarithm is closed in the same way. Because the field already contains 1, applying the exponential closure once shows that Euler's number e is in T. The construction proceeds in stages: each stage takes the current field, adds the exponentials and logarithms of all its elements, and then closes under field operations. The union of all these stages is T, and each stage is countable, so the whole field is countable.

The payoff concerns the inverse fine-structure constant α⁻¹, whose framework expression is 44·π·exp(−w₈·ln φ/(44·π)). Every operation in that expression, field operations plus one logarithm and one exponential, lands in T. The theorem alphaInv_mem_T proves this directly. The consequence is that the framework's entire stock of constants, including π, φ, e, and α⁻¹, can be constructed inside a countable field. The uncountable real line is not needed as a workspace; it serves only as the ambient space where the standard exponential and logarithm functions happen to be defined.

This matters because it removes the continuum from the framework's operations, not just from its outputs. The framework proves that its constants are produced without ever leaving a countable set, a structural fact about how its mathematics is organized. The theorem T_proper confirms that T is a proper subset of the reals: it is countable, while the real numbers are not.

What T_exp_closed does not claim is that the framework derives the numerical value of α⁻¹. The expression for α⁻¹ is an identification, not a derived coupling, and its exact value remains an open question. The theorem also does not claim that every real number can be reached by these operations, only that the specific constants the framework uses can be. Finally, it says nothing about whether the exponential closure property extends to any larger set; it is a statement about T alone.

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

/-- 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 numerical value of the inverse fine-structure constant is derived by the framework. Every real number can be reached by the field operations and exponential and logarithm functions. The exponential closure property extends to any set larger than T.

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: