bounded_search_implies_phase_equidistribution
plain-language theorem explainer
Bounded search engines imply prime phase equidistribution engines by lifting the bounded gate witness directly to an unbounded phase support witness. Number theorists reducing residual traps in the Erdős-Straus rotation hierarchy would cite this when separating admissible finite quotients. The proof is a term-mode one-line wrapper that cases on the bound_ok field and repackages its witness.
Claim. If there exists a bound function $b : ℕ → ℕ$ such that for every residual trap $n$ there is $c ≤ b(n)$ with an admissible hard gate at $c$ and phase support for $n$ at $c$, then for every residual trap $n$ there exists $c$ with an admissible hard gate at $c$ and phase support for $n$ at $c$.
background
The Erdős-Straus Recognition Rotation Hierarchy module converts the RCL attack into a proof skeleton that isolates two missing engines: prime phase separation across admissible residual quotients and reciprocal pair closure. BoundedSearchEngine is the structure whose bound_ok field asserts that for every ResidualTrap n there exists c ≤ bound n with AdmissibleHardGate c and GateHasPhaseSupport n c. PrimePhaseEquidistributionEngine is the weaker Prop whose phase_support field asserts only the existence of such a c without the bound. Upstream reciprocal definitions from CostAlgebra and LedgerForcing supply the automorphism and event inversion that close the broader hierarchy.
proof idea
The term proof refines the PrimePhaseEquidistributionEngine constructor. It introduces n and the ResidualTrap hypothesis hn, then cases on bounded.bound_ok n hn to extract c together with the gate and support witnesses. It immediately packages c, the gate, and the support into the required phase_support witness, discarding the bound check.
why it matters
This declaration supplies the prime phase separation engine required by the rotation hierarchy skeleton. It feeds directly into bounded_residual_trap_solved, which combines the resulting equidistribution engine with reciprocal pair closure to obtain HasRationalErdosStrausRepr for residual traps. The step aligns with the Recognition Composition Law by guaranteeing finite quotients before reciprocal closure is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.