SuccessfulWordPaths.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Prescribed word paths through the successful sheets

def OAI.PolycyclicRecognition.WordSheetsGood line 15
Source documentation
All the states at which a support leg is traversed are in the good set.
```
def WordSheetsGood (A : Set G) : G → List G → Prop
  | n, [] => n ∈ A
  | n, g :: u => n ∈ A ∧ WordSheetsGood A (n * g) u
```
theorem OAI.PolycyclicRecognition.WordSheetsGood.start line 19
theorem OAI.PolycyclicRecognition.wordSheetsGood_of_switchSuccessful line 27
Source documentation
The independent-switch event is exactly the good-sheet condition used by the geometric word paths, after adjoining the initial good sheet.
```
theorem wordSheetsGood_of_switchSuccessful (A : Set G) (m : ℕ)
    (p : Fin m → G × G) (n : G) (hn : n ∈ A) (j : ℕ)
    (hs : SwitchSuccessful (fun _ => A) j m n (vectorSwitchParameters m p)) :
    WordSheetsGood A n (List.ofFn (fun i => (p i).1 * (p i).2⁻¹)) := by
…
```
Mentions: OAI.PolycyclicRecognition.SwitchSuccessful, OAI.PolycyclicRecognition.vectorSwitchParameters, OAI.PolycyclicRecognition.WordSheetsGood

theorem OAI.PolycyclicRecognition.wordSheetsGood_sampled line 43

Source documentation

Apply the successful-event interpretation to the original real samples.

theorem wordSheetsGood_sampled (A : Set G) (f : ℕ → ℝ → G)
    (hf : ∀ j s t, f j s * (f j t)⁻¹ = f j (s - t)) (m : ℕ)
    (t : Fin (m + m) → ℝ) (n : G) (hn : n ∈ A)
    (hs : SwitchSuccessful (fun _ => A) 0 m n (sampledSwitchParameters f m t)) :
    WordSheetsGood A n (List.ofFn (fun j : Fin m =>
      f j.val (t (Fin.castAdd m j) - t (Fin.natAdd m j)))) := by
…

Mentions: OAI.PolycyclicRecognition.SwitchSuccessful, OAI.PolycyclicRecognition.sampledSwitchParameters, OAI.PolycyclicRecognition.WordSheetsGood

theorem OAI.PolycyclicRecognition.supportWordPath_good_bound line 62

Source documentation

Concatenation only asks for the good states actually visited by this word. The observable range need not be defined by a homomorphism.

theorem supportWordPath_good_bound (A S : Set G) (P : I → ℝ → Prop)
    {L κ : ℝ} (hL : 0 ≤ L) (hκ : 0 ≤ κ)
    (hbase : ∀ n ∈ A, n * d₀ ∈ S)
    (hstep : ∀ n ∈ A, ∀ i b, P i b → n * f i b ∈ A →
      PathMetricBound (supportVisitPath (d i) (hd i) (hd₀ i)
        (f i) (hf i) (hf₀ i) n d₀ r b) L κ ∧
      ∀ t, supportVisitPath (d i) (hd i) (hd₀ i)
        (f i) (hf i) (hf₀ i) n d₀ r b t ∈ S)
    (u : List (I × ℝ)) (hu : ∀ z ∈ u, P z.1 z.2) (n : G)
    (hgood : WordSheetsGood A n (u.map (fun z => f z.1 z.2))) :
    PathMetricBound (supportWordPath d f hd hf hd₀ hf₀ d₀ r u n)
      (L * 2 ^ u.length) (κ * 2 ^ u.length) ∧
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound, OAI.PolycyclicRecognition.supportVisitPath, OAI.PolycyclicRecognition.WordSheetsGood, OAI.PolycyclicRecognition.supportWordPath