ResidualPhaseQuotient
plain-language theorem explainer
ResidualPhaseQuotient defines the finite cyclic group Z/cZ as the phase quotient induced by a residual gate of order c. Number theorists extending the Erdős-Straus conjecture inside the Recognition framework cite it when establishing finite quotients from nonzero residuals. The declaration is a direct one-line abbreviation to Mathlib's ZMod type.
Claim. For a natural number $c$, the residual phase quotient is the cyclic group of integers modulo $c$, written $Z/cZ$.
background
The Erdős-Straus Recognition Rotation Hierarchy module converts the Recognition Composition Law attack into a theorem-shaped proof skeleton. It isolates the finite/gate pieces and leaves two missing number-theoretic engines as explicit structure fields: prime phase separation across admissible residual quotients and reciprocal pair closure once phase support appears. No new axioms are added.
proof idea
The declaration is a one-line abbreviation that directly equates ResidualPhaseQuotient c to the standard ZMod c type.
why it matters
This supplies the finite quotient type required by the finite_quotient_necessity theorem, which states that every nonzero residual gate induces a finite cyclic quotient Z/cZ. It also supports the GateHasPhaseSupport definition in the same module. Within the Recognition framework it advances the rotation hierarchy by providing the algebraic structure for the finite cyclic quotients needed in prime phase separation, as described in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.