module module moderate

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitEuclidean`

Fuelled Euclidean division and GCD on recognition orbits: quotient and remainder by repeated subtraction, with the first argument an orbit fuel rather than ordinary Nat. Supplies the divisibility arithmetic that factorization charts, the PRC kernel, and the J-cost layer import. Correctness is by fuelled recursion plus transport lemmas to Nat.

claimOn recognition orbits, define fuelled division: given fuel $f$ and divisor $d$, obtain quotient $q$ and remainder $r$ by repeated subtraction so that $n = q\cdot d + r$ with $r < d$ (when the fuel is adequate). Lift the same recursion to a fuelled $\gcd$. Transport lemmas identify these with the usual $\mathrm{Nat}$ quotient, remainder, and $\gcd$.

background

Primitive Recognition Calculus builds arithmetic without treating verifier Nat as primitive. Integer and rational structure live in the IntegerRational layer; OrbitDivisibility supplies the orbit-level divisibility predicates this module consumes.

Here the Euclidean step is re-implemented with an explicit orbit fuel: divModFuel / divMod produce quotient and remainder by repeated subtraction, and gcdFuel / gcd iterate that step. The fuel is an orbit resource, not a bare natural, so termination and well-foundedness stay inside the recognition calculus.

Companion lemmas (remainder_lt_divisor, quotient_mul_divisor_add_remainder_eq, and the *_toNat family) state the usual Euclidean identities and the bridge to Mathlib Nat division, so later layers can quote standard arithmetic while staying orbit-native at the definition site.

proof idea

Definition-heavy module with fuelled recursive constructions. divModFuel subtracts the divisor while fuel remains; divMod, quotient, and remainder package that pair. gcdFuel / gcd reuse the same fuel discipline on the Euclidean algorithm.

Proof content is mostly structural: auxiliary toNat lemmas relate fuelled results to ordinary natural division; remainder_lt_divisor and quotient_mul_divisor_add_remainder_eq discharge the two Euclidean invariants by induction on fuel. No deep analytic argument; the work is making orbit-fuel recursion match classical div-mod/GCD.

why it matters in Recognition Science

Factorization chart transitions, the PRC kernel, and the PRC J-cost module all import this file. They need orbit-native quotient, remainder, and GCD so divisibility and cost bookkeeping do not drop out of the recognition calculus into bare Nat.

In the broader Foundation stack this is plumbing under the forcing chain rather than a T5–T8 landmark: it equips later uniqueness and cost arguments with Euclidean arithmetic that still tracks orbit fuel. Without it, chart factorization and kernel identities would either sorry out or smuggle verifier naturals into the primitive layer.

scope and limits

Does not define J-cost, RCL, or any T5–T8 forcing step.
Does not prove uniqueness of factorization; only fuelled div-mod and GCD.
Does not replace Mathlib Nat division globally; only supplies orbit-fuel analogues plus transport.
Does not address real or continuous quotients; discrete orbit arithmetic only.
Does not specify physical units or mass-ladder rungs.

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