GlobalLabelWords.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.QuantitativeVanDerWaerden.CirclePartition line 15
Source documentation
Literal half-open cells on a single fundamental interval. A centered partition is represented by translating both its endpoints by 1/2.
```
structure CirclePartition (Label : Type uLabel) where
…
```
def OAI.QuantitativeVanDerWaerden.CirclePartition.label line 29
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.label_mem line 33
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.label_eq_iff line 38
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.label_eq_of_mem line 47
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.label_eq_of_fract_eq line 51
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.label_eq_of_sub_int line 57
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.label_add_int line 61
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.label_sub_int line 64
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.label_eq_of_lifted_mem line 69
Source documentation
Membership in one lifted half-open interval already determines the periodic label; the integer part need not be known in advance.
```
theorem label_eq_of_lifted_mem (x : ℝ) (z : ℤ) (l : Label)
    (hleft : P.left l + z ≤ x) (hright : x < P.right l + z) :
    P.label x = l := by
…
```
def OAI.QuantitativeVanDerWaerden.CirclePartition.word line 80
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.word_fract_parameters line 83
def OAI.QuantitativeVanDerWaerden.CirclePartition.parameterDomain line 91
Source documentation
Start and step representatives of the global counting argument.
```
def parameterDomain : Set (Fin 2 → ℝ) :=
…
```
def OAI.QuantitativeVanDerWaerden.CirclePartition.affinePoint line 94
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.affinePoint_mem line 97
abbrev OAI.QuantitativeVanDerWaerden.CirclePartition.ComparisonIndex line 109
Source documentation
Position, literal label, choice of endpoint, and integer translate.
```
abbrev ComparisonIndex (k : ℕ) (Label : Type uk) := Fin k × Label × Bool × Fin k
```
def OAI.QuantitativeVanDerWaerden.CirclePartition.endpoint line 111
def OAI.QuantitativeVanDerWaerden.CirclePartition.comparison line 114
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.comparison_eval line 118
def OAI.QuantitativeVanDerWaerden.CirclePartition.comparisons line 126
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.comparison_count line 129
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.word_eq_of_signVector_eq line 134
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.exists_exact_word_family line 185
Source documentation
The finite scalar-word family is derived from actual affine comparisons. The equivalence characterizes its exact image on normalized parameters.
```
theorem exists_exact_word_family (k : ℕ) :
    ∃ S : Finset (Fin k → Label),
      (∀ w, w ∈ S ↔ ∃ x ∈ parameterDomain, P.word k (x 0) (x 1) = w) ∧
      S.card ≤ 16 * (3 * k ^ 2 * Fintype.card Label + 1) ^ 6 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.CirclePartition.parameterDomain
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.exists_word_family line 205
Source documentation
Every real start and step belongs to the same counted family, by genuine integer-periodicity of the literal interval labels.
```
theorem exists_word_family (k : ℕ) :
    ∃ S : Finset (Fin k → Label), (∀ a b : ℝ, P.word k a b ∈ S) ∧
      S.card ≤ 16 * (3 * k ^ 2 * Fintype.card Label + 1) ^ 6 := by
…
```
def OAI.QuantitativeVanDerWaerden.CirclePartition.fullWord line 220
Source documentation
The actual full label word of two independent D-coordinate progressions.
```
def fullWord (Q : CirclePartition OtherLabel) (D k : ℕ)
    (firstStart firstStep secondStart secondStep : Fin D → ℝ) :
    Fin k → FullLabel D Label OtherLabel := fun j =>
…
```
Mentions: OAI.QuantitativeVanDerWaerden.CirclePartition, OAI.QuantitativeVanDerWaerden.FullLabel
theorem OAI.QuantitativeVanDerWaerden.CirclePartition.exists_fullWord_family line 230
Source documentation
Global full words have a finite cover derived from their actual scalar interval labels. The common endpoint budget is the sum of the two mesh sizes. The argument does not require or assume independence of actual cyclic orbit coordinates: counting all independent real starts and steps gives a cover.
```
theorem exists_fullWord_family (Q : CirclePartition OtherLabel) (D k : ℕ) :
    ∃ S : Finset (Fin k → FullLabel D Label OtherLabel),
      (∀ a b c d : Fin D → ℝ, P.fullWord Q D k a b c d ∈ S) ∧
      S.card ≤ (16 *
        (3 * k ^ 2 * (Fintype.card Label + Fintype.card OtherLabel) + 1) ^ 6) ^
          (2 * D) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.CirclePartition, OAI.QuantitativeVanDerWaerden.FullLabel