alphaLock
plain-language theorem explainer
The definition sets the locked fine-structure constant to α_lock = (1 − 1/φ)/2 with φ the golden-ratio fixed point. Researchers tracing the electromagnetic coupling from the J-cost equation cite this expression when bounding α inside the Recognition framework. The construction is a direct algebraic abbreviation that downstream lemmas unfold and simplify by ring arithmetic.
Claim. Define the locked fine-structure constant by $α_{lock} := (1 - 1/φ)/2$, where $φ > 1$ is the unique positive solution of $φ = 1 + 1/φ$.
background
Recognition Science obtains φ as the self-similar fixed point forced by J-uniqueness (T5) and the Recognition Composition Law. The Constants module works in RS-native units with the fundamental time quantum fixed at one tick. Upstream identities such as the zero-cost identity event and the various bridge structures supply the algebraic environment in which derived constants like α_lock are expressed without new axioms.
proof idea
The declaration is a direct noncomputable definition of the algebraic expression (1 − 1/φ)/2. No lemmas or tactics appear inside the definition body itself. Downstream results such as two_mul_alphaLock simply unfold the abbreviation and apply ring_nf to obtain the cleared form 1 − 1/φ.
why it matters
α_lock supplies the base expression that feeds the FineStructureConstant package, including the theorems establishing 0 < α_lock < 1 and the coarse numerical interval (0.18, 0.21). It participates in the chain that ultimately targets the observed α^{-1} band (137.030, 137.039) by linking the coupling strength to the phi-ladder and the eight-tick octave. The definition remains purely algebraic and leaves open the step that would identify α_lock with the physical fine-structure constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Golden-ratio exponent fixes a gravity kernel, then meets 147 galaxies
"α = ½(1 − φ⁻¹) ≈ 0.191 (Eq. 14)"