box_phase_hit_gives_balanced_pair
plain-language theorem explainer
If a square-budget box hits the balanced residual phase for gate c, then the divisor-complement pair extracted from it supplies balanced-pair phase support for n and c. Researchers closing the finite part of the Erdős-Straus conjecture via Recognition Science cite this closure lemma. The tactic proof unpacks the existential witness and reassembles the support structure using the box fields and the divisor-complement product identity.
Claim. Let $n, c$ be positive integers. Suppose there exist positive integers $x$ and $N$ together with a divisor-exponent box for $N$ such that $N = n x$, $c = 4x - n$, and $c$ divides both $N + d$ and $N + e$, where $d$ and $e$ are the divisor and complement of the box satisfying $d e = N^2$. Then the balanced-pair phase support holds for $n$ and $c$.
background
The module isolates the finite combinatorial part of the residual Erdős-Straus proof. For a square budget $N^2$, a divisor-exponent box is represented by a complementary pair $(d, e)$ with $d e = N^2$. This representation avoids unnecessary factorization overhead in the finite closure lemma. The balanced phase hit condition for $n$ and $c$ asserts the existence of $x$, $N$, and such a box satisfying $N = n x$, $c = 4x - n$, together with the divisibility conditions $c$ divides $N + d$ and $N + e$. These conditions encode that both reciprocal defects land in phase $-N$ modulo $c$. The lemma depends on the sibling definitions of the divisor and complement extracted from the box, as well as the upstream multiplication identity establishing their product equals $N^2$.
proof idea
The proof begins with case analysis on the hypothesis, extracting the witness values $x$, $N$, box and the associated conditions. It then refines the target balanced-pair phase support by substituting the divisor and complement extracted from the box into the pair slots, preserving the other fields from the witness. The final field is discharged by an exact application of the lemma establishing that the divisor times the complement equals the square.
why it matters
This is the finite box-to-pair closure lemma that connects a phase hit to the balanced-pair support required by the RCL skeleton. It feeds directly into the theorem that a box phase hit already gives a rational Erdős-Straus representation by composing the finite closure lemma with the RCL ledger theorem. In the Recognition Science framework the result closes the finite combinatorial reduction, linking square-budget box distributions to the Recognition Composition Law. It touches the eight-tick phase structure through the balanced residual phase condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.