abs_add_le_add_abs
plain-language theorem explainer
The triangle inequality holds for absolute value on signed orbits: |z+w| ≤ |z|+|w| as a Boolean comparison on distinction naturals. Anyone building order or metric structure on the internal integer model cites this. The proof rewrites both sides through the Int recovery maps and applies the standard Mathlib fact Int.natAbs_add_le.
Claim. For any signed orbits $z,w$, the Boolean order on distinction naturals satisfies $\mathrm{leq}(|z+w|,\,|z|+|w|)=\mathrm{true}$, i.e. $|z+w|\le|z|+|w|$ after recovery to ordinary integers.
background
Signed orbits are the internal integer model in Primitive Recognition Calculus: each value is a pair of finite δ-orbit positions (positive and negative legs). Absolute value is the distinction-natural absolute difference of those legs; addition is componentwise on the legs. DistinctionNat.leq is the Boolean ≤ defined by structural recursion on orbit positions, not by a verifier display.
Recovery maps connect this layer to ordinary arithmetic. SignedOrbit.toInt (via LogicInt) and abs_toNat identify internal absolute value with Int.natAbs of the recovered integer. Addition recovers as ordinary Int addition (add_toInt), and DistinctionNat addition recovers as Nat addition (toNat_add).
The local module develops the full order surface on signed orbits (reflexivity, totality, trichotomy, sign flags). This lemma is the metric half of that surface: absolute value is subadditive under internal addition.
proof idea
Rewrite the Boolean leq goal into a Nat inequality via leq_eq_true_iff. Unfold both absolute values with abs_toNat, the sum with add_toInt, and the right-hand Nat sum with toNat_add, so both sides become Int.natAbs expressions on recovered integers. Finish by exact application of Mathlib's Int.natAbs_add_le on z.toInt and w.toInt. No case split on signs is needed; the recovery maps carry the work.
why it matters
Feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (display lemmas for truncated subtraction, leq, absdiff, and nonneg flags). Without triangle inequality the absolute-value fragment of that certificate would be incomplete.
In the Recognition foundation stack this sits under ArithmeticFromLogic and IntegersFromLogic: integers and their order are recovered from pure logical/orbit structure before any continuum or physical constant appears. It is scaffolding for later cost and defect comparisons that use |·| on discrete carriers, not a forcing-chain (T0–T8) step itself. Closes one concrete inequality obligation on the path from orbit arithmetic to a certified ordered ring of integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.