OAI/Combinatorics/Ramsey/CycleClique/Construction/FiniteBallBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Soundness of the finite checker's numerical ball recurrence on labelled ground vertices. A matrix entry records a proved forbidden outside parameter.

  1. abbrev OAI.CycleClique.Construction.ForbiddenMatrix line 10
  2. def OAI.CycleClique.Construction.ForbiddenMatrix.Sound line 12
  3. def OAI.CycleClique.Construction.zeroAvoidSet line 16
  4. def OAI.CycleClique.Construction.ballAvoidSet line 19
  5. def OAI.CycleClique.Construction.indexedBallState line 22
  6. theorem OAI.CycleClique.Construction.indexedBallState_positive line 32
  7. theorem OAI.CycleClique.Construction.indexedBallState_sound line 47