PRCNullDistanceSetoidTarget
plain-language theorem explainer
Packages the exact setoid obligation for null J-cost distance on recognition Cauchy sequences: that relation must be an equivalence. Anyone building the PRC real quotient cites this Prop as the gate. The body is a one-line definition equating the target to Equivalence of the intended null-distance relation; reflexivity and symmetry are already available, transitivity is the live load closed downstream.
Claim. The null-distance relation on Cauchy sequences of recognition-calculus rationals (two sequences are related when the $J$-cost distance of corresponding terms can be made smaller than every positive rational threshold for all large indices) is an equivalence relation.
background
In the Primitive Recognition Calculus real-Cauchy layer, sequences of PRC rationals are Cauchy with respect to the $J$-cost distance induced by the recognition cost $J$. That distance is the natural metric surface coming from the Recognition Composition Law and the unique cost $J(x)=(x+x^{-1})/2-1$.
The intended identification of sequences that should represent the same real is null distance: for every positive rational $\varepsilon$ there exists $N$ so that for all $n\ge N$ the $J$-cost distance between the $n$th terms is $<\varepsilon$. That relation is already defined as the null-equivalent predicate on Cauchy ledgers.
This module sits after the rational field and trace-closure layers. The local goal is a first internal quotient carrier for a continuum of recognition values. Forming that quotient requires a setoid, hence a full equivalence proof on null distance.
proof idea
Definitional, not a proof. The Prop is literally Equivalence applied to the null-distance relation on PRC Cauchy sequences. No tactics or lemmas fire here; the mathematical work is deferred to proving reflexivity, symmetry, and especially transitivity of that relation. Upstream already supplies reflexivity (and symmetry) for the null-equivalent predicate; transitivity is discharged later by triangle-modulus certificates on the $J$-cost distance.
why it matters
This is the named gate for the PRC real setoid. Downstream, the increment-triangle certificate closes it: once the explicit rational increment modulus for $J$-cost distance is proved, a chain of of-theorems yields the null-distance setoid target, and a sibling records that the target is proved. Conditional certificates for the verifier-triangle and full triangle steps also route through this Prop as their terminal obligation.
In framework terms it is the continuum bridge inside Primitive Recognition Calculus: without a setoid on null $J$-distance there is no quotient carrier for recognition reals, and later continuum and ledger bridges cannot identify Cauchy ledgers. It does not itself invoke T5–T8, but it is the analytic setoid step that lets the forced $J$ and $\phi$-ladder geometry act on completed sequences rather than only on rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.