even_period_yields_factor
plain-language theorem explainer
If n divides b²−1 but divides neither b−1 nor b+1, then gcd(b−1,n) is a proper nontrivial divisor of n. Number theorists and anyone extracting factors from even-period witnesses cite this. The proof is elementary gcd arithmetic: the square-difference identity plus coprimality forces the gcd off both 1 and n.
Claim. Let $n,b\in\mathbb{N}$ with $n\ge 2$ and $b\ge 1$. Suppose $n\mid(b^2-1)$, yet $n\nmid(b-1)$ and $n\nmid(b+1)$. Then $1 < \gcd(b-1,n) < n$.
background
In the Primitive Recognition Calculus factorization layer, an even-period witness is a base $b$ whose square is congruent to 1 modulo the modulus $n$, without $b$ itself being $\pm 1$ mod $n$. That congruence is exactly $n\mid(b^2-1)$. The classical identity $(b-1)(b+1)=b^2-1$ (proved here for truncated natural subtraction when $b\ge 1$) then places $n$ as a divisor of a product.
The local module sits under Foundation factorization and feeds native $\delta$-level statements on DistinctionNat. Upstream, sub_mul_add_eq_sq_sub_one supplies the square-difference factorization in $\mathbb{N}$. Residue and orbit machinery (residue displays, ofNat embeddings) later lift the extracted gcd into the recognition arithmetic, but this theorem itself is pure Nat number theory: no orbit structure is required in the statement.
The conclusion $1<\gcd(b-1,n)<n$ is the standard nontrivial-factor certificate used throughout period-based factorization arguments.
proof idea
Apply the upstream square-difference lemma to get $(b-1)(b+1)=b^2-1$, so $n$ divides the product. Write $g=\gcd(b-1,n)$. Always $g\mid n$. If $g=n$ then $n\mid(b-1)$, contradicting the hypothesis, so $g<n$ (using $n\ge 2$ for positivity). If $g=1$ then $b-1$ and $n$ are coprime, hence $n$ divides the other factor $b+1$, again a contradiction. Positivity of $g$ is immediate from $n>0$, and omega closes $1<g$.
why it matters
This is the Nat core of even-period factor extraction in the Recognition factorization stack. Downstream, nontrivialFactorization_of_even_period_gap lifts it to DistinctionNat: an even-period gap on $N$ yields a native nontrivial factorization with extracted divisor ofNat(gcd(b-1,N)), using exactly the hypotheses a certified period witness supplies through the residue display. The certificate structure period_factor_certificate packages this theorem as the nat_even_period_extracts field of PeriodFactorCertificate.
In the broader framework, period structure on the recognition orbit is the arithmetic face of the eight-tick octave and self-similar $\phi$-ladder timing. Extracting a proper factor from an even period is the concrete computational content of that timing: it turns a modular order condition into a divisor. Without this lemma the $\delta$-level corollary and the certificate bundle have no Nat engine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.