le_trans
plain-language theorem explainer
Transitivity of the non-strict order on signed orbit differences: if a ≤ b and b ≤ c then a ≤ c. Anyone building ordered arithmetic, causal balls, or least-action arguments on the integer layer of Recognition Calculus cites this. The proof rewrites the order to ordinary integer comparison and closes by omega.
Claim. Let $a,b,c$ be signed orbit differences (each a pair of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If $a\le b$ and $b\le c$ in the internal order ($b-a$ and $c-b$ nonnegative), then $a\le c$.
background
Signed orbits are the integer layer of Primitive Recognition Calculus: a structure with nonnegative distinction-natural components pos and neg, intended as the difference $\mathrm{pos}-\mathrm{neg}$. The internal non-strict order is defined by nonnegativity of the difference: $a\le b$ means $b-a$ is nonnegative.
That order is characterized by transport to ordinary integers: $a\le b$ if and only if the integer image of $a$ is $\le$ the integer image of $b$. Upstream, the same transitivity pattern already exists on logic naturals, where $\le$ means existence of a summand ($n+k=m$) and transitivity concatenates the witnesses.
This module packages the order axioms (reflexivity, transitivity, antisymmetry on the balanced quotient, totality, trichotomy, sign-flag lemmas) so later arithmetic and geometry can treat signed orbits as an ordered integer type without reopening the construction.
proof idea
One short tactic proof. Rewrite both hypotheses and the goal with the characterization that internal $\le$ is equivalent to ordinary integer $\le$ on the toInt images. The goal becomes $a^{\mathbb{Z}}\le b^{\mathbb{Z}}$ and $b^{\mathbb{Z}}\le c^{\mathbb{Z}}$ imply $a^{\mathbb{Z}}\le c^{\mathbb{Z}}$, which omega discharges. No manual witness construction is needed once the relation sits on $\mathbb{Z}$.
why it matters
This is basic order infrastructure, not a physics claim, but it is heavily reused. Downstream it feeds monotonicity of causal balls (inBall_mono, ballP_subset_inBall), cone-cardinality bounds (card_ballFS_succ_le, card_bind_neighbors_le), gap-weight positivity, and the unconditional least-action theorem that turns a local minimum of actionJ into a global one via convexity.
In the Recognition stack, signed-orbit order is the discrete comparison layer beneath continuum cost and path action. Without transitivity, ball inclusions, reachability radii, and segment comparisons in the action functional would not compose. It sits well below the forcing chain (T5–T8) and the Recognition Composition Law, but those later structures inherit ordered arithmetic from this base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.