abs_sub_zero_eq
plain-language theorem explainer
Absolute value is invariant under subtracting zero on signed orbits: |a − 0| = |a|. Authors of the integer-order surface and its closure certificate cite this when normalizing signed differences before comparing magnitudes. The proof injects through the natural display of absolute value and reduces via the integer embedding of subtraction and zero.
Claim. For every signed orbit $a$, $\lvert a - 0 \rvert = \lvert a \rvert$, where absolute value is the orbit-position absolute difference of the positive and negative legs, and $0$ is the zero signed orbit.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: a pair of distinction-nat legs (pos, neg) with intended meaning pos − neg. DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Absolute value of a signed orbit is the orbit-position absolute difference of those two legs, displayed on naturals by Int.natAbs of the integer embedding.
Subtraction of signed orbits is defined so that its integer embedding is ordinary integer subtraction; the zero signed orbit embeds to 0. The local module builds the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). Upstream lemmas already equate the natural display of absolute value with Int.natAbs of the embedding, and equate the embedding of a difference with the difference of embeddings.
proof idea
Apply injectivity of the natural display on distinction-nats, so it suffices to check equality after toNat. Rewrite both sides with the absolute-value display lemma, then rewrite the left-hand difference using the integer embeddings of subtraction and of zero. The resulting identity Int.natAbs (a.toInt − 0) = Int.natAbs a.toInt is discharged by simp.
why it matters
Feeds the integer-order certificate, which asserts that the internal signed-orbit order surface is closed (nonnegativity, absolute-difference display, truncated subtraction, and related flag equalities). Without |a − 0| = |a|, magnitude comparisons after normalization against zero would not match the bare absolute value used elsewhere in the order surface. This is foundation scaffolding for the integer layer beneath the forcing chain, not a physics landmark itself; it keeps the signed-orbit model coherent before later rungs (J-cost, φ-ladder, eight-tick structure) are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.