alpha_inv_derived
plain-language theorem explainer
RS pins the inverse fine-structure constant at the numerical prediction 137.035999, obtained from the cost structure via 8π²/(φ·ln(φ²)) times a holographic correction. Anyone assembling dimensionless RS observables or checking CODATA compatibility cites this constant. The declaration is a bare real assignment, not a proved closed form.
Claim. The RS-derived inverse fine-structure constant is the real number $\alpha^{-1}_{\mathrm{RS}} := 137.035999$, predicted from the cost structure by $8\pi^2/(\varphi\cdot\ln(\varphi^2))$ with a holographic correction, and not fitted to CODATA.
background
The Observables module separates a cost-first core from an external-anchor seam. Core predictions are dimensionless numbers built from the golden ratio $\varphi$ and the Recognition cost $J$; empirical bounds import CODATA only at the comparison layer.
Among the tracked observables is $\alpha^{-1}$, the inverse fine-structure constant. In RS-native units the primer places $\alpha^{-1}$ in the band $(137.030, 137.039)$. The doc-comment states the intended derivation route: $8\pi^2/(\varphi\cdot\ln(\varphi^2))$ multiplied by a holographic correction, forced from the cost structure rather than calibrated.
Upstream rung and species data (electron, muon ladder positions) support sibling mass-ratio predictions; this constant is independent of those rungs and sits purely on the electromagnetic cost side of the exclusivity interface.
proof idea
There is no proof. The declaration is a noncomputable real definition that assigns the literal decimal $137.035999$. The mathematical content claimed in the doc-comment (the $8\pi^2/(\varphi\ln(\varphi^2))$ formula plus holographic factor) is not expanded or proved here; only the resulting numeral is stored for downstream packaging.
why it matters
This value is the $\alpha^{-1}$ field of rsObservables, the bundle of RS-predicted dimensionless observables derived from $\varphi$ via the cost structure. That bundle is the left-hand side of rs_within_bounds, which asserts that RS predictions lie inside CODATA 2022 intervals (an external-anchor theorem).
In the exclusivity track, a framework must emit concrete numbers comparable to measurement; hard-wiring the RS $\alpha^{-1}$ prediction is the first such emission. It sits inside the primer band $(137.030, 137.039)$ and is explicitly marked as a prediction, not a fit. Closing a fully expanded Lean derivation of the $8\pi^2/(\varphi\ln(\varphi^2))$ expression would replace this numeral with a proved term; until then the constant is the calibration-free stub the bounds theorem consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.