nontrivialFactorization_of_evenPeriodGapExists
plain-language theorem explainer
If an even-period gap exists for a modulus N (the residual Shor-style success condition), then N has a nontrivial factorization. Period-based factoring work in the Recognition calculus cites this as the existence-to-factor map. The proof unpacks Nonempty to a concrete witness and applies the witness-level factorization lemma.
Claim. Let $N$ be a nonzero distinction natural with $N\ge 2$ in ordinary value. If the even-period-gap existence statement holds for $N$ (there is a unit residue whose multiplicative order yields an even-period gap), then $N$ admits a nontrivial factorization.
background
In the Primitive Recognition Calculus factorization lane, moduli are distinction naturals (orbit-coded positives). A unit residue of $N$ is coprime to $N$. An even-period gap is the $\delta$-form of Shor's success condition: a base whose order produces a nontrivial gcd factor of $N$.
EvenPeriodGapExists names the single open residual: Nonempty of an even-period-gap witness for $N$. The doc states it asserts nothing; proving the $\ge 1/2$ counting bound over the unit group of a composite with at least two distinct odd prime factors would close period-based factoring end to end.
Upstream, the witness-level theorem already shows that any concrete even-period-gap witness yields a native nontrivial factorization of $N$. This declaration lifts that conditional from a witness to the existence proposition.
proof idea
One-line unpacking of existence. From EvenPeriodGapExists N hN, which is Nonempty (EvenPeriodGapWitness N hN), obtain a witness w. Apply nontrivialFactorization_of_evenPeriodGapWitness at the size hypothesis $2\le N.\mathrm{toNat}$ and w. No new arithmetic is done here; the factorization work lives in the witness theorem.
why it matters
This is the existence form of the even-period-gap reduction: the reduction itself is unconditional; only the existence input remains open. Downstream, even_period_gap_certificate packages both the witness map and this existence-to-factorization implication into a single certificate structure for the lane.
In framework terms it isolates the residual of period-based factoring inside Recognition arithmetic: close the counting bound on even-period gaps for suitable composites, and the native nontrivial factorization follows by this theorem. It does not touch the forcing chain (T0–T8), RCL, or the mass ladder; it is pure factorization scaffolding in the foundation calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.