EvenPeriodGapWitness
plain-language theorem explainer
Packages the classical even-period-gap success condition for a nonzero modulus N: a unit base whose double half-period returns to the identity residue, while the half-power avoids both +1 and -1. Anyone reducing period-based factoring (Shor-style) to a single existence claim in the δ-native calculus would cite it. Pure structure definition; no proof content.
Claim. For a nonzero distinction-natural $N$, an even-period-gap witness is a pair $(b,h)$ of distinction-naturals such that $b$ is coprime to $N$, $b^{2h}\equiv 1\pmod{N}$, yet $N$ divides neither $b^h-1$ nor $b^h+1$ (i.e., $b^h\not\equiv\pm 1\pmod{N}$).
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Residues and powers are native: orbitPow b k is δ-exponentiation of $b$ by orbit exponent $k$, and sameResidue N asserts equality of residues modulo $N$. A residue is a unit when it is δ-coprime to $N$ (unitResidue).
The module sits in the factorization lane of PrimitiveRecognitionCalculus. After period finding, classical Shor factoring needs a unit $b$ whose order is even and whose half-power is neither $\pm 1$ mod $N$; gcd steps then split $N$. This structure is exactly that configuration, stated entirely in distinction-natural language rather than ordinary $\mathbb{Z}/N\mathbb{Z}$.
proof idea
No proof: the declaration is a structure (data package). Fields record the base, the half-period, unit-ness of the base, the full-period return $b^{h+h}\equiv 1$, and the two non-divisibility side conditions that keep the half-power off $\pm 1$. Downstream theorems consume an inhabitant of this type.
why it matters
This is the native packaging of Shor's post-period-finding success condition. Downstream, nontrivialFactorization_of_evenPeriodGapWitness turns any such witness (for $N\ge 2$) into a nontrivial factorization of $N$, so period-based factoring reduces to a single existence statement. That residual is named by EvenPeriodGapExists (Nonempty of this structure) and is explicitly open: proving a counting bound $\ge 1/2$ over the unit group of a composite with at least two distinct odd prime factors would close the lane end to end. EvenPeriodGapCertificate records the proved conditional and flags that existence is not supplied here. In the broader RS foundation this is arithmetic infrastructure for recognition orbits, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.