OrbitEuclideanCertificate
plain-language theorem explainer
Bundling certificate that the finite distinction orbit carries a full Euclidean surface: native div/mod, gcd, coprimality, and ratio normalization all match ordinary natural-number arithmetic under the toNat embedding. Cited by anyone using the closed δ-only Euclidean layer or the first-pass PRC kernel. It is a Prop structure of display and algebraic laws; the inhabiting theorem wires already-proved component lemmas.
Claim. A certificate asserting that on the finite distinction orbit: quotient and remainder agree with ordinary $n/d$ and $n\bmod d$ under the natural embedding; the remainder is strictly smaller than the divisor; $q\cdot d+r=n$; native gcd and coprimality agree with $\mathrm{Nat.gcd}$ and $\mathrm{Nat.Coprime}$; every common divisor divides the gcd; if $b$ is coprime to $a$ and $a$ divides $b\cdot c$ then $a$ divides $c$; and ratio normalization holds.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Its verifier map toNat reads each orbit position as an ordinary natural number. Native divisibility is existential: $a$ divides $b$ when some orbit $k$ satisfies $a\cdot k=b$.
This module builds Euclidean division on that orbit. divMod (via fuelled subtraction) returns a quotient-remainder pair; quotient and remainder are its projections. Object-level gcd is the Euclidean algorithm on orbits; coprime means the gcd is a multiplicative unit (the one-step orbit).
The local setting is the Primitive Recognition Calculus Euclidean pass: close arithmetic on δ-orbits so later kernel stages can normalize ratios without leaving the native type. Upstream display lemmas already equate divMod, quotient, remainder, and gcd with Nat operations under toNat.
proof idea
No proof body: this is a Prop structure, a bundling interface. Each field is a named law (display equalities under toNat, the remainder bound, the $q\cdot d+r=n$ decomposition, gcd-as-greatest-divisor, Euclid-style cancellation, and RatioNormalizationTarget).
The inhabiting theorem orbit_euclidean_certificate fills the fields by direct appeal to sibling lemmas: divMod_toNat, quotient_toNat, remainder_toNat, remainder_lt_divisor, quotient_mul_divisor_add_remainder_eq, and the corresponding gcd/coprime/normalization results. The structure itself only packages those obligations.
why it matters
Closes the δ-only Euclidean orbit surface inside Primitive Recognition Calculus, including signed-rational normalization by native orbit GCD. Downstream, orbit_euclidean_certificate inhabits the bundle; KernelFirstPassCertificate (K7/A2) consumes it as part of the first theorem chain, where "the analytic specification has concrete Lean objects for each stage" without yet claiming final inevitability.
In the broader Recognition stack this is foundation arithmetic, not a forcing-chain landmark (T5–T8). It supplies the Euclidean toolkit needed before mass ladders, J-cost identities, or continuum limits can sit on a native discrete orbit. Open relative to the final kernel: the first-pass certificate remains a bundling layer, not the inevitability theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.