alpha_lt_one
plain-language theorem explainer
alpha_lt_one establishes that the ILG exponent α = (1 − 1/φ)/2 is strictly less than one. Perturbation theorists working in the Recognition Science framework cite it to confirm that the derived coupling remains small. The tactic proof unfolds the definition, invokes positivity of φ, and reduces the inequality by elementary division and linarith.
Claim. The ILG exponent defined by $α = (1 - 1/φ)/2$ satisfies $α < 1$, where $φ > 0$ is the recognition constant supplied by the Constants bundle.
background
The GRLimit.Parameters module derives ILG parameters from RS geometry and proves they remain perturbative. alpha_from_phi supplies the explicit formula $α = (1 - 1/Constants.phi)/2$. Constants is the abstract structure that bundles several real numbers, including the recognition constant phi together with its positivity property.
proof idea
The proof unfolds alpha_from_phi to obtain the expression (1 − 1/φ)/2. It obtains 0 < φ from Constants.phi_pos, deduces 0 < 1/φ, hence 1 − 1/φ < 1 by linarith, divides the strict inequality by the positive constant 2, and closes again with linarith.
why it matters
The result is invoked inside rs_params_small_proven to establish the conjunction α < 1 ∧ C_lag < 1. This fills the first item in the module's list of proven bounds, confirming that RS-derived parameters stay below unity and therefore support perturbative treatment. It rests directly on the definition supplied by alpha_from_phi and the positivity fact from Constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.