negate_mk
plain-language theorem explainer
Negation on rational orbits commutes with the unit-denominator embedding of a signed orbit: negating the embedded value equals embedding the pointwise-swapped signed orbit. Anyone rewriting RatioOrbit arithmetic under simp will hit this lemma. The proof is pure definitional equality (rfl).
Claim. For every signed orbit $a$ (pair of distinction-naturals read as $\mathrm{pos}-\mathrm{neg}$), $\mathrm{negate}(\iota(a)) = \iota(\mathrm{negate}(a))$, where $\iota$ embeds $a$ as a rational orbit with unit denominator and $\mathrm{negate}$ on signed orbits swaps the two components.
background
This module builds integer and rational displays on top of the primitive recognition calculus (PRC) orbit layer. A SignedOrbit is a pair of distinction-naturals with intended meaning $\mathrm{pos}-\mathrm{neg}$ (K4.6). Pointwise negation swaps those two fields; it is named negate rather than neg to avoid clashing with structure fields.
A RatioOrbit is an integer numerator over a nonzero orbit denominator (K4.7). The constructor mk embeds a signed orbit as a rational with unit denominator, so integer arithmetic sits inside rational orbit arithmetic. The ambient setting is the IntegerRational layer of PRC: native cost and orbit arithmetic before continuum displays.
Upstream, the signed-orbit negate is the pure swap pos \mapsto neg, neg \mapsto pos. The rational-level negate acts on the numerator. This lemma records that those two views of sign flip agree on the image of mk.
proof idea
One-line definitional proof: rfl. After unfolding mk, rational negate, and signed-orbit negate, both sides are the same RatioOrbit constructor application (swapped numerator components, unit denominator, same nonzero proof). No lemmas are invoked; simp can fire the equality by reduction alone.
why it matters
The lemma is a small but necessary simp bridge in the IntegerRational foundation: without it, every rewrite that moves a sign across an integer-to-rational embedding must unfold definitions by hand. It sits under K4.6–K4.7 (signed and rational orbit displays) in Primitive Recognition Calculus, the discrete arithmetic layer that later feeds cost uniqueness and the forcing chain toward J-uniqueness (T5) and the phi fixed point (T6).
No downstream theorems currently list this declaration as a direct dependency in the graph, so its role is infrastructure for RatioOrbit algebra rather than a named paper proposition. It closes a definitional gap so later mass-ladder and cost identities can treat integer negation and rational negation interchangeably on pure integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.