add_left_cancel
plain-language theorem explainer
Left cancellation for addition on distinction orbits: equal left sums force equal right summands. Anyone building arithmetic or cancellation lemmas on the primitive orbit type cites this. The proof pushes the equality through the verifier map toNat, rewrites with the addition recovery lemma, and finishes by ordinary Nat left cancellation plus injectivity.
Claim. Let $a,b,c$ be positions on the base-neutral distinction orbit. If $a+b=a+c$, then $b=c$.
background
DistinctionNat is the inductive orbit of repeated distinction (zero and successor), the base-neutral finite counter introduced in the primitive recognition calculus. Addition on this type is defined by recursion on the second argument, parallel to Peano addition.
The verifier map toNat sends each orbit position to an ordinary natural number by counting successors. The sibling lemma toNat_add states that this map is a homomorphism for addition: the image of a sum is the sum of the images. Injectivity of toNat (toNat_inj) recovers equality of orbits from equality of counts.
The same cancellation pattern already appears for LogicNat in ArithmeticFromLogic, proved by transferring through its own recovery isomorphism. Here the argument is specialized to the distinction-orbit carrier used by the primitive calculus.
proof idea
Apply injectivity of toNat so it suffices to show the Nat images of b and c agree. From the hypothesis a+b=a+c, congruence under toNat yields equal images of the two sums. Rewrite both sides with toNat_add to obtain toNat(a)+toNat(b)=toNat(a)+toNat(c). Finish with Mathlib's Nat.add_left_cancel.
why it matters
This is K4.5 in the orbit-arithmetic layer: left cancellation for the primitive distinction counter. The immediate sibling add_right_cancel is proved from it by commuting summands. Downstream, ArithmeticFromLogic reuses the same cancellation shape for LogicNat; DeltaSpine.CostUniqueness invokes cancellation when deriving reciprocal symmetry of the d'Alembert cost from the law and normalization; cosmology (RefineTrigger.lossless_iff) and gravity (QuotientFirstZ fiber-excess IFF) sit further along chains that need clean additive cancellation on discrete counters.
In the Recognition forcing picture this is scaffolding arithmetic, not a T0–T8 landmark itself, but it keeps the orbit monoid cancellative so later uniqueness and reconstruction arguments do not accumulate slack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.