FiniteWordDetection.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Sparse detection for the concrete recursive word model

The list-prefix vectors used by finiteWord satisfy the same exact recursion and period bounds as the function-prefix vectors. This closes the algebraic inputs of the finite spectral detector in the actual word-state presentation.

theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordState_finite line 25
def OAI.TreeEdit.BinaryLower.FiniteTree.pullStateHom line 32
Source documentation
Relabeling the product factors is additive, not merely a map of sets.
```
def pullStateHom (Q : (Fin k → Fin m) → ℕ) :
    (∀ l, ZMod (Q l)) →+ State (fun l => Q (leafEquiv m k l)) where
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.leafEquiv
def OAI.TreeEdit.BinaryLower.FiniteTree.wordLeafCoordinate line 40
Source documentation
The actual word-state cyclic coordinate, indexed by the same function leaves as the spectral tree's finite leaf set.
```
def wordLeafCoordinate (primes : Fin k → Fin m → ℕ) (f : Fin k → Fin m) :
    ZMod (FiniteVectors.leafPeriod primes f) →+ State (wordPeriods primes) :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods
theorem OAI.TreeEdit.BinaryLower.FiniteTree.extendPrefix_ofFn line 45
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordLeafCoordinate_one line 51
Source documentation
This is precisely the generator identity of the spectral tree theorem.
```
@[simp] theorem wordLeafCoordinate_one (primes : Fin k → Fin m → ℕ)
    (i₀ : Fin m) (f : Fin k → Fin m) :
    wordLeafCoordinate primes f 1 = wordW primes i₀ (List.ofFn f) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.wordLeafCoordinate, OAI.TreeEdit.BinaryLower.FiniteTree.wordW
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordLeafCoordinate_eq_val_zsmul line 61
Source documentation
Whole-coordinate averaging uses only integer multiples of the actual word leaf vector, as in the pointwise inexpensive-leaf-translation lemma.
```
theorem wordLeafCoordinate_eq_val_zsmul (primes : Fin k → Fin m → ℕ)
    (i₀ : Fin m) (f : Fin k → Fin m)
    [NeZero (FiniteVectors.leafPeriod primes f)]
    (z : ZMod (FiniteVectors.leafPeriod primes f)) :
    wordLeafCoordinate primes f z = (z.val : ℤ) • wordW primes i₀ (List.ofFn f) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod, OAI.TreeEdit.BinaryLower.FiniteTree.wordLeafCoordinate, OAI.TreeEdit.BinaryLower.FiniteTree.wordW
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod_pos line 74
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod_le line 79
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod_child line 84
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordW_eq_level_nsmul_wordU line 94
Source documentation
The distinguished word-state vector is the level product times the actual cheap word-state vector.
```
theorem wordW_eq_level_nsmul_wordU (primes : Fin k → Fin m → ℕ)
    (i₀ : Fin m) (p : List (Fin m)) (hp : p.length < k) :
    wordW primes i₀ p = FiniteVectors.levelProduct primes ⟨p.length, hp⟩ •
      wordU primes i₀ p := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.wordW, OAI.TreeEdit.BinaryLower.FiniteVectors.levelProduct, OAI.TreeEdit.BinaryLower.FiniteTree.wordU
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordU_eq_sum_child_wordW line 104
Source documentation
The cheap word-state vector is exactly the sum of the children's distinguished vectors, with the same list indices used for branching.
```
theorem wordU_eq_sum_child_wordW (primes : Fin k → Fin m → ℕ)
    (i₀ : Fin m) (p : List (Fin m)) (hp : p.length < k) :
    wordU primes i₀ p = ∑ i : Fin m, wordW primes i₀ (p ++ [i]) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.wordU, OAI.TreeEdit.BinaryLower.FiniteTree.wordW

theorem OAI.TreeEdit.BinaryLower.FiniteTree.word_sparse_detection line 115

Source documentation

A sparse active node is detected by short averages of cheap shifts in the canonical word-state group.

theorem word_sparse_detection (primes : Fin k → Fin m → ℕ) (i₀ : Fin m)
    (hk : 1 ≤ k) (hppos : ∀ q i, 0 < primes q i)
    (hp : ∀ q i, primes q i ≤ k ^ 5)
    (v : FiniteActivity.InternalNode (Fin m) k)
    (χ : AddChar (State (wordPeriods primes)) ℂ)
    (hsparse : FiniteActivity.characterSparse (wordW primes i₀) k v χ) :
    ((4 * k ^ (10 * k) : ℕ) : ℝ) ≤
      ∑ s : Fin (4 * k ^ (10 * k)),
        ‖1 - χ ((s.val + 1) • wordU primes i₀ (List.ofFn v.2))‖ ^ 2 := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.BinaryLower.FiniteActivity.characterSparse, OAI.TreeEdit.BinaryLower.FiniteTree.wordW, OAI.TreeEdit.BinaryLower.FiniteTree.wordU