OuterDichotomy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual outer-coloring dichotomy

The coloring is the selected coloring of literal full labels. A progression with many light positions is balanced by its global word test. Otherwise its actual closest heavy-label return supplies a primitive rational path. Short periods lift affinely; long periods satisfy the actual eligible block tests.

theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice.rich_or_affine line 29
Source documentation
Every actual cyclic progression is either rich in both outer colors or has an affine lift in the second representative system.
```
theorem OuterChoice.rich_or_affine {k : ℕ} (s : Data k) (hk : 3 ≤ k)
    (o : OuterChoice s hk) (hg : GeometryScales k) (a d : Group s) :
    (∀ b : Bool, k ≤ 100 * (Finset.univ.filter fun j : Fin k =>
      o.color (fullLabelWord s hk (a, d) j) = b).card) ∨
    ∃ A B : Fin (dimension k) → ℝ, ∀ j : Fin k,
      yRep s.q (dimension k) (lambda k) (a + (j.val : Group s) * d) =
        fun i => A i + (j.val : ℝ) * B i := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.OuterChoice, OAI.QuantitativeVanDerWaerden.ConstructionModel.Group, OAI.QuantitativeVanDerWaerden.ConstructionModel.fullLabelWord, OAI.QuantitativeVanDerWaerden.yRep, OAI.QuantitativeVanDerWaerden.ConstructionModel.lambda