generatedComplementPhase
plain-language theorem explainer
The generatedComplementPhase definition extracts the complementary divisor phase in ZMod c from a SubsetProductPhaseHit witness. Number theorists closing the Erdős-Straus residual proof would cite it to bridge an analytic phase hit to the finite box-phase predicate. It is realized as a direct cast of the boxComplement field of the witness.
Claim. Let $hit$ be a SubsetProductPhaseHit for $n,c$ consisting of a square-budget divisor $box$ together with conditions $N=nx$ and $c=4x-n$ ensuring both the generated divisor and its complement lie in the target phase modulo $c$. The complementary divisor phase is the image of the complementary divisor of $box$ in the ring $ZMod c$.
background
The Subset-Product Phase Layer isolates the finite subgroup-generation layer needed by the Erdős-Straus residual proof. The analytic prime-distribution theorem supplies only a square-budget divisor whose phase is the target phase; the finite layer converts that phase hit into the HitsBalancedPhase predicate. A SubsetProductPhaseHit $n$ $c$ is the structure containing $x$, $N$, $box$ : DivisorExponentBox $N$ with $N = n x$ and $c = 4 x - n$ plus the four positivity hypotheses. boxComplement returns the complementary divisor $e$ selected by the box point. Upstream results include the 8-tick phase definition (periodic with period $2π$) and the actualization operator $A$ that maps a configuration to its $J$-minimizer.
proof idea
One-line wrapper that applies boxComplement to the box field of the hit and casts the resulting natural number to ZMod c.
why it matters
This definition supplies the complementary divisor phase required by the Erdős-Straus closure module. It completes the conversion step that lets the analytic theorem supply only the phase hit while the finite layer produces the already-proved HitsBalancedPhase predicate. The module doc states that the analytic theorem should not construct unit fractions directly, only the square-budget divisor. It therefore occupies the exact interface between the Riemann-hypothesis wedge phase generator and the finite subgroup predicate inside the Recognition number-theory component.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.