coprime

In Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, standing in for nonnegative integers without committing to a numeral base.

Divisibility on these orbits is native. The unit predicate holds only for the one-step orbit: the sole multiplicative unit in the finite $\delta$-orbit. The object-level GCD is defined by subtractive Euclidean descent (gcdFuel on $a+b$), so it stays inside the orbit type rather than jumping to Nat.

Object-level coprimality packages those two ingredients: $a$ and $b$ are coprime precisely when that Euclidean GCD is the unit.

Definition, not a theorem. The body is the proposition that the object-level GCD of $a$ and $b$ satisfies the native unit predicate (equals the one-step orbit). No tactics or lemmas are applied at the definition site; downstream lemmas transport this to Nat.Coprime when needed.

This predicate is the native stand-in for coprimality throughout the Euclidean and factorization layers. Downstream, unitResidue defines a residue representative as a unit modulo $N$ exactly when it is $\delta$-coprime to $N$. Euclidean cancellation lemmas such as "if $a$ is coprime to $b$ and divides $b\cdot c$, then $a$ divides $c$" are stated with this predicate and only transport to Nat internally.

In the gap derivation, Gap45Cert records that $2^D$ is coprime to the dimension gap (45 at $D=3$), feeding the balance $\eta_B\cdot\Theta_{\mathrm{crit}}=\varphi$. The same notion appears in first-pass kernel certificates that bundle PRC logic surfaces. It is scaffolding for the arithmetic that forces odd spatial dimension and the 45-rung gap, not a physics claim by itself.