hitsBalancedPhase_iff_nonempty_subsetProductPhaseHit
plain-language theorem explainer
The predicate that a square-budget box hits the balanced residual phase for gate c is equivalent to the existence of a phase-generating subset-product witness for parameters n and c. Researchers on the finite layer of the Erdős-Straus residual proof cite this to interchange the existential predicate with the structural witness. The proof is a direct term-mode biconditional built from the two conversion lemmas.
Claim. For natural numbers $n$ and $c$, a square-budget box hits the balanced residual phase for gate $c$ if and only if there exists a phase-generating subset-product witness for $n$ and $c$.
background
The module isolates the finite subgroup-generation layer needed by the Erdős-Straus residual proof. The analytic prime-distribution theorem supplies a square-budget divisor whose phase matches the target; this layer converts the hit into the HitsBalancedPhase predicate used by the closure module. HitsBalancedPhase n c asserts existence of x, N and box such that N = n * x, c = 4*x - n, and both the divisor and its complement satisfy the phase conditions c | N + divisor and c | N + complement. SubsetProductPhaseHit packages the same data as a structure with explicit positivity proofs.
proof idea
The proof is a term-mode biconditional. One direction applies the theorem subsetProductPhaseHit_of_hitsBalancedPhase to obtain a nonempty witness from the phase predicate. The converse applies generated_phase_hit_gives_HitsBalancedPhase to the witness to recover the predicate.
why it matters
This equivalence bridges the existential HitsBalancedPhase predicate used in the Erdős-Straus closure module with the structural SubsetProductPhaseHit in the subset-product phase layer. It completes the finite-generation interface required by the Recognition Science treatment of the Erdős-Straus conjecture, allowing the prime-phase generator to feed directly into the already-proved balanced-phase conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.