boundedBalancedSearch_of_rsPrimePhaseBoxTheorem
plain-language theorem explainer
This definition converts an RS prime phase box theorem into a bounded balanced search engine by extracting and delegating its distribution field. Researchers addressing the Erdős-Straus conjecture through Recognition Science prime ledger machinery would cite it to obtain an arithmetic search engine once the phase distribution is in hand. The construction is a direct one-line wrapper over the prime phase box distribution converter.
Claim. Let $RS$ be a structure consisting of a prime phase box distribution $D$ together with a marker that $D$ derives from RCL prime ledger machinery. The map $RS$ to bounded balanced search engine returns the engine whose bound function and admissibility condition for residual traps are taken verbatim from $D$.
background
The module supplies the prime phase distribution interface for the Erdős-Straus problem. With RCL algebra and finite square-budget closure already at theorem grade, the remaining global step is a prime phase distribution strong enough to meet the required square-budget phase. RSPrimePhaseBoxTheorem is the structure that packages a PrimePhaseBoxDistribution together with the marker from_rcl_prime_ledger. BoundedBalancedSearchEngine is the stronger arithmetic structure that supplies an explicit bound function and a proof that every residual trap admits an admissible hard gate with balanced pair phase support. The upstream conversion boundedBalancedSearch_of_primePhaseBoxDistribution performs the finite-combinatorial extraction of that engine from any such distribution.
proof idea
One-line wrapper that applies the prime phase box distribution converter to the distribution field of the input RSPrimePhaseBoxTheorem.
why it matters
The definition supplies the final link that turns the RS prime phase box theorem into a usable search engine for residual traps. It is invoked directly in erdos_straus_residual_from_rs_prime_phase_box to obtain the rational Erdős-Straus representation via bounded_balanced_search_solved. Within the Recognition framework it instantiates the prime phase distribution step required for square-budget phase hits, closing the passage from RCL/J-cost prime ledger to the arithmetic engine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.