BoundedSearchEngine
plain-language theorem explainer
BoundedSearchEngine packages a bound function that, for any residual-trapped n, guarantees an admissible hard gate c below the bound with phase support in the divisor ledger. Number theorists extending the Erdős-Straus conjecture inside the Recognition Science rotation hierarchy cite the structure to interface the prime-phase separation engine. The declaration is a direct structure definition consisting of the bound map together with a single existence axiom over residual traps.
Claim. A bounded search engine consists of a function $b : ℕ → ℕ$ such that for every $n$ satisfying the residual trap condition ($1 < n$, $n ≡ 1 mod 24$, and all prime factors of both $n$ and $(n+3)/4$ are ≡ 1 mod 3), there exists $c ≤ b(n)$ with $c ≡ 3 mod 4$ and $(n,c)$ having phase support.
background
The Erdős-Straus Recognition Rotation Hierarchy module turns the RCL attack into a proof skeleton by isolating two missing engines: prime phase separation across admissible residual quotients and reciprocal pair closure. ResidualTrap n holds precisely when 1 < n, n mod 24 = 1, and both n and (n+3)/4 have exclusively prime factors ≡ 1 mod 3. AdmissibleHardGate c requires c mod 4 = 3. GateHasPhaseSupport n c asserts existence of a ResidualPhaseQuotient c that separates the phase for n in the divisor ledger.
proof idea
The declaration is a structure definition that directly encodes the bounded search property via its two fields: the bound map from ℕ to ℕ and the universal existence statement linking every residual trap to an admissible hard gate with phase support.
why it matters
This structure supplies the explicit assumption for the bounded search engine treated as a first-principles target in the module. It is invoked by bounded_residual_trap_solved to conclude that bounded search plus reciprocal pair closure yields a rational Erdős-Straus representation for residual-trapped n, and by bounded_search_implies_phase_equidistribution to derive the prime phase equidistribution engine. It closes one of the two gaps identified in the rotation hierarchy for the number-theoretic component of the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.