nontrivialFactorization
plain-language theorem explainer
A native orbit n admits a nontrivial factorization when it is a product of two nonzero, non-unit factors in the finite δ-orbit monoid. Factorization and period-gap certificates cite this predicate as the common target of proper-divisor and even-period-gap reductions. The body is a pure existential definition over DistinctionNat multiplication.
Claim. An orbit $n$ in the finite distinction monoid has a nontrivial factorization if there exist orbits $a,b$ with $a \neq 0$, $b \neq 0$, neither equal to the one-step unit, and $a \cdot b = n$.
background
The ambient carrier is DistinctionNat, the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, equipped with native multiplication from the orbit-arithmetic layer. Units are defined natively: the only multiplicative unit is the one-step orbit (unit a means a = one).
This sits in the Primitive Recognition Calculus divisibility module, which builds a δ-native divisibility theory before any passage to ordinary Nat. The predicate packages the usual ring-theoretic idea of a nontrivial factorization, but with both factors required nonzero and non-unit in the orbit monoid, matching the doc-comment: "Both factors must be nonzero and non-unit."
proof idea
Definitional, not a proved theorem. The predicate is the existential
$\exists a,b.; a\neq 0 \land b\neq 0 \land \neg\mathrm{unit}(a) \land \neg\mathrm{unit}(b) \land a\cdot b = n$
over DistinctionNat. No tactics or upstream lemmas are applied; downstream theorems inhabit this Prop by constructing explicit factors.
why it matters
This is the shared landing predicate for the factorization stack. Proper nonunit divisors produce it via nontrivialFactorization_of_proper_divisor ("reusable endpoint for period-readout factoring"). Even-period-gap witnesses and existence statements reduce to it (nontrivialFactorization_of_evenPeriodGapWitness, ...Exists), and the PeriodFactor layer extracts a concrete gcd divisor into the same shape. Chart-transition and even-period-gap certificates record that product displays and gap witnesses imply this factorization.
In the Recognition framework it is the native bridge from period/residue data on the δ-orbit to composite structure, feeding the path toward prime-orbit classification and the eight-tick octave arithmetic without leaving the orbit monoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.