IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCostOnField
The canonical J-cost sends the countable subfield T into itself, so cost values and the RS constants (phi, pi, alpha inverse) live in one field. Anyone tracking field-closure of the recognition cost cites these membership facts. Proofs are pure subfield arithmetic: J is built from addition, inversion, and the scalars 1 and 2 already in T.
claimLet $J(x)=\frac{x+x^{-1}}{2}-1$. If $T\subseteq\mathbb{R}$ is the countable subfield of the primitive recognition calculus, then $J(T)\subseteq T$. Iterates of $J$ and the images $J(\pi)$, $J(\varphi)$, $J(\alpha^{-1})$ likewise lie in $T$, so cost and the RS constants share one countable field.
background
In Recognition Science the unique cost functional forced by the Recognition Composition Law is $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), the T5 landmark. The Primitive Recognition Calculus builds a countable subfield $T\subseteq\mathbb{R}$ closed under addition, multiplication, inversion, and division, and containing $1$ and $2$ (imported from the exp/log field module).
Because Lean Subfield inversion is total ($0^{-1}=0$), evaluating $J$ on an element of $T$ never leaves $T$: the expression uses only field operations already available. No positivity or nonzero side condition is required. The module therefore records that $J$, its iterates, and the cost images of the standard RS constants all land back in $T$.
proof idea
Definition-level and short tactic proofs of field membership. Each lemma unfolds $J$ and applies subfield closure under $+$, scalar multiplication by $1/2$, and total inversion. Iterate membership is by induction on the iterate index. Constant membership ($\pi$, $\varphi$, $\alpha^{-1}$) reduces to the already-proved fact that those constants lie in $T$, then applies the base $J(T)\subseteq T$ fact. The summary theorem packages these into a single countable-field statement.
why it matters in Recognition Science
Closes the algebraic bookkeeping that the continuum forcing and completeness-independence developments import. Downstream, ForcedJOnCompletion needs $J$ to act on the completion of $T$ without leaving the ambient field language; PRCCompletenessIndependence needs cost and constants to share one countable carrier so completeness hypotheses can be stated uniformly. In the forcing chain this sits under T5 (J-uniqueness) and supports later continuum arguments that $J$ remains the unique cost after completion. Without $J(T)\subseteq T$, those modules would have to re-prove field closure ad hoc.
scope and limits
- Does not prove uniqueness of J; that is the separate T5 forcing result.
- Does not address positivity, minima, or the RCL functional equation on T.
- Does not construct T; it assumes the countable subfield from the exp/log module.
- Does not treat real-completion or continuity of J; those live downstream.
- Does not bound numerical values of J at phi, pi, or alpha inverse.