unit_or_unit_of_mul_eq_prime
plain-language theorem explainer
If a prime orbit position factors as a product of two orbit positions, at least one factor is a unit (the one-step orbit). Native δ-orbit arithmetic cites this as the Euclid-style primality lemma: primes admit no nontrivial native factorization. The proof is pure case analysis against the three clauses of the prime-orbit predicate (nonzero, non-unit, no nontrivial factorization).
Claim. Let $a$, $b$, and $p$ be positions in the finite distinction orbit $\mathrm{DistinctionNat}$. If $p$ is a prime orbit (nonzero, not equal to the one-step unit, and without a nontrivial factorization) and $a \cdot b = p$, then either $a$ is a unit or $b$ is a unit.
background
The ambient object is DistinctionNat, the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals with constructors zero and successor. Multiplication is the native orbit product from OrbitArithmetic, with the usual annihilation laws $a \cdot 0 = 0$ and $0 \cdot a = 0$.
A native unit is exactly the one-step orbit: $\mathrm{unit}(a)$ means $a = 1$. A nontrivial factorization of $p$ is a pair of factors that are both nonzero and both non-units. A prime orbit is then the conjunction of three clauses: nonzero, non-unit, and free of nontrivial factorization.
This lemma lives in the OrbitDivisibility layer of PrimitiveRecognitionCalculus, which builds a native divisibility surface on the δ-orbit before any bridge to classical $\mathbb{N}$.
proof idea
Tactic proof by nested case splits on the factors.
First, if $a = 0$, rewrite $a \cdot b = p$ via the left-zero law to get $p = 0$, contradicting the nonzero clause of primeOrbit. Symmetrically, if $b = 0$, the right-zero law forces the same contradiction.
With both factors nonzero, split on whether $a$ is a unit. If so, take the left disjunct. Otherwise split on whether $b$ is a unit; if so, take the right disjunct. The remaining case packages $\langle a, b\rangle$ as a nontrivial factorization of $p$, contradicting the third clause of primeOrbit.
why it matters
This is the native Euclid lemma for prime orbits: every factorization of a prime has a unit factor. It is the algebraic engine behind unit_or_eq_of_divides_prime (if $a$ divides a prime orbit $p$, then $a$ is a unit or $a = p$), which unpacks the divisor witness and applies this theorem directly.
Both results feed orbit_divisibility_certificate, the closure theorem stating that the native orbit divisibility surface is complete (display, reflexivity, transitivity, and the prime-factor laws). In the Recognition foundation this keeps divisibility internal to the δ-orbit before any classical transfer, so later forcing-chain steps that rely on discrete orbit arithmetic inherit a clean prime notion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.