PRCNullDistanceTransitiveTarget
plain-language theorem explainer
Names the exact Prop that null-equivalence of PRC Cauchy ledgers is transitive. Anyone building the real quotient from J-cost distance cites this as the remaining setoid obligation after reflexivity and symmetry. The body is a pure universal statement over three Cauchy sequences; no proof is attached here.
Claim. The target proposition asserts: 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$. Null-equivalence means that the J-cost distance between corresponding terms eventually falls below every positive PRC rational tolerance.
background
In the Primitive Recognition Calculus real construction, a PRC Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually drops below every positive PRC rational $\varepsilon$. The intended identification on that carrier is null-equivalence: two ledgers $u,v$ satisfy $\mathrm{PRCNullEquivalent},u,v$ when $\mathrm{PRCJCostDistance}(u_n,v_n)$ is eventually smaller than every positive tolerance.
Reflexivity and symmetry of that relation are already available on the Cauchy module. What remains for a setoid (and thus a quotient carrier for PRC reals) is triangle-style transitivity. Upstream setoid patterns in the logic-native integers and rationals follow the same shape: a relation plus refl/symm/trans packaged as Setoid.
The module keeps the final null-distance quotient as an exact Lean target rather than aliasing classical $\mathbb{R}$. This definition is that target Prop.
proof idea
No proof: this is a bare def of a Prop. The right-hand side is the standard three-variable transitivity schema specialized to null-equivalence of PRC Cauchy sequences. Downstream proofs discharge it by reducing to a triangle-modulus inequality for the J-cost distance surface, then applying the specialized constructor that turns a transitivity witness into a setoid.
why it matters
This is the exact blocker for the final null-distance quotient in the PRC real stack. Downstream, a transitivity witness feeds PRCNullDistanceSetoidOfTransitive, which installs null-equivalence as a Setoid on Cauchy ledgers; from that come the setoid-target theorem, the rational embedding ofRat, and the quotient type PRCRealNull.
The proved discharge path is PRCNullDistanceTransitiveTarget_proved, obtained from the triangle-modulus target via PRCNullDistanceTransitiveTarget_of_triangle_modulus, and recorded in the Build Order step 9c certificate alongside the increment formula for J-cost distance. The first-pass real Cauchy certificate deliberately leaves this quotient obligation explicit rather than hiding it behind a classical real alias.
In framework terms this sits under the foundation forcing chain: once the J-cost surface supports a genuine metric-style triangle inequality on Cauchy ledgers, the recognition-native reals exist as a quotient without external analysis axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.