Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.EvenPeriodGap

show as:
view Lean formalization →

Defines the even-period gap configuration on unit residues modulo N: a base whose order is twice a half-period, with the half-power avoiding both 1 and -1. Anyone citing the classical post-period-finding step of Shor-style factorization will use these witnesses and certificates. The module packages the gap as a Prop, derives a nontrivial factor from it, and exposes a certificate that MasterCertificate imports.

claimAn even-period gap witness for modulus $N$ is a unit residue $a$ together with a half-period $h$ such that $a^{2h}\equiv 1\pmod{N}$ while $a^h\not\equiv\pm 1\pmod{N}$. From any such witness one obtains a nontrivial factor of $N$. The module also records an existence form and a packaged certificate of the same gap.

background

In the Primitive Recognition Calculus factorization layer, one works with unit residues modulo a composite $N$ and with multiplicative periods of those residues. The sibling module PeriodFactor supplies the basic period-to-factor map: when a power lands on a nontrivial square root of unity, $\gcd(a^{r/2}\pm 1,N)$ splits $N$.

An even-period gap is the precise arithmetic configuration that makes that map fire. The base has full period $2h$ (so $a^{2h}\equiv 1$), yet the midpoint $a^h$ is neither $1$ nor $-1$ modulo $N$. The module doc states this is exactly the configuration Shor's algorithm needs after period finding.

The local setting is classical number-theoretic scaffolding inside the Foundation domain, not yet the RS forcing chain (T0--T8). It prepares a clean interface so later certificates can assert that a recognition-derived period yields a factor.

proof idea

The module is a thin factorization interface, not a deep proof development. It introduces a witness structure (base, half-period, and the three modular conditions), then a one-step lemma that feeds the witness into the upstream period-factor construction to obtain a nontrivial factor. Parallel existence and certificate wrappers rephrase the same data for downstream consumption. No heavy tactic scripts; the argument is the standard gcd extraction from a nontrivial square root of 1.

why it matters in Recognition Science

MasterCertificate imports this module, so every top-level factorization certificate in the Primitive Recognition Calculus stack can cite an even-period gap rather than re-deriving the half-period conditions. That keeps the Shor-style post-processing step modular: period finding (or its RS analogue) hands off a gap witness, and nontrivial factorization follows by the packaged lemma.

Within Recognition Science the module is infrastructure for the factorization side of the foundation, not a forcing-chain landmark. It does not invoke J-cost, phi, or the eight-tick octave; it only ensures that once an even period appears, the classical factor extraction is already proved and named for reuse.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)