HostNormalization.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Superstring.Hierarchical.host_normalized line 13

Source documentation

The complete host construction for records normalized into one cyclic turn. Different children share at most their Fine-Wilf overlap; any number of layers of one child may request at its single record. Their distinct budgets are summed with multiplicity.

theorem host_normalized (closed : SubstringClosed V) (D : Layer V A q)
    (hq : 0 < q) (per : Function.Periodic A (q : ℤ)) (letters : ∀ x, [A x] ∈ V)
    (H : ι → HostedGroup D) (g : κ → ι) (R : ∀ i, (H (g i)).Request)
    (child_letters : ∀ j x, [(H j).text x] ∈ V)
    (different : ∀ i j, i ≠ j → ∀ c, (H i).text ≠ fun x => (H j).text (x + c))
    (I : Finset κ) (z : ι) (hz : ∃ i ∈ I, g i = z)
    (hmin : ∀ i ∈ I, (H z).period ≤ (H (g i)).period)
    (horder : ∀ i ∈ I,
      (H z).start ≤ (H (g i)).start ∧ (H (g i)).start ≤ (H z).start + q ∧
      (H z).stop ≤ (H (g i)).stop ∧ (H (g i)).stop ≤ (H z).stop + q) :
    ∃ Q : Path V [] [], Q.cost ≤ q + ∑ i ∈ I, (H (g i)).period ∧
      D.TouchedBy Q ∧ ∀ i ∈ I, (R i).layer.TouchedBy Q := by
…

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

def OAI.Superstring.Hierarchical.Layer.translate line 165
Source documentation
Simultaneous coordinate transport of a child text and its layer.
```
def translate (D : Layer V A p) (δ : ℤ) : Layer V (fun x => A (x - δ)) p where
…
```
Mentions: OAI.Superstring.Hierarchical.Layer
theorem OAI.Superstring.Hierarchical.Layer.translate_first line 191
theorem OAI.Superstring.Hierarchical.Layer.translate_last line 197
theorem OAI.Superstring.Hierarchical.Layer.translate_touched line 200

theorem OAI.Superstring.Hierarchical.Layer.normalize_window line 223

Source documentation

A cyclic record can be placed between a fixed actual record and its next copy in BOTH coordinates. Equal-start vertical runs are treated explicitly.

theorem normalize_window (D : Layer V A p) (hp : 0 < p)
    {a b a₀ b₀ : ℤ} (hf : D.first a ≤ b) (hl : b ≤ D.last a)
    (hf₀ : D.first a₀ ≤ b₀) (hl₀ : b₀ ≤ D.last a₀) :
    ∃ m : ℤ, a₀ ≤ a + m * p ∧ a + m * p ≤ a₀ + p ∧
      b₀ ≤ b + m * p ∧ b + m * p ≤ b₀ + p := by
…

Mentions: OAI.Superstring.Hierarchical.Layer

def OAI.Superstring.Hierarchical.HostedGroup.translate line 278
Source documentation
Translate a hosted record by a whole number of host periods, transporting its entire child text, not only its interval endpoints.
```
def translate (H : HostedGroup D) (per : Function.Periodic A (q : ℤ)) (m : ℤ) :
    HostedGroup D where
…
```
Mentions: OAI.Superstring.Hierarchical.HostedGroup
def OAI.Superstring.Hierarchical.HostedGroup.Request.translate line 313
Source documentation
All requester windows and layer coordinates travel with their one record.
```
def translate {H : HostedGroup D} (R : H.Request)
    (per : Function.Periodic A (q : ℤ)) (m : ℤ) : (H.translate per m).Request where
…
```
Mentions: OAI.Superstring.Hierarchical.HostedGroup, OAI.Superstring.Hierarchical.HostedGroup.Request
theorem OAI.Superstring.Hierarchical.host_requests line 340
def OAI.Superstring.Hierarchical.Layer.Content line 394
Source documentation
The actual vertices of a fixed base layer, independent of its coordinate presentation. This is not the larger set of all recorded prefixes.
```
def Content (L : Layer V A p) : Set (List α) :=
…
```
Mentions: OAI.Superstring.Hierarchical.Layer
theorem OAI.Superstring.Hierarchical.Layer.content_mem line 397
theorem OAI.Superstring.Hierarchical.Layer.touched_iff line 401
theorem OAI.Superstring.Hierarchical.Layer.translate_content line 409
theorem OAI.Superstring.Hierarchical.Layer.content_loop line 431
Source documentation
Every actual vertex is retained when one full base turn is materialized.
```
theorem content_loop (L : Layer V A p) (closed : SubstringClosed V)
    (hp : 0 < p) (per : Function.Periodic A (p : ℤ)) :
    ∃ P : Loop V, P.cost = p ∧ ∀ w ∈ L.Content, P.Visits w := by
…
```
Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Loop
theorem OAI.Superstring.Hierarchical.Layer.below_baseline line 440
theorem OAI.Superstring.Hierarchical.fill_layers line 462
theorem OAI.Superstring.Hierarchical.root_upper line 482
Source documentation
The easy round trip through the top first window visits every lower first height on its up path. Its cost is the top window's length, not a sum of lengths.
```
theorem root_upper {α ι : Type} {V : Set (List α)} {A : ℤ → α} {p : ℕ}
    (closed : SubstringClosed V) (L : ι → Layer V A p) (top : ι)
    (hupper : ∀ i x, (L i).z x ≤ (L top).z x) (t : ℤ) :
    ∃ Q : Path V [] [], Q.cost = (textWord A t ((L top).first t)).length ∧
      ∀ i, (L i).TouchedBy Q := by
…
```
Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.Path, OAI.Superstring.Hierarchical.textWord