generated_phase_hit_gives_repr
plain-language theorem explainer
A SubsetProductPhaseHit witness for natural numbers n and c implies that the rational n admits a representation 4/n = 1/x + 1/y + 1/z with three nonzero rationals x, y, z. Number theorists studying the Erdős-Straus conjecture would cite this to link the finite subset-product generation layer to the representation result. The proof is a one-line term composition that first converts the phase hit into a HitsBalancedPhase predicate and then applies the box-phase representation theorem.
Claim. Given a phase-generating subset-product witness for natural numbers $n$ and $c$, the rational $n$ satisfies $4/n = 1/x + 1/y + 1/z$ for some nonzero rationals $x, y, z$.
background
The Subset-Product Phase Layer 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 is the target phase; this finite layer converts that phase hit into the already-proved HitsBalancedPhase predicate. SubsetProductPhaseHit is the structure with fields x, N, box : DivisorExponentBox N together with positivity and equality conditions N = n * x, c = 4 * x - n, plus divisibility conditions ensuring both the generated divisor and its complement land in the target phase -N modulo c. HitsBalancedPhase (n c) is the existential predicate asserting exactly those equalities and the two divisibility conditions on the box. HasRationalErdosStrausRepr (n : ℚ) asserts existence of nonzero rationals x, y, z such that 4/n equals the sum of their reciprocals. The upstream box_phase_hit_gives_repr states that a box phase hit already yields the representation by composing the finite closure lemma with the RCL ledger theorem.
proof idea
The proof is a one-line term that applies box_phase_hit_gives_repr to the output of generated_phase_hit_gives_HitsBalancedPhase applied to the input hit.
why it matters
This declaration completes the finite-layer bridge from a generated target phase to the rational Erdős-Straus representation. It depends on the conversion theorem generated_phase_hit_gives_HitsBalancedPhase and feeds the box-phase representation result. In the Recognition Science framework it supplies the number-theoretic closure step required for the residual proof inside the subset-product phase layer, supporting the overall forcing chain from T5 J-uniqueness through the RCL identity toward the mass formula and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.