alphaLock_pos
plain-language theorem explainer
The positivity of the locked fine-structure constant follows from its definition α_lock = (1 − 1/φ)/2 together with the inequality φ > 1. Cosmologists and gravity modelers cite the result to guarantee that derived quantities such as Ω_Λ remain positive. The proof is a one-line re-export of the lemma established in the parent Constants module.
Claim. $0 < α_lock$ where $α_lock = (1 - 1/φ)/2$.
background
In the Recognition Science framework the fine-structure constant is locked to the value α_lock = (1 − 1/φ)/2, which arises from the reciprocal symmetry of the J-cost function. The module FineStructureConstant re-exports basic properties of this constant to support derivations of cosmological and gravitational parameters. The upstream lemma in Constants establishes the same positivity statement by unfolding the definition and applying the fact that φ > 1 together with linarith.
proof idea
One-line wrapper that applies the lemma Constants.alphaLock_pos.
why it matters
This positivity statement is a prerequisite for the theorem fine_structure_derived that resolves registry item C-001 by showing α_lock has no free parameters. It is also invoked in proofs that Ω_Λ lies between zero and one and that the amplitude A satisfies 1 < A < 2. The result therefore anchors the entire chain from the phi-ladder to observable cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.