Foundation Primitive Recognition Calculus Prcexp Log Field Gens Finite

The finite seed set

The declaration gens_finite establishes a simple but foundational fact: the set of generators for the Recognition Science framework is finite, containing exactly two real numbers, π and the golden ratio φ. This is a theorem in the framework's machine-checked library of formal theorems. The proof is direct: it unfolds the definition of the generator set and applies the standard fact that a set with two elements is finite.

This matters because the framework builds all of its constants from these two seeds. The theorem states that the starting set, called gens, is precisely {π, φ}. Rational numbers, it notes, come for free as the prime field of any subfield, meaning they do not need to be added as separate generators. The framework then applies field operations, exponentiation, and logarithms to this seed set to reach every constant it uses.

In Recognition Science, this finite seed set is the first step in a construction that produces a countable field T. The framework proves that T contains π, φ, Euler's number e, and the inverse fine-structure constant α⁻¹, all built from the two seeds. The key point is that all these operations happen inside T, a countable set, not the uncountable real line. The continuum is removed from the framework's operations, not just its outputs.

What gens_finite does not claim is that the framework's constants are limited to these two numbers. It only establishes the starting point. The theorem does not say that the framework can generate all real numbers, nor does it assert that π and φ are the only constants the framework will ever use. It is a statement about the initial seed set, not about the full scope of the framework's reach.

theorem gens_finite : gens.Finite := by
  unfold gens
  exact (Set.finite_singleton _).insert _

/-- The generators of the exp/log closure: π and φ. Rationals come for free as the
prime field of any subfield, so these two transcendental/algebraic seeds plus the
field and exp/log operations reach every RS constant. -/
noncomputable def gens : Set ℝ := {Real.pi, Real.goldenRatio}

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 countable: a countable union of countable stages. -/
theorem T_countable : (T : Set ℝ).Countable := by
  rw [T_coe]
  exact Set.countable_iUnion S_countable

What this page does not claim

The framework's constants are limited to π and φ. The framework can generate all real numbers. π and φ are the only constants the framework will ever use.

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: