Schedule.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Superstring.Hierarchical.LayerCollection.process_group line 12

Source documentation

A whole group is processed, reserving at most one outgoing request record. Incoming reserves are spent once; every new block and request is included in this exact numerical budget.

theorem process_group (closed : SubstringClosed V) (supply : C.RecordSupply)
    (g : G) (R : Finset C.Pending) (targets : ∀ r ∈ R, r.1.1 = g)
    (distinct : Set.InjOn Pending.source (R : Set C.Pending)) :
    ∃ (Q : Path V [] []) (B : Finset C.PlannedBlock) (O : Finset C.Pending),
      Q.cost + (∑ b ∈ B, b.reserve) + (∑ r ∈ O, r.reserve) ≤
        2 * (C.size g * C.period g) + ∑ r ∈ R, r.reserve ∧
      (∀ i : Fin (C.size g), C.Covered Q B O ⟨g, i⟩) ∧
      (∀ r ∈ R, ∀ i ∈ r.ids, ∀ w ∈ (C.layerAt i).Content, Q.Visits w) ∧
      (∀ r ∈ O, r.source = g) ∧ O.card ≤ 1 := by
…

Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.LayerCollection.Pending.source, OAI.Superstring.Hierarchical.Path

theorem OAI.Superstring.Hierarchical.LayerCollection.Covered.mono line 81

theorem OAI.Superstring.Hierarchical.LayerCollection.schedule line 93

Source documentation

Finite period-order scheduling, with all previously spent and reserved budgets retained. Strict increase of outgoing requests is proved by their actual record, and prevents both backward requests and duplicate sources.

theorem schedule (closed : SubstringClosed V) (supply : C.RecordSupply)
    (I : Finset G) (P : Path V [] []) (B : Finset C.PlannedBlock) (R : Finset C.Pending)
    (upward : ∀ g ∈ I, ∀ h, C.period g < C.period h → h ∈ I)
    (targets : ∀ r ∈ R, r.1.1 ∈ I) (sources : ∀ r ∈ R, r.source ∉ I)
    (distinct : Set.InjOn Pending.source (R : Set C.Pending))
    (ready : ∀ i : C.Id, i.1 ∈ I ∨ C.Covered P B R i) :
    ∃ Q : Path V [] [],
      Q.cost ≤ P.cost + (∑ b ∈ B, b.reserve) + (∑ r ∈ R, r.reserve) +
        ∑ g ∈ I, 2 * (C.size g * C.period g) ∧
      (∀ 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, OAI.Superstring.Hierarchical.LayerCollection.Pending.source

theorem OAI.Superstring.Hierarchical.LayerCollection.connect line 206
Source documentation
The geometric main bound for any actual finite layer collection supplied by the count rule. All local plans, requests, and functional cycles are paid.
```
theorem connect [Fintype G] (closed : SubstringClosed V) (he : [] ∈ V)
    (supply : C.RecordSupply) :
    ∃ Q : Path V [] [], Q.cost ≤ 2 * ∑ g, C.size g * C.period g ∧
      ∀ i : C.Id, ∀ w ∈ (C.layerAt i).Content, Q.Visits w := by
…
```
Mentions: OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.Path
theorem OAI.Superstring.Counts.Data.superstring_of_counts line 224
Source documentation
Reading the fully connected actual layer graph gives a constructive numerical bound, without treating recorded prefixes as vertices.
```
theorem superstring_of_counts (D : Data α) (hD : D.WellFormed)
    (required_valid : ∀ s ∈ D.required, s ∈ D.vertices ∧ s ≠ []) :
    ∃ T : List α, T.length ≤ 2 * D.weight ∧ ∀ s ∈ D.required, s <:+: T := by
…
```
Mentions: OAI.Superstring.Counts.Data
theorem OAI.Superstring.exists_two_approximation line 257
Source documentation
The approximation inequality, separated from computational implementation. This lemma is NOT the main theorem: a polynomial bit implementation is required.
```
theorem exists_two_approximation (S : Instance) :
    ∃ T : Word, IsCommonSuperstring S T ∧ T.length ≤ 2 * opt S := by
…
```
Mentions: OAI.Superstring.Instance, OAI.Superstring.Word, OAI.Superstring.IsCommonSuperstring, OAI.Superstring.opt