nontrivialFactorization_of_proper_divisor
plain-language theorem explainer
A proper nonunit divisor of a nonzero distinction orbit yields a native nontrivial factorization of that orbit. Period-readout and spectrum arguments cite this once a gcd or residue witness produces such a divisor. The proof builds the complementary quotient, recovers the product via the Nat display, and rules out units by the properness hypotheses.
Claim. Let $N$ and $d$ be distinction orbits. If $N\neq 0$, $d\neq 0$, $d$ is not a unit, $d\neq N$, and $d$ divides $N$, then $N$ admits a nontrivial factorization: nonzero nonunit factors whose product is $N$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the primitive carrier for arithmetic in the Primitive Recognition Calculus. Its verifier display toNat reads the iteration count as a Lean natural; injectivity of that display (toNat_inj) and the recovery theorem for multiplication (toNat_mul) let native equalities be proved on Nat and pulled back.
Divisibility, quotient, and unit are the δ-native arithmetic layer on these orbits. A unit is the multiplicative identity orbit; a nontrivial factorization of $N$ is a pair of nonzero nonunit factors multiplying to $N$. The module sits in Factorization.ChartTransition, which packages magnitude ambiguity and chart-transition certificates for period factoring.
Upstream, ArithmeticFromLogic supplies the LogicNat/Nat bridge that OrbitArithmetic mirrors for DistinctionNat. The local setting is reusable endpoint infrastructure: once a period witness hands a proper divisor, this lemma turns it into a factorization without further period structure.
proof idea
Form the complementary quotient $q = N/d$. Nonzeroness of $q$ is quotient_ne_zero_of_divides from the nonzero modulus and the divides hypothesis. The Nat identity $q.\mathrm{toNat}\cdot d.\mathrm{toNat}=N.\mathrm{toNat}$ is quotient_mul_divisor_toNat_of_divides; lift it to $q\cdot d=N$ by toNat_mul then toNat_inj.
Non-unitness of $q$ is by contradiction: if $q$ were a unit, the product identity and one_mul_eq would force $d=N$, contradicting properness. Package $\langle q,d\rangle$ with the four side conditions as a nontrivial factorization witness.
why it matters
This is the reusable δ-endpoint for period-readout factoring: once a period witness supplies a proper gcd divisor, the divisibility layer yields a factorization. Downstream, period_divisor_to_nontrivialFactorization is a one-line application from a ProperDivisorFromPeriod certificate, and nontrivialFactorization_of_even_period_gap routes even-period gap hypotheses through the same endpoint (extracted divisor ofNat(gcd(b-1,N))).
It also feeds chart_transition_certificate in the same module, which records the obstruction surface where equal product magnitudes underdetermine left and right factors (the explicit $2\cdot 6=3\cdot 4$ ambiguity). In the Recognition stack this sits under Primitive Recognition Calculus factorization, supporting native arithmetic before mass-ladder or forcing-chain (T0–T8) physics; it does not itself invoke J-cost, phi, or the eight-tick octave, but closes the arithmetic step those later layers assume when periods factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.