alphaInv_pos
plain-language theorem explainer
The RS construction value of the inverse fine-structure constant is strictly positive. Anyone proving κ_γ-scaling, monotonicity, or Hartree/Rydberg dimensionless ratios cites this as the base positivity fact. The proof is a two-step strict inequality: 0 is less than a fixed numeric lower bound, which is less than the construction value.
Claim. The RS construction value $\alpha^{-1}$ (the dimensionless inverse fine-structure constant assembled from the seed and gap exponential, without CODATA fit) satisfies $0 < \alpha^{-1}$.
background
In Recognition Science the inverse fine-structure constant is assembled as a construction value, not fit to CODATA: $\alpha^{-1} = \alpha_{\mathrm{seed}},\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$, with seed $4\pi\cdot 11$. The exact infrared value $\alpha^{-1}(0)\approx 137.035999$ remains a boundary condition; the construction sits near $137.04$ inside the RS alpha band $(137.030, 137.039)$.
This module studies the $\kappa_\gamma$-scaling test: insert a free positive U(1) kinetic normalization so that the scaled inverse coupling is $\kappa\cdot\alpha^{-1}$. Forced free-energy closure on the 3-cube $Q_3$ (octahedral face-adjacency Laplacian, $\det'M=2304$) does not pin $\kappa_\gamma$, so $\alpha^{-1}$ stays a boundary datum parallel to a renormalization-scheme input, unlike $\hbar=\varphi^{-5}$.
Positivity of the unscaled construction value is the elementary inequality every later scaling and scorecard argument needs. It uses only a numeric lower bound on the construction, not as a derivation input.
proof idea
Term-mode chain of two strict inequalities via lt_trans. The left leg is norm_num, establishing $0$ is less than a fixed positive rational lower bound. The right leg is the existing numeric certificate Numerics.alphaInv_gt, which places that lower bound strictly below Constants.alphaInv. No algebraic expansion of the exponential construction is required.
why it matters
Base positivity for the entire $\kappa_\gamma$-irreducibility package. Downstream, alphaInvK_pos multiplies by $\kappa>0$; alphaInvK_strictMono uses it as the positive right factor in mul_lt_mul_of_pos_right; and the load-bearing irreducibility theorem alphaInv_irreducible_under_closure divides by $\alpha^{-1}$ to hit any positive target $t$ while keeping forced closure. That theorem states the forced-closure facts hold for every $\kappa_\gamma>0$ while scaled $\alpha^{-1}$ sweeps all positives, so closure does not pin the inverse coupling.
The same fact feeds Hartree/Rydberg scorecard identities (row_hartree_over_rest_eq and its lower/upper bounds), where field simplification and reciprocal inequalities need $\alpha^{-1}\neq 0$. In the broader RS constants story this keeps $\alpha^{-1}$ honest as a free U(1) normalization rather than a derived constant like $\hbar=\varphi^{-5}$ from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.