cLag_lt_one_tenth
plain-language theorem explainer
The theorem shows that the lag coupling derived from the golden ratio satisfies phi to the negative fifth power less than one tenth. Researchers establishing perturbative validity for Recognition Science gravity models cite this bound to control the coupling product. The proof works by establishing phi at least 8/5, applying monotonicity of the negative power map, and verifying the numerical fact that (8/5) to the fifth exceeds 10.
Claim. $phi^{-5} < 1/10$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The module proves bounds on the ILG parameters alpha and C_lag that arise from Recognition Science. C_lag equals phi to the negative fifth power and originates from the coherence energy scale in the eight-tick resonance construction. The Constants structure supplies the numerical value of phi as the positive root of x squared minus x minus one equals zero. This lemma sits inside the parameter limits section that connects the Recognition Science spine to general relativity limits. Upstream, the definition cLag_from_phi pulls the constant from the Constants structure, while positivity facts come from rs_params_positive.
proof idea
The tactic script unfolds the definition of cLag_from_phi. It proves phi is at least 8/5 by showing that the standard expression for phi exceeds 8/5, using a contradiction argument on the square root of five. Real.rpow_le_rpow_of_nonpos then gives the power inequality for the negative exponent. The right side is rewritten as the reciprocal of (8/5) to the fifth, and norm_num confirms that this fifth power equals 32768/3125 which is greater than 10. Transitivity of less-than closes the claim.
why it matters
This bound is invoked by cLag_lt_one to reach C_lag less than one and by rs_params_perturbative_proven to establish that the absolute value of the product alpha times C_lag is less than 0.1. It directly supports the module claim that the parameters are small enough for perturbative treatment. The result rests on the eight-tick resonance definition of the lag constant and the forcing chain's fixation of phi. It leaves the tighter product bound below 0.02 open, as noted in the downstream coupling_product_small_proven.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.