alphaLock_pos
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 in Recognition Science
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.
scope and limits
- Does not establish the conversion factor between RS-native α_lock and the laboratory value ≈ 1/137.
- Does not derive the numerical bounds 0.18 < α_lock < 0.21.
- Does not address higher-order corrections from the ledger-to-lab map.
formal statement (Lean)
30theorem alphaLock_pos : 0 < alphaLock := Constants.alphaLock_pos
proof body
Term-mode proof.
31
32/-- α_lock < 1 (re-export from Constants). -/