toInt_neg'

PRC integers (PRCInt) are the K4.8 construction of integers inside Primitive Recognition Calculus: quotient classes of signed orbits under the internal balanced-length relation. A signed orbit carries a positive and a negative orbit component; the verifier display into ordinary integers is the difference of their natural lengths, $\mathrm{toInt}(z) = z_{\mathrm{pos}} - z_{\mathrm{neg}}$ on representatives, lifted through the quotient.

Negation on PRCInt swaps the positive and negative legs of a representative (up to the setoid). The same display map appears upstream as the recovery map from logic-integers and as the iteration-count embedding of forced naturals; here it is specialized to the signed-orbit model.

The local module builds integer and rational structure on these quotient classes so that later recognition calculus can treat discrete counts without assuming $\mathbb{Z}$ as a primitive.

One-line simp. Unfolding toInt on the quotient and the definition of negation on signed-orbit representatives reduces both sides to the same integer difference with swapped signs, which Mathlib's simp set closes immediately. No separate lemmas are invoked beyond the definitional equations of the display and the quotient constructor.

K4.8 needs the display $\mathrm{PRCInt}\to\mathbb{Z}$ to be a group homomorphism so that recognition-native integers can be identified with ordinary integers for counting, rungs, and octave arithmetic. Preservation of negation is the first nontrivial sign law after zero preservation; together they underwrite additive structure used when the phi-ladder and eight-tick constructions talk about integer offsets.

No downstream dependents are recorded yet in the graph, so this is infrastructure rather than a leaf of a larger proved chain. It sits in the Foundation layer that feeds the forcing path (T0–T8) once discrete arithmetic is available, but it does not itself force $\varphi$, dimension, or the Recognition Composition Law.