Distribution.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Superstring.Hierarchical.LayerCollection.Child line 10
def OAI.Superstring.Hierarchical.LayerCollection.Child.ids line 23
def OAI.Superstring.Hierarchical.LayerCollection.Child.budget line 25
theorem OAI.Superstring.Hierarchical.LayerCollection.Child.later line 27
def OAI.Superstring.Hierarchical.LayerCollection.Child.hosted line 37
def OAI.Superstring.Hierarchical.LayerCollection.Child.request line 57
theorem OAI.Superstring.Hierarchical.LayerCollection.Child.hosted_different line 75

theorem OAI.Superstring.Hierarchical.LayerCollection.fulfill line 92

Source documentation

A nonempty collection of actual child groups can be fulfilled together. The reserve includes the original turn of every requesting layer and of the recipient. No other layer of the recipient group is charged or rooted here.

theorem fulfill {ι : Type} [Fintype ι] [Nonempty ι]
    (closed : SubstringClosed V) (d : C.Id) (R : ι → C.Child d)
    (distinct : Function.Injective (fun i => (R i).source)) :
    ∃ Q : Path V [] [], Q.cost ≤ 2 * C.period d.1 + 2 * ∑ i, (R i).budget ∧
      (∀ w ∈ (C.layerAt d).Content, Q.Visits w) ∧
      ∀ j i, i ∈ (R j).members → ∀ w ∈ (C.layer (R j).source i).Content, Q.Visits w := by
…

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

theorem OAI.Superstring.Hierarchical.combine_rooted line 145
Source documentation
Concatenate a finite family of rooted closed walks, preserving every visit and charging at most their sum. Abstracted only to avoid repeated splices.
```
theorem combine_rooted {α ι : Type} {V : Set (List α)} (he : [] ∈ V)
    (F : ι → Path V [] []) (I : Finset ι) :
    ∃ Q : Path V [] [], Q.cost ≤ ∑ i ∈ I, (F i).cost ∧
      ∀ i ∈ I, ∀ w, (F i).Visits w → Q.Visits w := by
…
```
Mentions: OAI.Superstring.Hierarchical.Path
theorem OAI.Superstring.Hierarchical.LayerCollection.empty_mem line 158
theorem OAI.Superstring.Hierarchical.LayerCollection.root_short line 161
theorem OAI.Superstring.Hierarchical.Processing.below_stopped line 188
Source documentation
Once the cardinality test stops, every layer strictly below the top k has last end strictly below the tested threshold.
```
theorem below_stopped {m : ℕ} (z : Fin m → ℤ) (hz : Monotone z) (H : ℤ) (p k : ℕ)
    (hstop : (qualifying z H p k).card ≤ k) (i : Fin m) (hi : i.val < m - k) :
    z i < H - (k * p : ℕ) := by
…
```
Mentions: OAI.Superstring.Hierarchical.Processing.qualifying
theorem OAI.Superstring.Hierarchical.LayerCollection.distribute_individuals line 207

theorem OAI.Superstring.Hierarchical.LayerCollection.distribute_record line 294

Source documentation

The hard-case distribution, using the ONE record already forced by the count rule. Collective and uncollected individual budgets are disjoint.

theorem distribute_record (closed : SubstringClosed V) (g : G)
    (I : Finset (Fin (C.size g))) (k : ℕ) (hk : 0 < k) (hkm : k ≤ C.size g)
    (hI : ∀ i : Fin (C.size g), C.size g - k ≤ i.val → i ∈ I)
    (d : C.Id) (R : (C.layerAt d).Record (C.text g))
    (foreign : C.text g ≠ fun x => C.text d.1 (x + R.offset))
    (hat : R.start ≤ C.distinguished g) (htb : C.distinguished g < R.stop)
    (hb : (C.layer g ⟨C.size g - 1, by have := C.nonempty g; omega⟩).first (C.distinguished g)
…

Mentions: OAI.Superstring.Hierarchical.SubstringClosed

def OAI.Superstring.Hierarchical.Threading.collection line 384
Source documentation
The finite ordered collection is the actual sorted base decomposition, not an arbitrary family substituted for its multiplicities.
```
noncomputable def collection (T : Threading V ι) (closed : SubstringClosed V) :
    LayerCollection V T.Groups where
…
```
Mentions: OAI.Superstring.Hierarchical.Threading, OAI.Superstring.Hierarchical.SubstringClosed, OAI.Superstring.Hierarchical.LayerCollection
def OAI.Superstring.Hierarchical.LayerCollection.RecordSupply line 407
theorem OAI.Superstring.Counts.Data.collection_records line 422