forced_difference_zero_iff
plain-language theorem explainer
Forced natural numbers have vanishing integer difference exactly on the diagonal: their displays in ℤ coincide iff the two values are equal. Anyone working the additive side of UniversalForcing (integers as forced differences) cites this null-locus law. The proof is a short bidirectional argument: display injectivity one way, substitution with ring the other.
Claim. For natural numbers $a$ and $b$ forced by the Law of Logic, writing $n(a)$ and $n(b)$ for their integer displays, one has $n(a)-n(b)=0$ if and only if $a=b$.
background
LogicNat is the inductive type of natural numbers forced by the Law of Logic: identity is the zero-cost element and step iterates the generator, mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive ray closed under multiplication by the generator. The display map sends each such value to an ordinary nonnegative integer, recovering the usual counting interpretation.
This module (UniversalForcing.ForcedIntegers) builds the additive layer parallel to ForcedRatios. Differences of displays are the forced integers; the present statement identifies when such a difference is the additive identity. The doc-comment frames it as the additive null locus $a=b$, mirroring the multiplicative unit locus on forced ratios.
Upstream, injectivity of the display map is the key prior: equal displays force equal LogicNat values. That fact, with elementary arithmetic on $\mathbb{Z}$, pins the null locus to the diagonal.
proof idea
Bidirectional constructor. Forward: from $n(a)-n(b)=0$, omega yields $n(a)=n(b)$, then apply injectivity of the display map to conclude $a=b$. Reverse: substitute $a=b$ and finish by ring (the difference is identically zero). No deep lemmas beyond display injectivity and the arithmetic tactics.
why it matters
This is the additive null-locus law, the direct counterpart of the multiplicative unit locus on ForcedRatios. Downstream, forced_difference_fixed_iff rewrites through the negation-swap identity and applies this theorem to prove that negation fixes a forced difference exactly on the diagonal $a=b$: "the additive analogue of the reciprocal fixed-point law." The two forced layers (integers and ratios) then carry the same comparison geometry: an involution that swaps two counts, fixed precisely where the counts agree.
In the Recognition Science foundation, integers arise as forced differences of LogicNat counts inside UniversalForcing, feeding the arithmetic substrate beneath the forcing chain and the ledger. Closing the diagonal characterization keeps the additive and multiplicative forced layers on the same geometric footing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.