OddGadgets.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Good gadgets over every sufficiently large eligible prime

The two probability thresholds are uniform before the prime is chosen. This extraction retains the actual sample space and both proved events; it does not use a gadget-existence assumption or prime subsequence.

theorem OAI.RyserCoveringCounterexample.Construction.exists_threshold_goodGadget line 20
Source documentation
Every sufficiently large prime congruent to two modulo three supports an actual good gadget. The threshold is chosen before the prime.
```
theorem exists_threshold_goodGadget :
    ∃ P : ℕ, ∀ p : ℕ, P ≤ p → ∀ hp : p.Prime, p % 3 = 2 →
      5 < p ∧
        (letI : Fact p.Prime := ⟨hp⟩
…
```