alphaLock_structure
plain-language theorem explainer
Packages the three structural facts about the ILG kernel exponent α_lock: it is positive, strictly less than one, and equals (1 − 1/φ)/2 by definition. Anyone citing the φ-native form of the information-limited-gravity kernel uses this bundle. The proof is a one-line product of the two bound lemmas with definitional reflexivity.
Claim. Let $\varphi$ be the golden ratio and set $\alpha_{\mathrm{lock}} := (1 - 1/\varphi)/2$. Then $0 < \alpha_{\mathrm{lock}} < 1$ and the equality $\alpha_{\mathrm{lock}} = (1 - 1/\varphi)/2$ holds.
background
In this module, $\alpha_{\mathrm{lock}} = (1 - 1/\varphi)/2 \approx 0.19$ is the information-limited-gravity (ILG) kernel exponent. Despite the historical module name, it is not the electromagnetic fine-structure constant $\alpha \approx 1/137$; the module header retracts any claim that it resolves the EM $\alpha$ problem.
The constant is defined in Constants by clearing halves of a $\varphi$-expression: $\alpha_{\mathrm{lock}} := (1 - 1/\varphi)/2$, with $\varphi$ the unique positive root of $x^2 = x + 1$ forced by the Recognition self-similarity fixed-point step (T6). Upstream lemmas already show $0 < \alpha_{\mathrm{lock}}$ from $1 < \varphi$, and $\alpha_{\mathrm{lock}} < 1$ from $1/\varphi > 0$.
The local setting is purely algebraic bookkeeping of that kernel exponent inside the RS constants layer, not a derivation of laboratory $\alpha$.
proof idea
Term-mode constructor packing three facts: positivity from the re-exported alphaLock_pos (itself linarith after unfolding and $1/\varphi < 1$), the upper bound from the re-exported alphaLock_lt_one (same style, using $1/\varphi > 0$), and rfl for the definitional equality $\alpha_{\mathrm{lock}} = (1 - 1/\varphi)/2$. No new arithmetic is performed here.
why it matters
Gives a single citation point for the full structural package of the ILG kernel exponent: unit-interval membership plus the exact $\varphi$-formula. Downstream code that needs all three conjuncts at once can import this rather than the separate bound lemmas.
In the broader Recognition framework this sits in the constants layer fed by $\varphi$-forcing (T6), not in the EM fine-structure story. The module header is explicit that the honest EM-$\alpha$ position lives in Constants.AlphaGenesis (free boundary datum under KappaGammaIrreducibility, first-order construction excluded by MeasurementVerdict). No used-by edges are recorded yet; the declaration is a local structural anchor and a deprecation target for the old name fine_structure_derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.