Threads.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Superstring.Counts.Data.down_descendants line 12
Source documentation
Prefix-subtree telescoping, stronger than the total-cost identity.
```
theorem down_descendants (D : Data α) (hD : D.WellFormed) {s : List α} (hs : s ≠ []) :
    (∑ r ∈ D.vertices with s <+: r, D.down r) = D.count s := by
…
```
Mentions: OAI.Superstring.Counts.Data
abbrev OAI.Superstring.Counts.Data.DownToken line 84
Source documentation
Each copy of an actual base down edge is a distinct token.
```
abbrev DownToken (D : Data α) := Σ s : D.vertices, Fin (D.down s.val)
…
```
Mentions: OAI.Superstring.Counts.Data
def OAI.Superstring.Counts.Data.DownToken.word line 90
theorem OAI.Superstring.Counts.Data.DownToken.mem line 92
theorem OAI.Superstring.Counts.Data.DownToken.nonempty line 94
theorem OAI.Superstring.Counts.Data.DownToken.histogram line 102
theorem OAI.Superstring.Counts.Data.DownToken.card line 112
theorem OAI.Superstring.Counts.Data.DownToken.prefix_count line 116
theorem OAI.Superstring.Counts.Data.DownToken.capacity line 122
Source documentation
The capacity condition needed to thread the down tokens into passages.
```
theorem capacity (hD : D.WellFormed) (s : List α) :
    (Finset.univ.filter (fun i : D.DownToken => s <+: (word D i).tail)).card ≤
      (Finset.univ.filter (fun i : D.DownToken => s <+: word D i)).card := by
…
```
Mentions: OAI.Superstring.Counts.Data.DownToken.word, OAI.Superstring.Counts.Data.DownToken.card
theorem OAI.Superstring.Counts.Data.down_permutation line 155
structure OAI.Superstring.Hierarchical.Threading line 167
Source documentation
Down-edge tokens threaded through the acyclic up-edge runs.
```
structure Threading (V : Set (List α)) (ι : Type) where
…
```
def OAI.Superstring.Hierarchical.Threading.text line 179
Source documentation
The letter removed by the down step at each integer start coordinate.
```
def text (i : ι) (x : ℤ) : α :=
…
```
theorem OAI.Superstring.Hierarchical.Threading.text_zpow line 182
theorem OAI.Superstring.Hierarchical.Threading.text_next line 186
theorem OAI.Superstring.Hierarchical.Threading.text_period line 189
theorem OAI.Superstring.Hierarchical.Threading.exists_primitive_text line 195
theorem OAI.Superstring.Hierarchical.Threading.word_spelled line 201
Source documentation
Following tails proves that every old vertex is spelled by the infinite text, even if it is longer than an entire turn of the threaded circulation.
```
theorem word_spelled (i : ι) :
    C.word i = textWord (C.text i) 0 (C.word i).length := by
…
```
Mentions: OAI.Superstring.Hierarchical.textWord
theorem OAI.Superstring.Hierarchical.Threading.translated_word line 231
Source documentation
The actual exit vertex seen at any translated token.
```
theorem translated_word (i : ι) (x : ℤ) :
    C.word ((C.next ^ x) i) =
      textWord (C.text i) x (x + (C.word ((C.next ^ x) i)).length) := by
…
```
Mentions: OAI.Superstring.Hierarchical.textWord
theorem OAI.Superstring.Hierarchical.Threading.exit_mono_one line 247
Source documentation
Entry-exit monotonicity before sorting; all entry windows are nonnegative.
```
theorem exit_mono_one (i : ι) :
    (C.word i).length ≤ 1 + (C.word (C.next i)).length := by
…
```
def OAI.Superstring.Counts.Data.threading line 262
Source documentation
Realize the base down multiset as a periodic circulation on actual vertices.
```
noncomputable def threading (D : Data α) (hD : D.WellFormed) :
    Hierarchical.Threading (D.vertices : Set (List α)) D.DownToken where
…
```
Mentions: OAI.Superstring.Counts.Data, OAI.Superstring.Hierarchical.Threading
theorem OAI.Superstring.OrderStats.card_filter_perm line 277
theorem OAI.Superstring.OrderStats.order_perm line 284
def OAI.Superstring.Hierarchical.Threading.Aligned line 295
Source documentation
Tokens with a specified full-text alignment, not just a matching finite word.
```
def Aligned (C : Threading V ι) (A : ℤ → α) := {i : ι // C.text i = A}
```
Mentions: OAI.Superstring.Hierarchical.Threading
instance OAI.Superstring.Hierarchical.Threading.(instance at line 297) line 297
def OAI.Superstring.Hierarchical.Threading.enumerate line 301
def OAI.Superstring.Hierarchical.Threading.periodPerm line 305
Source documentation
A text period permutes, rather than fixes, the multiple aligned passages.
```
def periodPerm (C : Threading V ι) {A : ℤ → α} {p : ℕ}
    (hp : Function.Periodic A (p : ℤ)) : Equiv.Perm (C.Aligned A) :=
…
```
Mentions: OAI.Superstring.Hierarchical.Threading
def OAI.Superstring.Hierarchical.Threading.exits line 321
Source documentation
Exit ends of the unsorted primitive passages.
```
noncomputable def exits (C : Threading V ι) (A : ℤ → α) (x : ℤ)
    (j : Fin (Fintype.card (C.Aligned A))) : ℤ :=
…
```
Mentions: OAI.Superstring.Hierarchical.Threading
theorem OAI.Superstring.Hierarchical.Threading.exits_step line 325
theorem OAI.Superstring.Hierarchical.Threading.exits_lower line 334
def OAI.Superstring.Hierarchical.Threading.sortedExit line 341
Source documentation
Sorting independently at every coordinate gives the monotone layer function.
```
noncomputable def sortedExit (C : Threading V ι) (A : ℤ → α)
    (j : Fin (Fintype.card (C.Aligned A))) (x : ℤ) : ℤ := OrderStats.order (C.exits A x) j
```
Mentions: OAI.Superstring.Hierarchical.Threading, OAI.Superstring.OrderStats.order
theorem OAI.Superstring.Hierarchical.Threading.sortedExit_mono line 344
theorem OAI.Superstring.Hierarchical.Threading.sortedExit_lower line 350
theorem OAI.Superstring.Hierarchical.Threading.exits_period line 358
theorem OAI.Superstring.Hierarchical.Threading.sortedExit_shift line 368
theorem OAI.Superstring.Hierarchical.Threading.exits_actual line 381
theorem OAI.Superstring.Hierarchical.Threading.sortedExit_actual line 389
Source documentation
The sorted windows are genuine substring vertices. No abstract completion of V or artificial layer windows are introduced.
```
theorem sortedExit_actual (C : Threading V ι) (closed : SubstringClosed V)
    (A : ℤ → α) (j : Fin (Fintype.card (C.Aligned A))) (x e : ℤ)
    (hlo : C.sortedExit A j (x - 1) ≤ e) (hhi : e ≤ C.sortedExit A j x) :
    textWord A x e ∈ V := by
…
```
Mentions: OAI.Superstring.Hierarchical.Threading, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.textWord
def OAI.Superstring.Hierarchical.Threading.layer line 401
Source documentation
The ordered-layer construction for a specified primitive-text group.
```
noncomputable def layer (C : Threading V ι) (closed : SubstringClosed V)
    {A : ℤ → α} {p : ℕ} (hp : Function.Periodic A (p : ℤ))
    (j : Fin (Fintype.card (C.Aligned A))) : Layer V A p where
…
```
Mentions: OAI.Superstring.Hierarchical.Threading, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Layer
theorem OAI.Superstring.Hierarchical.Threading.layers_ordered line 410

theorem OAI.Superstring.Hierarchical.Threading.sorted_edges line 415

Source documentation

Exact conservation of vertical unit edges under the sorting operation.

theorem sorted_edges (C : Threading V ι) (A : ℤ → α) (x e : ℤ) :
    (Finset.univ.filter (fun j => C.sortedExit A j (x - 1) ≤ e ∧
      e < C.sortedExit A j x)).card =
    (Finset.univ.filter (fun j => C.exits A (x - 1) j ≤ e ∧
      e < C.exits A x j)).card := by
…

Mentions: OAI.Superstring.Hierarchical.Threading