rs_params_positive
plain-language theorem explainer
Both the ILG exponent defined as (1 minus one over phi) over two and the lag constant defined as phi to the minus five are strictly positive. Modelers of the GR limit in Recognition Science cite the result when establishing that the parameters remain perturbative. The tactic proof splits the conjunction, unfolds each definition, invokes positivity and one-less-than-phi for the golden ratio, then closes with linarith and the positivity of real powers.
Claim. Let $phi$ be the golden ratio. Define $alpha = (1 - phi^{-1})/2$ and $C_{lag} = phi^{-5}$. Then $0 < alpha$ and $0 < C_{lag}$.
background
The module proves concrete bounds on ILG parameters that Recognition Science derives from its geometry and coherence scale. Alpha equals (1 minus one over phi) divided by two; C_lag equals phi to the minus five. These expressions appear directly in the module documentation as the objects whose smallness must be shown rather than assumed. Upstream lemmas supply phi greater than one and phi positive, both taken from the Constants module and the PhiSupport layer.
proof idea
Constructor splits the conjunction into separate goals. The first goal unfolds the alpha definition, obtains phi_pos and one_lt_phi, shows one over phi is less than one via div_lt_one, then applies linarith. The second goal unfolds the C_lag definition and applies Real.rpow_pos_of_pos to phi_pos.
why it matters
The result is invoked by the two downstream theorems that bound the product of the parameters below 0.1 and below 0.02. It supplies the positivity half of the perturbative regime required by the module's source derivation. The step sits inside the Recognition Science parameter chain that begins from the golden-ratio fixed point and feeds the GR-limit analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.