le_refl
plain-language theorem explainer
Every signed orbit is less than or equal to itself under the internal non-strict order. Anyone treating SignedOrbit as a preorder (path endpoints, gap weights, baryogenesis staging) cites this. The proof is a one-line reduction through the toInt characterization, closed by omega on ordinary integers.
Claim. For every signed orbit $a$ (a pair of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), $a \le a$, where $a \le b$ means that the difference $b-a$ is nonnegative.
background
SignedOrbit is the K4.6 carrier for integer differences built inside Primitive Recognition Calculus: a pair (pos, neg) of distinction naturals, intended as pos - neg. Its internal non-strict order is defined by le a b := nonneg (sub b a), i.e. the difference is a nonnegative signed orbit.
That order is tied to ordinary integer comparison by le_iff_toInt_le: le a b if and only if a.toInt ≤ b.toInt. Upstream, LogicNat already has the classical existential order n ≤ m := ∃ k, n+k = m with its own reflexivity lemma; here the same reflexivity is re-established on the signed-orbit layer after the toInt bridge.
The local module IntegerOrder packages the preorder/order facts (refl, trans, antisymm on balanced representatives, totality, trichotomy, sign-flag characterizations) that make SignedOrbit usable as an ordered integer type in later calculus.
proof idea
Term-mode one-liner. Apply the right-to-left direction of SignedOrbit.le_iff_toInt_le a a, which reduces the goal to a.toInt ≤ a.toInt on Lean integers. Discharge that inequality with omega. No induction and no unfolding of nonneg or sub is needed at the call site; the iff lemma already did that work.
why it matters
Reflexivity is the first axiom of the SignedOrbit preorder. Downstream it is consumed heavily: Action.PathSpace uses it to witness the Icc bounds in interp_zero and interp_one (the convex path interpolation that feeds variational calculus); Action.FunctionalConvexity's headline geodesic_minimizes_unconditional takes an endpoint inequality a ≤ b in the same ordered setting; Constants.GapWeight.Formula closes nonnegativity of geometric weights with a refl instance; Cosmology.BaryogenesisStaging theorems about B-final and B-L obstruction sit on the same ordered arithmetic stack.
In the Recognition framework this is pure foundation scaffolding under the forcing chain: before J-cost, phi, or the eight-tick octave can be ordered or minimized, the integer carrier must be a preorder. This lemma closes that trivial but load-bearing corner with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.