PRCRealNegCongruenceTarget_proved
plain-language theorem explainer
Negation of Cauchy ledgers preserves null equivalence: if two sequences are null-equivalent, so are their pointwise negations. Anyone assembling the PRC real quotient as a complete ordered field cites this to make negation well-defined on the null-distance quotient. The argument is a short term proof that rewrites J-cost distance under simultaneous negation and reuses the original Cauchy tail witness.
Claim. If $u$ and $v$ are PRC Cauchy sequences that are null-equivalent (their J-cost distance tends to zero in the PRC rationals), then the pointwise-negated raw ledgers are likewise null-equivalent: $-u$ and $-v$ have J-cost distance tending to zero.
background
In the Primitive Recognition Calculus, candidate reals are Cauchy sequences of PRC rationals. Cauchy-ness and null equivalence are measured by the J-cost distance, which routes additive separation through the positive ratio $1+(a-b)^2$ and then applies the PRC rational J-cost. Two Cauchy sequences are null-equivalent when that distance eventually falls below every positive rational threshold.
This module builds a complete ordered field on the quotient of Cauchy sequences by null equivalence. For negation to descend to the quotient, it must respect the relation: if $u\sim v$ then $-u\sim -v$. The named target is exactly that congruence obligation, recorded as the blocker for negation quotient well-definedness.
The key upstream algebraic fact is invariance of J-cost distance under simultaneous negation of both arguments. Order and distance live on PRC rationals, themselves ratio-orbit quotient classes.
proof idea
Fix null-equivalent Cauchy sequences $u,v$ and a positive rational threshold $\varepsilon$. Unpack the null-equivalence witness to a tail index $N$ beyond which the J-cost distance of the terms is strictly less than $\varepsilon$. Reuse the same $N$ for the negated sequences. On each tail index, change the goal to the strict order statement for the distance between $-u_n$ and $-v_n$, rewrite by the lemma that J-cost distance is unchanged under simultaneous negation of both arguments, and apply the original tail bound.
why it matters
This discharges the negation-congruence blocker in both the conditional and promoted certificates for a PRC complete ordered field. Those certificates reduce Order step 10 (quotient algebra) to exact closure and congruence targets; with this target proved, pointwise negation lifts through the null-distance quotient via the conditional negOf constructor on the closed null quotient.
It sits in the foundation layer that reconstructs the reals from recognition primitives, before the forcing chain (T0–T8) and physical constants attach. Sibling targets handle addition and multiplication congruence and the three closure obligations; this one closes only the negation half of well-definedness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.