alpha_inv_CODATA_pos
plain-language theorem explainer
The lemma establishes that the CODATA inverse fine-structure constant anchor is strictly positive. Any comparison of Recognition Science predictions against experimental data would cite it to confirm the anchor lies in the positive reals. The proof reduces the inequality to a direct numerical check via the norm_num tactic on the explicit decimal definition.
Claim. $0 < 137.035999177$
background
This lemma resides in the ExternalAnchors module, the single quarantined location for all empirical calibration data entering Recognition Science. The module documentation requires that the cost-first core never import it, creating a mechanical separation between pure RCL derivations and external CODATA values tagged with the external_anchor attribute.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to the definition of alpha_inv_CODATA. The constant is supplied explicitly as the positive decimal 137.035999177, so the tactic discharges the strict inequality without additional lemmas.
why it matters
The result secures the sign of the inverse fine-structure constant anchor used for calibration against experiment. It supports the alpha band (137.030, 137.039) referenced in the Recognition Science framework by confirming the CODATA value lies above zero. No downstream theorems depend on it directly, but it forms part of the external interface enabling quantitative checks against the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.