PRCNullDistanceSetoidTarget_of_triangle_modulus
plain-language theorem explainer
Once the J-cost rational distance admits a local triangle modulus, the null-distance relation on PRC Cauchy data is an equivalence, hence a setoid. Anyone building the real carrier from Primitive Recognition Calculus cites this reduction. The proof is a pure composition: modulus implies null-distance transitivity, and transitivity plus already-proved reflexivity and symmetry yields the setoid target.
Claim. Assume the J-cost-derived rational distance has a local triangle modulus: for every positive tolerance $\varepsilon$ there exists a positive $\delta$ such that if $d_J(a,b)<\delta$ and $d_J(b,c)<\delta$ then $d_J(a,c)<\varepsilon$. Then the intended null-distance relation is an equivalence relation (reflexive, symmetric, and transitive), so it defines the real null setoid.
background
In the Primitive Recognition Calculus, candidate reals are built from rational Cauchy data equipped with a distance derived from the J-cost. The null-distance relation identifies sequences that become arbitrarily close in that distance; the exact setoid target is the statement that this relation is an equivalence. Reflexivity and symmetry are already settled; transitivity is the remaining mathematical obligation.
The sharper analytic blocker is the local triangle modulus for the J-cost rational distance: for each positive tolerance there is a strictly smaller positive tolerance so that two small legs force the composed leg below the original tolerance. That modulus is the exact analytic input needed before any quotient bookkeeping.
Upstream, the modulus-to-transitivity lemma reduces null-distance transitivity to completed-orbit index bookkeeping once the modulus is granted. A separate one-line lemma then packages reflexivity, symmetry, and that transitivity into the full equivalence target.
proof idea
One-line term-mode composition. Apply the upstream lemma that turns the triangle-modulus hypothesis into null-distance transitivity (orbit-index bookkeeping under the modulus). Feed that transitivity witness into the sibling lemma that builds the full setoid target from any proof of transitivity, using the already-established reflexivity and symmetry of the null-distance relation. No new analytic work occurs at this layer.
why it matters
This is the clean bridge from the analytic triangle-modulus obligation to the exact null-distance setoid target in the real-construction stack. Downstream, the conditional certificate for Build Order step 9 records this arrow explicitly: once the local J-cost triangle modulus is proved, no quotient mechanics remain. The verifier path also routes through it: after the verifier-rational inequality yields the modulus, this theorem discharges the final setoid target.
In framework terms it sits inside the foundation layer that turns recognition cost structure into a real carrier, before metric and gravity constructions consume that carrier. The audit note on the sibling certificate is precise: the final null-distance quotient still lives under trace closure, and the open obligation is analytic, not a new primitive. Closing the modulus therefore closes this setoid step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.