module module moderate

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder`

Defines the internal order on signed orbits (and thus integers) from signed-orbit comparison and balanced length, independent of any verifier display. Supplies reflexivity, transitivity, balanced antisymmetry, totality, and trichotomy, plus exclusive/exhaustive sign flags. Downstream ratio-orbit and divisibility layers import it as the native ≤ bridge. Structure is a compact order-theory package over the IntegerRational substrate.

claimOn signed orbits (the internal model of integers), a comparison $\leq$ is defined from signed-orbit order and balanced length. It is reflexive, transitive, antisymmetric on balanced representatives, total, and satisfies trichotomy. Sign flags for nonnegative and negative are mutually exclusive and exhaustive, with $0 \leq n$ iff the nonnegative flag holds and $n < 0$ iff the negative flag holds.

background

Primitive Recognition Calculus builds integers and rationals from orbits and signed orbits rather than from a pre-given $\mathbb{Z}$. The upstream module IntegerRational supplies that substrate: signed orbits with a balanced-length presentation and a bridge to ordinary integer comparison when needed.

This module installs the internal order selector on that substrate. The doc-comment is explicit: comparison is taken from signed-orbit order and balanced length, not from the verifier's integer display. That keeps the foundation choice-free and display-independent while still recovering the usual order facts.

Sibling lemmas package the standard order axioms (reflexivity, transitivity, balanced antisymmetry, totality, trichotomy) and the Boolean sign-flag calculus (exclusive, exhaustive, and the zero-threshold characterizations).

proof idea

Definition-and-lemmas module over the IntegerRational import. Order is selected from signed-orbit comparison plus balanced length; the listed siblings then discharge the classical order and sign-flag identities relative to that selector. No single deep theorem: a short suite of elementary order and flag lemmas that later modules quote as the native $\leq$ bridge (including the purified SignedOrbit.le_iff_toInt_le path used downstream).

why it matters in Recognition Science

Feeds the Grow layer that builds ratio-orbit order and arithmetic. Downstream importers include RatioOrbitLeReflTotal (cross-multiplication order leQ via signed orbits of $p.num\cdot q.den$ and $q.num\cdot p.den$), RatioOrbitLeTransAntisymm (transitivity of that delta-native order, routed through the signed-orbit bridge and Int cancellation), RatioOrbitLeNeg, RatioOrbitLtTrichotomy, RatioOrbitMulPos, RatioOrbitDenseMediant, IntegerDivisibility, and EtaCompletionM0a.

Without a display-independent integer order, the cross-multiplication order on ratio orbits and the later density/mediant and divisibility arguments have no native comparison to stand on. In the Recognition stack this is foundation plumbing under the forcing chain, not a T5–T8 landmark itself, but it is required infrastructure for any later quantitative comparison on the phi-ladder or mass formulas that routes through rational orbits.

scope and limits

Does not define rationals or ratio-orbit order; those live in downstream Grow modules.
Does not derive order from verifier integer display; comparison is signed-orbit native.
Does not prove density, mediants, or divisibility; only the integer-order substrate.
Does not address J-cost, RCL, or T5–T8 forcing; pure order infrastructure.
Antisymmetry is stated in the balanced-representative sense, not raw orbit equality.

used by (21)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational module_import

declarations in this module (443)

theorem le_refl L28
theorem le_trans L31
theorem le_antisymm_balanced L37
theorem le_total L44
theorem trichotomy L49
theorem negativeFlag_eq_true_iff_nonnegFlag_eq_false L59
theorem negativeFlag_eq_false_iff_nonnegFlag_eq_true L64
theorem signFlags_exclusive L69
theorem signFlags_exhaustive L77
theorem zero_le_iff_nonnegFlag L86
theorem lt_zero_iff_negativeFlag L91
theorem zero_lt_iff_nonnegFlag_and_not_balanced_zero L96
theorem nonnegFlag_eq_of_balanced L108
theorem negativeFlag_eq_of_balanced L126
theorem nonneg_iff_of_balanced L132
theorem add_congr_of_balanced L145
theorem negate_congr_of_balanced L151
theorem sub_congr_of_balanced L157
theorem sub_congr_of_balanced_left L164
theorem sub_congr_of_balanced_right L171
theorem nonnegFlag_sub_eq_of_balanced_left L178
theorem nonnegFlag_sub_eq_of_balanced_right L185
theorem negativeFlag_sub_eq_of_balanced_left L192
theorem negativeFlag_sub_eq_of_balanced_right L199
theorem nonnegFlag_sub_eq_of_balanced L206
theorem negativeFlag_sub_eq_of_balanced L213
theorem scaleByNat_congr_of_balanced L220
theorem scaleByNat_balanced_zero_of_balanced_zero L226
theorem mul_ofOrbit_balanced_scaleByNat L233
theorem ofOrbit_mul_balanced_scaleByNat L241
theorem abs_mul L250
theorem mul_balanced_zero_iff L256
theorem mul_not_balanced_zero_iff L276
theorem balanced_mul_left_iff_of_not_balanced_zero L294
theorem balanced_mul_right_iff_of_not_balanced_zero L312
theorem le_mul_left_iff_of_nonnegFlag_of_not_balanced_zero L330
theorem lt_mul_left_iff_of_nonnegFlag_of_not_balanced_zero L348
theorem le_mul_right_iff_of_nonnegFlag_of_not_balanced_zero L366
theorem lt_mul_right_iff_of_nonnegFlag_of_not_balanced_zero L384
theorem le_mul_left_iff_of_negativeFlag L402
theorem lt_mul_left_iff_of_negativeFlag L413
theorem le_mul_right_iff_of_negativeFlag L424
theorem lt_mul_right_iff_of_negativeFlag L435
theorem abs_mul_eq_zero_iff L446
theorem abs_mul_ne_zero_iff L465
theorem abs_mul_eq_zero_iff_balanced_zero L482
theorem abs_mul_ne_zero_iff_not_balanced_zero L502
theorem abs_scaleByNat L520
theorem abs_mul_ofOrbit_right L527
theorem abs_mul_ofOrbit_left L534
theorem mul_ofOrbit_right_balanced_zero_iff L542
theorem mul_ofOrbit_left_balanced_zero_iff L567
theorem mul_ofOrbit_right_not_balanced_zero_iff L592
theorem mul_ofOrbit_left_not_balanced_zero_iff L610
theorem nonnegFlag_scaleByNat_of_ne_zero L628
theorem negativeFlag_scaleByNat_of_ne_zero L652
theorem scaleByNat_balanced_zero_iff L658
theorem scaleByNat_not_balanced_zero_iff L682
theorem abs_scaleByNat_eq_zero_iff L699
theorem abs_scaleByNat_ne_zero_iff L720
theorem abs_mul_ofOrbit_right_eq_zero_iff L737
theorem abs_mul_ofOrbit_left_eq_zero_iff L758
theorem abs_mul_ofOrbit_right_ne_zero_iff L779
theorem abs_mul_ofOrbit_left_ne_zero_iff L796
theorem le_scaleByNat_of_le L813
theorem le_scaleByNat_iff_of_ne_zero L821
theorem lt_scaleByNat_iff_of_ne_zero L837
theorem balanced_scaleByNat_iff_of_ne_zero L853
theorem le_congr_left_of_balanced L869
theorem le_congr_right_of_balanced L875
theorem lt_congr_left_of_balanced L881
theorem lt_congr_right_of_balanced L887
theorem le_congr_of_balanced L893
theorem lt_congr_of_balanced L899
def cmp L907
theorem cmp_eq_lt_of_lt L915
theorem cmp_eq_eq_of_balanced L927
theorem cmp_eq_gt_of_gt L932
theorem cmp_eq_lt_iff L944
theorem cmp_eq_eq_iff L960

… and 363 more