alpha_inv_lock
plain-language theorem explainer
Fixes a single real constant α^{-1}_lock = 137.035999 used as the target inverse fine-structure value in the (deprecated) DerivesObservables interface. Anyone reading exclusivity certificates that still mention derives_alpha will hit this lock. The body is a bare numeric assignment; no proof.
Claim. Define the locked inverse fine-structure constant $\alpha^{-1}_{\mathrm{lock}} := 137.035999 \in \mathbb{R}$.
background
The module supplies shared PhysicsFramework scaffolding for NoAlternatives and necessity arguments, keeping core definitions free of circular imports.
In Recognition Science the inverse fine-structure constant is predicted to lie in a narrow band near the CODATA value (primer band roughly $(137.030, 137.039)$). The exclusivity layer needs a concrete real to compare against when stating that a framework "derives $\alpha$".
alpha_inv_lock is that fixed real. The sibling structure DerivesObservables uses it in the field derives_alpha, which asserts $137.035 \le \alpha^{-1}_{\mathrm{lock}} \le 137.037$. That structure is explicitly deprecated in favor of DerivesObservablesStrong, which demands predictions inside empirical bounds rather than a tautological lock.
proof idea
No proof. One-line noncomputable definition equating the identifier to the literal real 137.035999.
why it matters
Exists only so the deprecated DerivesObservables structure can write a closed inequality about $\alpha^{-1}$ without hard-coding the numeral in every field. Downstream, DerivesObservables.derives_alpha is the sole consumer.
In the broader RS picture the interesting claim is the forced $\alpha^{-1}$ band from the forcing chain and RCL, not this lock. The module doc and the deprecation note both push new work toward DerivesObservablesStrong in Observables.lean, where a PredictionFunction must land inside empirical bounds. Keeping the constant preserves backward compatibility with existing certificates that still mention the old interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.