alphaLock_numerical_bounds
plain-language theorem explainer
The locked fine-structure constant α_lock = (1 − 1/φ)/2 satisfies 0.18 < α_lock < 0.21 when φ lies in (1.61, 1.62). Researchers deriving coupling constants from the Recognition Science ledger would cite this bound to confirm the numerical range of the parameter-free coupling. The proof unfolds the definition, invokes the two phi bounds, derives the reciprocal inequalities via division properties, and closes both sides with linear arithmetic.
Claim. $0.18 < α_{lock} < 0.21$, where $α_{lock} = (1 - φ^{-1})/2$ and $φ$ satisfies $1.61 < φ < 1.62$.
background
In the FineStructureConstant module the RS derivation of the fine-structure constant is formalized as α_lock = (1 − 1/φ)/2. This expression follows directly from the reciprocal symmetry J(x) = J(1/x) of the ledger and the self-similar fixed point φ forced by the J-uniqueness condition T5. The module records the conversion to the observed α ≈ 1/137 as a separate ledger-to-lab calibration step.
proof idea
The tactic proof first unfolds alphaLock. It then applies phi_gt_onePointSixOne to obtain 1/φ < 1/1.61 via div_lt_div_iff_of_pos_left and closes the lower bound with linarith. The symmetric upper bound is obtained from phi_lt_onePointSixTwo by showing 1/1.62 < 1/φ and again applying linarith.
why it matters
This supplies the coarse numerical interval for the RS-native coupling α_lock, directly discharging the C-001 resolution that the constant is determined by φ with no free parameters. It anchors the fine-structure derivation inside the forcing chain (T5–T8) and the reciprocal symmetry of the ledger. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.