PRCJCostDistance_sq_lt_of_display_lt_delta
plain-language theorem explainer
If the one-step rational J-cost distance display of a rational t lies below a threshold delta controlled by eta, then t squared is strictly less than eta. Arguments that build a modulus of continuity for multiplication of recognition reals cite this square bound. The proof is contradiction plus monotonicity of the rewritten display s |-> s^2/(2(1+s)) on nonnegative s.
Claim. Let $t,\eta,\delta\in\mathbb{Q}$ with $\eta>0$, $\delta>0$, and $\delta\le \eta^2/(4(1+\eta))$. Write $D(t)$ for the one-increment rational J-cost distance display of $t$. If $D(t)<\delta$, then $t^2<\eta$.
background
In Primitive Recognition Calculus, reals are assembled from rational data equipped with a J-cost distance that records recognition defect between endpoints. The one-increment display is the displayed rational J-cost between $0$ and an increment $t$. An upstream formula lemma rewrites it as
$$D(t)=\frac{t^4}{2(1+t^2)}=\frac{s^2}{2(1+s)},\qquad s=t^2.$$
The module develops quantitative continuity of multiplication under this distance. The present lemma turns a small display bound into a strict square bound $t^2<\eta$, provided delta is no larger than the explicit rational $\eta^2/(4(1+\eta))$. That comparison constant is exactly what the later product-modulus construction feeds in.
Positivity of $\eta$ keeps denominators positive and anchors the monotone comparison of the rational function of $s$.
proof idea
Contradiction: assume $\eta\le t^2$. Rewrite the smallness hypothesis with the display formula lemma, so $t^4/(2(1+t^2))<\delta$. Set $s=t^2\ge\eta>0$.
Prove $\eta^2/(4(1+\eta))\le s^2/(2(1+s))$ in two steps. First, enlarge the left side by shrinking the denominator from $4(1+\eta)$ to $2(1+\eta)$. Second, show $u\mapsto u^2/(2(1+u))$ is monotone for $u\ge\eta$ by clearing denominators and checking nonnegativity of the cross difference $(s-\eta)(s+\eta+s\eta)$. Transitivity with the hypothesis $\delta\le\eta^2/(4(1+\eta))$ forces $D(t)\ge\delta$, contradicting strict inequality. The argument is pure rational field arithmetic (nlinarith, field_simp, positivity).
why it matters
Directly used by the proved product-continuity target for J-cost distance on bounded recognition reals, and by the square-difference modulus lemma in RealOrderCongruence. Those parents discharge continuity of multiplication in the PRC real structure.
That step is foundation work: it lifts rational J-cost control toward completed reals so later layers can carry the Recognition Composition Law and J-uniqueness (forcing chain T5) off the rationals. Without a quantitative implication "small display implies small square," the product modulus cannot close.
Siblings in the same module package the bound into a certificate object for real product continuity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.