alphaInv_is_term
plain-language theorem explainer
Evaluating the inverse fine-structure constant atom of the F_RS carrier syntax recovers the Recognition Science α⁻¹ value in the minimal field. Anyone assembling the Phase 3 carrier soundness package cites this identity. The proof is pure definitional reflexivity: the evaluator is defined to send that constructor to the named minimal-field constant.
Claim. Evaluating the inverse fine-structure constant constructor of the $F_{RS}$ carrier syntax yields the Recognition Science value $\alpha^{-1}$ in the minimal field: $\mathrm{eval}(\alpha^{-1}_{\mathrm{syn}}) = \alpha^{-1}_{\mathrm{RS}}$.
background
The module constructs an explicit finite-description carrier for Recognition Science constants. The carrier syntax is an inductive type of finite terms over the rationals and a fixed inventory (φ, π, e, α⁻¹), closed under negation, addition, multiplication, and inversion. Evaluation is the recursive map from those trees into ℝ.
The minimal-field α⁻¹ is the named RS transcendental
$\alpha^{-1} = 44\pi,\exp(-w_8\ln\varphi/(44\pi))$. A sibling constant in Constants.Alpha is a related exponential resummation (~137.04) whose exact infrared value is flagged OPEN; the carrier identity uses the PRC minimal-field form, not that assembly.
Local goal: pin each inventory atom so the Phase 3 headline can assert that every term lands in the countable RS field and that the named constants evaluate correctly.
proof idea
One-line term proof by rfl. The evaluator is defined by structural recursion on the carrier syntax so that the α⁻¹ constructor is sent exactly to the minimal-field constant; the equality is definitional and needs no lemmas.
why it matters
Feeds the Phase 3 headline frs_carrier, which packages: every term evaluates into the countable field rsField; the inventory identities for φ, π, e, and α⁻¹; countability and proper-subset status of term values; and protocol display in the ℝδ interface. Downstream doc: "The carrier the framework actually computes on is finite generation over a fixed inventory, not the uncountable continuum."
Places α⁻¹ inside the RS constant inventory that the forcing chain and mass ladder later consume. Touches the framework alpha band (α⁻¹ inside (137.030, 137.039)) only by naming the constant; the open exact IR boundary condition on the assembled Constants.Alpha form remains upstream and untouched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.