PRCJCostDistanceIncrementTriangleTarget_proved
plain-language theorem explainer
For every positive PRC-rational tolerance ε an explicit positive δ is built so that if two J-cost increment displays lie below δ, their combined increment stays below ε. The null-distance setoid closure and the increment-triangle certificate both cite this modulus. The proof constructs δ from ε by the cascade ρ=ε/(1+ε), η=ρ/4, δ=η²/(4(1+η)), then reduces the triangle claim to square bounds via sibling comparison lemmas.
Claim. For every positive PRC-rational $\varepsilon$ there exists a positive PRC-rational $\delta$ such that if $p,q$ are real increments whose J-cost increment displays are each strictly less than $\delta$, then the combined increment display obeys the triangle bound below $\varepsilon$.
background
Primitive Recognition Calculus (PRC) develops the J-cost geometry on a rational carrier PRCRat before completing to reals. The J-cost is the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$. Distances built from $J$ need a quantitative triangle modulus so that the null set ${d=0}$ is a setoid (reflexive, symmetric, and transitive up to controlled error).
This module supplies that modulus in fully explicit rational form. The increment display is a nonnegative rational proxy for the local J-cost increment; sibling lemmas relate display size to squares (sq_lt_of_display_lt_delta, increment_display_lt_of_sq_lt). The target proposition asserts: given any positive tolerance $\varepsilon$, a positive $\delta=\delta(\varepsilon)$ exists that forces the triangle inequality for increments whose displays lie below $\delta$.
Upstream arithmetic is the PRCRat API (toRat, one_toRat, positivity and field lemmas). The construction never leaves the rationals, so the later real completion inherits a uniform modulus.
proof idea
Tactic proof. Fix positive eps. Define the cascade inside PRCRat:
two := 1+1, four := two+two, rho := eps/(1+eps), eta := rho/four, delta := (eta*eta)/(four*(1+eta)).
First goal: delta > 0. Transport everything through toRat, evaluate two.toRat = 2 and four.toRat = 4 by toRat_add and one_toRat, then close by positivity on the resulting rational expression.
Second goal: for increments p,q with display $< delta$, the combined display is $< eps. Again push to ℚ. Establish 0 < rho < 1, 0 < eta < 1, and the exact formula for delta.toRat. Apply sq_lt_of_display_lt_deltato obtain $p^2 < \eta$ and $q^2 < \eta$. Feed those square bounds into the companion comparisonincrement_display_lt_of_sq_lt(and the display formula) to recover the $\varepsilon$-triangle bound. All steps are elementary field arithmetic andnlinarith`.
why it matters
This is the quantitative heart of the J-cost null-distance setoid on PRC. Downstream, PRCJCostDistanceVerifierTriangleTarget_proved is a one-line wrapper applying the verifier-of-increment lemma to this result; PRCNullDistanceSetoidTarget_proved likewise discharges the setoid target from the same modulus. Both are packaged by prc_jcost_distance_increment_triangle_certificate, whose doc-comment states that "the explicit rational increment estimate closes the whole J-cost null-distance setoid chain."
In the broader Recognition framework the setoid is the quotient on which the forced cost $J$ (T5 J-uniqueness) becomes a genuine distance before the phi-ladder and eight-tick structure are imposed. Without an explicit rational modulus the null-set would not be provably transitive inside PRC, blocking later measure-forcing and Hamiltonian emergence steps that assume a well-defined recognition metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.