even_period_gap_certificate
plain-language theorem explainer
Packages the even-period-gap reduction as a single Prop certificate: any even-period-gap witness (or its bare existence) yields a nontrivial factorization of N. Factorization and master-certificate authors cite it to discharge the period-gap branch without replaying the witness algebra. The proof fills the two certificate fields by direct application of the two already-proved reduction lemmas.
Claim. There is a certificate asserting: for every nonzero distinction integer $N$ with $N\ge 2$, (i) an even-period-gap witness for $N$ implies $N$ admits a nontrivial factorization, and (ii) mere existence of such a witness likewise implies a nontrivial factorization of $N$.
background
In the Primitive Recognition Calculus factorization layer, period data on the unit residue of a distinction integer $N$ can force a split of $N$. An even-period-gap witness records a base unit residue whose period spectrum exhibits an even gap; the companion existence predicate asserts that some such witness exists, without naming it.
The local module isolates the conditional half of that story. Upstream, nontrivialFactorization_of_evenPeriodGapWitness already shows that any concrete witness produces a native nontrivial factorization of $N$, and nontrivialFactorization_of_evenPeriodGapExists unwraps an existence hypothesis and applies the same reduction. The certificate structure records exactly those two implications and states explicitly that the existence input itself is not supplied here.
proof idea
Tactic proof that constructs an inhabitant of the certificate structure. The witness_factorizes field is discharged by introducing $N$, the size hypothesis, and a witness $w$, then applying nontrivialFactorization_of_evenPeriodGapWitness. The existence_reduces_to_factorization field likewise introduces the existence hypothesis and applies nontrivialFactorization_of_evenPeriodGapExists. No new algebra is performed; both fields are one-line wrappers around the upstream reductions.
why it matters
This certificate is the even-period-gap leaf of the factorization master certificate. Downstream, delta_factorization_character_theory_certificate assembles chart-transition, residue-orbit, unit-group, and period-spectrum certificates into the character-theory factorization package; the present result is the period-gap reduction that package relies on when the spectrum is even.
In the Recognition foundation it keeps the forcing chain honest: period-based factoring is reduced to a single open existence statement rather than left as an ad-hoc case split. It does not close the existence question; it only certifies that once existence (or a witness) is granted, nontrivial factorization follows unconditionally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.