OuterBalanced.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The exact two balancing properties consumed by the geometric dichotomy. The existence proof, including actual pattern counts, is in EligibleOuterColoring.

structure OAI.QuantitativeVanDerWaerden.OuterBalanced line 13

Source documentation

The two balancing properties of the selected outer label coloring.

structure OuterBalanced {D k : ℕ} (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh)
    (eta : ℝ) (lambda M : ℕ)
    (words : Finset (Fin k → FullLabel D (Fin n) A.Label)) (periods : Finset ℕ)
    (color : FullLabel D (Fin n) A.Label → Bool) : Prop where
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.FullLabel