generatedDivisorPhase
plain-language theorem explainer
generatedDivisorPhase extracts the modular phase of the divisor selected inside a SubsetProductPhaseHit witness, returning it in ZMod c. Researchers proving the Erdős-Straus conjecture through finite phase layers cite it when converting a square-budget divisor into its target residue class. The definition is a direct one-line projection that applies the boxDivisor accessor and performs the cast.
Claim. Let $n,c>0$ be positive integers and let $h$ be a SubsetProductPhaseHit witness with parameters $n,c$. Then the generated divisor phase is the integer $d$ selected by the box field of $h$, viewed as an element of the ring of integers modulo $c$.
background
The Subset-Product Phase Layer isolates the finite subgroup-generation step required by the Erdős-Straus residual proof. The analytic prime-distribution theorem is expected only to supply a square-budget divisor whose phase matches the target; the finite layer below converts that hit into the already-proved HitsBalancedPhase predicate. SubsetProductPhaseHit is the structure carrying the witness: it records positive integers $x,N$ together with a DivisorExponentBox $N$ such that $N=nx$ and $c=4x-n$, guaranteeing that both the generated divisor and its complement land in the target phase $-N$ modulo $c$.
proof idea
One-line definition that applies boxDivisor to the box field of the supplied hit and casts the resulting natural number into ZMod c.
why it matters
This definition supplies the divisor-phase component needed to establish the HitsBalancedPhase predicate inside the Erdős-Straus chain. It belongs to the finite layer that bridges the RiemannHypothesis.Wedge phase construction to the EightTick.phase structure (the 8-tick phases $kπ/4$). The module doc states that the analytic theorem should not be asked to construct unit fractions directly; this accessor therefore closes one link in that separation of concerns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.