PRCNullDistanceSetoidTarget_of_increment_triangle
plain-language theorem explainer
Assuming the additive two-leg modulus for rational J-cost increments, the PRC null-distance relation is a setoid. Anyone closing the Primitive Recognition Calculus distance chain cites this bridge. The proof is a one-line composition: increment modulus implies the verifier triangle, which implies the null-distance setoid target.
Claim. If the additive two-leg modulus holds for rational increments of the J-cost distance display (for every positive rational $\varepsilon$ there exists a positive rational $\delta$ such that whenever the increment displays of $p$ and $q$ are both less than $\delta$, the increment display of $p+q$ is less than $\varepsilon$), then the PRC null-distance relation is a setoid.
background
In the Primitive Recognition Calculus (PRC), distances are built from the J-cost on rational displays. The null-distance setoid target asks that the relation "J-cost distance is zero" be an equivalence relation on the relevant carrier, so quotients and Cauchy completions are well-defined.
The sharper blocker is the increment-only triangle target: an additive two-leg modulus on rational increments of the J-cost distance display. For every positive rational $\varepsilon$ one needs a positive $\delta$ such that if the increment displays of $p$ and of $q$ are both below $\delta$, then the increment display of $p+q$ is below $\varepsilon$. That is the mathematical core behind the three-endpoint verifier-rational triangle.
Upstream, the verifier triangle already implies the null-distance setoid ("Once the verifier-rational inequality is proved, the final null-distance setoid target follows"), and the increment target implies the verifier triangle. This declaration chains those two implications.
proof idea
One-line term-mode wrapper. Apply the upstream implication from increment triangle to verifier-rational three-endpoint triangle, then feed that hypothesis into the upstream implication from verifier triangle to null-distance setoid. No new arithmetic is performed here.
why it matters
This is the last logical bridge before the null-distance setoid is discharged by an explicit rational increment modulus. Downstream, PRCNullDistanceSetoidTarget_proved cites it with the proved increment target: "The PRC null-distance setoid target is now closed by the explicit rational increment modulus." It is also packaged into the Build Order step 9b conditional certificate, which records that the verifier triangle (and hence the setoid) reduces to a one-dimensional additive increment estimate.
In the Recognition foundation stack this sits inside the PRC J-cost distance development that underwrites later forcing and continuum constructions; it does not itself invoke T5--T8, but it clears a setoid hypothesis those layers need once distances are quotiented.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.