CyclicWitness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The unconditional cyclic two-coloring witness

Every parameter, mesh, literal label, outer coloring, geometric key, and finite probability budget is supplied by its actual construction theorem. The absolute threshold is chosen before the prime scale and before any final color count.

theorem OAI.QuantitativeVanDerWaerden.construction_key_fiber_card_le_four line 23
theorem OAI.QuantitativeVanDerWaerden.eventually_cyclic_coloring line 48
Source documentation
The eventual construction uses the actual counted outer witness and the actual rich-or-affine dichotomy, then samples only the finite geometric-key image.
```
theorem eventually_cyclic_coloring :
    ∀ᶠ k : ℕ in atTop, ∃ N : ℕ, 2 ≤ N ∧
      (k : ℝ) ^ ((1 / 100000 : ℝ) * k) ≤ (N : ℝ) ∧
        ∃ C : ZMod N → Bool, CyclicAvoids C k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.CyclicAvoids
theorem OAI.QuantitativeVanDerWaerden.exists_cyclic_coloring line 106