PRCJCostDistanceIncrementTriangleTarget
plain-language theorem explainer
Defines the additive two-leg modulus property for the rational J-cost increment display: small increments p and q force a small sum p+q in the displayed distance. Anyone proving the three-endpoint verifier triangle or the null-distance setoid cites this Prop as the exact blocker. It is a pure Prop packaging, not a proof.
Claim. For every positive PRC-rational $\varepsilon$ there exists a positive PRC-rational $\delta$ such that for all rationals $p,q$, if the one-increment J-cost display of $p$ is less than the verifier display of $\delta$ and the same holds for $q$, then the one-increment J-cost display of $p+q$ is less than the verifier display of $\varepsilon$.
background
In the Primitive Recognition Calculus layer, distances are first displayed on verifier rationals before any real completion. The one-increment display of the rational J-cost distance is the two-point display evaluated from $0$ to $t$; by translation invariance it depends only on the increment between endpoints.
PRC rationals are ratio-orbit quotient classes (nonzero-denominator orbits identified by cross-multiplication). Positivity is the PRC-native signed-numerator condition. The map toRat is the verifier display of such a class as an ordinary rational.
The local module isolates a sharper exact blocker than the full three-endpoint triangle: an additive two-leg modulus on increments alone. That modulus is the mathematical core behind the verifier-rational triangle target used later in the null-distance setoid chain.
proof idea
No proof: this is a def equating a name to a Prop. The body is the quantified modulus statement itself (universal positive $\varepsilon$, existential positive $\delta$, then the two-premise implication on rational increments $p,q$). Downstream theorems discharge or consume the Prop; the definition only packages it.
why it matters
Build-order step 9c treats this Prop as the remaining exact blocker. The increment-triangle certificate records both the closed-form increment formula and this target. A proved instance implies the three-endpoint verifier triangle target by a short reduction, and that in turn closes the whole PRC null-distance setoid chain via the conditional certificate whose only open field is this modulus.
In the Recognition stack this sits under the J-cost geometry that later feeds T5 J-uniqueness and the composition law: control of displayed J-distance under addition of small rational increments is what lets null-distance behave like an equivalence before continuum limits. The sibling proved theorem constructs an explicit $\delta$ from $\varepsilon$ (via ratios such as $\varepsilon/(1+\varepsilon)$), so the scaffold path is already closed in the increment-triangle module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.