abs
plain-language theorem explainer
Absolute value on a signed orbit difference returns the unsigned distinction-orbit distance between its positive and negative legs. Anyone building integer or rational magnitudes from primitive recognition orbits cites it when a non-negative size is required. The body is a one-line application of absolute difference to the two components.
Claim. Let $z=(p,n)$ be a signed orbit difference of finite distinction-orbit positions (intended meaning $p-n$). Its absolute value is the absolute difference $|p-n|$, returned as a distinction-orbit natural.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: zero and successor only, with no preferred radix. Signed orbits (K4.6) package a pair of such positions (pos, neg) with intended meaning pos - neg, the internal stand-in for an integer difference before quotienting to logic integers.
Absolute difference of two orbit positions is defined by truncated subtraction in both orders: $|a-b| := (a\dot{-}b)+(b\dot{-}a)$. That construction is already available in this module and is the only arithmetic ingredient needed here.
The local setting is the IntegerRational layer of the foundation stack: integers and rationals assembled from orbit arithmetic rather than assumed as primitives. Absolute value is the bridge from a signed pair back to a single non-negative orbit position.
proof idea
One-line definitional wrapper. Unpack the signed orbit into its positive and negative legs and apply the existing absolute-difference operator on distinction-orbit naturals. No further lemmas or case splits are required.
why it matters
Signed orbits are the K4.6 carrier for integer-like differences inside the recognition calculus. Absolute value recovers a pure magnitude, which is what cost comparisons, truncation lemmas, and later rational constructions need when only size (not sign) enters the argument.
It sits beside toInt, zero, and the truncated-subtraction family in the same module, closing the basic signed-arithmetic toolkit before rationals-from-logic. Downstream magnitude and bound arguments across constants and cosmology ultimately rest on having a well-defined non-negative size for such differences; this definition is the orbit-native form of that size.
No forcing-chain step (T5–T8) is discharged here; the declaration is pure scaffolding for the integer layer that those later numerical claims consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.