EvenPeriodGapExists
plain-language theorem explainer
Names the residual open proposition for modulus N: existence of a unit residue whose multiplicative order has an even-period gap (full period 2·half returns to 1, while the half-power avoids ±1). Anyone citing the period-to-factor reduction or the δ-form of Shor success uses this name. The body is a one-line Nonempty wrapper around the witness structure; it asserts nothing.
Claim. For a nonzero distinction modulus $N$, write $\mathrm{EvenPeriodGapExists}(N)$ for the proposition that there exists a unit residue $a$ modulo $N$ together with a half-period $h$ such that $a^{2h}\equiv 1\pmod{N}$ while $a^h\not\equiv\pm 1\pmod{N}$. Equivalently, the type of even-period-gap witnesses for $N$ is inhabited.
background
In the primitive recognition calculus, moduli and residues live on DistinctionNat, the base-neutral finite orbit of repeated distinction (K2.12). Multiplicative dynamics are written via orbit powers: repeated distinction steps play the role of modular exponentiation.
An even-period-gap witness packages exactly the configuration Shor needs after period finding: a unit residue base and a half-period half such that the full period half+half returns to the identity residue, while the half-power is divisible by neither the $+1$ nor the $-1$ difference modulo $N$. The surrounding factorization module already proves that any such witness yields a nontrivial factorization of $N$ (when $N\ge 2$).
This definition does not prove existence. It only names the open existence proposition as nonemptiness of that witness type, so downstream certificates can quantify over a single residual hypothesis.
proof idea
Definitional, not a proof. The right-hand side is Nonempty (EvenPeriodGapWitness N hN), so the named proposition is literally inhabitance of the witness structure. No tactics, no lemmas, no reduction steps.
why it matters
This is the single open lane in the period-based factoring stack inside PrimitiveRecognitionCalculus. Downstream, nontrivialFactorization_of_evenPeriodGapExists turns any proof of this proposition (for $N\ge 2$) into a nontrivial factorization by unpacking the witness and applying the already-proved witness-to-factor map. EvenPeriodGapCertificate records that conditional: the reduction is closed; only the existence input remains open.
In Recognition terms the object is the δ-form of Shor's success condition. Closing it means establishing a counting lower bound (classically $\ge 1/2$) over the unit group of a composite with at least two distinct odd prime factors. Until that bound is formalized, period-based factoring is end-to-end conditional on this named residual. It sits in the Foundation factorization layer rather than the T0–T8 forcing chain, but it is the precise hinge between orbit period structure and nontrivial factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.