alpha_locked_pos
The lemma establishes positivity of the ILG modification parameter defined as (1 minus one over phi) divided by two. Researchers deriving coupling lock-in bounds in Recognition Science cite it to confirm the parameter lies in the open unit interval. The proof reduces the claim to the known inequality phi greater than one, then applies elementary real arithmetic to the resulting difference and division.
claim$0 < (1 - 1/φ)/2$, where φ denotes the golden ratio satisfying φ > 1.
background
In the Constants.ILG module the locked coupling parameter is introduced by the definition alpha_locked := (1 - 1/phi)/2. This rests on the golden-ratio constant phi imported from Constants and PhiSupport. The upstream lemma one_lt_phi supplies the strict inequality 1 < phi, which is required to guarantee that the numerator 1 - 1/phi remains positive. The local theoretical setting is the derivation of fixed constants under the Recognition Composition Law and the forcing chain that produces the eight-tick octave and three spatial dimensions.
proof idea
The proof first dsimps the definition of alpha_locked. It obtains 0 < phi from phi_pos and 1 < phi from one_lt_phi. These yield 1/phi < 1 by div_lt_one, hence 1 - 1/phi > 0 by linarith. The final step applies div_pos to the positive numerator and the constant 2 to conclude positivity after division by two. The key upstream result invoked is one_lt_phi.
why it matters in Recognition Science
The result is invoked by alpha_locked_in_unit in RecognitionBandwidth to close the unit-interval claim 0 < alpha_locked ∧ alpha_locked < 1. It supplies the lower bound required for the ILG modification parameter in the coupling-lock-in condition. Within the framework it anchors the alpha band constraints that appear after the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.
scope and limits
- Does not compute a numerical approximation of the parameter.
- Does not relate the parameter to the fine-structure constant 1/137.
- Does not derive the golden ratio from the Recognition functional equation.
- Does not address stability under renormalization-group flow.
Lean usage
theorem alpha_in_unit : 0 < alpha_locked ∧ alpha_locked < 1 := ⟨alpha_locked_pos, alpha_locked_lt_one⟩formal statement (Lean)
11lemma alpha_locked_pos : 0 < alpha_locked := by
proof body
Tactic-mode proof.
12 dsimp [alpha_locked]
13 have hφ : 0 < phi := phi_pos
14 have hφ_gt_1 : 1 < phi := one_lt_phi
15 -- 1/φ < 1 because φ > 1
16 have hinv_lt_one : 1 / phi < 1 := by
17 rw [div_lt_one hφ]
18 exact hφ_gt_1
19 have hsub : 0 < 1 - 1 / phi := by
20 linarith
21 have hdiv : 0 < (1 - 1 / phi) / 2 := by
22 apply div_pos hsub
23 exact zero_lt_two
24 exact hdiv
25