PRCRawNeg

In the Primitive Recognition Calculus path to a real complete ordered field, a raw rational ledger is simply a sequence of PRC rationals indexed by ℕ, written before any Cauchy certificate is attached. The forgetful map raw strips a Cauchy ledger down to this underlying sequence.

Field operations are first defined on these raw sequences, then lifted through Cauchy and null-equivalence quotients. Negation is the additive inverse candidate: apply ordinary rational negation at each index. The same pattern is used for addition and multiplication on raw ledgers in this module.

Distance and Cauchy-ness are measured with the J-cost distance inherited from the recognition cost functional, not the usual absolute-value metric; that enters only when one asks whether the negated sequence remains Cauchy.

Pure definition: the returned ledger is the function fun n => -u n. No lemmas, no tactics, no side conditions. Downstream targets must still prove that this operation preserves the Cauchy predicate and respects null equivalence.

This is the raw carrier for additive inverse in the PRC construction of ℝ. It is the operand in the two exact blockers PRCRealNegClosureTarget (pointwise negations of Cauchy ledgers are Cauchy) and PRCRealNegCongruenceTarget (negation respects null equivalence on the quotient). Until those Props are discharged, the real completion cannot carry a well-defined group inverse. The definition itself is scaffolding-free; the open work sits in those closure and congruence targets that cite it.