OAI/Combinatorics/SphericalRamsey/Coloring.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GrahamSpherical.rounding_obstruction line 19

   Source documentation

   The actual fifty-residue rounding obstruction. No nonnegativity or geometric surrogate is required of the twelve input energies.

   theorem rounding_obstruction (e : (Fin 3 × Fin 4) → ℝ)
       (henergy : ∑ i, (if i.1 = 2 then (-2 : ℝ) else 1) * e i = 8) :
       ∃ i j, (Int.floor (3 * e i)) % 50 ≠ (Int.floor (3 * e j)) % 50 := by
   …