PRCJCostDistanceIncrementDisplay_lt_of_sq_lt
plain-language theorem explainer
If a rational increment t satisfies t² < η with 0 < η < 1 and η²/2 < ε, then the one-step rational J-cost distance display of t is strictly below ε. Continuity arguments for the PRC J-cost under bounded multiplication cite this bound. The proof rewrites the closed-form display and chains elementary rational inequalities.
Claim. Let $t,\eta,\varepsilon\in\mathbb{Q}$ satisfy $0<\eta<1$, $t^{2}<\eta$, and $\eta^{2}/2<\varepsilon$. Then the one-increment rational $J$-cost distance display of $t$ is strictly less than $\varepsilon$.
background
In the Primitive Recognition Calculus, the rational J-cost distance is tracked by a display functional. The one-increment display of an increment $t\in\mathbb{Q}$ is defined as the displayed distance from $0$ to $t$; it is translation-invariant and depends only on the increment between endpoints.
An upstream closed form gives the display explicitly: $$\mathrm{display}(t)=\frac{(t^{2})^{2}}{2(1+t^{2})}.$$ The present lemma is a modulus-style comparison: smallness of $t^{2}$ relative to a parameter $\eta\in(0,1)$, together with $\eta^{2}/2<\varepsilon$, forces the display below $\varepsilon$. The ambient module develops real-product continuity of this cost from rational bounds and a boundedness modulus.
proof idea
Rewrite the goal via the closed-form formula for the increment display. Nonnegativity of $t^{2}$ and positivity of the denominator $2(1+t^{2})$ are immediate. Transitivity with $\eta<1$ yields $t^{2}<1$. Then $(t^{2})^{2}<\eta^{2}$ by nonlinear arithmetic. Because the denominator is at least $2$, the fraction is at most $(t^{2})^{2}/2$, which is strictly less than $\eta^{2}/2$, hence less than $\varepsilon$ by the last hypothesis. The final step is lt_of_le_of_lt on that chain.
why it matters
This comparison is the quantitative engine behind PRCJCostDistanceMulBoundedContinuityTarget_proved, which discharges the bounded-multiplication continuity target for the PRC J-cost distance and feeds the real-product continuity certificate in the same module. In the Recognition foundation, J-cost uniqueness (forcing step T5) and the Recognition Composition Law make continuity of cost under products a structural necessity when lifting rational displays to real regular sequences. The lemma closes a concrete $\varepsilon$-$\delta$ gap on the rational side so the product continuity certificate can be stated without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.