fine_structure_derived
plain-language theorem explainer
The theorem proves that the locked fine-structure constant satisfies positivity, lies strictly below one, and equals exactly (1 - 1/φ)/2 with no free parameters. Researchers deriving constants from the Recognition Science ledger cite it as the formal resolution of C-001. The proof is a one-line term that packages the positivity lemma, the upper-bound lemma, and reflexivity on the defining expression.
Claim. 0 < α_lock ∧ α_lock < 1 ∧ α_lock = (1 - 1/φ)/2, where α_lock is the canonical locked fine-structure constant in RS-native units.
background
The module derives the fine-structure constant from φ under the Recognition Science ledger. The definition α_lock := (1 - 1/φ)/2 follows directly from the reciprocal symmetry J(x) = J(1/x) of the J-cost function. Upstream results supply α_lock > 0 and α_lock < 1 by elementary comparison with φ > 1; these are re-exported inside the module. The setting is the abstract Constants bundle that collects the fundamental RS parameters Knet, Cproj, Ceng, Cdisp.
proof idea
The proof is a term-mode construction that supplies the three conjuncts of the goal. It applies the positivity lemma alphaLock_pos, the strict inequality lemma alphaLock_lt_one, and reflexivity to match the explicit formula (1 - 1/φ)/2.
why it matters
This theorem resolves registry item C-001 by exhibiting the unique coupling compatible with reciprocal symmetry and self-similar closure. It supplies the RS-native value that converts to the observed α ≈ 1/137 via λ_rec calibration. The result anchors the fine-structure constant inside the phi-forcing chain and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.