BalancedPairPhaseSupport
plain-language theorem explainer
BalancedPairPhaseSupport(n, c) encodes the exact finite witness for a balanced reciprocal pair under square-budget constraints in the Erdős-Straus rotation hierarchy. Researchers closing the RCL skeleton to rational representations cite it when building bounded search certificates. The predicate is introduced as a direct existential packaging of positivity, product, and divisibility conditions extracted from phase hits.
Claim. $BalancedPairPhaseSupport(n,c)$ holds precisely when there exist positive integers $x,N,d,e$ such that $N=nx$, $c=4x-n$, $de=N^2$, and $c$ divides both $N+d$ and $N+e$.
background
The Erdős-Straus Recognition Rotation Hierarchy module converts the Recognition Composition Law attack into a finite proof skeleton. It isolates two missing engines: prime phase separation across residual quotients and reciprocal-pair closure once phase support appears. No new axioms are added; the missing pieces remain explicit structure fields for future theorems.
proof idea
Direct existential definition. It packages the arithmetic relations (N = n x, c = 4x - n, d e = N², and the two divisibility statements) that a box-phase hit supplies, with positivity guards to keep denominators nonzero.
why it matters
This predicate is the exact support condition required by the finite reciprocal-pair closure theorem balanced_pair_phase_support_gives_repr, which produces a rational Erdős-Straus representation. It also feeds the BoundedBalancedSearchEngine and FiniteBoundedBalancedSearchCert structures that certify bounded searches. In the Recognition framework it completes the gate-to-representation step of the rotation hierarchy while leaving the prime-phase engine open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.