OuterModelChoice.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.eventually_outerChoice line 20
Source documentation
One eventual range works for every admissible prime-power choice. The finite word count, scale inequalities, and probability budget are all supplied by the actual construction rather than assumed of the selected coloring.
```
theorem eventually_outerChoice :
    ∀ᶠ k : ℕ in atTop, ∃ hk : 3 ≤ k, ∀ s : Data k, Nonempty (OuterChoice s hk) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.exists_outerChoice_threshold line 76
Source documentation
Absolute threshold form of the actual outer-coloring choice. It is chosen before the prime scale or any requested number of final colors.
```
theorem exists_outerChoice_threshold :
    ∃ K : ℕ, 32 ≤ K ∧ ∀ k ≥ K, ∃ hk : 3 ≤ k,
      ∀ s : Data k, Nonempty (OuterChoice s hk) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice