OAI/Computability/Superstring/Tables.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Superstring.Computable.stage_zero line 9
2. theorem OAI.Superstring.Computable.input_stage_bound line 20
3. def OAI.Superstring.Computable.stageTable line 28
4. theorem OAI.Superstring.Computable.lookup_stageTable line 31
5. def OAI.Superstring.Computable.rawCountStep line 40

   Source documentation

   Only finite materialized tables are passed between consecutive iterations.

   def rawCountStep (q : List (List α) × Table α) : List (List α) × Table α :=
   …

   Mentions: OAI.Superstring.Computable.Table

6. def OAI.Superstring.Computable.initialTable line 43
7. theorem OAI.Superstring.Computable.rawCountStep_stage line 45
8. theorem OAI.Superstring.Computable.iterate_rawCountStep line 58
9. def OAI.Superstring.Computable.countCap line 68

   Source documentation

   A proved polynomial workspace guard. The cap is part of the implemented loop; the mathematical bound proves it never fires on an actual input.

   def countCap (S : List (List α)) : ℕ :=
   …

10. def OAI.Superstring.Computable.countDepth line 71
11. def OAI.Superstring.Computable.computeCounts line 74
12. theorem OAI.Superstring.Computable.stageTable_size line 77
13. theorem OAI.Superstring.Computable.computeCounts_eq line 90
14. theorem OAI.Superstring.Computable.lookup_computeCounts line 99
15. theorem OAI.Superstring.Computable.poly_initialTable line 108
16. theorem OAI.Superstring.Computable.poly_rawCountStep line 112
17. theorem OAI.Superstring.Computable.poly_countCap line 117
18. theorem OAI.Superstring.Computable.poly_countDepth line 122
19. theorem OAI.Superstring.Computable.poly_computeCounts line 128
20. def OAI.Superstring.PrefixGreedy.Capacity line 139
21. theorem OAI.Superstring.PrefixGreedy.exists_supply line 143
22. theorem OAI.Superstring.PrefixGreedy.capacity_erase line 153

    Source documentation

    Deleting a longest request and any of its extensions preserves all subtree capacities.

    theorem capacity_erase {req : β → List α} {sup : γ → List α} {R : Finset β} {S : Finset γ}
        (h : Capacity req sup R S) {a : β} {b : γ} (ha : a ∈ R) (hb : b ∈ S)
        (hm : ∀ r ∈ R, (req r).length ≤ (req a).length) (hp : req a <+: sup b) :
        Capacity req sup (R.erase a) (S.erase b) := by
    …

    Mentions: OAI.Superstring.PrefixGreedy.Capacity

23. abbrev OAI.Superstring.PrefixGreedy.Token line 182
24. def OAI.Superstring.PrefixGreedy.prefer line 184
25. def OAI.Superstring.PrefixGreedy.largest line 186
26. theorem OAI.Superstring.PrefixGreedy.fold_prefer line 188
27. theorem OAI.Superstring.PrefixGreedy.largest_spec line 209
28. def OAI.Superstring.PrefixGreedy.prefixB line 221
29. def OAI.Superstring.PrefixGreedy.remove line 223
30. theorem OAI.Superstring.PrefixGreedy.mem_remove line 226
31. theorem OAI.Superstring.PrefixGreedy.toFinset_remove line 229
32. def OAI.Superstring.PrefixGreedy.extension line 233
33. theorem OAI.Superstring.PrefixGreedy.extension_spec line 236
34. abbrev OAI.Superstring.PrefixGreedy.State line 252
35. def OAI.Superstring.PrefixGreedy.step line 254
36. theorem OAI.Superstring.PrefixGreedy.remove_nodup line 265
37. theorem OAI.Superstring.PrefixGreedy.remove_perm line 268
38. theorem OAI.Superstring.PrefixGreedy.iterate_correct line 282

    Source documentation

    The explicit greedy loop returns a complete matching, with no search over permutations.

    theorem iterate_correct (n : ℕ) (R S : List (Token α)) (P : List (Token α × Token α))
        (hR : R.Nodup) (hS : S.Nodup) (hc : Capacity Prod.snd Prod.snd R.toFinset S.toFinset)
        (hlen : R.length = S.length) (hn : R.length ≤ n)
        (hP : ∀ p ∈ P, p.1.2 <+: p.2.2) :
        let q := step^[n] (R,S,P)
    …

    Mentions: OAI.Superstring.PrefixGreedy.Token, OAI.Superstring.PrefixGreedy.Capacity, OAI.Superstring.PrefixGreedy.step