Foundation Primitive Recognition Calculus Prcexp Log Field T Countable

A countable home for constants

In the Recognition Science framework, the ledger (a discrete record of events) builds its constants from a few seeds using only the ordinary operations of arithmetic, exponentiation, and logarithms. The declaration T_countable proves that all of those constants live inside a single countable subfield of the real numbers. Countable means the set can be matched one-to-one with the natural numbers 1, 2, 3, and so on, even though the full real line cannot be so matched. The framework's entire workspace, for the constants it derives, is therefore no larger than the integers in size.

The construction starts with two seeds: the number π and the golden ratio φ. From those, the framework builds a chain of fields. At each stage it adds the exponentials and logarithms of every number already present, then closes under addition, subtraction, multiplication, and division. The union of all these stages is the field called T. The theorem T_countable shows this union is countable, because it is a countable union of countable stages. The same proof shows T is a proper subset of the reals: it is not the whole continuum. The framework's operations happen inside T, not across the entire real line.

The theorem also establishes that T is closed under exponentiation and logarithms, and that it contains π, φ, Euler's number e, and the framework's expression for the inverse fine-structure constant. The machine-checked library of formal theorems records this as a single result: there exists a countable subfield of the reals that is closed under exactly the operations the framework's constants use, contains the seeds, and is not the whole real line. The continuum is removed from the framework's operations, not just from its outputs.

What T_countable does not claim is more modest than it might seem. It does not say that every real number is reachable, nor that the framework can construct all of mathematics inside a countable set. It does not assert that the framework's expression for the inverse fine-structure constant equals the measured physical value; that comparison is a separate empirical check. The theorem is a structural fact about where the framework's constants live, not a claim about which constants exist or what they are worth.

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

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

What this page does not claim

The theorem does not claim every real number is reachable inside T. The theorem does not assert the framework can construct all of mathematics within a countable set. The theorem does not claim the framework's expression for the inverse fine-structure constant equals the measured physical 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: