AnchoredPatternDefinitions.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Actual eligible return-period words

The literal real paths, mesh labels, eligibility predicate, and finite event indices are shared by counting and long-period geometry. Their definitions do not depend on arrangement estimates. Counting is proved in AnchoredPatterns.

structure OAI.QuantitativeVanDerWaerden.AnchoredPatterns.Realization line 23
Source documentation
Starts and drift vectors of an actual local path.
```
structure Realization (D : ℕ) where
…
```
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.stationary line 33
Source documentation
Equivalent to reduced denominator one when h > 0; no drift restriction is part of stationarity.
```
def stationary (lambda : ℕ) (t : Fin D → Fin h) (i : Fin D) : Prop :=
…
```
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.firstPath line 36
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.secondPath line 39
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.regular line 43
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.regularPositions line 47
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.fullLabel line 52
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.recordedWord line 57
structure OAI.QuantitativeVanDerWaerden.AnchoredPatterns.EligibleRealization line 64
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.eligibleOptionFullLabel line 76
Source documentation
The word itself is the pattern. Distinct realizing parameters do not give distinct eligible objects.
```
def eligibleOptionFullLabel (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh) (eta : ℝ)
    (lambda : ℕ) (t : Fin D → Fin h)
    (word : Fin h → Option (FullLabel D (Fin n) A.Label)) : Prop :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.FullLabel
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.eligiblePairs line 83
Source documentation
Actual step/word pairs, rather than a family of realizing parameters.
```
def eligiblePairs (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh) (eta : ℝ)
    (lambda : ℕ) :
    Finset ((Fin D → Fin h) × (Fin h → Option (FullLabel D (Fin n) A.Label))) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.FullLabel
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.through line 90
Source documentation
Incidences with one fixed literal full label.
```
def through (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh) (eta : ℝ) (lambda : ℕ)
    (beta : FullLabel D (Fin n) A.Label) :
    Finset ((Fin D → Fin h) × (Fin h → Option (FullLabel D (Fin n) A.Label))) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.FullLabel
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.mem_eligiblePairs line 96
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.mem_through line 104
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.recordedWord_eq_some_iff line 112