lt_iff_toInt_lt
plain-language theorem explainer
Strict order on signed orbits agrees with ordinary integer comparison of their verifier displays. Anyone building order, comparison, or translation-invariance lemmas on the PRC integer surface cites this bridge. The proof unfolds the internal strict order, rewrites via the non-strict and balanced characterizations, and finishes both directions by omega.
Claim. For signed orbits $a,b$ (pairs of distinction-natural lengths intended as $\mathrm{pos}-\mathrm{neg}$), the internal strict order $a < b$ holds if and only if the recovered integers satisfy $a^{\mathbb{Z}} < b^{\mathbb{Z}}$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction-natural lengths (pos, neg), read as the formal difference pos - neg. The recovery map toInt sends each signed orbit to an ordinary ℤ value used only as a conservative verifier display.
Equivalence of signed orbits is the balanced-length relation: a and b are balanced when a.pos + b.neg = b.pos + a.neg. Upstream, that internal relation is already identified with equality of displays: balanced iff a.toInt = b.toInt. The non-strict order has the matching characterization a ≤ b iff a.toInt ≤ b.toInt.
The strict order is the residual of that non-strict order after removing balance. This lemma is the corresponding display bridge for <.
proof idea
Term-mode proof. Unfold the definition of the internal strict order (non-strict order and not balanced). Rewrite with the already-proved bridges le_iff_toInt_le and balanced_iff_toInt_eq, so the goal becomes
a.toInt ≤ b.toInt ∧ a.toInt ≠ b.toInt ↔ a.toInt < b.toInt.
Both directions are pure integer arithmetic; each is discharged by omega (one direction as a single implication, the converse as a pair of omega goals).
why it matters
This is the strict-order half of the PRC-to-ℤ dictionary for signed orbits. Downstream IntegerOrder lemmas use it constantly: comparison flags (cmp_eq_lt_of_lt, cmp_eq_gt_of_gt, and the corresponding iff forms), left/right translation invariance of < under signed-orbit addition, and congruence of < under balanced replacement. Those facts feed the closed integer_order_certificate, which packages the signed-orbit order surface as complete relative to the verifier displays.
In the Recognition foundation stack this sits under arithmetic-from-logic and integers-from-logic: once strict order matches ℤ, later forcing and ledger constructions can treat signed-orbit inequalities as ordinary integer inequalities without leaving the δ-orbit language. It does not itself touch T5–T8 or the J-cost; it is pure order infrastructure those layers rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.