Collections.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Superstring.Hierarchical.exists_greatest_rotation line 8

Source documentation

A distinguished rotation exists by inspecting one finite period.

theorem exists_greatest_rotation {α : Type} [LinearOrder α] (A : ℤ → α)
    (p : ℕ) (hp : 0 < p) (per : Function.Periodic A (p : ℤ)) :
    ∃ t : ℤ, 0 ≤ t ∧ t < p ∧ ∀ x, forward A x ≤ forward A t := by
…

Mentions: OAI.Superstring.Hierarchical.forward

theorem OAI.Superstring.Hierarchical.Layer.letters line 41
Source documentation
Every text letter occurs on the fixed layer's last actual window.
```
theorem letters (L : Layer V A p) (closed : SubstringClosed V) (x : ℤ) : [A x] ∈ V := by
…
```
Mentions: OAI.Superstring.Hierarchical.Layer, OAI.Superstring.Hierarchical.SubstringClosed
structure OAI.Superstring.Hierarchical.LayerCollection line 54
Source documentation
Finite ordered primitive-text groups supplied by the fixed base decomposition. All fields describe actual layers, never connecting walks.
```
structure LayerCollection {α : Type} (V : Set (List α)) (G : Type) where
…
```
abbrev OAI.Superstring.Hierarchical.LayerCollection.Id line 69
def OAI.Superstring.Hierarchical.LayerCollection.layerAt line 71
def OAI.Superstring.Hierarchical.LayerCollection.distinguished line 73
theorem OAI.Superstring.Hierarchical.LayerCollection.distinguished_max line 76
def OAI.Superstring.Hierarchical.LayerCollection.rank line 80
theorem OAI.Superstring.Hierarchical.LayerCollection.letters line 83

theorem OAI.Superstring.Hierarchical.fill_same_layers line 93

Source documentation

Constant-period version of base saturation, retaining every already visited vertex. The finite index set is allowed to omit other layers.

theorem fill_same_layers {α ι : Type} {V : Set (List α)} {A : ℤ → α} {p : ℕ}
    (closed : SubstringClosed V) (L : ι → Layer V A p) (hp : 0 < p)
    (per : Function.Periodic A (p : ℤ)) (I : Finset ι) (P : Loop V)
    (htouch : ∀ i ∈ I, (L i).TouchedBy P.path) :
    ∃ Q : Loop V, Q.base = P.base ∧ Q.cost ≤ P.cost + I.card * p ∧
      (∀ w, P.Visits w → Q.Visits w) ∧
      ∀ i ∈ I, ∀ w ∈ (L i).Content, Q.Visits w := by
…

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

theorem OAI.Superstring.Hierarchical.forward_shift line 103
def OAI.Superstring.Hierarchical.LayerCollection.groupIds line 116
theorem OAI.Superstring.Hierarchical.LayerCollection.card_groupIds line 119
theorem OAI.Superstring.Hierarchical.LayerCollection.groupIds_same line 122
structure OAI.Superstring.Hierarchical.LayerCollection.PlannedBlock line 129
Source documentation
A concrete outgoing plan. Its local walks include each constituent base turn exactly once in the reserve.
```
structure PlannedBlock [LinearOrder α] where
…
```
def OAI.Superstring.Hierarchical.LayerCollection.PlannedBlock.content line 152
def OAI.Superstring.Hierarchical.LayerCollection.PlannedBlock.word line 154
theorem OAI.Superstring.Hierarchical.LayerCollection.PlannedBlock.word_content line 156
theorem OAI.Superstring.Hierarchical.LayerCollection.PlannedBlock.same_short line 161
theorem OAI.Superstring.Hierarchical.LayerCollection.covers_groupIds line 177

def OAI.Superstring.Hierarchical.LayerCollection.individualPlan line 186

Source documentation

A single upper layer satisfies exactly the ordinary individual-link conditions. The short contact is proved by the three-window path.

noncomputable def individualPlan (closed : SubstringClosed V)
    (g : G) (i : Fin (C.size g)) (target : C.Id)
    (R : (C.layerAt target).Record (C.text g))
    (hne : C.text g ≠ fun x => C.text target.1 (x + R.offset))
    (hf : (C.layer g i).first R.start ≤ R.stop)
    (hl : R.stop ≤ (C.layer g i).last R.start + C.period g) : C.PlannedBlock := by
…

Mentions: OAI.Superstring.Hierarchical.SubstringClosed

def OAI.Superstring.Hierarchical.LayerCollection.collectivePlan line 232

Source documentation

A collective top block is valid INCLUDING k=1. Its ordinary link, free period internal alternative, and maximal-rank short-contact realization are all materialized, with every constituent base turn included once.

noncomputable def collectivePlan (closed : SubstringClosed V)
    (g : G) (I : Finset (Fin (C.size g))) (lo hi : Fin (C.size g))
    (hlom : lo ∈ I) (hhim : hi ∈ I)
    (hlo : ∀ j ∈ I, lo ≤ j) (hhi : ∀ j ∈ I, j ≤ hi)
    (target : C.Id) (R : (C.layerAt target).Record (C.text g))
    (hne : C.text g ≠ fun x => C.text target.1 (x + R.offset))
    (hat : R.start ≤ C.distinguished g) (htb : C.distinguished g < R.stop)
    (hsharp : (C.layer g hi).first (C.distinguished g) -
      (C.layer g lo).last (C.distinguished g) ≤ ((I.card - 1) * C.period g : ℕ))
    (hH : (C.layer g hi).first (C.distinguished g) ≤ R.stop + (I.card * C.period g : ℕ))
    (hlast : R.stop ≤ (C.layer g lo).last R.start + (I.card * C.period g : ℕ)) :
    C.PlannedBlock := by
…

Mentions: OAI.Superstring.Hierarchical.SubstringClosed

def OAI.Superstring.Hierarchical.LayerCollection.PlannedBlock.reserve line 323
theorem OAI.Superstring.Hierarchical.LayerCollection.PlannedBlock.execute line 328
Source documentation
Execute the concrete geometrically proved plans. Target ownership does not require a disjointness assumption: any covering block can be chosen, and every reserve is charged once. Group processing will prove the total budget.
```
theorem execute (closed : SubstringClosed V) (I : Finset C.PlannedBlock)
    (P : Path V [] [])
    (covered : ∀ i : C.Id, (∀ w ∈ (C.layerAt i).Content, P.Visits w) ∨
      ∃ B ∈ I, i ∈ B.members) :
    ∃ Q : Path V [] [], Q.cost ≤ P.cost + ∑ B ∈ I, B.reserve ∧
      (∀ w, P.Visits w → Q.Visits w) ∧
      ∀ i : C.Id, ∀ w ∈ (C.layerAt i).Content, Q.Visits w := by
…
```
Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path