PRCNullDistanceSetoidTarget_of_verifier_triangle
plain-language theorem explainer
Once the verifier-rational triangle inequality for displayed J-cost distances holds, the null-distance relation on the PRC real carrier is an equivalence, hence a setoid. Anyone finishing the real-completion quotient in Primitive Recognition Calculus cites this bridge. The proof is a pure one-line composition: transport the verifier inequality to the triangle-modulus target, then apply the modulus-to-setoid lemma.
Claim. If the verifier-rational triangle inequality holds for displayed J-cost distances on rationals (for every positive rational $\varepsilon$ there exists a positive rational $\delta$ such that $d(x,y)<\delta$ and $d(y,z)<\delta$ imply $d(x,z)<\varepsilon$), then the intended null-distance relation on the PRC real carrier is an equivalence relation.
background
In Primitive Recognition Calculus, pairwise cost is measured by the J-cost $J(x)=(x+x^{-1})/2-1$, the unique cost forced by the Recognition Composition Law. Before full real completion, distances are compared through conservative rational displays of that cost.
The null-distance setoid target is the proposition that the intended null-distance relation is an equivalence. Reflexivity and symmetry are already proved; transitivity is the remaining obligation. Upstream, a sharper triangle-modulus target (uniform control of the third leg by a positive modulus) implies that transitivity, and the modulus target itself is obtained from a purely rational verifier inequality by display transport.
The local module packages the conditional closure of Build Order step 9a: once the rational display inequality is granted, the setoid target follows.
proof idea
One-line term proof. Apply the display-transport lemma that turns the verifier-rational triangle inequality into the PRC triangle-modulus target; feed the result into the upstream lemma that derives the null-distance setoid (equivalence) from any triangle-modulus witness. No fresh arithmetic is performed.
why it matters
This is the last structural link from the remaining rational inequality to the setoid required for the PRC real quotient. It is recorded in the Build Order step 9a conditional certificate, whose doc-comment states that "PRC triangle transport is reduced to the displayed rational inequality." A second parent routes the increment-only triangle blocker through the same bridge, so that a single analytic estimate closes the whole null-distance setoid chain. Completing that setoid is prerequisite foundation work before Cauchy sequences of recognition traces can serve as a real carrier for later continuum and Hamiltonian limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.