phi_gt_three_halves
plain-language theorem explainer
The golden ratio exceeds 3/2. This bound is invoked to confirm that the lag coupling C_lag equals phi to the minus five stays below one tenth, permitting perturbative expansions in the GR limit of Recognition Science. Researchers deriving alpha and C_lag from the phi-ladder would cite the result to justify small-coupling approximations. The tactic proof first obtains sqrt(5) greater than 11/5 by contradiction on the square, then chains three rational inequalities to reach 3/2 less than 8/5 less than phi.
Claim. $phi > 3/2$ where $phi = (1 + sqrt(5))/2$ is the golden ratio appearing in the Constants bundle.
background
The module proves that RS-derived parameters alpha equals (1 minus 1 over phi) over 2 and C_lag equals phi to the minus five remain small enough for perturbative GR limits. The Constants structure collects the core CPM quantities Knet, Cproj, Ceng, Cdisp with non-negativity on Knet. C_lag is defined directly as phi inverse to the fifth power and is stated to approximate 0.09. The local setting is the explicit verification that both alpha and C_lag lie below 1 and that their product lies below 0.1, as required by the source derivation of coherence energy.
proof idea
The tactic proof proceeds by contradiction: assume sqrt(5) is at most 11/5, derive that 5 is at most (11/5) squared, and obtain an immediate numerical falsehood. From the negation it extracts 11/5 less than sqrt(5) via lt_of_not_ge. Adding 1 to both sides, dividing by 2, and rewriting 8/5 as the left-hand side produces 8/5 less than phi. The final step applies lt_trans to the already-proven 3/2 less than 8/5.
why it matters
The inequality supplies the elementary lower bound needed to discharge the claim that phi to the minus five is less than 1/10, which the module documentation lists as proven. It therefore feeds the sibling results rs_params_perturbative_proven and coupling_product_small_proven. Within the Recognition Science framework the bound anchors the self-similar fixed point phi (T6) before the eight-tick octave and the derivation of three spatial dimensions can be treated perturbatively.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.