forced_difference_neg_swap
plain-language theorem explainer
Negation swaps the two sides of a forced difference of logic-naturals: −(ι(a)−ι(b))=ι(b)−ι(a). Anyone comparing the integer layer to the ratio layer cites this as the additive twin of reciprocal swap. The proof is a one-line ring identity on ℤ.
Claim. For logic-naturals $a,b$ with embedding $\iota$ into $\mathbb{Z}$, $-( \iota(a) - \iota(b) ) = \iota(b) - \iota(a)$.
background
Logic-naturals are the inductive type forced by the Law of Logic: identity is the zero-cost unit and step iterates the generator, mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. The local map $\iota$ sends each such count into $\mathbb{Z}$ (nonnegative image), so differences $\iota(a)-\iota(b)$ are ordinary integers.
The module builds the forced integer layer parallel to forced ratios. On ratios the reciprocal automorphism swaps $a/b$ to $b/a$. Here negation plays the same role for differences. The surrounding UniversalForcing development treats both layers as comparison geometries with an involution fixed exactly on the diagonal.
proof idea
One-line tactic proof: ring closes the identity $-(x-y)=y-x$ in the ring $\mathbb{Z}$ after unfolding the two embeddings. No Recognition-specific lemmas are required beyond the fact that $\iota(a),\iota(b)$ land in $\mathbb{Z}$.
why it matters
Feeds forced_difference_fixed_iff, which states that negation fixes a forced difference if and only if $a=b$. That parent is the additive analogue of the reciprocal fixed-point law on forced ratios: the involution is fixed precisely where the two counts agree.
Together the pair shows that the integer and ratio layers carry the same comparison geometry inside UniversalForcing. It sits in the foundation stack that recovers arithmetic from logic before the T0–T8 forcing chain (J-uniqueness, $\varphi$, eight-tick, $D=3$) is applied to physics. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.