PRCNullDistanceTransitiveTarget_proved
plain-language theorem explainer
Null-distance equivalence on PRC Cauchy sequences is transitive, so the relation is a genuine equivalence and the null-distance quotient is well-defined. Anyone building the PRC real carrier or embedding rationals into it cites this. The proof is a one-line application of the triangle-modulus bridge to the already-proved J-cost triangle modulus.
Claim. For all PRC Cauchy sequences $u,v,w$, if $u$ is null-equivalent to $v$ and $v$ is null-equivalent to $w$, then $u$ is null-equivalent to $w$.
background
Primitive Recognition Calculus builds a real carrier from Cauchy ledgers on a J-cost distance surface. Two sequences are null-equivalent when their J-cost distance can be driven below every positive threshold along a completed orbit; the intended reals are the quotient of Cauchy sequences by that relation.
The exact blocker for that quotient is the Prop PRCNullDistanceTransitiveTarget: triangle-style transitivity of null-equivalence on PRCCauchySeq. Upstream, the analytic triangle modulus for the J-cost distance has already been closed by an explicit rational increment estimate (PRCJCostDistanceTriangleModulusTarget_proved). A separate bridge lemma records that any such modulus is enough for null-distance transitivity, with only completed-orbit index bookkeeping left.
proof idea
One-line term wrapper. Feed the proved J-cost triangle modulus (PRCJCostDistanceTriangleModulusTarget_proved) into PRCNullDistanceTransitiveTarget_of_triangle_modulus, which states that the analytic triangle modulus is sufficient for null-distance transitivity. That bridge unpacks the modulus at a given $\varepsilon$, obtains a positive $\delta$, and chains the two null-equivalence witnesses through completed-orbit indices; none of that bookkeeping is repeated here.
why it matters
This discharges the last equivalence-law obligation for the null-distance setoid. Downstream, PRCRealNullClosed is defined as the Cauchy-ledger quotient under this proved transitivity, and ofRat embeds PRC rationals into that closed carrier. Completeness work (PRCRawCauchyQuotientPointTarget_proved) builds quotient points via the setoid of this transitive relation. The module certificate prc_jcost_distance_increment_triangle_certificate packages the whole increment-triangle chain; this theorem is the setoid-facing tip of that chain. In the broader RS foundation it supplies the real carrier on which later forcing and constant extractions sit, without itself invoking T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.