truncatedSub
plain-language theorem explainer
Truncated subtraction on finite δ-orbit positions: monus on the free inductive type generated by zero and successor. When the subtrahend exceeds the minuend the result is zero; otherwise it is ordinary difference. Downstream Euclidean division, GCD, absolute difference, and the integer-order certificate all call it. The body is pure structural recursion on both arguments.
Claim. Define truncated subtraction $\ominus$ on finite $\delta$-orbit positions by structural recursion: $a \ominus 0 = a$, $0 \ominus (n+1) = 0$, and $(a+1) \ominus (b+1) = a \ominus b$. Equivalently, $a \ominus b$ is the unique orbit position whose verifier natural is $\max(a^{\mathbb{N}} - b^{\mathbb{N}}, 0)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, isomorphic to ordinary Nat but kept internal to the recognition calculus so that arithmetic is not imported from the verifier. Successor is one more application of the generator, matching the Peano structure proved rather than assumed in ArithmeticFromLogic.
This module builds integer and rational structure on those orbits. Truncated subtraction (monus) is the first arithmetic primitive that is not mere addition of orbit lengths: it must stay inside DistinctionNat, so underflow is clamped to zero rather than producing a signed value.
The definition depends only on the inductive shape of DistinctionNat and the successor constructor; no external Nat subtraction is used in the body.
proof idea
Definition by pattern matching, not a proof. Three exhaustive cases on the pair of constructors: minuend against zero returns the minuend; zero against a successor returns zero; both successors recurse on the predecessors. Termination is immediate from structural descent on both arguments. No lemmas are applied.
why it matters
This is the internal monus that lets the recognition calculus do subtraction without leaving the δ-orbit type. Absolute difference is defined as truncatedSub a b + truncatedSub b a. The verifier display theorem toNat_truncatedSub proves that the definition matches ordinary Nat monus after toNat.
Fuelled Euclidean division (divModFuel) and subtractive GCD (gcdFuel) repeatedly call it to reduce the dividend. IntegerOrderCertificate requires truncated_sub_display: for all orbit positions, (truncatedSub a b).toNat equals a.toNat - b.toNat. That certificate is the step-1 bridge from internal signed-orbit order to verifier integers, so the definition sits on the path from primitive distinction orbits toward integer and rational structure in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.