lt_zero_sub_left_iff
plain-language theorem explainer
Zero minus a signed orbit is strictly less than b exactly when the pointwise negation of that orbit is strictly less than b. Order-theory work on the signed-orbit integers cites this to rewrite left-hand sides of the form 0−a. The proof is a one-line application of left-congruence of strict order under balanced equality, using that 0−a is balanced with −a.
Claim. For signed orbits $a,b$ (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), one has $0-a < b$ if and only if $-a < b$, where $-a$ swaps the positive and negative components and $<$ is the internal strict order (nonnegative difference and not balanced).
background
Signed orbits are the integer layer of the primitive recognition calculus: a structure with components pos and neg of distinction-natural type, intended as the difference pos − neg. Negation swaps those components. Strict order on signed orbits is defined internally as the weak order together with failure of balanced equality (the two sides represent the same integer).
Balanced equality is the congruence that identifies different orbit presentations of the same integer value. The companion lemma zero_sub_balanced_negate records that subtracting from zero is balanced with pointwise negation: both map to the same underlying integer. Left-congruence of strict order under balanced equality then lets one replace 0−a by −a in any strict comparison on the left.
The ambient module builds the ordered-integer surface on top of arithmetic-from-logic, so that later certificates can treat signed-orbit order as closed and displayable.
proof idea
One-line term proof. Apply left-congruence of strict order under balanced equality (lt_congr_left_of_balanced) to the pair $(0-a,,-a)$, discharging the balanced hypothesis by zero_sub_balanced_negate a. That congruence itself reduces both sides via the characterization of < in terms of the integer embedding and uses that balanced pairs have equal embeddings.
why it matters
Feeds the integer-order certificate (integer_order_certificate), whose doc-comment states that the internal signed-orbit order surface is closed. The certificate packages display lemmas for truncated subtraction, weak order, absolute difference, and nonnegativity flags; rewriting 0−a as −a is part of keeping that surface coherent under the signed arithmetic operations.
In the Recognition foundation stack this sits below the forcing chain (T0–T8) and the cost calculus: it is bookkeeping that makes the integer layer of primitive recognition a usable ordered ring-like object, not a physics identity itself. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.