forced_difference_fixed_iff
plain-language theorem explainer
Negation fixes a forced difference of two logic-naturals if and only if those naturals are equal. Anyone citing the forced-integers certificate or the additive mirror of the ratio-layer fixed-point law needs this biconditional. The proof rewrites via the negation-swap identity, then splits: one side reduces the fixed-point equation to a zero difference and applies the zero-iff lemma; the other substitutes equality and closes by ring.
Claim. For logic-naturals $a,b$, writing $n\mapsto\iota(n)$ for the forced embedding into $\mathbb{Z}$, one has $\iota(a)-\iota(b)=-(\iota(a)-\iota(b))$ if and only if $a=b$.
background
Logic-naturals (LogicNat) are the Peano object forced by the Law of Logic: two constructors, identity (zero-cost unit) and step (one generator iterate), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. The local map $\iota$ embeds them into $\mathbb{Z}$, preserving $0,1,+$, and $\times$, as part of the forced-arithmetic layer built on the canonical initial Peano object.
This module develops the additive group of integers as forced by distinction: differences of embedded counts exhaust $\mathbb{Z}$, and comparison geometry is carried by the negation involution $d\mapsto -d$. The companion facts already proved are that a difference vanishes exactly on the diagonal, and that negation swaps the two orderings of a pair.
The doc-comment frames the result as the additive twin of the reciprocal fixed-point law on the ratio layer: an involution that swaps two counts is fixed precisely where the counts agree.
proof idea
Rewrite the goal with the sibling forced_difference_neg_swap, which turns the fixed-point equation into an equivalent form under order swap. Split the biconditional.
Forward: from $\iota(a)-\iota(b)=-(\iota(a)-\iota(b))$, omega forces the difference to be zero; apply forced_difference_zero_iff to conclude $a=b$.
Reverse: substitute $a=b$ and close by ring (the difference is zero, hence equal to its negative).
why it matters
Feeds directly into forcedIntegersCert_holds, the certificate that forced arithmetic embeds in $\mathbb{Z}$ preserving $0,1,+$,$\times$, that differences are exactly $\mathbb{Z}$, and that the negation involution fixes a difference precisely on the diagonal. The certificate doc states that "the integer layer the δ paper names is forced, canonical, and carries the additive mirror of the ratio layer's comparison geometry."
In the Recognition framework this seals the additive half of the comparison geometry that parallels the ratio layer (reciprocal fixed on the unit). It is foundation scaffolding for the integers that sit under later forcing (mass ladder, calibration), not a T5–T8 landmark itself, but the discrete additive group those landmarks presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.