IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCostOnField
The canonical J-cost sends the countable subfield T into itself by pure field arithmetic. Recognition-calculus work cites this so cost values, their iterates, and the RS constants (phi, pi, alpha inverse) all live in one countable field. Closure needs no positivity or nonzero side conditions: subfield inversion is total.
claimThe cost $J(x)=\frac{x+x^{-1}}{2}-1$ maps the countable field $T$ into itself. Hence iterates $J^{\circ n}(x)$ and the constants $\pi$, $\varphi$, $\alpha^{-1}$ lie in $T$ when their inputs do, so cost and the Recognition constants share one countable field.
background
Primitive Recognition Calculus works inside a countable subfield $T\subseteq\mathbb{R}$ closed under addition, multiplication, inversion, and division, and containing $1$ and $2$. The companion module on the exp-log field supplies that $T$ and the ambient field operations used here.
The canonical cost is the T5 J-functional $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$ on positives). It is a field expression in $x$, $x^{-1}$, and the constants $1,2$. Because Mathlib subfield inversion is total ($0^{-1}=0$), membership proofs never need $x\neq 0$ or $x>0$.
The module therefore records that $J(T)\subseteq T$, that iterates stay in $T$, and that the standard RS constants ($\pi$, $\varphi$, $\alpha^{-1}$) already sit in $T$. The headline fact is that cost and those constants share one countable field.
proof idea
Definition-and-closure module, not a deep existence proof. Each membership lemma is a short calculation: expand $J$ (or an iterate) and invoke subfield closure under $+$, $\cdot$, ${}^{-1}$, and the presence of $1$ and $2$. Constant lemmas ($\pi$, $\varphi$, $\alpha^{-1}\in T$) cite the ambient field construction from the exp-log module. The summary statement packages those facts into a single countable-field claim.
why it matters in Recognition Science
Forced uniqueness of $J$ on the continuum completion (ForcedJOnCompletion) needs $J$ already well-defined and closed on the countable dense core $T$. Completeness-independence results (PRCCompletenessIndependence) likewise need cost and the RS constants to live in one countable field so analytic completion does not smuggle in new algebraic data.
In the forcing chain this sits under T5 (J-uniqueness) and supports later use of $\varphi$ (T6), the eight-tick structure, and the $\alpha^{-1}$ band, all evaluated inside the same $T$. Without this closure, continuum arguments would have to re-prove field membership at every step.
scope and limits
- Does not prove uniqueness of J; only that the canonical formula preserves T.
- Does not construct T; that comes from the exp-log field module.
- Does not address positivity, minima, or the Recognition Composition Law identities.
- Does not force continuum values of J beyond the countable subfield T.
- Does not derive numerical bounds on alpha inverse or mass-ladder rungs.