rsField_mem_alphaInv
plain-language theorem explainer
The RS inverse fine-structure constant α⁻¹ lies in the minimal constant field, the subfield of ℝ generated by {φ, π, e, α⁻¹}. Cite this for the countable-carrier claim and for FRS evaluation soundness. Proof is a one-line closure membership: α⁻¹ is one of the four named generators.
Claim. The Recognition-Science inverse fine-structure constant $\alpha^{-1} = 44\pi\,\exp\bigl(-w_8\ln\varphi/(44\pi)\bigr)$ belongs to the subfield of $\mathbb{R}$ generated by $\{\varphi,\,\pi,\,e,\,\alpha^{-1}\}$.
background
In the Primitive Recognition Calculus minimal-field module, the named RS constants are collected as the finite set ${\varphi,,\pi,,e,,\alpha^{-1}}$. The minimal field carrying RS physics is the subfield of $\mathbb{R}$ obtained by closing that set under field operations; it automatically contains $\mathbb{Q}$ as the prime field.
The local $\alpha^{-1}$ is the explicit transcendental $44\pi,\exp(-w_8\ln\varphi/(44\pi))$, matching the framework's dimensionless inverse fine-structure construction (canonical exponential resummation, value near $137.04$). Upstream, the global Constants.Alpha form is the same assembled expression with seed $4\pi\cdot 11$; the exact IR boundary $\alpha^{-1}(0)=137.035999$ remains open.
The module's thesis is that RS physics lives in this countable subfield, not in the full continuum.
proof idea
One-line term proof. Apply Subfield.subset_closure: every element of a generating set sits in the subfield it generates. Unfold the constants set and simp to discharge the membership goal, since $\alpha^{-1}$ is literally one of the four generators.
why it matters
Closes one conjunct of the Item-1 headline rs_physics_below_continuum: every named RS constant lives in one countable proper subfield of $\mathbb{R}$, so the continuum is not required as the home of the constants. Downstream FRS carrier soundness (eval_mem) uses the sibling memberships for $\varphi$, $\pi$, and $e$; this lemma is the matching fact for $\alpha^{-1}$, keeping every finite-description carrier term inside the countable field.
In the broader framework this pins the alpha band (primer: $\alpha^{-1}$ inside $(137.030,,137.039)$) to the same countable carrier as $\varphi$ (T6 fixed point) and the other named constants. It does not settle the open IR boundary condition on $\alpha^{-1}(0)$; it only places the assembled RS expression inside the minimal field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.