AnchoredPatterns.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.secondOutput line 20
Source documentation
Only rotating coordinates can produce a dummy scalar output.
```
def secondOutput (A : AdaptiveMesh) (eta : ℝ) (R : Realization D) (lambda : ℕ)
    (t : Fin D → Fin h) (i : Fin D) (z : Fin h) : Option A.Label := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.Realization
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.secondOutput_eq_some_of_regular line 27
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.recordedWord_eq_assembleWord line 38
Source documentation
Scalar outputs determine the whole recorded word, including its mask. There is no extra independent factor 2^h.
```
theorem recordedWord_eq_assembleWord (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh)
    (eta : ℝ) (R : Realization D) (lambda : ℕ) (t : Fin D → Fin h) :
    recordedWord n hn A eta R lambda t =
      assembleWord (fun i z => UniformMesh.label n hn (firstPath R t z i))
        (secondOutput A eta R lambda t) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.Realization, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.recordedWord, OAI.QuantitativeVanDerWaerden.assembleWord, OAI.QuantitativeVanDerWaerden.UniformMesh.label, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.firstPath, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.secondOutput
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.anchorCoefficient line 62
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.anchoredFirst line 64
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.anchoredSecond line 69
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.firstPath_reanchor line 75
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.secondPath_reanchor line 81
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.firstLabel_reanchor line 88
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.secondLabel_reanchor line 95
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.rho_reanchor line 101
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.abs_anchorCoefficient_lt_one line 107
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.stationary_translation_integer line 119
Source documentation
Stationary rational translations are integer shifts, even though the drift may be nonzero.
```
theorem stationary_translation_integer (lambda : ℕ) (t : Fin D → Fin h)
    (hh : 0 < h) (i : Fin D) (hi : stationary lambda t i) (z0 z : Fin h) :
    ∃ m : ℤ, anchorCoefficient z0 z * ((lambda : ℝ) * (t i).val) = m := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AnchoredPatterns.stationary, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.anchorCoefficient
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.scalarDomain line 131
Source documentation
The two genuinely free scalar parameters are anchor position and drift.
```
def scalarDomain (left right width : ℝ) : Set (Fin 2 → ℝ) :=
…
```
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.scalarValue line 134
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.scalarValue_mem line 137
def OAI.QuantitativeVanDerWaerden.AnchoredPatterns.comparisonForm line 151
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.comparisonForm_eval line 155

theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.scalar_family line 162

Source documentation

A scalar word is counted by its actual affine comparisons. The breakpoint sets are fixed before the two real parameters are selected.

private theorem scalar_family {K : ℕ} {Label : Type uLabel}
    (c tau : Fin h → ℝ) (domain : Set (Fin 2 → ℝ))
    (output : Fin h → ℝ → Label) (B : Fin h → Finset ℝ)
    (hB : ∀ z, (B z).card ≤ K)
    (hfactor : ∀ p ∈ domain, ∀ q ∈ domain, ∀ z,
      (∀ b ∈ B z,
        ternarySign (scalarValue c tau p z - b) =
          ternarySign (scalarValue c tau q z - b)) →
      output z (scalarValue c tau p z) = output z (scalarValue c tau q z)) :
    ∃ S : Finset (Fin h → Label),
      (∀ w, w ∈ S ↔ ∃ p ∈ domain, (fun z => output z (scalarValue c tau p z)) = w) ∧
      S.card ≤ 16 * (K * h + 1) ^ 6 := by
…

Mentions: OAI.QuantitativeVanDerWaerden.ternarySign, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.scalarValue

theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.uniform_scalar_family line 202
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.stationary_scalar_family line 232
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.rotating_scalar_family line 249
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.first_anchored_family line 275
Source documentation
The first-coordinate family depends only on the fixed literal anchor, step vector, and anchor position, not on a realizing path.
```
theorem first_anchored_family (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh)
    (lambda : ℕ) (beta : FullLabel D (Fin n) A.Label) (hD : 0 < D) (hh : 0 < h)
    (t : Fin D → Fin h) (z0 : Fin h) (i : Fin D) :
    ∃ S : Finset (Fin h → Fin n),
      S.card ≤ 16 * (16004 * D * h + 1) ^ 6 ∧
      ∀ R : Realization D,
        EligibleRealization n hn A (1 / (1000 * (D : ℝ))) lambda t R →
        recordedWord n hn A (1 / (1000 * (D : ℝ))) R lambda t z0 = some beta →
        (fun z => UniformMesh.label n hn (firstPath R t z i)) ∈ S := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.FullLabel, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.Realization, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.EligibleRealization, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.recordedWord, OAI.QuantitativeVanDerWaerden.UniformMesh.label, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.firstPath
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.second_anchored_family line 302
Source documentation
Stationary coordinates use an untruncated mesh label; rotating coordinates use the actual distance-to-cut truncation. Both have the same uniform bound.
```
theorem second_anchored_family (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh)
    (lambda : ℕ) (beta : FullLabel D (Fin n) A.Label) (hD : 0 < D) (hh : 0 < h)
    (t : Fin D → Fin h) (z0 : Fin h) (i : Fin D) :
    ∃ S : Finset (Fin h → Option A.Label),
      S.card ≤ 16 * (16004 * D * h + 1) ^ 6 ∧
      ∀ R : Realization D,
        EligibleRealization n hn A (1 / (1000 * (D : ℝ))) lambda t R →
        recordedWord n hn A (1 / (1000 * (D : ℝ))) R lambda t z0 = some beta →
        secondOutput A (1 / (1000 * (D : ℝ))) R lambda t i ∈ S := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.FullLabel, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.Realization, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.EligibleRealization, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.recordedWord, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.secondOutput
theorem OAI.QuantitativeVanDerWaerden.AnchoredPatterns.card_through_le line 360
Source documentation
The actual union incidence count. The literal eligibility predicate is filtered before counting. Its pairwise distinctness and half-regular conditions are retained in the family, although this bound only needs a regular anchor. No family-cardinality, label-factorization, or independent-mask premise occurs in this theorem.
```
theorem card_through_le (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh) (lambda : ℕ)
    (beta : FullLabel D (Fin n) A.Label) (hD : 0 < D) (hh : 0 < h) :
    (through (h := h) n hn A (1 / (1000 * (D : ℝ))) lambda beta).card ≤
…
```
Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.FullLabel, OAI.QuantitativeVanDerWaerden.AnchoredPatterns.through