generated_phase_hit_gives_HitsBalancedPhase
plain-language theorem explainer
A SubsetProductPhaseHit witness for natural numbers n and c directly yields the HitsBalancedPhase predicate. Researchers closing the finite layer of the Erdős-Straus residual proof in Recognition Science cite this result to convert a generated target phase into the balanced box condition. The proof is a one-line wrapper that extracts the x, N, box and all accompanying positivity and equality fields from the input structure.
Claim. Let $n,c$ be positive integers. If a phase-generating subset-product witness exists for $n$ and $c$, then there exist $x,N$ and a divisor-exponent box such that $N=nx$, $c=4x-n$, and both the divisor and its complement satisfy the balanced residual phase condition 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; this module converts that phase hit into the already-proved HitsBalancedPhase predicate. SubsetProductPhaseHit(n,c) is the structure containing x, N, box : DivisorExponentBox N together with the conditions 0<n, 0<c, N=nx, c=4x-n and the two divisibility statements that place both generated divisor and complement in phase -N modulo c. HitsBalancedPhase(n,c) is the existential statement of exactly those same data plus the divisibility conditions c | N + boxDivisor box and c | N + boxComplement box.
proof idea
The proof is a one-line wrapper. It applies the refine tactic to the existential quantifiers of HitsBalancedPhase by supplying the fields hit.x, hit.N, hit.box together with the positivity, equality and phase conditions already stored inside the SubsetProductPhaseHit witness.
why it matters
The declaration supplies the forward direction of the equivalence between HitsBalancedPhase and nonempty SubsetProductPhaseHit, and is invoked inside generated_phase_hit_gives_repr to obtain the rational Erdős-Straus representation. It therefore closes the finite subgroup-generation layer that sits between the prime-phase generator and the Erdős-Straus closure module. The construction relies on the eight-tick phase definitions imported from Foundation.EightTick and on the box-phase predicate defined in ErdosStrausBoxPhase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.