alphaInv_mem_T
plain-language theorem explainer
The inverse fine-structure constant α⁻¹, written as 44·π·exp(−w₈·ln φ/(44·π)), lies in the countable exp/log-closed subfield T of ℝ. Anyone assembling the RS constants-below-continuum claim cites this. The proof threads field operations, one log, and one exp through the closure lemmas for T, starting from the seeds π and φ.
Claim. The RS inverse fine-structure constant $\alpha^{-1} = 44\,\pi\,\exp\bigl(-w_8\,\ln\varphi/(44\,\pi)\bigr)$ belongs to the countable subfield $T\subseteq\mathbb{R}$ obtained as the directed union of the exp/log-closure chain.
background
In this module, $T$ is the exp/log-closed Recognition Science field: the directed union $T=\bigsqcup_n S_n$ of a countable chain of subfields of $\mathbb{R}$. By construction $T$ is a subfield, and the companion lemmas establish that it is closed under $\exp$ and $\log$. The seeds $\pi$ and the golden ratio $\varphi$ sit in $T$ at stage zero of the chain.
The constant in view is the MinimalField form of $\alpha^{-1}$, namely $44\cdot\pi\cdot\exp(-w_8\ln\varphi/(44\pi))$, with $w_8=4$. Upstream, the Constants.Alpha package records the same exponential-resummation shape (seed times $\exp$ of a gap over the seed) and notes that the precise infrared CODATA match remains an open boundary condition; here the only claim is membership of that algebraic expression in $T$.
The local setting is Primitive Recognition Calculus: show that every operation used to build the RS constants stays inside one countable carrier strictly below the continuum.
proof idea
Tactic proof by stepwise membership. First import $\pi\in T$ and $\varphi\in T$ from the seed lemmas, and cast $44$ and $w_8=4$ into $T$ via natural-number membership. Apply log-closure to get $\ln\varphi\in T$. Build the argument $-w_8\ln\varphi/(44\pi)$ by field operations (negation, multiplication, division), all of which preserve $T$. Exp-closure puts the exponential of that argument in $T$. Unfold the MinimalField definition of $\alpha^{-1}$ and finish by multiplying $44\cdot\pi$ by the exponential, again inside $T$.
why it matters
This is the payoff step for $\alpha^{-1}$ inside the exp/log field: every field operation, the single log, and the single exp in the formula land in $T$, so the constant is produced without leaving the countable carrier. Downstream it feeds rs_operations_below_continuum (Item 1: one countable subfield closed under the RS operations and containing $\pi$, $\varphi$, $e$, and $\alpha^{-1}$), the cost-side lemma that $J(\alpha^{-1})\in T$, and the unified headline that cost and constants share one countable field.
In the broader framework this places the RS $\alpha^{-1}$ band construction on the same countable workspace as the forcing-chain constants ($\varphi$ from T6, the eight-tick structure behind $w_8$). It does not settle the OPEN infrared boundary condition against CODATA; it only certifies that the expression lives in $T$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.