boundedBalancedSearch_of_effectivePrimePhaseInput
plain-language theorem explainer
Effective prime phase supply converts to a bounded balanced search engine via distribution extraction. Researchers on the residual Erdős-Straus conjecture cite it to obtain arithmetic search bounds from phase supply assumptions. The construction is a one-line wrapper applying the prime phase box distribution function then the balanced search engine builder.
Claim. Let $I$ be an effective prime phase input consisting of a bound function $b : ℕ → ℕ$ and the condition that for every residual trap $n$ there exists $c ≤ b(n)$ with admissible hard gate and nonempty subset product phase hit. The definition yields a bounded balanced search engine with the same bound $b$ and the strengthened property that for every residual trap $n$ there exists $c ≤ b(n)$ with admissible hard gate and balanced pair phase support on $n, c$.
background
The module supplies the precise prime-distribution input required for the residual Erdős-Straus proof and shows it implies PrimePhaseBoxDistribution. EffectivePrimePhaseInput is the structure with bound : ℕ → ℕ and supplies_generators : ∀ n, ResidualTrap n → ∃ c ≤ bound n, AdmissibleHardGate c ∧ Nonempty (SubsetProductPhaseHit n c). BoundedBalancedSearchEngine is the stronger structure requiring BalancedPairPhaseSupport n c in place of the nonempty hit. Upstream results include the 8-tick phase definition (kπ/4 for k : Fin 8) and the conversion boundedBalancedSearch_of_primePhaseBoxDistribution that turns a PrimePhaseBoxDistribution into the search engine.
proof idea
The definition is a one-line wrapper. It first invokes primePhaseBoxDistribution_of_effectivePrimePhaseInput on the input to obtain the distribution, then applies boundedBalancedSearch_of_primePhaseBoxDistribution to that distribution to construct the engine.
why it matters
This definition supplies the search engine required by boundedBalancedSearch_of_phaseBudget in the PhaseBudgetToErdosStraus module, completing one link in the residual Erdős-Straus chain. It sits inside the eight-tick octave structure of the Recognition framework through the imported phase definitions. The module deliberately avoids the bit-rotted PrimeDistributionBridge, leaving that as an open upstream candidate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.