alphaLock_lt_one
plain-language theorem explainer
The theorem establishes that the RS-locked fine-structure constant α_lock is strictly less than one. Researchers deriving the fine structure constant from the Recognition Science ledger would cite it to confirm the coupling lies inside the open unit interval. The proof is a one-line re-export of the algebraic lemma from the base Constants module.
Claim. Let $α_{lock} := (1 - φ^{-1})/2$. Then $α_{lock} < 1$.
background
In the Recognition Science framework the fine structure constant is locked by the reciprocal symmetry of the J-cost function, J(x) = (x + x^{-1})/2 - 1. The module derives α_lock = (1 − 1/φ)/2 directly from the ledger's self-similar closure under J(x) = J(1/x), with φ the self-similar fixed point forced at T6. This theorem re-exports the strict inequality α_lock < 1 from the parent Constants module, where it follows from the positivity of φ.
proof idea
The proof is a one-line wrapper that applies the lemma alphaLock_lt_one from IndisputableMonolith.Constants. It unfolds the definition of alphaLock and uses linarith after establishing positivity of 1/φ via phi_pos.
why it matters
This bound is required by the parent theorem fine_structure_derived, which resolves C-001 by showing α_lock = (1 − 1/φ)/2 with no free parameters. It is also used to establish positivity of Ω_Λ in EarlyUniverse and to bound the amplitude A and steepness p in GravityParameters. The result sits inside the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain, confirming that the derived coupling lies inside the unit interval as required by the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.