boundedBalancedSearch_of_phaseBudget
plain-language theorem explainer
This definition converts a PhaseBudgetEngine into a BoundedBalancedSearchEngine by routing through the effective prime phase input. Number theorists working on residual traps in the Recognition Science Erdős-Straus chain would cite it to obtain explicit bounded search from budget data. The implementation is a one-line wrapper that composes effectivePrimePhaseInput_of_phaseBudgetEngine with boundedBalancedSearch_of_effectivePrimePhaseInput.
Claim. Let $E$ be a phase-budget engine supplying, for each residual trap $n$, a bound $b(n)$ and a witness $c$ with $c$ an admissible hard gate and nonempty subset-product phase hit. Then the map yields a bounded balanced search engine whose bound satisfies that for every such $n$ there exists $c$ at most $b(n)$ with admissible hard gate and balanced pair phase support.
background
The module composes the phase-budget interface with the Erdős-Straus RCL closure chain. A PhaseBudgetEngine is the structure that for every natural number $n$ that is a residual trap supplies a bound function together with a witness $c$ at most that bound such that $c$ is an admissible hard gate and the subset-product phase hit for $n$ and $c$ is nonempty. This rests on the eight-tick phase definition giving phases $kπ/4$ for $k$ in Fin 8 and the constant $A=1$ for active edges per fundamental tick from the integration gap and masses anchor.
proof idea
This is a one-line wrapper. It first converts the phase-budget engine to an effective prime phase input via effectivePrimePhaseInput_of_phaseBudgetEngine, then applies boundedBalancedSearch_of_effectivePrimePhaseInput to obtain the bounded balanced search engine.
why it matters
This declaration bridges phase-budget engines to the bounded balanced search engines required by the Erdős-Straus rotation hierarchy. It is invoked downstream by boundedBalancedSearch_of_boundedVisibilityEngine in the PhaseBudgetEngineFromRS module. The step advances the T1 phase budget bound and RCL stable-budget interface toward explicit gate witnesses for residual traps, consistent with the eight-tick octave and the $D=3$ spatial structure of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.