toInt_negate
plain-language theorem explainer
Negation on PRC integers is compatible with the integer display: the display of a negated class equals the ordinary additive inverse of its display. Anyone assembling ring operations on the signed-orbit quotient cites this simp fact. The proof is quotient induction that reduces immediately to the pointwise signed-orbit identity.
Claim. For every PRC integer $a$ (a class of signed orbits under the balanced-length relation), the integer display of its negation equals the additive inverse of its display: $\mathrm{toInt}(\mathrm{negate}\,a)=-\mathrm{toInt}(a)$.
background
In the Primitive Recognition Calculus, integers are not postulated. A signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg. Pointwise negation swaps the two components. PRC integers are the quotient of signed orbits by the internal balanced-length setoid; the verifier map toInt sends a class to an ordinary ℤ value.
The sibling lemma on representatives already records that swapping components negates the integer difference: (negate a).toInt = -a.toInt for a raw SignedOrbit, proved by a one-line ring calculation on the two toNat casts. The present statement lifts that identity through the quotient constructor so that arithmetic on classes matches arithmetic on displays.
Local setting is K4.8 of the IntegerRational module: build PRC integers as signed-orbit classes and prove that the display into ℤ is a well-behaved homomorphism before injectivity is stated.
proof idea
Term-mode proof by quotient induction. Apply Quot.induction_on to the class a, reducing the goal to the representative form (SignedOrbit.negate a).toInt = -a.toInt. Discharge that goal by the upstream lemma SignedOrbit.negate_toInt, which expands both sides as differences of natural casts and finishes with ring. No setoid-respect side conditions appear because toInt and negate are already defined to descend.
why it matters
This is a small but load-bearing simp lemma in the K4 integer package. Downstream, toInt_sub defines subtraction as add a (negate b) and rewrites via toInt_add and toInt_negate to obtain (sub a b).toInt = a.toInt - b.toInt. Without the present identity, the display would not be a group homomorphism, and later injectivity of toInt (K4.8) would not connect distinct classes to distinct verifier integers.
In the broader Recognition foundation, integers are forced from logic rather than assumed (cf. IntegersFromLogic / ForcedIntegers). Compatibility of negation with the display is one step in showing that the PRC construction recovers ordinary ℤ arithmetic, which later supports mass-ladder bookkeeping and discrete counting on the eight-tick octave. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.