nontrivialFactorization_of_even_period_gap
plain-language theorem explainer
An even-period gap on a distinction integer N (some b with N dividing b²−1 but neither b−1 nor b+1) yields a native nontrivial factorization of N. The extracted factor is the gcd of b−1 with N, lifted back to DistinctionNat. Anyone citing period-based factoring in the primitive recognition calculus uses this bridge. The proof feeds the Nat-level gcd bounds into the proper-divisor factorization endpoint.
Claim. Let $N$ and $b$ be distinction naturals with $N \neq 0$, $N.toNat \ge 2$, and $b.toNat \ge 1$. If $N.toNat$ divides $b.toNat^2 - 1$ but divides neither $b.toNat - 1$ nor $b.toNat + 1$, then $N$ admits a nontrivial factorization in the native $\delta$-divisibility sense (via the proper divisor $\mathrm{ofNat}(\gcd(b.toNat-1, N.toNat))$).
background
In the primitive recognition calculus, integers live as DistinctionNat (orbit-count data), with toNat reading the underlying Nat and ofNat embedding back. Divisibility and units are the native $\delta$-layer predicates; a nontrivial factorization is the existence of a proper nonunit factor in that layer.
An even-period gap is the classical congruence condition $b^2 \equiv 1 \pmod n$ with $b \not\equiv \pm 1 \pmod n$. Upstream, even_period_yields_factor proves the Nat fact: under those hypotheses with $n \ge 2$ and $b \ge 1$, $\gcd(b-1,n)$ is strictly between $1$ and $n$. Separately, nontrivialFactorization_of_proper_divisor is the reusable endpoint: any proper nonunit divisor of a nonzero $N$ supplies a native nontrivial factorization. The present theorem is the $\delta$-form glue between those two surfaces; its hypotheses match what a certified period witness supplies through the residue display.
proof idea
Term-mode composition of two lemmas. First apply even_period_yields_factor to the underlying Nats to obtain $1 < \gcd(b.toNat-1, N.toNat) < N.toNat$. Then refine with nontrivialFactorization_of_proper_divisor, taking the candidate divisor $d := \mathrm{ofNat}(\gcd(b.toNat-1, N.toNat))$. The four side goals ($d \neq 0$, $d$ nonunit, $d \neq N$, and $d$ divides $N$) are discharged by transporting equalities through toNat_ofNat / toNat_zero and closing with omega, plus the standard Nat.gcd_dvd_right for the divisibility obligation.
why it matters
This is the $\delta$-layer bridge from even-period gap data to native factorization. Downstream, nontrivialFactorization_of_evenPeriodGapWitness closes the conditional path: an EvenPeriodGapWitness on $N$ produces a nontrivial factorization by reducing to a single existence statement. It is also wired into period_factor_certificate as the delta_even_period_factorizes field of the period-factor extraction surface.
In the Recognition framework this sits in Foundation factorization infrastructure supporting period readout, not a T0–T8 forcing step itself. Period structure elsewhere (eight-tick octave, pulsar period ladders) motivates why even-period gaps appear; the theorem itself is pure arithmetic glue. It does not invent new physics constants; it certifies that certified period witnesses factor $N$ natively once the residue display supplies the gap hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.