lt_sub_zero_left_iff
plain-language theorem explainer
Strict order on signed orbits is invariant under left subtraction of zero: a−0 < b if and only if a < b. Anyone normalizing integer comparisons in the Primitive Recognition Calculus cites this. The proof is a one-line term application of left-congruence of < under the balanced relation, using that a−0 is balanced with a.
Claim. For signed orbits $a$ and $b$, writing $0$ for the zero signed orbit, one has $a-0 < b$ if and only if $a < b$.
background
Signed orbits are the PRC integer layer: a pair of distinction-nats (pos, neg) with intended meaning pos − neg. Two signed orbits are balanced when they represent the same integer (equivalently, equal under the toInt embedding). The internal strict order is a < b iff a ≤ b and not balanced.
The module builds a closed order surface on this representation before rationals and Cauchy reals. Upstream, sub_zero_balanced records that subtracting the zero orbit does not change the integer value: a − 0 is balanced with a. Left-congruence lt_congr_left_of_balanced then says balanced left arguments may be swapped under <.
Related order facts in the same file include trichotomy, sign-flag characterizations of nonnegativity, and lt_zero_iff_negativeFlag.
proof idea
One-line term proof. Apply lt_congr_left_of_balanced to the hypothesis sub_zero_balanced a, which supplies the balanced witness balanced (a − 0) a. Congruence immediately rewrites the left argument of <, yielding (a − 0) < b ↔ a < b.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, ≤, absolute difference, and nonnegativity flags). Without left-invariance of < under subtracting zero, the certificate cannot treat a − 0 as interchangeable with a in strict comparisons.
This sits in the Foundation arithmetic stack that reconstructs integers from distinction structure before the forcing chain (T5–T8) and the Recognition Composition Law are used at the physics layer. It is bookkeeping, not a landmark forcing step, but it is required glue so later PRC order and mass-ladder constructions can normalize against the zero orbit without case splits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.