alphaLock_lt
plain-language theorem explainer
The locked ILG exponent α_lock = (1 − 1/φ)/2 is strictly less than 0.192. Anyone validating the a priori α prediction against SPARC (0.19 ± 0.02) cites this upper bound. The proof unfolds the definition, applies the sibling lower bound 1/φ > 0.617, and finishes by elementary real arithmetic.
Claim. The locked fine-structure exponent $\alpha_{\mathrm{lock}} = (1 - 1/\varphi)/2$ satisfies $\alpha_{\mathrm{lock}} < 0.192$, where $\varphi$ is the golden ratio.
background
This module certifies that the ILG fractional exponent α is an a priori prediction from self-similarity, not a post-hoc SPARC fit. The paper had treated (A, α, r₀) as free parameters; here the chain RCL → unique J-cost → φ-forced self-similarity → memory kernel forces α = (1 − 1/φ)/2 ≈ 0.191 and C = φ⁻² ≈ 0.382.
The constant alphaLock is defined as (1 − 1/φ)/2. The sibling lemma one_div_phi_gt supplies 1/φ > 0.617 from the elementary bound φ < 1.62. Together with a matching lower bound elsewhere in the file, these pin α_lock inside (0.189, 0.192), tight enough for a 1σ comparison to the SPARC best-fit 0.19 ± 0.02.
proof idea
Unfold alphaLock to (1 − 1/φ)/2. Invoke the sibling one_div_phi_gt to get 1/φ > 0.617. Subtract from 1 (linarith) to obtain 1 − 1/φ < 1 − 0.617. Divide by the positive constant 2, then compare (1 − 0.617)/2 = 0.1915 against 0.192 by norm_num. The whole argument is a short calc chain of strict inequalities; no physics lemmas beyond the φ bound are required.
why it matters
Feeds directly into alpha_prediction_validated, the module's key theorem that |α_lock − 0.19| < 0.02 (within 1σ of SPARC). That theorem's doc-comment records the sandwich 0.189 < α_lock < 0.192 and stresses that the match is a genuine prediction, not a fit.
In the Recognition forcing chain this closes the last numerical step after T5 (J-uniqueness) and T6 (φ forced): self-similarity of the discrete ledger forces the fractional kernel exponent to (1 − 1/φ)/2. Without a machine-checked upper bound, the a priori certificate could not separate prediction from validation. The result is pure real arithmetic once φ is fixed, so the only residual risk is the upstream φ bound itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.