SubsetProductPhaseHit
plain-language theorem explainer
SubsetProductPhaseHit n c packages an auxiliary scaling x, the product N = n x, a divisor-exponent box, and the positivity and divisibility witnesses showing both box divisors land in the target phase modulo c. Researchers constructing explicit Erdős-Straus gates via phase-budget engines cite this record when converting a prime-phase generator output into an admissible hit. The declaration is a plain structure definition with no proof body or reduction steps.
Claim. For $n, c : ℕ$, a structure SubsetProductPhaseHit$(n,c)$ consists of $x, N : ℕ$, a DivisorExponentBox for $N$, and proofs that $n > 0$, $c > 0$, $x > 0$, $N > 0$, $N = n x$, $c = 4x - n$, and that $c$ divides both $N + d$ and $N + e$ where $d$ and $e$ are the divisor and complement extracted from the box.
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 supplies only a square-budget divisor whose phase matches the target; this finite layer converts that phase hit into the HitsBalancedPhase predicate already proved upstream.
proof idea
This is a structure definition. It directly records the fields x, N, box together with the four positivity conditions, the two linear relations N = n x and c = 4x - n, and the two divisibility conditions that place both boxDivisor and boxComplement into the target phase modulo c. No lemmas or tactics are applied.
why it matters
SubsetProductPhaseHit supplies the concrete witness consumed by PhaseBudgetEngine, EffectivePrimePhaseInput, and BoundedFiniteQuotientPhaseVisibility. Downstream it feeds MinimalVisibilityEngine to produce admissible gates and HitsBalancedPhase. It closes the finite-generation layer of the Erdős-Straus argument, bridging the prime-phase generator to the balanced-phase predicate while respecting the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.