TargetPhase
plain-language theorem explainer
TargetPhase supplies the target phase for the residual quotient as the additive inverse of N modulo c. Workers on the Erdős-Straus residual argument in the subset-product layer cite it to receive a phase hit from the analytic side. The definition is a direct one-line assignment in the ZMod ring.
Claim. The target phase in the residual quotient is defined by $-N$ in the ring of integers modulo $c$.
background
The module isolates the finite subgroup-generation layer required by the Erdős-Straus residual proof. The analytic prime-distribution theorem is expected only to supply a square-budget divisor whose phase equals the target phase; the finite layer then converts that hit into the already-proved HitsBalancedPhase predicate.
proof idea
one-line definition that assigns the additive inverse of N inside ZMod c
why it matters
This definition occupies the target-phase slot inside the subset-product phase layer that feeds the Erdős-Straus residual argument. It sits immediately downstream of the eight-tick phase (kπ/4) and the wedge phase (e^{i w}) constructions, allowing the analytic side to hand off a divisor whose phase matches the required residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.