alphaLock_lt_one
plain-language theorem explainer
alphaLock_lt_one shows that the locked fine-structure constant α_lock = (1 - 1/φ)/2 is strictly less than one. Cosmologists and gravity modelers cite it when bounding dark-energy density and amplitude parameters. The proof is a short term reduction that unfolds the definition, invokes positivity of φ, and closes with linarith.
Claim. The locked fine-structure constant satisfies $α_{lock} < 1$, where $α_{lock} := (1 - φ^{-1})/2$.
background
Recognition Science fixes φ as the self-similar fixed point of the J-cost function J(x) = (x + x^{-1})/2 - 1. The constant α_lock is introduced as the canonical RS-native fine-structure coupling (1 - 1/φ)/2. Upstream lemmas supply φ > 1 and the explicit definition of α_lock. The module treats τ₀ = 1 tick as the fundamental RS time quantum.
proof idea
The term proof unfolds alphaLock, applies phi_pos to obtain 1/φ > 0 via one_div_pos, and finishes with linarith.
why it matters
It feeds fine_structure_derived, which states that α_lock has no free parameters and resolves C-001. Downstream uses appear in omega_lambda_pos for cosmology and in A_amplitude_bounds together with p_steepness_pos for gravity parameters. The lemma closes the algebraic step from the eight-tick octave to observable couplings inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.