pith. machine review for the scientific record. sign in
def definition def or abbrev high

alphaLock

show as:
view Lean formalization →

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.

claimDefine 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 in Recognition Science

α_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.

scope and limits

formal statement (Lean)

 219@[simp] noncomputable def alphaLock : ℝ := (1 - 1 / phi) / 2

proof body

Definition body.

 220
 221/-- Useful bridge identity: the “acceleration-parameterized” exponent is `2·alphaLock`.
 222
 223This is purely algebraic (no physics): it just clears the `/2` in the definition. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.