Consequence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The sequence of matrix counterexamples rules out every polynomial removal bound.

theorem OAI.Problem348.no_polynomial_removal_bound_of_sequence line 16
Source documentation
Exponential decay of the copy density rules out polynomial removal bounds.
```
theorem no_polynomial_removal_bound_of_sequence
    (hseq : ∀ h : ℕ, 1 ≤ h →
      let d : ℕ := 386 * h + 2
…
```