`BoundedBalancedSearchEngine`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.ErdosStrausRotationHierarchy
domain: NumberTheory
line: 196 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.ErdosStrausRotationHierarchy on GitHub at line 196.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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
 220  refine ⟨B, ?_⟩
 221  intro n hnmax hntrap
 222  rcases engine.bound_ok n hntrap with ⟨c, hcbound, hc, hpair⟩
 223  refine ⟨c, ?_, hc, hpair⟩
 224  exact le_trans hcbound (Finset.le_sup (Finset.mem_range.mpr (Nat.lt_succ_of_le hnmax)))
 225
 226/-- Rotation separation + reciprocal closure solve the residual class. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.