PRCNullDistanceSetoidOfTransitive
plain-language theorem explainer
Given transitivity of null J-cost distance on PRC Cauchy sequences, the null-equivalence relation becomes a setoid. Anyone building the PRC real carrier as a quotient of Cauchy ledgers cites this. The construction packages reflexivity and symmetry already proved for null-equivalence with the supplied transitivity hypothesis.
Claim. If null-distance equivalence of PRC Cauchy sequences is transitive, then that relation is a setoid on the type of PRC Cauchy sequences: two sequences are related when their termwise $J$-cost distance eventually falls below every positive rational tolerance.
background
In the Primitive Recognition Calculus, a PRC Cauchy sequence is an orbit-indexed rational ledger whose $J$-cost distance eventually drops below every positive PRC rational tolerance. The intended real numbers are equivalence classes of such sequences under null distance: $u \sim v$ when the $J$-cost distance between corresponding terms is eventually smaller than every positive rational $\varepsilon$.
That relation already has reflexivity and symmetry. The remaining analytic blocker is triangle-style transitivity, packaged as the proposition that null-equivalence is transitive on all triples of Cauchy sequences. The present definition sits in the RealNullSetoid module and turns a proof of that blocker into a Lean Setoid, so the quotient type can be formed.
Upstream, null-equivalence is defined from the $J$-cost distance surface on rational terms; the transitivity target is exactly the missing piece for the final null-distance quotient.
proof idea
Definitional packaging, not a deep argument. The relation field is set to null-equivalence. Equivalence is assembled by constructor: reflexivity and symmetry are the existing lemmas on null-equivalence; the third leg applies the supplied transitivity hypothesis to an arbitrary triple of sequences.
why it matters
This is the hinge between the analytic triangle/transitivity work and the PRC real carrier. Downstream, the conditional real type is the quotient by this setoid; rational embedding sends a constant Cauchy ledger to that quotient; and the setoid-target theorem is literally the iseqv field of this construction. Completeness material uses the quotient map built from the same setoid once transitivity is discharged.
In the broader Recognition stack this is foundation plumbing for a real complete ordered field built from recognition ledgers and $J$-cost geometry, not a forcing-chain landmark (T5–T8) itself. It closes the setoid step once the triangle-modulus or direct transitivity target is proved, so the null-distance real quotient can be named and used.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.