alpha_lt_half
plain-language theorem explainer
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.
Claim. Let φ > 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.