sub_toInt
plain-language theorem explainer
The integer display of a signed-orbit difference equals the difference of the two displays. Anyone proving absolute-value, order, or balance facts for signed orbits cites this homomorphism. The proof unfolds subtraction as addition of the pointwise negate, rewrites by the already-proved add and negate maps, and closes by ring arithmetic on ℤ.
Claim. Let $a,b$ be signed orbits (each a pair of distinction-naturals read as positive part minus negative part). Writing $(\cdot)^{\mathbb{Z}}$ for the integer display map, $(a-b)^{\mathbb{Z}} = a^{\mathbb{Z}} - b^{\mathbb{Z}}$.
background
In the primitive recognition calculus, a signed orbit is a pair (pos, neg) of distinction-naturals, intended as the difference pos − neg (K4.6). Its integer display is the ordinary difference of the underlying natural values: $z^{\mathbb{Z}} = \mathrm{toNat}(z.\mathrm{pos}) - \mathrm{toNat}(z.\mathrm{neg})$.
Pointwise negation swaps the two components, and the module already proves that this display sends negation to ordinary integer negation and addition of signed orbits to addition of integers. Subtraction is defined as addition of the negate, so the present statement is the remaining ring-homomorphism identity for difference.
The surrounding module builds integers and rationals from orbit arithmetic rather than postulating ℤ; the display map is the verifier bridge from that constructive carrier into Mathlib integers.
proof idea
Term-mode proof. First rewrite the goal by the definition of subtraction: show that the display of add a (negate b) equals $a^{\mathbb{Z}} - b^{\mathbb{Z}}$. Apply the upstream lemmas that the display preserves addition and that the display of the pointwise negate is ordinary negation. The resulting identity on ℤ is closed by ring.
why it matters
This is the subtraction half of the display homomorphism for signed orbits. Downstream order machinery depends on it heavily: absolute value of a difference vanishes iff the inputs are balanced; the triangle inequality for absolute difference; absolute value of $a-0$ and $0-a$; and several balance-transport lemmas that move balanced pairs across a subtraction. Without the identity, those rewrites cannot pass from orbit syntax to integer arithmetic (omega, natAbs, etc.).
In the Recognition foundation stack this sits under the forcing of integers from logic/orbit structure, feeding the integer-order layer that later supports rational and field constructions. It is pure carrier algebra, not a physics forcing step (T5–T8), but it is load-bearing scaffolding for any later numeric claim stated in signed-orbit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.