nontrivialFactorization_of_evenPeriodGapWitness
plain-language theorem explainer
An even-period-gap witness on a nonzero modulus N (with N ≥ 2) yields a native nontrivial factorization of N. Anyone reducing period-based factoring to a single existence claim cites this. The proof builds the classical x² ≡ 1 (mod N) with x ≉ ±1 from the witness fields, then hands off to the even-period-gap factorization lemma.
Claim. Let $N$ be a nonzero distinction-natural with $N \ge 2$ in ordinary naturals. Suppose there is a unit residue $b$ modulo $N$ and a half-period $h$ such that $b^{2h} \equiv 1 \pmod{N}$, while $b^h \not\equiv 1 \pmod{N}$ and $b^h \not\equiv -1 \pmod{N}$. Then $N$ admits a nontrivial factorization.
background
In the Primitive Recognition Calculus factorization lane, moduli live as DistinctionNat values, with ordinary size read off by toNat. A unit residue is a base coprime to $N$. Powers are formed by the orbit iterator orbitPow; addition of exponents recovers ordinary addition under toNat_add.
An even-period-gap witness packages exactly Shor's post-period-finding configuration: a unit base whose full period is twice a half-exponent, the full power returns to the identity residue, and the half-power avoids both $+1$ and $-1$ modulo $N$. The sibling structure records those four fields as native residue and divisibility statements.
The local module isolates the conditional half of period-based factoring. Upstream, nontrivialFactorization_of_even_period_gap already turns the numerical gap ($N \mid x^2-1$ with $x \not\equiv \pm 1$) into a nontrivial factor. This theorem only has to manufacture that numerical gap from the witness.
proof idea
Tactic proof in six steps. First, unit-residue implies the base is coprime to $N$, so its toNat is at least 1 (zero would force $N=1$, contradicting coprimality). Second, orbitPow_toNat and Nat.one_le_pow lift that positivity to the half-power. Third, two applications of orbitPow_toNat plus toNat_add and pow_add give $(b^{h+h}).\mathrm{toNat} = (b^h.\mathrm{toNat})^2$. Fourth, sameResidue_iff_mod_eq turns the full-period field into a congruence $b^{2h} \equiv 1 \pmod{N}$. Fifth, rewrite that congruence as $N \mid x^2-1$ via Nat.modEq_iff_dvd'. Finally, feed the size hypotheses and the two half-power avoidance fields into nontrivialFactorization_of_even_period_gap.
why it matters
This is the conditional closure of the even-period-gap lane: once a witness exists, factorization is unconditional and native. Downstream, nontrivialFactorization_of_evenPeriodGapExists simply unpacks an existence hypothesis and applies this theorem; even_period_gap_certificate packages the same arrow as the witness_factorizes field of the certificate structure.
The module doc states the residual open lane precisely: existence of such a unit with an even-period gap (the $\delta$ form of Shor's success condition, including the classical $\ge 1/2$ counting bound over the unit group of a composite with at least two distinct odd prime factors). Proving that existence would close period-based factoring end to end. This theorem does not touch that counting problem; it only seals the witness-to-factor arrow so the open residue is a pure existence statement.
In the broader Recognition foundation this sits inside the Primitive Recognition Calculus factorization stack, not the T0–T8 forcing chain itself. It is infrastructure for arithmetic consequences of the modular logic realization, not a claim about $\varphi$, the eight-tick octave, or the $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.