OAI/NumberTheory/Ostmann/QuadraticCenter/WitnessGridGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The grid error is smaller than the small-kernel witness gap

  1. theorem OAI.Ostmann.witness_grid_gap line 9
  2. theorem OAI.Ostmann.small_witness_failure_survives_grid line 32