PRCRealNegClosureTarget_proved
plain-language theorem explainer
Pointwise negation preserves the Cauchy property for PRC ledger sequences under J-cost distance. Anyone assembling the real complete ordered field from recognition calculus cites this to close negation on the Cauchy surface. The argument is short: reuse the original Cauchy witness and apply J-cost distance invariance under simultaneous negation of both endpoints.
Claim. For every Cauchy sequence $u$ of PRC rationals (measured by J-cost distance), the pointwise negated sequence $n \mapsto -u_n$ is again Cauchy: for every positive rational $\varepsilon$ there exists $N$ such that whenever $m,n \ge N$, the J-cost distance between $-u_m$ and $-u_n$ is strictly less than $\varepsilon$.
background
Primitive Recognition Calculus builds reals from ledger data rather than from classical Dedekind or Cauchy constructions imported wholesale. Sequences live on PRC rationals (ratio-orbit quotient classes), and the Cauchy surface uses J-cost distance: additive separation is sent through the positive ratio $1+(a-b)^2$, then scored by the PRC rational J-cost. A raw sequence is Cauchy when that distance eventually falls below every positive rational threshold.
Negation is defined pointwise on the raw ledger. The local target asserts that if $u$ is Cauchy, then the raw sequence of negated terms is Cauchy in the same metric. The key algebraic fact upstream is that J-cost distance is invariant under negating both endpoints: $d_J(-a,-b)=d_J(a,b)$. That identity is already proved by transport to a rational display and a ring normalization.
The module sits inside the ordered-field assembly path: once addition, multiplication, and negation close on Cauchy ledgers and respect null equivalence, the quotient can carry a complete ordered field structure.
proof idea
Term-mode proof of the universal target. Fix a Cauchy sequence $u$ and a positive rational $\varepsilon$. Unpack the Cauchy witness $N$ for $u$ at $\varepsilon$. Reuse the same $N$ for the negated raw sequence. For indices $m,n\ge N$, the goal is $d_J(-u_m,-u_n)<\varepsilon$. Rewrite by the endpoint-negation invariance of J-cost distance, which reduces the inequality to $d_J(u_m,u_n)<\varepsilon$, exactly the original Cauchy bound.
why it matters
Negation closure is one of the exact blockers on the path from PRC Cauchy ledgers to a complete ordered field. Downstream, the conditional certificate for the real complete ordered field packages this proved target among the closure and congruence obligations (Order step 10, first pass). The promoted certificate likewise wires the same fact as the negation-closure field of the promoted structure.
Without this lemma, pointwise negation would not descend to the null-equivalence quotient, so the additive inverse on PRC reals would be ill-defined or would leave the Cauchy surface. In the broader Recognition stack this is pure foundation work: it supplies the ordered-field carrier on which later forcing (J-uniqueness, $\varphi$, eight-tick structure, $D=3$) can be stated over a completed continuum rather than over rationals alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.