increment_display_lt_of_sq_lt
plain-language theorem explainer
If η ∈ (0,1), t² < η, and η²/2 < ε, then the one-increment rational J-cost distance display of t is strictly less than ε. The increment-triangle target cites this bound when choosing a modulus of continuity for small steps. Proof rewrites the closed form t⁴/(2(1+t²)) and chains 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 display of the rational $J$-cost distance at $t$ obeys $\dfrac{t^{4}}{2(1+t^{2})}<\varepsilon$.
background
In the Primitive Recognition Calculus, the rational J-cost distance between endpoints is displayed by a translation-invariant increment functional. The one-increment display at a rational step $t$ is defined as the displayed distance from $0$ to $t$; its closed form is
$$\mathrm{display}(t)=\frac{t^{4}}{2(1+t^{2})}.$$
That identity is the sibling lemma PRCJCostDistanceIncrementDisplay_formula.
The ambient J-cost is the unique cost forced by the Recognition Composition Law (forcing chain T5): $J(x)=(x+x^{-1})/2-1$. The display above is the rational shadow of an incremental J-distance used to build a metric-style triangle inequality on the PRC ledger.
Parameters $\eta$ and $\varepsilon$ are positive rationals controlling a small-step regime: $\eta$ caps $t^{2}$, and $\varepsilon$ is the target tolerance that the display must undercut.
proof idea
Rewrite the goal via the closed-form formula, replacing the display by $t^{4}/(2(1+t^{2}))$.
Nonnegativity of $t^{2}$ and positivity of the denominator $2(1+t^{2})$ are immediate. Transitivity of $<$ with $\eta<1$ yields $t^{2}<1$. Squaring the hypothesis $t^{2}<\eta$ gives $t^{4}<\eta^{2}$.
Because the denominator is at least $2$, the fraction is at most $t^{4}/2$. Then $t^{4}/2<\eta^{2}/2$, and the remaining hypothesis $\eta^{2}/2<\varepsilon$ finishes the chain by lt_of_le_of_lt and lt_trans. The arithmetic steps are discharged by positivity, nlinarith, and a one-sided div_le_div_of_nonneg_left.
why it matters
This lemma is the quantitative small-step engine for PRCJCostDistanceIncrementTriangleTarget_proved, which discharges the increment-triangle certificate in the same module. That certificate is one link in the PRC J-cost distance triangle package (siblings cover the verifier triangle, null-distance setoid, and modulus targets).
In the Recognition framework the J-cost is forced uniquely (T5) by the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Controlling the rational display of incremental J-distance is how the formal development turns that algebraic cost into a metric-like structure on recognition steps. Without a strict bound of display by an arbitrary positive $\varepsilon$ under a square-smallness hypothesis, the triangle target cannot choose its continuity modulus.
No open scaffold remains here: the claim is fully proved and only feeds the already-stated triangle target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.