BoundedSearchEngine

formal source

 178
 179/-- Effective bounded search: the separating gate can be chosen below a
 180specific bound. -/
 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. -/
 189structure ReciprocalPairClosureEngine : Prop where
 190  close :
 191    ∀ n c : ℕ, ResidualTrap n → AdmissibleHardGate c → GateHasPhaseSupport n c →
 192      GateClosureWitness n c
 193
 194/-- Stronger, fully arithmetic bounded search: the search returns the actual
 195balanced phase pair, not merely abstract phase support. -/
 196structure BoundedBalancedSearchEngine : Type where
 197  bound : ℕ → ℕ
 198  bound_ok :
 199    ∀ n : ℕ, ResidualTrap n →
 200      ∃ c : ℕ, c ≤ bound n ∧ AdmissibleHardGate c ∧ BalancedPairPhaseSupport n c
 201
 202/-- A finite-range bounded balanced-search certificate.  This is the form
 203that computation can honestly certify: all trapped `n ≤ maxN` have a gate
 204`c ≤ bound`. -/
 205structure FiniteBoundedBalancedSearchCert where
 206  maxN : ℕ
 207  bound : ℕ
 208  verified :
 209    ∀ n : ℕ, n ≤ maxN → ResidualTrap n →
 210      ∃ c : ℕ, c ≤ bound ∧ AdmissibleHardGate c ∧ BalancedPairPhaseSupport n c
 211