cLag_lt_one
plain-language theorem explainer
The theorem establishes that the lag constant C_lag equals phi to the power negative five satisfies C_lag less than 1. Researchers checking perturbative validity of ILG parameters in the GRLimit module cite it to confirm smallness. The proof chains the stricter bound C_lag less than one tenth with the numerical fact one tenth less than 1 via transitivity of less than.
Claim. $C_ {lag} < 1$ where $C_{lag} := phi^{-5}$ and $phi$ is the golden ratio.
background
The Relativity.GRLimit.Parameters module proves that the ILG parameters alpha and C_lag derived from Recognition Science are small and perturbative. From the source, alpha equals (1 minus 1 over phi) over 2 and C_lag equals phi to the power of negative 5. The definition cLag_from_phi sets the lag constant to phi^{-5} approximately 0.090.
proof idea
The tactic proof obtains the intermediate bound cLag_from_phi less than 1/10 from the sibling theorem cLag_lt_one_tenth. It establishes 1/10 less than 1 by norm_num and applies lt_trans to conclude the result.
why it matters
This theorem is invoked by rs_params_small_proven to prove both parameters are less than 1, confirming the perturbative regime for the Recognition spine connection. The module documentation lists it as part of the requirement that parameters satisfy alpha less than 1 and C_lag less than 1. It touches the open question of tighter product bounds such as less than 0.02.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.