boundedBalancedSearch_of_primePhaseBoxDistribution
plain-language theorem explainer
This definition converts a prime phase box distribution into a bounded balanced search engine by extracting the supplied bound function and verifying each hit yields balanced pair support. Number theorists working on the Erdős-Straus conjecture via phase methods would cite it as the direct bridge from distribution to search engine. The construction is a one-line wrapper that applies the box phase hit conversion lemma to the hits witness.
Claim. Given a prime phase box distribution, which supplies for every residual trap $n$ a bounded admissible gate $c$ that hits the balanced phase, the associated bounded balanced search engine is obtained by taking the distribution's bound function and confirming that each such hit satisfies the balanced pair phase support condition.
background
The Prime Phase Distribution module sets up the interface for the Erdős-Straus problem by naming the distribution statement and showing it instantiates the existing bounded balanced search engine. The structure PrimePhaseBoxDistribution asserts that for every residual trap $n$ there exists $c$ with $c$ at most the bound of $n$, where $c$ is an admissible hard gate and hits the balanced phase. The upstream theorem box phase hit gives balanced pair states that a box phase hit is exactly the balanced pair support required by the RCL skeleton.
proof idea
The definition sets the bound field directly to that of the input distribution. The bound_ok field is proved by introducing $n$ and the residual trap hypothesis, extracting the witness $c$ from the hits field of the distribution, and applying the box phase hit gives balanced pair theorem to obtain the required balanced pair phase support.
why it matters
This supplies the exact finite-combinatorial conversion that lets any prime phase box distribution yield the bounded balanced search engine, which then feeds the residual Erdős-Straus representation theorem via erdos straus residual from prime phase box distribution. It completes the interface step named in the module doc comment and prepares the ground for the RS prime phase box theorem. The construction sits inside the RCL algebra and the eight-tick phase structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.