alpha_locked_lt_one
plain-language theorem explainer
Researchers modeling the ILG modification parameter in Recognition Science cite this lemma to bound alpha_locked below one. It pairs with the positivity result to place the parameter inside the unit interval. The tactic proof reduces the claim to a short chain of real inequalities that begins from phi greater than one and applies division and subtraction rules.
Claim. $ (1 - 1/phi)/2 < 1 $, where phi denotes the golden ratio satisfying phi > 1.
background
In the Constants.ILG module alpha_locked is defined by the expression (1 - 1/phi)/2. The upstream lemma one_lt_phi supplies the fact 1 < phi, which is the sole nontrivial input required for the bound. The module imports Mathlib together with the parent Constants file and relies on phi_pos for the positivity of the golden ratio.
proof idea
The proof dsimps the definition of alpha_locked, obtains 0 < phi and 1 < phi from phi_pos and one_lt_phi, proves 1/phi < 1 by div_lt_one, derives 1 - 1/phi < 1 by linarith, applies div_lt_div_of_pos_right to reach a quotient less than 1/2, notes 1/2 < 1 by norm_num, and concludes by linarith.
why it matters
The lemma is invoked by alpha_locked_in_unit to establish the full statement 0 < alpha_locked and alpha_locked < 1. That theorem appears in Unification.RecognitionBandwidth and supplies the unit-interval bound required for the demanded recognition rate. It thereby closes the parameter range asserted by the Phase-2 lock-in condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.