TargetPhase
plain-language theorem explainer
TargetPhase supplies the target residue class -N mod c in the cyclic ring Z/cZ for the subset-product construction in the Erdős-Straus residual proof. It is referenced by the finite-layer conversion lemmas that turn a phase hit into the HitsBalancedPhase predicate. The definition performs a direct cast of N into ZMod c followed by additive inversion.
Claim. For natural numbers $N$ and $c$, the target phase is the element $-N$ in the cyclic ring $Z/cZ$.
background
The module isolates the finite subgroup-generation layer required by the Erdős-Straus residual proof. The analytic theorem supplies a divisor whose phase matches the target phase; the finite layer then converts the hit into the HitsBalancedPhase predicate. The 8-tick phases are defined as $kπ/4$ for $k=0,…,7$ and are periodic with period $2π$. The unimodular phase map sends a real angle $w$ to the complex number $e^{iw}$.
proof idea
The declaration is a one-line definition that embeds the natural number N into ZMod c and returns its additive inverse.
why it matters
This definition supplies the target residue class for the residual quotient in the subset-product phase layer. It supports the conversion lemmas that produce the HitsBalancedPhase predicate from a phase hit, completing the finite part of the Erdős-Straus argument. It sits downstream of the eight-tick phase construction in the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.