EligiblePatternTests.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Actual tests from eligible return-period patterns

The index records the period and the literal pair of rational step and recorded word. Realizing parameters are existential witnesses, not extra test indices. Incidence with a label is exactly the anchored family AnchoredPatterns.through.

abbrev OAI.QuantitativeVanDerWaerden.EligiblePatternTests.TestIndex line 24
Source documentation
Each event keeps its actual period, rational step and recorded word.
```
abbrev TestIndex (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh) (eta : ℝ)
    (lambda : ℕ) (periods : Finset ℕ) :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh
def OAI.QuantitativeVanDerWaerden.EligiblePatternTests.period line 31
def OAI.QuantitativeVanDerWaerden.EligiblePatternTests.step line 33
def OAI.QuantitativeVanDerWaerden.EligiblePatternTests.word line 36
def OAI.QuantitativeVanDerWaerden.EligiblePatternTests.support line 40
Source documentation
Only the actual non-dummy recorded labels are used by an event.
```
def support (i : TestIndex (D := D) n hn A eta lambda periods) :
…
```
Mentions: OAI.QuantitativeVanDerWaerden.EligiblePatternTests.TestIndex
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.period_mem line 43
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.word_eligible line 46
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.mem_support line 50
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.word_labelsInjective line 55
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.word_regular_many line 59
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.support_card_eq line 63
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.period_le_two_support_card line 67
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.period_le_eight_colored line 75
Source documentation
The actual positions of each balanced color occupy at least an eighth of the period.
```
theorem period_le_eight_colored
    (i : TestIndex (D := D) n hn A eta lambda periods)
…
```
Mentions: OAI.QuantitativeVanDerWaerden.EligiblePatternTests.TestIndex
def OAI.QuantitativeVanDerWaerden.EligiblePatternTests.incidentSlice line 84
Source documentation
Incidences in a single period slice of the concrete event index.
```
def incidentSlice (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh) (eta : ℝ)
    (lambda : ℕ) (periods : Finset ℕ) (h : ℕ)
    (beta : FullLabel D (Fin n) A.Label) :
    Finset (TestIndex (D := D) n hn A eta lambda periods) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.FullLabel, OAI.QuantitativeVanDerWaerden.EligiblePatternTests.TestIndex
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.mem_incidentSlice line 91
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.incidentSlice_card_eq_through line 98
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.incidentSlice_eq_empty_of_not_mem line 132
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.incident_card_le_of_through line 143
Source documentation
A bound on canonical anchored pairs applies to the incident slice at every natural period, including periods outside the finite family.
```
theorem incident_card_le_of_through (countBound : ℕ → ℕ)
    (hcount : ∀ h ∈ periods, ∀ beta : FullLabel D (Fin n) A.Label,
      (through (h := h) n hn A eta lambda beta).card ≤ countBound h)
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FullLabel
theorem OAI.QuantitativeVanDerWaerden.EligiblePatternTests.incident_card_le line 166
Source documentation
The proved geometric anchored bound applies directly to the actual second family of outer-coloring events.
```
theorem incident_card_le (hD : 0 < D)
    (hperiods : ∀ h ∈ periods, 0 < h)
    (beta : FullLabel D (Fin n) A.Label) (h : ℕ) :
    (Finset.univ.filter (fun i : TestIndex (D := D) n hn A
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FullLabel, OAI.QuantitativeVanDerWaerden.EligiblePatternTests.TestIndex