nontrivialFactorization_of_not_primeOrbit
plain-language theorem explainer
If a nonzero, non-unit finite distinction orbit is not prime, it admits a nontrivial factorization into two nonzero non-units. Number theorists working in the δ-orbit arithmetic cite this as the classical dichotomy between primes and composites. The proof is a one-line contradiction against the definition of a prime orbit.
Claim. Let $N$ be a finite distinction orbit. If $N \neq 0$, $N$ is not the multiplicative unit (the one-step orbit), and $N$ is not prime in the native orbit sense, then there exist nonzero non-unit orbits $a,b$ with $a \cdot b = N$.
background
The ambient object is DistinctionNat, the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, carrying a native multiplicative structure. In this arithmetic the only multiplicative unit is the one-step orbit (unit a means $a = 1$).
A nontrivial factorization of $n$ is a pair of factors both nonzero and non-unit whose product recovers $n$. A prime orbit is then defined exactly as nonzero, non-unit, and free of any such factorization. The present lemma is the contrapositive half of that definition: once zero and units are excluded, failure of primality is equivalent to existence of a nontrivial factorization.
The surrounding module builds a δ-native prime-coordinate transform by transporting Mathlib's Nat.primeFactorsList across the established δ/Nat display equivalence; this dichotomy is the first gate in that construction.
proof idea
One-line contradiction. Assume there is no nontrivial factorization. Package the three hypotheses (nonzero, non-unit, no factorization) into a witness of primeOrbit N, which directly contradicts the given ¬ primeOrbit N. No auxiliary lemmas are required beyond the definitional unfolding of primeOrbit.
why it matters
Feeds nativePrimeCoordinateData_exists, which asserts that every nonzero non-unit distinction orbit carries a nonempty prime-coordinate datum. That existence theorem is the classical-transport core of the δ prime-coordinate transform: it moves Mathlib's canonical prime-factor list across the δ/Nat equivalence rather than inventing a new factoring algorithm.
In the Recognition Science foundation layer this sits inside Primitive Recognition Calculus factorization, the arithmetic substrate on which later forcing-chain material (T5 J-uniqueness, T6 φ fixed point, T7 eight-tick octave) ultimately rests. Without the prime/composite dichotomy in native δ language, the coordinate transform cannot even state its domain. The result is fully proved; it closes no open scaffold, it simply makes the classical dichotomy available in orbit syntax.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.