EvenPeriodGapCertificate
plain-language theorem explainer
Packages the even-period-gap reduction as a Prop certificate: any Shor-style even-period witness on a modulus N (size at least 2), or mere existence of one, implies a native nontrivial factorization of N. Downstream master ledgers and the local inhabitant cite it as the closed conditional half of period-based factoring. Definitional structure only; the two fields name already-proved implications and explicitly leave existence open.
Claim. A certificate consisting of two implications for every nonzero orbit modulus $N$ with $N\ge 2$: (i) if a unit residue $a$ has even period $2h$ with $a^h\not\equiv\pm 1\pmod{N}$, then $N$ admits a nontrivial factorization; (ii) if such a residue merely exists, then $N$ likewise admits a nontrivial factorization. Existence of the residue is not asserted.
background
In the Primitive Recognition Calculus, moduli and bases live in DistinctionNat, the base-neutral finite orbit of repeated distinction, with toNat the verifier reading as ordinary naturals. A native nontrivial factorization of $N$ is a product $N=ab$ with both factors nonzero and non-units.
An even-period-gap witness is exactly Shor's post-period-finding configuration: a unit residue base whose full period is half+half back to the identity, while the half-power avoids both $1$ and $-1$ modulo $N$. EvenPeriodGapExists is the residual open proposition that such a witness is nonempty for $N$; the module doc treats it as the $\delta$ form of Shor's success condition and does not prove the usual $\ge 1/2$ counting bound over the unit group of a composite with two distinct odd prime factors.
This structure sits in the factorization lane that reduces period-based factoring to that single open existence input.
proof idea
No proof body: the declaration is a structure ... : Prop whose two fields are named implications. The first field is the type of the already-proved map from an even-period-gap witness to a nontrivial factorization. The second is the type of the corresponding map from mere nonempty existence. Inhabitation is deferred to the sibling theorem that fills both fields by applying those two reduction lemmas.
why it matters
This is the explicit ledger entry for the closed half of the even-period-gap story: reduction is unconditional; only existence is open. The sibling inhabitant even_period_gap_certificate builds a term of this type, and the master structure DeltaFactorizationCharacterTheoryCertificate pulls the factorization character-theory lane together (chart transition, residue orbit, unit group, period spectrum, finite multiplicative characters). Closing EvenPeriodGapExists via the standard counting bound on composites with at least two distinct odd prime factors would finish period-based factoring end to end inside the PRC factorization stack. The certificate itself records that boundary cleanly so downstream ledgers do not smuggle an existence proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.