le
plain-language theorem explainer
Non-strict order on signed orbits: a is at most b exactly when the difference b−a is nonnegative. Cited wherever the primitive recognition calculus compares integer-like orbit differences. One-line definitional reduction to nonnegativity of the signed subtraction.
Claim. For signed orbits $a,b$ (each a pair of distinction naturals read as positive minus negative part), $a\leq b$ holds if and only if $b-a$ is nonnegative: there exists a distinction natural $k$ such that $b-a$ balances with the orbit of $k$.
background
Signed orbits (K4.6) package a difference of two distinction naturals as positive part minus negative part. They are the integer-like carriers of the primitive recognition calculus, built above distinction naturals and orbit arithmetic.
Nonnegativity of a signed orbit $z$ means $z$ balances against some positive orbit: there is a distinction natural $k$ with $z$ balanced to the orbit of $k$. Upstream, the order on logic naturals is the witness form $n\leq m$ iff $n+k=m$ for some $k$.
This module reconstructs integer and rational structure from recognition orbits; the present relation is the internal comparison used throughout that arithmetic layer.
proof idea
One-line definitional wrapper. The relation $a\leq b$ is defined to be nonnegativity of the signed-orbit difference $b-a$. No tactics or lemmas; the Prop is exactly that nonnegativity predicate applied to the subtraction.
why it matters
This is the comparison primitive for signed-orbit arithmetic and has broad fan-out (dozens of use sites). Downstream it supports path-space straight-line interpolation, Einstein-constant identities, uniqueness of the alpha residual closing load, BIT kernel shape forcing (no-phantom sign bound and rung-scaling lattice uniqueness), and eta_B interval certificates on negative powers of phi. It supplies the ordered structure once integers are rebuilt from recognition orbits, feeding constant and cosmology layers above the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.