Foundation Primitive Recognition Calculus Prccost On Field Jcost Mem T

The countable carrier

The real numbers contain countable subfields: subsets that are themselves fields, closed under addition, multiplication, and division, yet small enough to be listed in an infinite sequence. The theorem jcost_mem_T concerns one such subfield, denoted T. It establishes that if a real number x lies in T, then the canonical cost function J(x) = (x + x⁻¹)/2 − 1 also lies in T. The proof is short: J is built from field operations, and T is closed under those operations. No positivity or nonzero hypothesis is needed, because the field's inversion is total, treating 0⁻¹ as 0.

The consequence is a closure property with a physical flavor. In Recognition Science, the cost function measures the forced expense of a recognition event, and the framework's constants, such as π and the golden ratio φ, are built from it. The theorem shows that iterating the cost function never escapes T: the entire forward orbit of any T-element under repeated application of J remains in T. A companion theorem, cost_and_constants_share_one_countable_field, strengthens this: there exists a single countable subfield of ℝ, strictly below the continuum, that is closed under field operations, exp, log, and the cost function, and contains π, φ, e, and α⁻¹. The cost function, the operations, and the constants all live in one countable carrier.

What this does not claim is equally precise. The theorem does not assert that T is unique, nor that it is the smallest such field. It does not claim that the cost function is defined only on T, or that the constants are somehow generated by J alone. The existence of the countable field is a structural fact, not a uniqueness result. The framework's larger claims, such as the forcing of physical constants, rest on additional theorems, not on this closure property alone. The theorem is a foundation stone: it shows the cost-and-constants loop runs on a countable field, without requiring the uncountable continuum.

/-- The canonical cost `Cost.Jcost x = (x + x⁻¹)/2 − 1` maps the countable field `T`
into itself: it is a field expression, and `T` is a subfield (closed under `+`, `⁻¹`,
`/`, `−`, and containing `1` and `2`). No positivity or nonzero hypothesis is needed,
because `Subfield` inversion is total (`0⁻¹ = 0`). -/
theorem jcost_mem_T {x : ℝ} (hx : x ∈ T) : Cost.Jcost x ∈ T := by
  have h2 : (2 : ℝ) ∈ T := by exact_mod_cast natCast_mem T 2
  unfold Cost.Jcost
  exact sub_mem (div_mem (add_mem hx (inv_mem hx)) h2) (one_mem _)

/-- **The cost dynamics stay countable.** The entire forward orbit of any
`T`-element under repeated application of the cost function remains in `T`. Iterating
recognition cost never escapes the countable field. -/
theorem jcost_iterate_mem_T {x : ℝ} (hx : x ∈ T) (n : ℕ) :
    (Cost.Jcost^[n] x) ∈ T := by
  induction n with
  | zero => simpa using hx
  | succ k ih =>
      rw [Function.iterate_succ_apply']
      exact jcost_mem_T ih

/-- **The unified headline (Items 1 + 3).** There is ONE countable subfield `T` of ℝ,
strictly below the continuum, that simultaneously
  * is closed under field operations, `exp`, and `log`;
  * is closed under the canonical recognition cost `Cost.Jcost`;
  * contains the seeds π and φ and the derived constants `e` and `α⁻¹`.
The cost function, the operations the constants are built from, and the constants
themselves therefore share a single countable carrier. "A single primitive for
physics runs on the countable field fed by the δ cost" is literally true: nowhere in
the cost-and-constants loop is the uncountable continuum required. -/
theorem cost_and_constants_share_one_countable_field :
    ∃ K : Subfield ℝ,
      (K : Set ℝ).Countable
        ∧ (∀ x ∈ K, Real.exp x ∈ K)
        ∧ (∀ x ∈ K, Real.log x ∈ K)
        ∧ (∀ x ∈ K, Cost.Jcost 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,
    fun _ hx => jcost_mem_T 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 prove that T is the unique countable subfield with these closure properties. The theorem does not claim that the cost function is defined only on T or that the constants are generated solely by J. The theorem does not by itself force the numerical values of the physical constants; that requires the broader forcing chain.

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/PRCCostOnField.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: