PRCRealNegCongruenceTarget
plain-language theorem explainer
Negation is well-defined on the null quotient of PRC Cauchy ledgers: if two Cauchy sequences are null-equivalent under J-cost distance, their pointwise negations remain null-equivalent as raw ledgers. Anyone building the real carrier from the recognition calculus cites this as the exact congruence blocker for unary minus. The declaration is a pure Prop target; the companion proof discharges it by transporting the Cauchy tail through pointwise sign flip.
Claim. For all PRC Cauchy sequences $u,v$, if $u$ and $v$ are null-equivalent (J-cost distance of corresponding terms eventually below every positive rational tolerance), then the pointwise negations of their underlying raw rational ledgers are likewise null-equivalent.
background
The Primitive Recognition Calculus constructs candidate reals as Cauchy ledgers of PRC rationals, with distance measured by the J-cost metric rather than absolute value. A PRC Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually falls below every positive PRC rational tolerance. Null equivalence says that two such ledgers stay J-close termwise in the tail; it is the intended kernel of the real quotient once transitivity is available.
Raw operations act pointwise on the forgotten term map: negation sends $n \mapsto -u_n$. Raw null equivalence is the same tail-closeness predicate on those maps. This module packages the exact blockers needed before the null quotient can carry a complete ordered-field structure; the present definition isolates the congruence half of the negation package.
proof idea
No proof body: this is a bare Prop definition naming the congruence obligation. The mathematical content is the universal statement that null equivalence of Cauchy ledgers implies raw null equivalence of their pointwise negations. Discharge lives in the companion theorem, which unpacks the null-equivalence witness at a given tolerance, reuses the same tail index, and applies J-cost symmetry under sign flip on corresponding terms.
why it matters
Without negation congruence, unary minus does not descend to the null quotient, so the real carrier cannot yet be an additive group. The target is bundled into PRCRealCompleteOrderedFieldTargets as neg_congruence and is required by the conditional complete-ordered-field certificate and the promoted Step 10 certificate. The companion proved theorem closes this blocker; together with the matching closure target it lets the internal null quotient support the additive inverse surface demanded by the complete ordered-field layer of the recognition foundation. This is infrastructure under the forcing chain's real-analytic substrate, not a T0–T8 landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.