module module moderate

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational`

Integer and rational scaffolding on finite δ-orbit positions: truncated subtraction, absolute difference, Boolean comparison, and a signed-orbit type with an embedding into ℤ. Downstream Grow modules cite it for cross-multiplication order on ratio orbits, forced trichotomy, and integer divisibility. The module is mostly definitions plus elementary Nat/Int identities.

claimOn finite $\delta$-orbit positions one defines truncated subtraction $a \dot{-} b$, absolute difference $|a-b|$, and a Boolean order $\mathrm{leq}(a,b)$. A signed orbit type carries a map $\mathrm{toInt}$ into $\mathbb{Z}$, with a distinguished zero, so that numerators and denominators of ratio orbits can be compared by cross-multiplication in $\mathbb{Z}$.

background

Primitive Recognition Calculus works with finite discrete orbits under a recognition step $\delta$, not with bare $\mathbb{N}$ or $\mathbb{Q}$. The Orbit and OrbitArithmetic modules supply the underlying position type and basic arithmetic; this module adds the integer-like operations needed for ordered comparison and rational structure.

Truncated subtraction $a\dot{-}b$ is the Nat-style difference that floors at zero. Absolute difference and a Boolean $\mathrm{leq}$ are built from it, with lemmas relating their Boolean values to ordinary inequalities after casting to $\mathbb{N}$. SignedOrbit packages a sign with an orbit position and embeds into $\mathbb{Z}$ via $\mathrm{toInt}$, so products of numerators and denominators become ordinary integers.

That embedding is the bridge used later: positive distinctions (denominators) are cast in via $\mathrm{SignedOrbit.ofOrbit}$, and order on ratio orbits is defined by comparing signed products.

proof idea

Definition module with supporting Nat/Int lemmas, not a single theorem. Core objects are introduced as defs: truncatedSub, absDiff, leq, SignedOrbit, toInt, and zero. Companion lemmas (toNat_truncatedSub, leq_eq_true_iff / leq_eq_false_iff, toNat_absDiff, toInt_mk, zero_toInt) are short rewrites that connect the Boolean and truncated operations to Mathlib's Nat and Int arithmetic. No deep forcing argument lives here; the work is interface and casting hygiene.

why it matters in Recognition Science

Ratio-orbit order and trichotomy need a signed integer carrier for cross-multiplication. Downstream, RatioOrbitLeReflTotal defines $\mathrm{leQ},p,q$ by comparing the signed orbits $p.\mathrm{num}\cdot q.\mathrm{den}$ and $q.\mathrm{num}\cdot p.\mathrm{den}$ after casting dens through SignedOrbit.ofOrbit. Sibling Grow modules (ForcedTrichotomy, RatioOrbitLtTrichotomy, RatioOrbitLeNeg, RatioOrbitLeTransAntisymm, RatioOrbitDenseMediant, IntegerDivisibility, EtaCompletionM0a) import this layer so that order, density of mediants, and divisibility statements can be stated in $\mathbb{Z}$ rather than ad hoc on bare orbits.

In the broader RS foundation this is plumbing under the primitive calculus that eventually supports discrete forcing structure (octave period, dimension counts), not a T5–T8 landmark itself. It closes the gap between orbit positions and ordinary integer comparison.

scope and limits

Does not prove uniqueness of J or force φ; those live in the UnifiedForcingChain.
Does not define ratio-orbit order itself; only the signed integer carrier used by leQ.
Does not establish trichotomy, density of mediants, or divisibility; Grow modules do.
Does not treat infinite orbits or continuous reals; only finite δ-orbit positions.
Does not claim a full ordered field structure on orbits beyond the exported casts and lemmas.

used by (26)

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic module_import

declarations in this module (175)

def truncatedSub L36
def leq L42
def absDiff L48
theorem toNat_truncatedSub L52
theorem leq_eq_true_iff L68
theorem leq_eq_false_iff L86
theorem toNat_absDiff L92
structure SignedOrbit L130
def toInt L138
theorem toInt_mk L141
def zero L146
theorem zero_toInt L149
def one L154
theorem one_toInt L157
def ofOrbit L162
theorem ofOrbit_toInt L165
def add L171
theorem add_pos L175
theorem add_neg L178
theorem add_toInt L181
def negate L192
theorem negate_pos L196
theorem negate_neg L199
theorem negate_toInt L202
def mul L210
theorem mul_pos L214
theorem mul_neg L217
theorem mul_toInt L220
def sub L233
theorem sub_toInt L236
def scaleByNat L243
theorem scaleByNat_pos L247
theorem scaleByNat_neg L250
theorem scaleByNat_toInt L253
def balanced L266
instance instDecidableBalanced L269
theorem balanced_iff_toNat_eq L275
theorem balanced_iff_toInt_eq L291
theorem balanced_refl L301
theorem balanced_symm L305
theorem balanced_trans L310
theorem balanced_equivalence L315
def nonneg L324
def nonnegFlag L328
def negativeFlag L332
def le L336
def lt L340
def abs L344
theorem nonnegFlag_eq_true_iff L347
theorem nonnegFlag_eq_false_iff L355
theorem nonneg_iff_toInt_nonneg L363
theorem nonnegFlag_eq_true_iff_nonneg L378
theorem negativeFlag_eq_true_iff_toInt_neg L382
theorem abs_toNat L401
theorem abs_eq_zero_iff_toInt_eq_zero L406
theorem abs_ne_zero_of_toInt_ne_zero L418
theorem abs_ne_zero_of_not_balanced_zero L424
theorem le_iff_toInt_le L432
theorem lt_iff_toInt_lt L438
def signedOrbitEquiv L447
theorem signedOrbitEquiv_equivalence L450
theorem signedOrbitEquiv_iff_toInt_eq L454
def signedOrbitSetoid L459
def PRCInt L466
def mk L472
theorem mk_eq_mk_of_balanced L502
theorem add_respects_balanced L510
theorem add_mk L529
theorem toInt_add L533
theorem negate_respects_balanced L541
theorem negate_mk L556
theorem toInt_negate L560
theorem toInt_injective L568
theorem mul_respects_balanced L578
theorem mul_mk L598
theorem toInt_mul L602
theorem toInt_sub L613
theorem add_comm L621
theorem add_assoc L625
theorem zero_add L630

… and 95 more