alphaLock_pos
plain-language theorem explainer
alphaLock_pos establishes that the locked fine-structure constant exceeds zero. Cosmologists and particle physicists working in the Recognition Science framework cite it when confirming positivity of derived quantities such as dark-energy density. The proof is a short algebraic reduction that unfolds the definition, invokes one_lt_phi, and applies real-number inequalities.
Claim. $0 < (1 - 1/phi)/2$ where $phi > 1$ is the golden ratio.
background
The Constants module introduces the locked fine-structure constant as alphaLock = (1 - 1/phi)/2. This expression follows from the reciprocal symmetry of the Recognition ledger and the self-similar fixed point phi. The supporting lemma one_lt_phi states that 1 < phi and is imported from PhiSupport.
proof idea
The proof obtains one_lt_phi, unfolds alphaLock, applies div_lt_one to deduce 1/phi < 1, and concludes with linarith.
why it matters
It is invoked by alphaLock_in_unit_interval and fine_structure_derived to place the coupling in (0,1) with no free parameters. It also feeds omega_lambda_pos, omega_lambda_lt_one, and gravitational bounds such as A_amplitude_bounds. The result anchors the phi-determined fine-structure constant in the framework, consistent with the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.