abs_sub_le_add_abs
plain-language theorem explainer
The triangle inequality on signed orbits: absolute value of a difference is at most the sum of absolute values, stated in the internal Boolean order on distinction naturals. Anyone assembling the integer-order certificate cites it. The proof rewrites through recovery maps to Mathlib's Int.natAbs_add_le.
Claim. For all signed orbits $z,w$, writing $|\cdot|$ for the absolute-value map into distinction naturals and $\le_{\mathrm{Bool}}$ for the internal Boolean order, one has $|z-w|\le_{\mathrm{Bool}}|z|+|w|$.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: each is a pair of distinction-natural positions (positive and negative legs). Absolute value sends a signed orbit to the absolute difference of those legs, landing in DistinctionNat. Subtraction is the corresponding signed difference.
Boolean order leq on distinction naturals is defined by structural recursion only (zero is least; successors compare after stripping). The recovery theorem leq_eq_true_iff states that this Boolean order agrees with ordinary Nat order under toNat, with axiom footprint only propext.
Absolute value recovers as ordinary integer absolute value: abs_toNat says z.abs.toNat = Int.natAbs z.toInt. Addition of distinction naturals recovers as Nat addition via toNat_add. Together these maps let internal inequalities be checked on the verifier side as ordinary integer facts.
proof idea
Rewrite the Boolean goal via leq_eq_true_iff into a Nat inequality on toNat images. Unfold both absolute values with abs_toNat, the difference with sub_toInt, and the sum with toNat_add, so the goal becomes Int.natAbs(z.toInt - w.toInt) ≤ Int.natAbs(z.toInt) + Int.natAbs(w.toInt). Rewrite subtraction as addition of negation and cancel natAbs of a negation, then apply Mathlib's Int.natAbs_add_le to z.toInt and -w.toInt.
why it matters
This is one of the elementary order facts that close the internal signed-orbit order surface. The sole downstream consumer is integer_order_certificate, whose doc-comment states that surface is closed and packages display lemmas for truncated subtraction, Boolean order, absolute difference, and nonnegativity flags.
In the Recognition foundation stack, integers and their order are recovered from logic rather than postulated. Triangle inequality for absolute value is the standard metric compatibility needed before signed orbits can serve as the integer layer under the forcing chain (T0–T8) and the later phi-ladder mass and cost constructions. Without it the certificate cannot assert that the internal absolute-value display matches the verifier triangle inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.