unit_or_eq_of_divides_prime
plain-language theorem explainer
If a prime orbit position is divisible by another orbit position, that divisor is either the multiplicative unit or the prime itself. Number theorists working in native δ-orbit arithmetic cite this as the orbit analogue of the classical divisor property of primes. The proof unpacks the division witness, applies the product-equals-prime factorization dichotomy, and reduces the unit-cofactor case by right-multiplication by one.
Claim. Let $a$ and $p$ be positions in the distinction orbit. If $p$ is a prime orbit (nonzero, non-unit, and free of nontrivial factorizations) and $a$ divides $p$ under native orbit multiplication, then either $a$ is the unit (the one-step orbit) or $a = p$.
background
The module builds native divisibility on the distinction orbit: the base-neutral finite orbit of repeated distinction (K2.12), an inductive zero/successor type carrying its own addition and multiplication. Divisibility is existential: $a$ divides $b$ when some orbit position $k$ satisfies $a \cdot k = b$. The unit predicate singles out the one-step orbit as the unique multiplicative unit. A prime orbit is nonzero, non-unit, and admits no nontrivial factorization (both factors nonzero and non-unit).
This is pure foundation arithmetic inside the Primitive Recognition Calculus layer, before cost uniqueness and $p$-adic display. The immediate upstream fact is the product dichotomy: if a product equals a prime orbit, then one of the two factors is a unit. Right-multiplication by the unit recovers the original factor.
proof idea
Unpack the divisibility hypothesis to a witness $k$ with $a \cdot k = p$. Feed that equation into the upstream dichotomy for products equal to a prime orbit: either $a$ is a unit or $k$ is a unit. The first branch is the left disjunct of the claim. On the second branch, unfold the unit predicate to $k = 1$, rewrite the product equation with the right-unit law $a \cdot 1 = a$, and obtain $a = p$.
why it matters
Closes a standard prime-divisor lemma on the native orbit monoid and is consumed by the bundling certificate that the orbit divisibility surface is closed. Downstream, the PRC native cost uniqueness layer applies it to force vanishing $p$-adic valuations on off-axis prime directions: if $r \neq p$ are both prime orbits, the $p$-adic valuation of the rational display of $r$'s prime direction is zero (with specialized forms for the two- and three-axes). Those valuation identities pin uniqueness of the native cost structure on the recognition ladder. The result is foundation scaffolding for later J-cost uniqueness, not itself a T5–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.