rat_sq_lt_sq_bounds
plain-language theorem explainer
For positive rational γ and rational x, x² < γ² forces −γ < x < γ. Order-congruence arguments for the primitive recognition J-cost distance cite this elementary square bound before lifting to absolute differences. The proof is a two-sided contradiction closed by linear and nonlinear arithmetic on the difference-of-squares factors.
Claim. Let $x,\gamma\in\mathbb{Q}$ with $\gamma>0$. If $x^{2}<\gamma^{2}$, then $-\gamma<x$ and $x<\gamma$.
background
The module develops real-order congruence facts for the primitive recognition calculus, working first over rationals so that later certificates can compare J-cost distances without premature real analysis. Local notation uses a positive rational bound γ and a rational sample x; the squared comparison x·x < γ·γ is the natural modulus test before taking absolute values.
Despite name collisions in the dependency graph, the symbol γ here is only a positive rational parameter. It is not the Euler-Mascheroni constant and not the PPN post-Newtonian parameter. The lemma is the standard strict square-root bound specialized to ℚ, stated privately so downstream order lemmas can invoke it without re-proving the arithmetic each time.
proof idea
Split the target conjunction. Left half: assume ¬(−γ < x), so x ≤ −γ by linear arithmetic. Then both −x − γ and −x + γ are nonnegative (using γ > 0), hence their product is nonnegative. Nonlinear arithmetic rewrites that product as x² − γ² and contradicts x² < γ². Right half is symmetric: assume γ ≤ x, form the nonnegative product (x − γ)(x + γ), and again obtain x² ≥ γ², a contradiction.
why it matters
The sole recorded consumer is PRCJCostDistance_abs_diff_lt_of_lt_order_delta, which converts a squared-modulus hypothesis into a strict absolute-difference bound on the primitive recognition J-cost distance at rational points. That step is required for the real-order congruence certificate in the same module (PRCRealOrderCongruenceTarget_proved and the accompanying certificate). The result is foundation scaffolding rather than a forcing-chain landmark: it does not touch T5 J-uniqueness, the RCL, or the phi ladder, but it keeps the rational intermediate layer self-contained before continuity arguments are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.