OAI/Computability/Superstring/Hierarchical.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Superstring.Hierarchical.SubstringClosed line 12
2. inductive OAI.Superstring.Hierarchical.Path line 17

   Source documentation

   An explicit hierarchical-graph walk. Up edges append one symbol and down edges delete the first symbol. Transitivity retains every edge of both walks.

   inductive Path (V : Set (List α)) : List α → List α → Type
     | nil (s) (hs : s ∈ V) : Path V s s
     | up (s) (a) (hs : s ∈ V) (ht : s ++ [a] ∈ V) : Path V s (s ++ [a])
     | down (a) (s) (hs : a :: s ∈ V) (ht : s ∈ V) : Path V (a :: s) s
     | trans {s t u} : Path V s t → Path V t u → Path V s u
   
   namespace Path
   
   variable {V : Set (List α)} {s t u : List α}

3. def OAI.Superstring.Hierarchical.Path.cost line 27
4. def OAI.Superstring.Hierarchical.Path.Visits line 34

   Source documentation

   Vertices, including both endpoints, with no quotient of the edge data.

   def Visits (w : List α) : {s t : List α} → Path V s t → Prop
     | _, _, .nil s _ => w = s
     | _, _, .up s a _ _ => w = s ∨ w = s ++ [a]
     | _, _, .down a s _ _ => w = a :: s ∨ w = s
     | _, _, .trans P Q => P.Visits w ∨ Q.Visits w

   Mentions: OAI.Superstring.Hierarchical.Path

5. theorem OAI.Superstring.Hierarchical.Path.cost_trans line 40
6. theorem OAI.Superstring.Hierarchical.Path.visits_start line 43
7. theorem OAI.Superstring.Hierarchical.Path.visits_end line 50
8. theorem OAI.Superstring.Hierarchical.Path.mem_of_visits line 57
9. def OAI.Superstring.Hierarchical.Path.copy line 65

   Source documentation

   Reindex an explicit walk along equality of its endpoint words.

   def copy (P : Path V s t) {s' t' : List α} (hs : s = s') (ht : t = t') :
       Path V s' t' := hs ▸ ht ▸ P

   Mentions: OAI.Superstring.Hierarchical.Path

10. theorem OAI.Superstring.Hierarchical.Path.cost_copy line 68
11. theorem OAI.Superstring.Hierarchical.Path.visits_copy line 72
12. def OAI.Superstring.Hierarchical.Path.deletePrefix line 77

    Source documentation

    Delete an arbitrary prefix, costing zero.

    def deletePrefix (closed : SubstringClosed V) (a b : List α) (h : a ++ b ∈ V) :
        Path V (a ++ b) b :=
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path

13. theorem OAI.Superstring.Hierarchical.Path.cost_deletePrefix line 85
14. def OAI.Superstring.Hierarchical.Path.appendSuffix line 92

    Source documentation

    Append an arbitrary suffix, staying within prefixes of the final word.

    def appendSuffix (closed : SubstringClosed V) (a b : List α) (h : a ++ b ∈ V) :
        Path V a (a ++ b) :=
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path

15. theorem OAI.Superstring.Hierarchical.Path.cost_appendSuffix line 102
16. def OAI.Superstring.Hierarchical.Path.readGap line 110

    Source documentation

    A path that reads a word one letter at a time, always returning to empty. This supplies the gap case of ordered windows without adding non-substring words.

    def readGap (h0 : ([] : List α) ∈ V) (w : List α)
        (h : ∀ a ∈ w, [a] ∈ V) : Path V [] [] :=
    …

    Mentions: OAI.Superstring.Hierarchical.Path

17. theorem OAI.Superstring.Hierarchical.Path.cost_readGap line 119
18. def OAI.Superstring.Hierarchical.textWord line 131

    Source documentation

    The finite integer window of a two-sided text.

    def textWord (A : ℤ → α) (a b : ℤ) : List α :=
    …

19. theorem OAI.Superstring.Hierarchical.length_textWord line 134
20. theorem OAI.Superstring.Hierarchical.textWord_self line 138
21. theorem OAI.Superstring.Hierarchical.textWord_append line 141
22. theorem OAI.Superstring.Hierarchical.textWord_infix line 155
23. theorem OAI.Superstring.Hierarchical.mem_textWord line 161
24. theorem OAI.Superstring.Hierarchical.textWord_translate line 168

    Source documentation

    Translate a window by a period of its text, preserving the graph vertex.

    theorem textWord_translate (A : ℤ → α) (h : ℤ) (per : ∀ x, A (x + h) = A x)
        (a b : ℤ) : textWord A (a + h) (b + h) = textWord A a b := by
    …

    Mentions: OAI.Superstring.Hierarchical.textWord

25. theorem OAI.Superstring.Hierarchical.ordered_windows line 177
26. theorem OAI.Superstring.Hierarchical.Path.deletePrefix_visits line 226
27. theorem OAI.Superstring.Hierarchical.Path.appendSuffix_visits line 234
28. theorem OAI.Superstring.Hierarchical.window_delete line 247

    Source documentation

    Delete through a range of starting coordinates, visiting every suffix.

    theorem window_delete {V : Set (List α)} (closed : SubstringClosed V)
        (A : ℤ → α) {a b c : ℤ} (hac : a ≤ c) (hcb : c ≤ b)
        (hw : textWord A a b ∈ V) :
        ∃ P : Path V (textWord A a b) (textWord A c b), P.cost = 0 ∧
          ∀ x, a ≤ x → x ≤ c → P.Visits (textWord A x b) := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.textWord, OAI.Superstring.Hierarchical.Path

29. theorem OAI.Superstring.Hierarchical.window_append line 272

    Source documentation

    Append through a range of ends, visiting every prefix.

    theorem window_append {V : Set (List α)} (closed : SubstringClosed V)
        (A : ℤ → α) {a b d : ℤ} (hab : a ≤ b) (hbd : b ≤ d)
        (hw : textWord A a d ∈ V) :
        ∃ P : Path V (textWord A a b) (textWord A a d),
          P.cost = (d - b).toNat ∧
          ∀ y, b ≤ y → y ≤ d → P.Visits (textWord A a y) := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.textWord, OAI.Superstring.Hierarchical.Path

30. theorem OAI.Superstring.Hierarchical.ordered_windows_suffixes line 297

    Source documentation

    An ordered-window transition can be chosen to contain every overlap suffix up to its next start. This strengthens the contact assertion used for links.

    theorem ordered_windows_suffixes {V : Set (List α)} (closed : SubstringClosed V)
        (A : ℤ → α) (letters : ∀ x, [A x] ∈ V)
        {a b c d : ℤ} (hab : a ≤ b) (hcd : c ≤ d) (hac : a ≤ c) (hbd : b ≤ d)
        (h₁ : textWord A a b ∈ V) (h₂ : textWord A c d ∈ V) :
        ∃ P : Path V (textWord A a b) (textWord A c d),
          P.cost = (d - b).toNat ∧
          (∀ x, a ≤ x → x ≤ c → x ≤ b → P.Visits (textWord A x b)) ∧
          ∃ w, P.Visits w ∧ (w.length : ℤ) ≤ max 0 (b - c) := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.textWord, OAI.Superstring.Hierarchical.Path

31. structure OAI.Superstring.Hierarchical.Layer line 317
32. def OAI.Superstring.Hierarchical.Layer.first line 328
33. def OAI.Superstring.Hierarchical.Layer.last line 329
34. theorem OAI.Superstring.Hierarchical.Layer.first_le_last line 331
35. theorem OAI.Superstring.Hierarchical.Layer.start_le_first line 334
36. theorem OAI.Superstring.Hierarchical.Layer.first_actual line 336
37. theorem OAI.Superstring.Hierarchical.Layer.last_actual line 339
38. theorem OAI.Superstring.Hierarchical.Layer.shift_mul line 342
39. theorem OAI.Superstring.Hierarchical.Layer.meets_height line 350

    Source documentation

    An actual height crossing in any finite horizontal range.

    theorem meets_height (D : Layer V A p) (a Y : ℤ) (K : ℕ)
        (hfirst : D.first a ≤ Y) (hlast : Y ≤ D.last (a + K)) :
        ∃ x : ℤ, a ≤ x ∧ x ≤ a + K ∧ D.first x ≤ Y ∧ Y ≤ D.last x := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer

40. def OAI.Superstring.Hierarchical.Layer.TouchedBy line 368
41. theorem OAI.Superstring.Hierarchical.periodic_mul line 374

    Source documentation

    Periods can be multiplied without assuming they are least.

    theorem periodic_mul (A : ℤ → α) (p : ℕ) (per : ∀ x, A (x + p) = A x)
        (k : ℕ) (x : ℤ) : A (x + (k * p : ℕ)) = A x := by
    …

42. theorem OAI.Superstring.Hierarchical.collective_link line 382
43. theorem OAI.Superstring.Hierarchical.join_band line 429
44. def OAI.Superstring.Hierarchical.forward line 473

    Source documentation

    Forward rotations carry the usual lexicographic order, not a coordinatewise order on streams.

    def forward (A : ℤ → α) (t : ℤ) : Lex (ℕ → α) :=
    …

45. theorem OAI.Superstring.Hierarchical.lex_at_le line 476
46. theorem OAI.Superstring.Hierarchical.stream_eq_of_max line 485

    Source documentation

    If a stream dominates its shift by q, then no smaller q-periodic stream can have its first q letters. This is the first-difference argument in the maximal-rotation lemma, expressed as strong induction.

    theorem stream_eq_of_max [LinearOrder α] (s d : Lex (ℕ → α)) (q : ℕ)
        (hq : 0 < q) (hd : ∀ n, d (n + q) = d n)
        (hshift : toLex (fun n => s (n + q)) ≤ s) (hle : d ≤ s)
        (hprefix : ∀ n < q, s n = d n) : s = d := by
    …

47. theorem OAI.Superstring.Hierarchical.periodic_emod line 510

    Source documentation

    Integer periodic functions can be evaluated at their Euclidean residue.

    theorem periodic_emod (A : ℤ → α) (p : ℤ) (per : ∀ x, A (x + p) = A x)
        (x : ℤ) : A (x % p) = A x := by
    …

48. theorem OAI.Superstring.Hierarchical.periodic_eq_of_forward_eq line 517

    Source documentation

    Two periodic, two-sided texts are determined by their forward words.

    theorem periodic_eq_of_forward_eq (A D : ℤ → α) (p q : ℕ)
        (hp : 0 < p) (hq : 0 < q) (hA : ∀ x, A (x + p) = A x)
        (hD : ∀ x, D (x + q) = D x) (t : ℤ) (heq : forward A t = forward D t) :
        A = D := by
    …

    Mentions: OAI.Superstring.Hierarchical.forward

49. theorem OAI.Superstring.Hierarchical.maximal_rotation line 543
50. def OAI.Superstring.Hierarchical.AgreeOn line 565

    Source documentation

    Agreement on the half-open integer interval [a,b).

    def AgreeOn (A D : ℤ → α) (a b : ℤ) : Prop :=
    …

51. theorem OAI.Superstring.Hierarchical.textWord_eq_of_agree line 568
52. theorem OAI.Superstring.Hierarchical.periodic_mod_at line 577
53. theorem OAI.Superstring.Hierarchical.same_period_eq line 584

    Source documentation

    Agreement for one period determines an aligned periodic text.

    theorem same_period_eq (A D : ℤ → α) (p : ℕ) (hp : 0 < p)
        (hA : ∀ x, A (x + p) = A x) (hD : ∀ x, D (x + p) = D x)
        (a : ℤ) (h : AgreeOn A D a (a + p)) : A = D := by
    …

    Mentions: OAI.Superstring.Hierarchical.AgreeOn

54. theorem OAI.Superstring.Hierarchical.eq_of_long_agreement line 596
55. theorem OAI.Superstring.Hierarchical.agreement_bound line 618
56. theorem OAI.Superstring.Hierarchical.same_period_agreement_bound line 627
57. theorem OAI.Superstring.Hierarchical.Layer.first_mono line 640
58. theorem OAI.Superstring.Hierarchical.Layer.last_mono line 643
59. theorem OAI.Superstring.Hierarchical.Layer.first_shift line 645
60. theorem OAI.Superstring.Hierarchical.Layer.last_shift line 649
61. def OAI.Superstring.Hierarchical.Layer.HasShort line 653

    Source documentation

    An actual vertex of a layer whose symbol length is at most the allowance.

    def HasShort (D : Layer V A p) (q : ℕ) : Prop :=
    …

    Mentions: OAI.Superstring.Hierarchical.Layer

62. theorem OAI.Superstring.Hierarchical.Layer.first_long_of_not_short line 656
63. theorem OAI.Superstring.Hierarchical.collective_short_sweep line 667
64. theorem OAI.Superstring.Hierarchical.cycle_collective_contact line 724
65. def OAI.Superstring.Hierarchical.Path.written line 761

    Source documentation

    The word written by a hierarchical walk: exactly one symbol per up edge.

    def written : {s t : List α} → Path V s t → List α
      | _, _, .nil _ _ => []
      | _, _, .up _ a _ _ => [a]
      | _, _, .down _ _ _ _ => []
      | _, _, .trans P Q => P.written ++ Q.written

    Mentions: OAI.Superstring.Hierarchical.Path

66. theorem OAI.Superstring.Hierarchical.Path.length_written line 767
67. theorem OAI.Superstring.Hierarchical.Path.end_suffix_written line 770
68. theorem OAI.Superstring.Hierarchical.Path.visited_infix_written line 780

    Source documentation

    The exact output invariant in the main proof: every visited vertex occurs contiguously in the starting word followed by the appended letters.

    theorem visited_infix_written (P : Path V s t) {w : List α} (hw : P.Visits w) :
        w <:+: s ++ P.written := by
    …

    Mentions: OAI.Superstring.Hierarchical.Path

69. theorem OAI.Superstring.Hierarchical.Path.split line 801

    Source documentation

    Split at an actual visited vertex, preserving costs and every visit.

    theorem split (P : Path V s t) {w : List α} (hw : P.Visits w) :
        ∃ (U : Path V s w) (D : Path V w t),
          U.cost + D.cost = P.cost ∧
          ∀ v, P.Visits v ↔ U.Visits v ∨ D.Visits v := by
    …

    Mentions: OAI.Superstring.Hierarchical.Path

70. theorem OAI.Superstring.Hierarchical.Path.rotate line 837

    Source documentation

    Rotate a closed walk to any of its visited vertices without adding edges.

    theorem rotate (P : Path V s s) {w : List α} (hw : P.Visits w) :
        ∃ Q : Path V w w, Q.cost = P.cost ∧ ∀ v, Q.Visits v ↔ P.Visits v := by
    …

    Mentions: OAI.Superstring.Hierarchical.Path

71. theorem OAI.Superstring.Hierarchical.Path.splice line 846

    Source documentation

    Euler splicing in its exact needed form: edge-disjointness is unnecessary because edge copies remain distinct in the path data.

    theorem splice (P : Path V s s) (Q : Path V t t) (w : List α)
        (hP : P.Visits w) (hQ : Q.Visits w) :
        ∃ R : Path V s s, R.cost = P.cost + Q.cost ∧
          ∀ v, R.Visits v ↔ P.Visits v ∨ Q.Visits v := by
    …

    Mentions: OAI.Superstring.Hierarchical.Path

72. theorem OAI.Superstring.Hierarchical.Path.root_loop line 859

    Source documentation

    Rooting at a short vertex costs exactly its symbol length.

    theorem root_loop (closed : SubstringClosed V) (w : List α) (hw : w ∈ V) :
        ∃ P : Path V [] [], P.cost = w.length ∧ P.Visits w := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path

73. theorem OAI.Superstring.Hierarchical.ordered_chain line 870

    Source documentation

    Concatenate any finite ordered list of actual windows.

    theorem ordered_chain {V : Set (List α)} (closed : SubstringClosed V)
        (A : ℤ → α) (letters : ∀ x, [A x] ∈ V)
        (a b : ℕ → ℤ) (ha : Monotone a) (hb : Monotone b) (n : ℕ)
        (hab : ∀ i ≤ n, a i ≤ b i) (hV : ∀ i ≤ n, textWord A (a i) (b i) ∈ V) :
        ∃ P : Path V (textWord A (a 0) (b 0)) (textWord A (a n) (b n)),
          P.cost = (b n - b 0).toNat ∧
          ∀ i ≤ n, P.Visits (textWord A (a i) (b i)) := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.textWord, OAI.Superstring.Hierarchical.Path

74. theorem OAI.Superstring.Hierarchical.individual_link line 903
75. theorem OAI.Superstring.Hierarchical.one_free_period line 939
76. theorem OAI.Superstring.Hierarchical.Layer.passage line 955

    Source documentation

    Realize one entire vertical passage and its following down step.

    theorem passage (L : Layer V A p) (closed : SubstringClosed V) (x : ℤ) :
        ∃ P : Path V (textWord A x (L.first x))
            (textWord A (x + 1) (L.first (x + 1))),
          P.cost = (L.first (x + 1) - L.first x).toNat ∧
          ∀ e, L.first x ≤ e → e ≤ L.last x → P.Visits (textWord A x e) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path, OAI.Superstring.Hierarchical.textWord

77. theorem OAI.Superstring.Hierarchical.Layer.segment line 973

    Source documentation

    A finite segment of a layer, including every window at its traversed starts.

    theorem segment (L : Layer V A p) (closed : SubstringClosed V) (t : ℤ) (n : ℕ) :
        ∃ P : Path V (textWord A t (L.first t))
            (textWord A (t + n) (L.first (t + n))),
          P.cost = (L.first (t + n) - L.first t).toNat ∧
          ∀ x e, t ≤ x → x < t + n → L.first x ≤ e → e ≤ L.last x →
            P.Visits (textWord A x e) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path, OAI.Superstring.Hierarchical.textWord

78. theorem OAI.Superstring.Hierarchical.Layer.turn line 1003

    Source documentation

    One primitive turn is an explicit closed walk of exactly the period cost.

    theorem turn (L : Layer V A p) (closed : SubstringClosed V)
        (per : ∀ x, A (x + p) = A x) (t : ℤ) :
        ∃ P : Path V (textWord A t (L.first t)) (textWord A t (L.first t)),
          P.cost = p ∧
          ∀ x e, t ≤ x → x < t + p → L.first x ≤ e → e ≤ L.last x →
            P.Visits (textWord A x e) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path, OAI.Superstring.Hierarchical.textWord

79. theorem OAI.Superstring.Hierarchical.Layer.shift_int line 1025
80. theorem OAI.Superstring.Hierarchical.Layer.first_shift_int line 1036
81. theorem OAI.Superstring.Hierarchical.Layer.full_turn line 1042

    Source documentation

    An entire layer is covered by one turn, because every actual window is a period translate of a window in that turn.

    theorem full_turn (L : Layer V A p) (closed : SubstringClosed V) (hp : 0 < p)
        (per : ∀ x, A (x + p) = A x) (t : ℤ) :
        ∃ P : Path V (textWord A t (L.first t)) (textWord A t (L.first t)),
          P.cost = p ∧ ∀ x e, L.first x ≤ e → e ≤ L.last x →
            P.Visits (textWord A x e) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path, OAI.Superstring.Hierarchical.textWord

82. structure OAI.Superstring.Hierarchical.Loop line 1080

    Source documentation

    A closed walk with its base vertex retained as explicit data.

    structure Loop (V : Set (List α)) where
    …

83. def OAI.Superstring.Hierarchical.Loop.cost line 1088
84. def OAI.Superstring.Hierarchical.Loop.Visits line 1089
85. def OAI.Superstring.Hierarchical.Loop.Meets line 1091
86. theorem OAI.Superstring.Hierarchical.Loop.saturate line 1096

    Source documentation

    Saturate a closed walk by splicing every accessible loop from a finite collection. The resulting visited set is closed under that collection, and no loop budget is spent twice.

    theorem saturate {ι : Type} (F : ι → Loop V) (I : Finset ι) (P : Loop V) :
        ∃ Q : Loop V, Q.base = P.base ∧ Q.cost ≤ P.cost + ∑ i ∈ I, (F i).cost ∧
          (∀ w, P.Visits w → Q.Visits w) ∧
          (∀ i ∈ I, Q.Meets (F i) → ∀ w, (F i).Visits w → Q.Visits w) ∧
          (∀ w, Q.Visits w → P.Visits w ∨ ∃ i ∈ I, (F i).Visits w) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Loop, OAI.Superstring.Hierarchical.Loop.cost, OAI.Superstring.Hierarchical.Loop.Visits

87. def OAI.Superstring.Hierarchical.Loop.Connected line 1136

    Source documentation

    Used-support connectivity in a form that exactly expresses closure under closed walks. It ignores incidental isolated vertices and records a root.

    def Connected {ι : Type} (F : ι → Loop V) (I : Finset ι) (root : List α) : Prop :=
    …

    Mentions: OAI.Superstring.Hierarchical.Loop

88. theorem OAI.Superstring.Hierarchical.Loop.of_connected line 1142
89. theorem OAI.Superstring.Hierarchical.host_target_bounds line 1159

    Source documentation

    The host proof's modified target remains inside its recorded host window, and lies within one child period of the prescribed requester window.

    theorem host_target_bounds (a₀ b₀ a b e T : ℤ) (p₀ p : ℕ)
        (hmin : p₀ ≤ p) (horderA : a₀ ≤ a) (horderT : a ≤ T)
        (horderB : b₀ ≤ b)
        (hreq₁ : a + p < e) (hreq₂ : e ≤ b - p)
        (hleft : b₀ - a < p₀ + p) (hright : b - T < p + p₀)
        (hbase : b₀ < T + p₀) :
        let s := min (a + p) T
    …

90. theorem OAI.Superstring.Hierarchical.request_attachment line 1197

    Source documentation

    The child-period loop used to attach each later requester at its modified target; no recipient budget is consumed by this operation.

    theorem request_attachment {V : Set (List α)} (closed : SubstringClosed V)
        (A : ℤ → α) (letters : ∀ x, [A x] ∈ V) (p : ℕ)
        (per : ∀ x, A (x + p) = A x)
        {a e s h : ℤ} (hae : a ≤ e) (hsh : s ≤ h)
        (has : a ≤ s) (hsa : s ≤ a + p) (heh : e ≤ h) (hhe : h ≤ e + p)
        (hR : textWord A a e ∈ V) (hQ : textWord A s h ∈ V) :
        ∃ P : Path V (textWord A s h) (textWord A s h),
          P.cost = p ∧ P.Visits (textWord A a e) := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.textWord, OAI.Superstring.Hierarchical.Path

91. theorem OAI.Superstring.Hierarchical.host_excursion line 1223

    Source documentation

    The central cost-q excursion in the host text, for a nonempty ordered list of later targets. It includes the initial requesters' whole vertical range and ends with a contact shorter than the minimum child period.

    theorem host_excursion {V : Set (List α)} (closed : SubstringClosed V)
        (A : ℤ → α) (letters : ∀ x, [A x] ∈ V) (q p₀ : ℕ)
        (hp₀ : 0 < p₀) (per : ∀ x, A (x + q) = A x)
        (a₀ b₀ e₀ : ℤ) (he₀ : a₀ + p₀ < e₀) (heb : e₀ ≤ b₀)
        (hR : textWord A a₀ b₀ ∈ V)
        (s h : ℕ → ℤ) (hs : Monotone s) (hh : Monotone h) (n : ℕ)
        (hbounds : ∀ i ≤ n, a₀ ≤ s i ∧ s i ≤ a₀ + q ∧ s i ≤ h i ∧
          b₀ ≤ h i ∧ h i < a₀ + q + p₀)
        (hQ : ∀ i ≤ n, textWord A (s i) (h i) ∈ V) :
        ∃ P : Path V (textWord A a₀ e₀) (textWord A a₀ e₀),
          P.cost = q ∧ P.Visits (textWord A a₀ b₀) ∧
          (∀ e, e₀ ≤ e → e ≤ b₀ → P.Visits (textWord A a₀ e)) ∧
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.textWord, OAI.Superstring.Hierarchical.Path

92. theorem OAI.Superstring.Hierarchical.host_excursion_single line 1270

    Source documentation

    The no-later-record case of the same host excursion.

    theorem host_excursion_single {V : Set (List α)} (closed : SubstringClosed V)
        (A : ℤ → α) (letters : ∀ x, [A x] ∈ V) (q p₀ : ℕ)
        (hp₀ : 0 < p₀) (per : ∀ x, A (x + q) = A x)
        (a₀ b₀ e₀ : ℤ) (he₀ : a₀ + p₀ < e₀) (heb : e₀ ≤ b₀)
        (hshort : b₀ < a₀ + q + p₀) (hR : textWord A a₀ b₀ ∈ V) :
        ∃ P : Path V (textWord A a₀ e₀) (textWord A a₀ e₀),
          P.cost = q ∧ P.Visits (textWord A a₀ b₀) ∧
          (∀ e, e₀ ≤ e → e ≤ b₀ → P.Visits (textWord A a₀ e)) ∧
          ∃ w, P.Visits w ∧ w.length < p₀ := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.textWord, OAI.Superstring.Hierarchical.Path

93. theorem OAI.Superstring.Hierarchical.Loop.attach line 1290

    Source documentation

    Splice a family of request attachments into its host excursion.

    theorem attach {ι : Type} (F : ι → Loop V) (I : Finset ι) (P : Loop V)
        (hmeet : ∀ i ∈ I, P.Meets (F i)) :
        ∃ Q : Loop V, Q.base = P.base ∧ Q.cost ≤ P.cost + ∑ i ∈ I, (F i).cost ∧
          (∀ w, P.Visits w → Q.Visits w) ∧
          (∀ i ∈ I, ∀ w, (F i).Visits w → Q.Visits w) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Loop, OAI.Superstring.Hierarchical.Loop.cost, OAI.Superstring.Hierarchical.Loop.Visits

94. theorem OAI.Superstring.Hierarchical.Loop.root_at line 1302

    Source documentation

    A short contact roots the whole closed excursion for its length.

    theorem root_at (closed : SubstringClosed V) (P : Loop V) (w : List α)
        (hw : P.Visits w) :
        ∃ Q : Path V [] [], Q.cost = P.cost + w.length ∧
          ∀ v, P.Visits v → Q.Visits v := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Loop, OAI.Superstring.Hierarchical.Path

95. theorem OAI.Superstring.Hierarchical.Loop.root_attachments line 1314

    Source documentation

    Host requests consume the host cost, the later attachments' costs, and one unused minimum-child budget. The initial requesters remain visited.

    theorem root_attachments {ι : Type} (closed : SubstringClosed V)
        (P : Loop V) (F : ι → Loop V) (I : Finset ι) (p₀ : ℕ)
        (hmeet : ∀ i ∈ I, P.Meets (F i))
        (hshort : ∃ w, P.Visits w ∧ w.length ≤ p₀) :
        ∃ Q : Path V [] [], Q.cost ≤ P.cost + (∑ i ∈ I, (F i).cost) + p₀ ∧
          (∀ w, P.Visits w → Q.Visits w) ∧
          (∀ i ∈ I, ∀ w, (F i).Visits w → Q.Visits w) := by
    …

    Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Loop, OAI.Superstring.Hierarchical.Path, OAI.Superstring.Hierarchical.Loop.cost, OAI.Superstring.Hierarchical.Loop.Visits