TargetPhase
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute any subset product or divisor.
- Does not impose primality or other conditions on c.
- Does not reference the 8-tick periodicity or complex exponential map.
formal statement (Lean)
43def TargetPhase (N c : ℕ) : ZMod c :=
proof body
Definition body.
44 -(N : ZMod c)
45
46/-- The generated divisor phase. -/