SuccessfulBlockPaths.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Paths for individual blocks of a successful sampled word

The initial point of each block is the exact product of all preceding blocks. This is needed when successive blocks use different profile labels.

theorem OAI.PolycyclicRecognition.WordSheetsGood.ofFn_block line 18
Source documentation
Restrict successful sheets to any complete block, retaining its true starting state rather than restarting the full word at the identity.
```
theorem WordSheetsGood.ofFn_block {A : Set G} {x : G} {h : ℕ}
    (u : ℕ → List G)
    (hg : WordSheetsGood A x (List.ofFn (fun j : Fin h => u j.val)).flatten)
    (i : Fin h) :
    WordSheetsGood A (x * wordPrefix (fun j => (u j).prod) i.val) (u i.val) := by
…
```
Mentions: OAI.PolycyclicRecognition.WordSheetsGood, OAI.PolycyclicRecognition.wordPrefix

theorem OAI.PolycyclicRecognition.successful_block_path line 39

Source documentation

Each block has its own controlled path through the good sheets. The whole-word success condition supplies all the block starting states.

theorem successful_block_path
    (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)
    {h : ℕ} (u : ℕ → List (I × ℝ)) (n : G)
    (hparam : ∀ i : Fin h, ∀ z ∈ u i.val, P z.1 z.2)
    (hgood : WordSheetsGood A n
      (List.ofFn (fun j : Fin h => (u j.val).map (fun z => f z.1 z.2))).flatten)
…

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