sq_lt_of_display_lt_delta
plain-language theorem explainer
If the one-step rational J-cost display of an increment t lies below a positive threshold delta that is at most eta squared over four times one plus eta, then t squared is strictly less than eta. Used when forcing small increments in the PRC J-cost distance triangle argument. Proof is contradiction: the closed-form display is monotone in t squared, so a large square would force the display at least as large as delta.
Claim. Let $t,\eta,\delta\in\mathbb{Q}$ with $\eta>0$, $\delta>0$, and $\delta\le \eta^2/(4(1+\eta))$. If the one-increment rational J-cost display of $t$ satisfies $\mathrm{display}(t)<\delta$, then $t^2<\eta$.
background
In the Primitive Recognition Calculus, distances are assembled from the rational J-cost. The one-increment display of a rational $t$ is the displayed J-cost distance from $0$ to $t$. A sibling formula records the closed form $$\mathrm{display}(t)=\frac{t^4}{2(1+t^2)}.$$
This module treats the increment form of the triangle inequality for that display, as a step toward a full triangle modulus for PRC J-cost distance. The parameter $\eta$ is a smallness scale on $t^2$; $\delta$ is a display-scale threshold forced below $\eta^2/(4(1+\eta))$ so that a small display implies a small square.
(The dependency graph also lists unrelated delta and eta symbols from other modules; here both names are ordinary positive rationals.)
proof idea
Contradiction. Assume $t^2\ge\eta$. Rewrite the smallness hypothesis with the closed-form display formula. Set $s:=t^2\ge\eta>0$ and prove
$$\frac{\eta^2}{4(1+\eta)}\le\frac{s^2}{2(1+s)}.$$
First compare denominators to get $\eta^2/(4(1+\eta))\le\eta^2/(2(1+\eta))$. Then show $u\mapsto u^2/(2(1+u))$ is monotone for $u\ge\eta$ by verifying nonnegativity of $s^2(1+\eta)-\eta^2(1+s)$ (factor as $(s-\eta)(s+\eta+s\eta)$). Transitivity with $\delta\le\eta^2/(4(1+\eta))$ yields $\mathrm{display}(t)\ge\delta$, contradicting the strict bound. Rational positivity and nlinarith close the inequalities.
why it matters
Direct lemma for the proved increment-triangle target in the same module, which discharges the certificate that the one-increment J-cost display obeys a controlled triangle inequality. That target sits in the foundation stack upgrading rational J-cost displays into a genuine distance (triangle, null-setoid, modulus).
In Recognition Science the J-cost is the unique cost forced by T5 (J-uniqueness from the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$). Elementary square-control of displayed increments is the calculus step before continuum and geometric layers. Without this implication the small-increment case of the triangle certificate does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.