PRCNullDistanceTransitiveTarget_of_triangle_modulus
plain-language theorem explainer
The local triangle modulus for J-cost rational distance implies transitivity of null-equivalence on PRC Cauchy sequences. Anyone building the null-distance quotient (the PRC real carrier) cites this reduction. The argument is pure index bookkeeping: pull a smaller tolerance from the modulus, stabilize both legs past a common orbit index, and reassemble.
Claim. Assume that the $J$-cost rational distance has a local triangle modulus: for every positive rational tolerance $\varepsilon$ there is a positive $\delta$ such that two legs each smaller than $\delta$ force the composed leg below $\varepsilon$. Then null-equivalence of PRC Cauchy sequences is transitive: if $u\sim v$ and $v\sim w$, then $u\sim w$.
background
In the Primitive Recognition Calculus, candidate reals are Cauchy sequences of PRC rationals. Two sequences are null-equivalent when their pairwise $J$-cost distance eventually falls below every positive rational tolerance. The exact blocker for the final null-distance quotient is transitivity of that relation (PRCNullDistanceTransitiveTarget).
The sharper analytic hypothesis is the triangle modulus on the $J$-cost distance surface itself: for each positive $\varepsilon$ one finds a positive $\delta$ so that $d_J(a,b)<\delta$ and $d_J(b,c)<\delta$ imply $d_J(a,c)<\varepsilon$. That property is the named hypothesis of this theorem. The module sits in the foundation layer that constructs logic-native reals by quotienting completed orbits; once null-equivalence is a setoid, the PRC real carrier is the corresponding quotient.
proof idea
Tactic proof, not a one-liner. Fix Cauchy sequences $u,v,w$ with $u\sim v$ and $v\sim w$, and fix a positive tolerance $\varepsilon$. From the triangle-modulus hypothesis obtain a positive $\delta$ that forces the composed leg below $\varepsilon$. Apply null-equivalence of $(u,v)$ and of $(v,w)$ at that $\delta$ to get stabilizing indices $N_{uv}$ and $N_{vw}$. Take $N=\max(N_{uv},N_{vw})$. For every $n\ge N$, both legs at term $n$ are $<\delta$, so the modulus yields $d_J(u_n,w_n)<\varepsilon$. The only arithmetic used is transitivity of $\le$ on the index naturals (via le_trans and Nat.le_max_*).
why it matters
This is the bridge from the analytic $J$-cost triangle modulus to the setoid structure on null distance. Downstream, PRCNullDistanceSetoidTarget_of_triangle_modulus feeds this lemma into the setoid target, and real_null_setoid_conditional_certificate packages it as Order step 9 conditional closure: once the local modulus is proved, no quotient mechanics remain. The sibling PRCNullDistanceTransitiveTarget_proved discharges the target outright by supplying the proved modulus. In the broader RS stack this clears the path to the PRC real carrier (Cauchy ledgers quotiented by null distance), which underpins later continuum constructions sitting above the forcing chain and the Recognition Composition Law for $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.