BoundedBalancedSearchEngine
plain-language theorem explainer
BoundedBalancedSearchEngine packages a bound function together with the guarantee that every residual-trapped n receives an admissible gate c and a concrete balanced-pair phase-support witness. Number theorists reducing the Erdős-Straus conjecture to finite certificates would cite the structure when converting phase-budget or prime-phase engines into explicit search bounds. The definition is a direct record whose bound_ok field universally quantifies over ResidualTrap and extracts the required gate and support pair.
Claim. A structure consisting of a function $b : ℕ → ℕ$ such that for every $n$ satisfying the residual trap condition ($n > 1$, $n ≡ 1 mod 24$, all prime factors of $n$ and of $(n+3)/4$ congruent to 1 mod 3) there exists $c ≤ b(n)$ with $c ≡ 3 mod 4$ and positive integers $x,N,d,e$ obeying $N = n·x$, $c = 4x - n$, $de = N²$, and $c$ dividing both $N+d$ and $N+e$.
background
The Erdős-Straus Recognition Rotation Hierarchy module isolates two missing engines: prime phase separation across admissible residual quotients and reciprocal pair closure once phase support appears. ResidualTrap collects the hard arithmetic class: $n > 1$, $n ≡ 1 mod 24$, and both $n$ and $(n+3)/4$ have all prime factors ≡ 1 mod 3. AdmissibleHardGate requires the gate $c$ to satisfy $c ≡ 3 mod 4$ when $n ≡ 1 mod 4$. BalancedPairPhaseSupport encodes the finite-quotient witness: existence of $x,N,d,e$ with the listed relations that place both defects in phase $-N mod c$.
proof idea
The declaration is a structure definition whose two fields directly encode the bound function and the universal property over ResidualTrap. No lemmas or tactics are invoked inside the definition; downstream converters such as boundedBalancedSearch_of_primePhaseBoxDistribution simply supply concrete values for the fields.
why it matters
The structure supplies the interface that bounded_balanced_search_solved invokes to obtain HasRationalErdosStrausRepr for every trapped $n$ by extracting the pair support and applying balanced_pair_phase_support_gives_repr. It thereby closes the finite-certification path in the rotation hierarchy and links the Recognition Composition Law to an explicit arithmetic certificate. The definition also feeds finite_cert_of_global_engine and the chain of converters from PhaseBudgetEngine and PrimePhaseBoxDistribution, leaving open the concrete supply of the prime-phase separation engine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.