PRCRealNegClosureTarget
plain-language theorem explainer
Defines the exact closure obligation for negation on PRC Cauchy ledgers: pointwise negation of any Cauchy sequence remains Cauchy under J-cost distance. Cited by the complete-ordered-field target bundle and its conditional/promoted certificates. Pure Prop packaging; the content is discharged by the companion proved theorem.
Claim. The negation-closure target asserts: for every PRC Cauchy sequence $u$, the raw ledger $n \mapsto -u_n$ is itself Cauchy with respect to $J$-cost distance (for every positive rational tolerance $\varepsilon$ there exists $N$ such that $m,n \ge N$ implies $d_J(-u_m,-u_n) < \varepsilon$).
background
In the Primitive Recognition Calculus real-completion layer, reals are built as null-quotients of Cauchy sequences of PRC rationals. A PRC Cauchy sequence is an orbit-indexed rational ledger whose pairwise $J$-cost distance eventually falls below every positive rational tolerance. The raw forgetful map extracts the underlying term function; the raw Cauchy predicate is the same eventual smallness condition written on bare ledgers.
Pointwise negation on raw ledgers is $n \mapsto -u_n$. For the null quotient to carry a well-defined additive inverse, this operation must preserve the Cauchy property and respect null equivalence. The present definition isolates the first of those two obligations as a named Prop target.
The ambient module assembles exact blockers for addition, negation, and multiplication (closure and congruence) before packaging them into a conditional complete-ordered-field certificate.
proof idea
No proof body: this is a bare Prop abbreviation equating the name to the universal statement $\forall u,\ \mathrm{PRCRawCauchy}(\mathrm{PRCRawNeg}, u.\mathrm{raw})$. The mathematical work lives in the companion theorem that discharges it by reusing $u$'s Cauchy witness and the $J$-cost invariance $d_J(-a,-b)=d_J(a,b)$.
why it matters
Negation closure is one of the exact blockers bundled in the complete-ordered-field targets structure (field neg_closure). The conditional certificate and the promoted Step-10 certificate both require this target before they can expose a closed additive inverse on the null quotient. The companion proved theorem already discharges it, so the definition is the stable interface that lets later packaging treat negation as a finished obligation rather than an open scaffold. In the broader Recognition foundation this is plumbing toward an internal complete ordered field on the PRC carrier, not a physics forcing step (T0–T8), but it is required infrastructure for any real-analytic layer built on the $J$-cost metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.