HitsBalancedPhase
plain-language theorem explainer
HitsBalancedPhase n c holds precisely when a square-budget divisor exponent box for some multiple N of n yields gate c = 4x - n such that both reciprocal defects lie in phase -N modulo c. Number theorists closing the finite part of the Erdős-Straus argument inside Recognition Science cite this predicate to obtain balanced-pair support. The definition is an existential encoding over boxes and the two divisibility conditions; no lemmas are invoked.
Claim. Let $n,c$ be positive integers. The predicate holds if there exist positive integers $x,N$ and a divisor-exponent box for $N$ satisfying $N=nx$, $c=4x-n$, and $c$ divides both $N+d$ and $N+e$, where $(d,e)$ is the complementary pair of the box.
background
The module isolates the finite combinatorial fragment of the residual Erdős-Straus argument. For square budget $N^2$ a divisor-exponent box is represented by a complementary pair $(d,e)$ with $d e = N^2$; this representation sidesteps explicit prime-factorization bookkeeping. The two divisibility conditions $c | (N+d)$ and $c | (N+e)$ are exactly the statement that both reciprocal defects land in phase $-N$ modulo $c$, linking directly to the eight-tick phase structure and the balanced-ledger predicate.
proof idea
The declaration is a definition, not a theorem. It directly encodes the balanced-phase hit as an existential quantifier over $x,N$ and a divisor-exponent box together with the three positivity, two equality, and two divisibility conditions. No upstream lemmas are applied; the predicate is the primitive object consumed by the subsequent closure theorems.
why it matters
HitsBalancedPhase supplies the predicate that the finite box-to-pair closure lemma box_phase_hit_gives_balanced_pair consumes to produce BalancedPairPhaseSupport; that support in turn yields a rational Erdős-Straus representation via the RCL ledger theorem. The definition therefore closes the combinatorial step of the Erdős-Straus argument inside the Recognition Science framework, connecting the square-budget box construction to the balanced-ledger condition and the eight-tick phase. It leaves open whether every non-identity reciprocal admits such a phase hit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.