OAI/Computability/Superstring/Attachments.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Superstring.Hierarchical.LayerCollection.attach_layer line 11

    Source documentation

    Complete one touched base layer and splice it into the rooted walk. Only this layer's base turn and its one geometric connection are charged.

    theorem attach_layer (closed : SubstringClosed V) (g : G) (i : Fin (C.size g))
    (P : Path V [] []) (F : Loop V) (hcF : F.cost ≤ C.period g)
    (ht : (C.layer g i).TouchedBy F.path) (hmeet : (Loop.mk [] P).Meets F) :
    ∃ Q : Path V [] [], Q.cost ≤ P.cost + 2 * C.period g ∧
      (∀ w, P.Visits w → Q.Visits w) ∧
      ∀ w ∈ (C.layer g i).Content, Q.Visits w := by
…

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

  2. theorem OAI.Superstring.Hierarchical.LayerCollection.root_below line 29

    Source documentation

    Root each as-yet-unspent layer below the chosen recipient baseline. The baseline itself is already fully retained by the incoming-request operation.

    theorem root_below (closed : SubstringClosed V) (g : G) (base : Fin (C.size g))
    (P : Path V [] []) (hp : ∀ w ∈ (C.layer g base).Content, P.Visits w)
    (a b : ℤ) (hbf : (C.layer g base).first a ≤ b)
    (hbl : b ≤ (C.layer g base).last a) (hlen : b - a < 2 * C.period g)
    (I : Finset (Fin (C.size g))) (hbelow : ∀ i ∈ I, i ≤ base) :
    ∃ Q : Path V [] [], Q.cost ≤ P.cost + 2 * (I.card * C.period g) ∧
      (∀ w, P.Visits w → Q.Visits w) ∧
      ∀ i ∈ I, ∀ w ∈ (C.layer g i).Content, Q.Visits w := by
…

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

  3. theorem OAI.Superstring.Hierarchical.LayerCollection.root_upper_budget line 61

    Source documentation

    Easy upper round-trip branch, including all upper base turns.

    theorem root_upper_budget (closed : SubstringClosed V) (g : G)
    (I : Finset (Fin (C.size g))) (top : Fin (C.size g))
    (hupper : ∀ i ∈ I, i ≤ top) (t : ℤ)
    (hcost : (C.layer g top).first t - t ≤ (I.card * C.period g : ℕ)) :
    ∃ Q : Path V [] [], Q.cost ≤ 2 * (I.card * C.period g) ∧
      ∀ i ∈ I, ∀ w ∈ (C.layer g i).Content, Q.Visits w := by
…

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

  4. theorem OAI.Superstring.Hierarchical.LayerCollection.attach_upper_band line 88

    Source documentation

    Easy upper band branch, paid only by upper layers, not by the already rooted baseline's budget.

    theorem attach_upper_band (closed : SubstringClosed V) (g : G)
    (I : Finset (Fin (C.size g))) (base top : Fin (C.size g))
    (horder : ∀ i ∈ I, base ≤ i ∧ i ≤ top) (hbt : base ≤ top)
    (P : Path V [] []) (hp : ∀ w ∈ (C.layer g base).Content, P.Visits w) (t : ℤ)
    (hband : (C.layer g top).first t - (C.layer g base).last t ≤ (I.card * C.period g : ℕ)) :
    ∃ Q : Path V [] [], Q.cost ≤ P.cost + 2 * (I.card * C.period g) ∧
      (∀ w, P.Visits w → Q.Visits w) ∧
      ∀ i ∈ I, ∀ w ∈ (C.layer g i).Content, Q.Visits w := by
…

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

  5. abbrev OAI.Superstring.Hierarchical.LayerCollection.Pending line 131
  6. def OAI.Superstring.Hierarchical.LayerCollection.Pending.source line 135
  7. def OAI.Superstring.Hierarchical.LayerCollection.Pending.ids line 136
  8. def OAI.Superstring.Hierarchical.LayerCollection.Pending.reserve line 137
  9. theorem OAI.Superstring.Hierarchical.LayerCollection.Pending.later line 139
  10. theorem OAI.Superstring.Hierarchical.LayerCollection.Pending.same line 141
  11. def OAI.Superstring.Hierarchical.LayerCollection.upper line 145
  12. theorem OAI.Superstring.Hierarchical.LayerCollection.mem_upper line 148
  13. theorem OAI.Superstring.Hierarchical.LayerCollection.card_upper line 151
  14. def OAI.Superstring.Hierarchical.LayerCollection.Covered line 167
  15. theorem OAI.Superstring.Hierarchical.LayerCollection.complete_upper line 174

    Source documentation

    Complete exactly the unspent upper interval. The failed count test is resolved by the proved record supply, not taken as a plan oracle.

    theorem complete_upper (closed : SubstringClosed V) (supply : C.RecordSupply)
    (g : G) (cut : ℕ) (hcut : cut ≤ C.size g) (P : Path V [] [])
    (hp : ∀ i : Fin (C.size g), i.val < cut →
      ∀ w ∈ (C.layer g i).Content, P.Visits w) :
    ∃ (Q : Path V [] []) (B : Finset C.PlannedBlock) (R : Finset C.Pending),
      Q.cost + (∑ b ∈ B, b.reserve) + (∑ r ∈ R, r.reserve) ≤
        P.cost + 2 * ((C.size g - cut) * C.period g) ∧
      (∀ w, P.Visits w → Q.Visits w) ∧
      (∀ i ∈ C.upper g cut, C.Covered Q B R ⟨g, i⟩) ∧
      (∀ r ∈ R, r.source = g) ∧ R.card ≤ 1 := by
…

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

  16. def OAI.Superstring.Hierarchical.LayerCollection.Pending.onTarget line 307
  17. theorem OAI.Superstring.Hierarchical.LayerCollection.Pending.at_source line 309
  18. theorem OAI.Superstring.Hierarchical.LayerCollection.Pending.at_budget line 313
  19. theorem OAI.Superstring.Hierarchical.LayerCollection.Pending.at_ids line 317
  20. theorem OAI.Superstring.Hierarchical.LayerCollection.fulfill_fibre line 324

    Source documentation

    Fulfill precisely the pending requests on one fixed recipient.

    theorem fulfill_fibre (closed : SubstringClosed V) (d : C.Id) (R : Finset C.Pending)
    (hne : R.Nonempty) (ht : ∀ r ∈ R, r.1 = d)
    (distinct : Set.InjOn Pending.source (R : Set C.Pending)) :
    ∃ Q : Path V [] [], Q.cost ≤ 2 * C.period d.1 + ∑ r ∈ R, r.reserve ∧
      (∀ w ∈ (C.layerAt d).Content, Q.Visits w) ∧
      ∀ r ∈ R, ∀ i ∈ r.ids, ∀ w ∈ (C.layerAt i).Content, Q.Visits w := by
…

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

  21. theorem OAI.Superstring.Hierarchical.LayerCollection.fulfill_all line 352