period_factor_certificate
plain-language theorem explainer
Packages even-period factor extraction into one certificate: if $b^2\equiv 1\pmod n$ while $b\not\equiv\pm 1$, then $\gcd(b-1,n)$ is a proper nontrivial divisor of $n$, and the same arithmetic on a distinction integer yields a native nontrivial factorization. Cited by the delta factorization master certificate in the character-theory stack. Proof is a two-field structure instance that applies the two extraction lemmas.
Claim. A period-factor certificate holds: (i) for $n,b\in\mathbb{N}$ with $n\ge 2$, $b\ge 1$, if $n\mid b^2-1$ yet $n\nmid(b-1)$ and $n\nmid(b+1)$, then $1<\gcd(b-1,n)<n$; (ii) for a nonzero distinction integer $N$ with $N\ge 2$ in underlying naturals and $b\ge 1$, the same divisibility hypotheses produce a nontrivial factorization of $N$.
background
In the Primitive Recognition Calculus factorization layer, an even-period gap is the arithmetic situation $b^2\equiv 1\pmod n$ with $b\not\equiv\pm 1\pmod n$. Classically this forces a proper divisor via $\gcd(b-1,n)$, since $n$ divides $(b-1)(b+1)$ but shares neither factor fully.
The module works in two presentations: plain naturals, and DistinctionNat (the $\delta$-form native integers of the recognition calculus). Upstream, even-period factor extraction states that under those congruences $\gcd(b-1,n)$ lies strictly between $1$ and $n$. The $\delta$-form companion lifts the same hypotheses to a native nontrivial factorization of $N$, with extracted divisor built from that gcd.
PeriodFactorCertificate is the Prop-structure bundling both surfaces so downstream master certificates can cite a single named object rather than the raw lemmas.
proof idea
Structure-instance proof with two tactic fields. The natural-number field introduces the five hypotheses ($n\ge 2$, $b\ge 1$, square congruence, and the two non-divisibilities) and closes by exact even_period_yields_factor on those hypotheses. The distinction-integer field does the same for the $\delta$-form hypotheses and closes by exact nontrivialFactorization_of_even_period_gap. No extra algebra: pure packaging of the two upstream extraction theorems into the certificate record.
why it matters
Supplies the period_factor leg of the factorization character-theory stack. Downstream, delta_factorization_character_theory_certificate assembles chart transition, residue orbit, unit group, period spectrum, and related surfaces into one master certificate; this declaration is the period-factor extraction surface that stack depends on.
In Recognition Science terms, even-period gaps are how certified period witnesses on the residue display force nontrivial factorizations of distinction integers. That feeds the broader forcing and spectrum story (period spectrum, eight-tick octave structure) without itself claiming dimensional or J-cost uniqueness. It closes the certificate interface for period-factor extraction so the master certificate can stay sorry-free on this edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.