NonzeroResidual
plain-language theorem explainer
NonzeroResidual c N asserts that c and N are both positive natural numbers, encoding the condition for a nonzero residual fraction c/N in the Erdős-Straus rotation hierarchy. Number theorists examining finite cyclic quotients from residual gates cite this predicate when building phase structures. The definition is implemented as the direct conjunction of the two strict inequalities 0 < c and 0 < N.
Claim. The predicate holds precisely when $c > 0$ and $N > 0$ for $c, N$ natural numbers, capturing a nonzero residual $c/N$ with positive finite modulus.
background
The Erdős-Straus Recognition Rotation Hierarchy module converts the RCL attack into a theorem-shaped skeleton. It isolates finite gate pieces while leaving two missing engines: prime phase separation across admissible residual quotients and reciprocal pair closure. No new axioms appear; the missing engines remain explicit structure fields for future proofs.
proof idea
The definition is a direct conjunction of the two positivity conditions on c and N. No lemmas are invoked; it functions as a primitive predicate supplying the hypothesis for downstream results.
why it matters
This definition supplies the hypothesis for finite_quotient_necessity, which establishes that every nonzero residual gate induces a finite cyclic quotient Z/cZ. It completes the finite/gate piece of the module skeleton and connects to the eight-tick octave via the upstream phase definitions (kπ/4 for k = 0..7 and the unimodular e^{i w}). It touches the open question of prime phase separation across admissible residuals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.