181structure BoundedSearchEngine : Type where 182 bound : ℕ → ℕ 183 bound_ok : 184 ∀ n : ℕ, ResidualTrap n → 185 ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ GateHasPhaseSupport n c 186 187/-- Reciprocal pair closure: once a gate has enough phase support, it yields 188the actual reciprocal divisor-pair witness required by RCL. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.