subsetProductPhaseHit_of_hitsBalancedPhase
plain-language theorem explainer
If the balanced residual phase condition holds for parameters n and c, then a subset-product phase witness structure exists. Number theorists extending the Erdős-Straus argument via phase methods cite this to switch between existential and structured formulations. The proof unpacks the existential quantifier in the hypothesis and repackages the extracted data into the structure constructor.
Claim. For natural numbers $n$ and $c$, if there exist $x$, $N$ and a divisor exponent box such that the positivity conditions hold, $N = n x$, $c = 4x - n$, and $c$ divides both $N$ plus the box divisor and $N$ plus the box complement, then the structure type packaging those data is inhabited.
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 in the target phase; this layer converts that hit into the balanced residual phase predicate. The balanced residual phase condition asserts existence of $x$, $N$ and a box satisfying $N = n x$, $c = 4x - n$, and the two divisibility conditions on the defects. The subset-product phase witness is the structure whose fields are exactly those components together with their proofs. This rests on the balanced phase definition in the Erdős-Straus box phase module.
proof idea
The term proof performs rcases on the hypothesis to extract the existential witness components $x$, $N$, box and the accompanying positivity, equality and divisibility proofs. It then applies the mk constructor of the witness structure to those components, producing an element that witnesses nonemptiness.
why it matters
This supplies the forward direction of the equivalence between the existential predicate and the nonempty structure type. The sibling theorem records the converse and states the two formulations are equivalent. Downstream, the minimal visibility engine applies the result to obtain a phase witness from an admissible gate. It closes the finite layer that prepares structured data for the residual proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.