ReciprocalPairClosureEngine

formal source

 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
 212/-- A global engine implies every finite-range certificate. -/
 213theorem finite_cert_of_global_engine
 214    (engine : BoundedBalancedSearchEngine)
 215    (maxN : ℕ) :
 216    ∃ B : ℕ, ∀ n : ℕ, n ≤ maxN → ResidualTrap n →
 217      ∃ c : ℕ, c ≤ B ∧ AdmissibleHardGate c ∧ BalancedPairPhaseSupport n c := by
 218  classical
 219  let B : ℕ := (Finset.range (maxN + 1)).sup engine.bound