PRCNullDistanceSetoidTarget_of_transitive
plain-language theorem explainer
Given transitivity of the null-distance relation on PRC Cauchy sequences, that relation is a full equivalence and therefore meets the exact real-setoid target. Anyone wiring the J-cost null quotient into the PRC real carrier would cite this. The argument is a one-line extraction of the equivalence certificate from the setoid constructor that already packages reflexivity and symmetry.
Claim. If the null-distance relation $\sim$ on PRC Cauchy sequences is transitive (for all $u,v,w$, $u\sim v$ and $v\sim w$ imply $u\sim w$), then $\sim$ is an equivalence relation, i.e. the exact target that turns null-distance into the real setoid holds.
background
In Primitive Recognition Calculus, candidate reals are Cauchy sequences equipped with a null-distance relation built from the J-cost surface. The intended real carrier is the quotient by that relation. Reflexivity and symmetry of null-equivalence are already established; the live mathematical obligation is triangle-style transitivity.
The transitive target is the universal statement: for all Cauchy sequences $u,v,w$, null-equivalence of $u$ with $v$ and of $v$ with $w$ implies null-equivalence of $u$ with $w$. The setoid target is simply the proposition that null-equivalence is an Equivalence. A local helper turns any proof of the transitive target into a full Setoid structure on Cauchy sequences by adjoining the known refl and symm proofs.
This module sits in the foundation layer that builds logic-native integers and rationals and then lifts them toward a real quotient, feeding later forcing-chain material.
proof idea
One-line term proof. Feed the transitivity hypothesis into the helper that builds a Setoid on PRC Cauchy sequences with relation equal to null-equivalence. Project the .iseqv field of that setoid; by definition that field is exactly the setoid target (an Equivalence proof for null-equivalence).
why it matters
This is the thin bridge from the transitive blocker to the exact setoid target on the null-distance relation. Downstream, the triangle-modulus theorem routes through it: prove the sharper J-cost triangle-modulus target, deduce transitivity, then apply this result to obtain the setoid target. The conditional certificate for Build Order step 9 records the same arrow (setoid_from_transitive), stating that once the local J-cost triangle modulus is proved, no quotient mechanics remain.
In the broader Recognition stack this closes a foundation obligation on the way from logic-native arithmetic to a real carrier usable by later landmarks (J-uniqueness, phi fixed point, eight-tick structure). It does not itself touch T5–T8; it clears the setoid interface those layers expect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.