PRCJCostDistanceIncrementDisplay_sq_lt_one

In the primitive recognition calculus, comparison cost is measured by the J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). On rational display increments the J-cost distance collapses to an explicit rational function of the ordinary increment $t$.

The upstream identity PRCJCostDistanceIncrementDisplay_formula records that closed form: $$\mathrm{display}(t)=\frac{(t^2)^2}{2(1+t^2)}.$$ The fixed numerical threshold $1/8$ is the module's boundedness delta (the cutoff used to force Cauchy targets to stay inside a unit ball in the ordinary square metric).

This lemma lives in the real-boundedness-modulus layer: it converts a small J-cost display into a plain rational bound $t^2<1$, which later upgrades to square-difference control on pairs of PRC rationals.

Proof by contradiction. Assume $\neg(t^2<1)$. Non-negativity of squares and nlinarith give $t^2\ge 1$. Rewrite the hypothesis via PRCJCostDistanceIncrementDisplay_formula, set $s:=t^2\ge 1$, and note the denominator $2(1+s)>0$. A short field_simp/nlinarith block (using $s^2\ge 0$) shows $$\frac{s^2}{2(1+s)}\ge\frac18,$$ hence the display is at least $1/8$, contradicting the strict upper bound. No external analytic lemmas are required.

Immediate parent is PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta, which lifts the scalar statement to pairs of PRC rationals: small J-cost distance below the fixed boundedness delta forces $(a-b)^2<1$ in ordinary rationals. That parent feeds the real-boundedness-modulus certificate and the proved Cauchy-sequence eventual-boundedness target in the same module.

Framework role: the display is the rational shadow of J-cost distance, so the lemma is a concrete bridge from T5 J-uniqueness (and the RCL-forced cost) down to ordinary metric control needed before completing to real displays. It does not itself force dimension or the eight-tick octave; it only supplies the square-bound step inside the PRC real-completion path.