PeriodFactorCertificate
plain-language theorem explainer
Certificate packaging two period-factor extraction claims: if n≥2 divides b²−1 but neither b−1 nor b+1, then gcd(b−1,n) is a proper nontrivial divisor of n; the same arithmetic on nonzero distinction orbits yields a native nontrivial factorization. Factorization-lane authors cite it as the period-factor surface. Pure Prop interface; the companion theorem fills both fields.
Claim. A certificate asserting two claims. (i) For natural numbers $n \ge 2$ and $b \ge 1$, if $n \mid (b^2-1)$ while $n \nmid (b-1)$ and $n \nmid (b+1)$, then $1 < \gcd(b-1,n) < n$. (ii) For a nonzero distinction-orbit position $N$ with $N$ at least $2$ in verifier naturals, and $b$ at least $1$, the same divisibility hypotheses imply that $N$ admits a nontrivial factorization (both factors nonzero and non-unit).
background
In the primitive recognition calculus, distinction orbits are the base-neutral finite counters DistinctionNat (zero and successor). The verifier map toNat reads an orbit as an ordinary natural number. Native arithmetic on orbits includes an object-level GCD by subtractive Euclidean descent and a native notion of nontrivial factorization: existence of factors that are nonzero, non-unit, and multiply back to the original orbit.
The local module sits in the factorization lane of the foundation stack. Period-factor extraction is the classical observation that if $n$ divides $b^2-1=(b-1)(b+1)$ yet divides neither factor, then $\gcd(b-1,n)$ is a proper nontrivial divisor of $n$. The certificate lifts that surface from Lean Nat to distinction orbits, so later character-theory and period-spectrum work can quote a single Prop bundle rather than raw lemmas.
proof idea
Definitional certificate structure: two named Prop fields and no proof body. The first field is the pure-Nat extraction statement (proper nontrivial gcd). The second field is the orbit-level restatement concluding native nontrivial factorization. Discharge is deferred to the companion theorem period_factor_certificate, which fills the Nat field by the sibling lemma even_period_yields_factor and the orbit field by the corresponding distinction-nat argument.
why it matters
This is the period-factor extraction surface for the factorization character-theory lane. Downstream, period_factor_certificate inhabits the structure, and the master ledger DeltaFactorizationCharacterTheoryCertificate aggregates chart transition, residue orbit, unit group, period spectrum, and finite multiplicative character certificates; period-factor work feeds that ledger's period-spectrum and factorization spine.
In Recognition Science terms, period structure is the arithmetic shadow of the eight-tick octave (forcing step T7, period $2^3$) and of orbit divisibility used to force discrete factors. Packaging the even-period gcd extraction as a certificate keeps the foundation stack auditable: the claim surface is fixed here, while proofs live in named inhabitants. No open scaffold remains on this declaration itself; it is pure interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.