Windows.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Superstring.Hierarchical.greatest_window line 11

Source documentation

A finite chain of windows has a simultaneous greatest start and end. The sum is used only to choose a point of the already totally ordered chain.

theorem greatest_window {ι : Type} (I : Finset ι) (s h : ι → ℤ)
    (hne : I.Nonempty)
    (hchain : ∀ i ∈ I, ∀ j ∈ I,
      (s i ≤ s j ∧ h i ≤ h j) ∨ (s j ≤ s i ∧ h j ≤ h i)) :
    ∃ j ∈ I, ∀ i ∈ I, s i ≤ s j ∧ h i ≤ h j := by
…

theorem OAI.Superstring.Hierarchical.finite_ordered_windows line 25

Source documentation

Finite ordered-window routing. Repeated windows and distinct requesters at the same coordinates are allowed; this is not a disjointness assumption.

theorem finite_ordered_windows {V : Set (List α)} (closed : SubstringClosed V)
    (A : ℤ → α) (letters : ∀ x, [A x] ∈ V)
    {ι : Type} (I : Finset ι) (s h : ι → ℤ)
    (hchain : ∀ i ∈ I, ∀ j ∈ I,
      (s i ≤ s j ∧ h i ≤ h j) ∨ (s j ≤ s i ∧ h j ≤ h i))
    (hvalid : ∀ i ∈ I, s i ≤ h i ∧ textWord A (s i) (h i) ∈ V)
    (a b c d : ℤ) (hab : a ≤ b) (hcd : c ≤ d) (hac : a ≤ c) (hbd : b ≤ d)
    (hstart : textWord A a b ∈ V) (hend : textWord A c d ∈ V)
    (hbounds : ∀ i ∈ I, a ≤ s i ∧ s i ≤ c ∧ b ≤ h i ∧ h i ≤ d) :
    ∃ P : Path V (textWord A a b) (textWord A c d),
      P.cost = (d - b).toNat ∧ ∀ i ∈ I, P.Visits (textWord A (s i) (h i)) := by
…

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

theorem OAI.Superstring.Hierarchical.host_excursion_finite line 66

Source documentation

Host excursion for any finite chain of later targets, including the empty case. No enumeration/sorting oracle is assumed by the conclusion.

theorem host_excursion_finite {V : Set (List α)} (closed : SubstringClosed V)
    (A : ℤ → α) (letters : ∀ x, [A x] ∈ V) (q p₀ : ℕ)
    (hp₀ : 0 < p₀) (per : Function.Periodic A (q : ℤ))
    (a₀ b₀ e₀ : ℤ) (he₀ : a₀ + p₀ < e₀) (heb : e₀ ≤ b₀)
    (hR : textWord A a₀ b₀ ∈ V) (hshort : b₀ < a₀ + q + p₀)
    {ι : Type} (I : Finset ι) (s h : ι → ℤ)
    (hchain : ∀ i ∈ I, ∀ j ∈ I,
      (s i ≤ s j ∧ h i ≤ h j) ∨ (s j ≤ s i ∧ h j ≤ h i))
    (hbounds : ∀ i ∈ I, a₀ ≤ s i ∧ s i ≤ a₀ + q ∧ s i ≤ h i ∧
      b₀ ≤ h i ∧ h i < a₀ + q + p₀)
    (hQ : ∀ i ∈ I, textWord A (s i) (h i) ∈ V) :
    ∃ P : Path V (textWord A a₀ e₀) (textWord A a₀ e₀),
…

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

structure OAI.Superstring.Hierarchical.BlockPlan line 122
theorem OAI.Superstring.Hierarchical.BlockPlan.connect line 145
theorem OAI.Superstring.Hierarchical.Layer.window_order line 259
Source documentation
Actual vertices on one monotone host path inherit the order of starts; within a vertical run they are ordered by their ends.
```
theorem window_order (D : Layer V A q) {a b c d : ℤ}
    (hb : b ≤ D.last a) (hd : D.first c ≤ d) (hac : a < c) : b ≤ d := by
…
```
Mentions: OAI.Superstring.Hierarchical.Layer
structure OAI.Superstring.Hierarchical.HostedGroup line 268
Source documentation
One child group's single recorded host window, in host coordinates. This includes the actual recipient and full-window agreement, not just a common substring or an assumed possibility of connecting it.
```
structure HostedGroup (D : Layer V A q) where
…
```
Mentions: OAI.Superstring.Hierarchical.Layer
theorem OAI.Superstring.Hierarchical.HostedGroup.start_le_stop line 284
theorem OAI.Superstring.Hierarchical.HostedGroup.host_mem line 287
theorem OAI.Superstring.Hierarchical.HostedGroup.child_mem line 290
theorem OAI.Superstring.Hierarchical.HostedGroup.length_lt line 293
theorem OAI.Superstring.Hierarchical.HostedGroup.overlap_lt line 299
Source documentation
Cross-child overlaps cannot contain a full sum of their periods.
```
theorem overlap_lt (J : HostedGroup D)
    (hstart : H.start ≤ J.start) (hstop : H.stop ≤ J.stop)
    (hne : H.text ≠ J.text) : H.stop - J.start < H.period + J.period := by
…
```
Mentions: OAI.Superstring.Hierarchical.HostedGroup

theorem OAI.Superstring.Hierarchical.HostedGroup.next_overlap_lt line 309

Source documentation

Overlap with the next q-translate of another record transports that child's full text.

theorem next_overlap_lt (J : HostedGroup D) (per : Function.Periodic A (q : ℤ))
    (hstart : H.start ≤ J.start + q) (hstop : H.stop ≤ J.stop + q)
    (hne : H.text ≠ fun x => J.text (x - q)) :
    H.stop - (J.start + q) < H.period + J.period := by
…

Mentions: OAI.Superstring.Hierarchical.HostedGroup

structure OAI.Superstring.Hierarchical.HostedGroup.Request line 323
Source documentation
The primitive-layer requester uses an actual child vertex at this record.
```
structure Request (H : HostedGroup D) where
…
```
Mentions: OAI.Superstring.Hierarchical.HostedGroup
theorem OAI.Superstring.Hierarchical.HostedGroup.Request.word_mem line 335
theorem OAI.Superstring.Hierarchical.HostedGroup.Request.touched line 338