DivisorCharacterSumBound
plain-language theorem explainer
The declaration packages the honest target proposition for the residual gap: every n satisfying the trapped class predicate admits an admissible gate c such that the divisor box meets the two-sided balanced phase condition. A researcher closing the Erdos-Straus rotation hierarchy would cite this as the precise statement that replaces the one-sided divisor congruence. The structure simply assembles the universal quantifier over residual traps with the existence claim for an admissible hard gate and the balanced phase predicate; no proof body is
Claim. Let $R(n)$ denote the predicate that $n>1$, $n≡1 mod 24$, and every prime factor of both $n$ and $(n+3)/4$ is congruent to 1 modulo 3. Let $A(c)$ mean $c≡3 mod 4$. Let $H(n,c)$ mean there exists $x,N$ and a divisor exponent box for $N=nx$ with gate $c=4x-n$ such that both divisors of $N^2$ satisfy the phase condition modulo $c$. The proposition asserts that for every natural number $n$, if $R(n)$ holds then there exists $c$ with $A(c)$ and $H(n,c)$.
background
The module records the honest obstruction: natural finite-phase mismatch cost decreases with gate size and cannot itself justify a uniform floor. Upstream, the residual trapped class predicate requires $n≡1 mod 24$ together with all prime factors of $n$ and $(n+3)/4$ lying in the 1 mod 3 class. The admissible hard gate predicate restricts to gates congruent to 3 mod 4 when the input class is 1 mod 4. The balanced phase predicate encodes the two-sided divisor condition that both $d$ and the complementary $e=N^2/d$ land in residue $-N$ modulo $c$. The eight-tick phase supplies the discrete angles $kπ/4$ for $k=0..7$.
proof idea
This is a structure definition that directly encodes the target proposition; it contains no proof body and serves as the interface for a future theorem.
why it matters
This supplies the precise statement of the missing prime/divisor distribution result required to produce an actual phase hit once the natural mismatch cost is acknowledged to decay. It stands as the final target before the framework can close the gap on uniform floors in the rotation hierarchy. No downstream theorems yet depend on it, leaving open whether the two-sided condition holds uniformly for all residual traps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.