alpha_lt_half
The theorem proves that the ILG exponent α derived from the golden ratio satisfies α < 1/2. Researchers verifying perturbative validity of Recognition Science gravity corrections would cite this bound when confirming that the coupling product remains below 0.1. The proof unfolds the explicit definition of α and applies positivity of φ together with a division inequality to reach the strict bound.
claimLet φ > 1 denote the golden ratio constant. Define α = (1 - φ^{-1})/2. Then α < 1/2.
background
The GRLimit.Parameters module derives the ILG exponent directly from Recognition Science geometry via the definition α = (1 - 1/φ)/2. The upstream Constants structure supplies φ together with its positivity property. This bound on α pairs with the companion result α < 1 and supports the module's goal of showing that both α and the lag constant C_lag = φ^{-5} remain small enough for perturbative treatment.
proof idea
The tactic proof unfolds alpha_from_phi to expose (1 - 1/φ)/2. It obtains positivity of φ from Constants.phi_pos, proves the auxiliary fact 1 - 1/φ < 1 by linarith on the positive reciprocal term, and finishes by applying div_lt_div_of_pos_right to divide the inequality by 2.
why it matters in Recognition Science
This result supplies the α < 1/2 bound that rs_params_perturbative_proven invokes to close the product estimate |α C_lag| < 0.1. It completes the second item in the module's list of proven parameter limits drawn from the Recognition Science spine. The bound anchors the small-coupling regime required for the GRLimit analysis and aligns with the phi-ladder and eight-tick octave constructions.
scope and limits
- Does not compute a numerical value for α beyond the stated inequality.
- Does not address the fine-structure constant or other physical couplings.
- Does not extend the bound to higher-order perturbative corrections.
- Does not establish the corresponding upper bound for C_lag.
Lean usage
have hα_lt : alpha_from_phi < 1 / 2 := alpha_lt_halfformal statement (Lean)
57theorem alpha_lt_half : alpha_from_phi < 1 / 2 := by
proof body
Tactic-mode proof.
58 unfold alpha_from_phi
59 have hφ_pos : 0 < Constants.phi := Constants.phi_pos
60 have : 1 - 1 / Constants.phi < 1 := by
61 have : 0 < 1 / Constants.phi := div_pos (by norm_num) hφ_pos
62 linarith
63 exact div_lt_div_of_pos_right this (by norm_num)
64
65-- (helper lemma removed)
66
67/-- φ > 3/2. -/