EligibleOuterColoring.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Outer coloring of the actual eligible geometric patterns

The event indices contain exactly a period and a literal (step, word) pair. Existential real realizations of one word do not increase its event count.

theorem OAI.QuantitativeVanDerWaerden.recordedWord_coloredPositions_eq line 18
theorem OAI.QuantitativeVanDerWaerden.exists_outer_coloring_of_eligible_counts line 37

theorem OAI.QuantitativeVanDerWaerden.exists_outer_balanced line 88

Source documentation

Actual eligible patterns obey the anchored count theorem, so outer selection requires only its explicit numerical incident-weight budget.

theorem exists_outer_balanced {D k : ℕ} (n : ℕ) (hn : 0 < n)
    (A : AdaptiveMesh) (lambda M : ℕ) (hD : 0 < D) (hM : 0 < M) (hMk : M ≤ k)
    (words : Finset (Fin k → FullLabel D (Fin n) A.Label)) (periods : Finset ℕ)
    (hrow : (100 : ℝ) ≤ (M : ℝ) / 10 - 1)
    (hperiodLower : ∀ h ∈ periods, 200 ≤ h)
    (hbudget : ((k * words.card : ℕ) : ℝ) * Real.exp (-((M : ℝ) / 10 - 1) / 32) +
      (∑ h ∈ periods, (((16005 * D * h) ^ (14 * D) : ℕ) : ℝ) *
        Real.exp (-(h : ℝ) / 64)) ≤ 1 / 500) :
    ∃ color : FullLabel D (Fin n) A.Label → Bool,
      OuterBalanced n hn A (1 / (1000 * (D : ℝ))) lambda M words periods color := by
…

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