jcost_alphaInv_mem_T
plain-language theorem explainer
The recognition cost J of the inverse fine-structure constant lies in the countable carrier field T. Cite this when assembling the unified cost-and-constants headline: one countable subfield holds the seeds, the derived constants, and all J-images. Proof is a one-line application of J-closure of T to membership of α⁻¹ in T.
Claim. If $T\subseteq\mathbb{R}$ is the countable subfield of the primitive recognition calculus (closed under field operations, $\exp$, $\log$, and $J$), and $\alpha^{-1}$ denotes the canonical RS inverse fine-structure constant, then $J(\alpha^{-1})\in T$, where $J(x)=(x+x^{-1})/2-1$.
background
In the Primitive Recognition Calculus cost-on-field module, one builds a single countable subfield $T\subset\mathbb{R}$, strictly below the continuum, meant to carry every constant and every cost evaluation that the recognition loop needs. The recognition cost is the standard RS functional $J(x)=(x+x^{-1})/2-1$ (also written $\cosh(\log x)-1$), forced uniquely at T5 of the unified forcing chain and obeying the Recognition Composition Law.
The inverse fine-structure constant here is the dimensionless RS expression $\alpha^{-1}=\alpha_{\mathrm{seed}},e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ (seed $4\pi\cdot 11$), assembled without CODATA fit; its numerical band sits near $137.04$, with the exact IR value left as an open boundary condition. Sibling lemmas already place $\pi$, $\varphi$, and $\alpha^{-1}$ themselves in $T$, and establish that $T$ is closed under $J$.
proof idea
One-line term proof. Apply the general closure lemma that $J$ sends $T$ into itself, to the prior membership fact that the canonical $\alpha^{-1}$ already lies in $T$. No further arithmetic or analytic work is done at this site.
why it matters
This is one of the constant-specific legs under the unified headline that a single countable carrier holds the cost function, the field operations, and the physical seeds together: closed under $+,-,\cdot,/,\exp,\log,J$, and containing $\pi$, $\varphi$, $e$, and $\alpha^{-1}$. Without $J(\alpha^{-1})\in T$, the cost-and-constants loop would still appear to need a continuum point outside $T$.
In framework terms it ties the T5 $J$-uniqueness landmark to the RS $\alpha$ construction (the $\alpha^{-1}$ band near $137.03$–$137.04$). Downstream it supports the module's headline theorem that cost and constants share one countable field; the present declaration has no further external uses listed. The exact IR value $\alpha^{-1}(0)=137.035999$ remains an open boundary condition, not discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.