jcost_mem_T
plain-language theorem explainer
The canonical recognition cost J(x)=(x+1/x)/2−1 maps the countable exp/log-closed subfield T⊆ℝ into itself. Cited by anyone proving cost-closure of T, completeness independence from cost axioms, or the single countable carrier for cost and constants. Proof is a short subfield-closure chase: T contains 2 and is closed under +, inversion, division, and subtraction of 1.
Claim. If $x$ belongs to the countable exp/log-closed subfield $T \subseteq \mathbb{R}$, then the recognition cost $J(x) = (x + x^{-1})/2 - 1$ also belongs to $T$. No positivity or nonzero hypothesis on $x$ is required.
background
In the Primitive Recognition Calculus, $T$ is the exp/log-closed RS field: the directed union $T = \bigsqcup_n S_n$ realized as a Subfield of $\mathbb{R}$. It is countable, closed under field operations, and (by construction of the chain) under real exp and log.
The canonical cost is $J(x) = (x + x^{-1})/2 - 1$, the unique continuous solution forced by the Recognition Composition Law and normalization (forcing-chain step T5). The same formula appears as the RS recognition cost of a positive ratio and as the cost of a recognition event.
This module records that cost dynamics never leave $T$. Because $T$ is already a subfield, every field expression built from elements of $T$ lands back in $T$; the theorem is the instance for $J$.
proof idea
Tactic proof, four closure steps. First obtain $2 \in T$ by casting the natural number $2$ into the subfield (natCast_mem). Unfold $J$ to $(x + x^{-1})/2 - 1$. Apply subfield lemmas in order: $x^{-1} \in T$ by inv_mem, $x + x^{-1} \in T$ by add_mem, the quotient by $2$ by div_mem, and finally subtract $1$ by sub_mem with one_mem. Inversion is total on a Subfield ($0^{-1}=0$), so no nonzero side condition appears.
why it matters
This is the basic cost-closure fact for $T$. Downstream it discharges the $J$-closure conjunct in the unified headline that one countable subfield carries field operations, exp/log, $J$, and the seeds $\pi$, $\varphi$, $e$, $\alpha^{-1}$. Sibling corollaries apply it at $\varphi$ and $\alpha^{-1}$, and the iterate lemma uses it to keep the entire forward $J$-orbit inside $T$.
It is the first conjunct of both completeness-independence theorems: $T$ is $J$-closed and countable yet fails the LUB property, while $\mathbb{R}$ is $J$-closed and complete, so order-completeness is not entailed by cost/field axioms (nor by the genuine cost laws $J(1)=0$, reciprocity, nonnegativity). That separation keeps the continuous completion an independent commitment rather than a $\delta$-consequence.
On the continuum side it supports the capstone forcing of $J$ on the completion and the open one-point-calibration target. Framework landmark: T5 $J$-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.