module module moderate

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitEuclidean`

Defines Euclidean division and GCD on orbit fuel by repeated subtraction, not on verifier naturals. Quotient, remainder, and gcd are extracted from a fuelled div-mod pair, with lemmas tying them to ordinary Nat arithmetic. Downstream factorization, kernel, and J-cost modules import this layer so divisibility stays inside the recognition orbit calculus.

claimOn orbit fuel $f$ (not verifier $\mathbb{N}$), fuelled division yields a pair $(q,r)$ by repeated subtraction so that the corresponding naturals satisfy $n = q\cdot d + r$ with $r < d$ when $d > 0$. The module also defines $\gcd$ on fuel via the Euclidean algorithm (repeated remainder), with transport lemmas to $\mathrm{Nat}$.

background

Primitive Recognition Calculus works with orbit fuel rather than bare verifier naturals: fuel is the resource that bounds recognition steps along an orbit. Integer and rational structure, and orbit-level divisibility, are already available from the imported IntegerRational and OrbitDivisibility modules.

This module supplies the classical Euclidean toolkit in that fuel setting. Division is implemented as fuelled repeated subtraction (divModFuel / divMod), exposing quotient and remainder. Parallel fuelled GCD (gcdFuel / gcd) follows the usual remainder loop. Companion lemmas relate these operations to Nat via toNat, including the standard identities remainder strictly less than the divisor and $q\cdot d + r = n$.

proof idea

Definition-and-lemma module, not a single theorem. Core objects are recursive fuelled procedures: div-mod by repeated subtraction with an explicit fuel argument, then quotient/remainder projections; gcd by the Euclidean remainder iteration on fuel. Correctness is discharged by transport to Nat (divMod_toNat, quotient_toNat, remainder_toNat) plus the two classical identities remainder_lt_divisor and quotient_mul_divisor_add_remainder_eq. No deep analytic argument; structural recursion on fuel plus Nat bridge lemmas.

why it matters in Recognition Science

Gives the foundation layer a fuel-native Euclidean algorithm so later PRC modules never drop to ad-hoc verifier Nat division. Imported by Factorization.ChartTransition (chart changes and factor moves), by Kernel (core recognition kernel constructions), and by PRCJCost (J-cost bookkeeping on recognition orbits). Without orbit-level quotients, remainders, and gcd, factorization and cost identities cannot stay inside the forcing/recognition calculus that feeds the T5–T8 chain and the RCL cost $J$.

scope and limits

Does not redefine division or gcd on bare verifier Nat; only orbit fuel with Nat transport.
Does not prove uniqueness of factorization or primality; only div-mod and gcd primitives.
Does not introduce J-cost, charts, or kernel axioms; those live in downstream modules.
Does not address real or continuous Euclidean algorithm; discrete fuelled subtraction only.
Does not claim termination independent of fuel; recursion is fuel-bounded by construction.

used by (3)

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ChartTransition module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Kernel module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitDivisibility module_import

declarations in this module (36)

def divModFuel L28
def divMod L39
def quotient L43
def remainder L47
theorem divModFuel_toNat_aux L50
theorem divMod_toNat L94
theorem quotient_toNat L107
theorem remainder_toNat L112
theorem remainder_lt_divisor L117
theorem quotient_mul_divisor_add_remainder_eq L129
def gcdFuel L140
def gcd L153
def coprime L157
theorem gcdFuel_toNat_aux L160
theorem gcd_toNat L220
theorem coprime_iff_nat_coprime L226
theorem gcd_divides_left L231
theorem gcd_divides_right L237
theorem divides_gcd_of_divides_left_right L243
theorem coprime_divides_of_divides_mul_left L255
theorem gcd_ne_zero_of_right_ne_zero L264
theorem quotient_mul_divisor_toNat_of_divides L275
theorem quotient_ne_zero_of_divides L281
def signedQuotient L297
theorem signedQuotient_abs_toNat L305
theorem signedQuotient_mul_divisor_toInt_of_divides L328
def normalizeRatio L366
theorem normalizeRatio_num_mul_gcd_toInt L379
theorem normalizeRatio_den_mul_gcd_toNat L388
theorem normalizeRatio_toRat L397
theorem normalizeRatio_crossEq L429
theorem normalizeRatio_coprime L434
def RatioNormalizationTarget L457
theorem ratio_normalization_target L463
structure OrbitEuclideanCertificate L468
theorem orbit_euclidean_certificate L499