OAI/Computability/Superstring/ThreadSupport.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Superstring.ArrayPerm.Edges line 8
2. def OAI.Superstring.ArrayPerm.Valid line 10
3. def OAI.Superstring.ArrayPerm.next line 13
4. theorem OAI.Superstring.ArrayPerm.poly_next line 16
5. theorem OAI.Superstring.ArrayPerm.next_mem line 22
6. theorem OAI.Superstring.ArrayPerm.next_lt line 44
7. theorem OAI.Superstring.ArrayPerm.next_injective line 48
8. def OAI.Superstring.ArrayPerm.perm line 54
9. theorem OAI.Superstring.ArrayPerm.perm_apply line 61
10. theorem OAI.Superstring.ArrayPerm.next_size line 65
11. def OAI.Superstring.ArrayPerm.advance line 84
12. theorem OAI.Superstring.ArrayPerm.poly_advance line 86
13. theorem OAI.Superstring.ArrayPerm.iterate_advance line 88
14. theorem OAI.Superstring.ArrayPerm.poly_iterate_advance line 94
15. def OAI.Superstring.ArrayPerm.power line 108
16. theorem OAI.Superstring.ArrayPerm.poly_power line 110
17. theorem OAI.Superstring.ArrayPerm.power_perm line 114
18. theorem OAI.Superstring.ArrayPerm.power_lt line 123
19. theorem OAI.Superstring.Computable.poly_replicate line 133
20. def OAI.Superstring.Computable.indexed line 138
21. theorem OAI.Superstring.Computable.poly_indexed line 141
22. theorem OAI.Superstring.Computable.indexed_fst line 148
23. theorem OAI.Superstring.Computable.indexed_snd line 153
24. theorem OAI.Superstring.Computable.indexed_nodup line 161
25. theorem OAI.Superstring.Computable.mem_indexed line 165
26. def OAI.Superstring.Computable.downValue line 177
27. theorem OAI.Superstring.Computable.poly_downValue line 180
28. theorem OAI.Superstring.Computable.downValue_eq line 184
29. def OAI.Superstring.Computable.downWords line 202
30. theorem OAI.Superstring.Computable.poly_downWords line 205
31. theorem OAI.Superstring.Computable.downWords_count line 211
32. def OAI.Superstring.Computable.requests line 221
33. theorem OAI.Superstring.Computable.poly_requests line 225
34. theorem OAI.Superstring.Computable.requests_fst line 230
35. theorem OAI.Superstring.Computable.requests_snd line 235
36. theorem OAI.Superstring.Computable.requests_nodup line 241
37. theorem OAI.Superstring.Computable.down_capacity line 244
38. def OAI.Superstring.Computable.computePairs line 263
39. theorem OAI.Superstring.Computable.poly_computePairs line 266
40. theorem OAI.Superstring.Computable.computePairs_correct line 270
41. theorem OAI.Superstring.Computable.downWords_mem line 277
42. theorem OAI.Superstring.Computable.downWords_length line 296
43. theorem OAI.Superstring.Computable.mem_requests line 308
44. def OAI.Superstring.Computable.edges line 319
45. theorem OAI.Superstring.Computable.poly_edges line 322
46. theorem OAI.Superstring.Computable.edges_valid line 326
47. theorem OAI.Superstring.Computable.edge_follows line 336
48. def OAI.Superstring.Computable.arrayThreading line 352

    Source documentation

    The actual polynomially computed greedy matching, used as a mathematical threading. Only its finite inverse proof is noncomputable; the forward table is code.

    noncomputable def arrayThreading (S : List (List α)) :
        Hierarchical.Threading ((Input.data S).vertices : Set (List α)) (Fin (downWords S).length) where
    …

    Mentions: OAI.Superstring.Hierarchical.Threading, OAI.Superstring.Input.data, OAI.Superstring.Computable.vertices, OAI.Superstring.Computable.downWords

49. theorem OAI.Superstring.Computable.countP_sum line 363
50. theorem OAI.Superstring.Computable.card_get_filter line 370
51. theorem OAI.Superstring.Computable.arrayThreading_histogram line 374
52. theorem OAI.Superstring.Computable.arrayThreading_recorded_count line 380
53. theorem OAI.Superstring.Computable.arrayThreading_budget line 388
54. theorem OAI.Superstring.Hierarchical.Threading.short_text_period line 401

    Source documentation

    A single orbit, not the (potentially exponentially large) order of the whole permutation, bounds each stored primitive phase word.

    theorem short_text_period (C : Threading V ι) (i : ι) :
        ∃ p : ℕ, 0 < p ∧ p ≤ Fintype.card ι ∧ Function.Periodic (C.text i) (p : ℤ) := by
    …

    Mentions: OAI.Superstring.Hierarchical.Threading

55. theorem OAI.Superstring.Hierarchical.Threading.primitive_le_card line 411
56. def OAI.Superstring.Hierarchical.Threading.finiteKey line 416
57. theorem OAI.Superstring.Hierarchical.Threading.length_finiteKey line 419
58. theorem OAI.Superstring.Hierarchical.Threading.finiteKey_get line 424
59. theorem OAI.Superstring.Hierarchical.Threading.finiteKey_eq_iff line 430
60. theorem OAI.Superstring.Hierarchical.Threading.sameText_bounded line 446
61. abbrev OAI.Superstring.ThreadArray.Code line 478
62. structure OAI.Superstring.ThreadArray.Represents line 481

    Source documentation

    Finite array semantics: no periodic/oracle tests are hidden in the code.

    structure Represents {V : Set (List α)} (K : Code α)
        (C : Threading V (Fin K.1.length)) : Prop where
    …

    Mentions: OAI.Superstring.ThreadArray.Code

63. def OAI.Superstring.ThreadArray.key line 486
64. theorem OAI.Superstring.ThreadArray.poly_key line 491
65. theorem OAI.Superstring.ThreadArray.power_eq line 503
66. theorem OAI.Superstring.ThreadArray.key_eq line 514
67. def OAI.Superstring.ThreadArray.compatible line 532
68. theorem OAI.Superstring.ThreadArray.poly_compatible line 535
69. theorem OAI.Superstring.ThreadArray.compatible_eq line 543
70. def OAI.Superstring.ThreadArray.first line 554

    Source documentation

    A bounded first-admissible search. Its proof gives both success and order; it does not assume a choice primitive in the computational model.

    def first (n : ℕ) (P : ℕ → Bool) : ℕ := ((List.range n).filter P).headD 0
    …

71. theorem OAI.Superstring.ThreadArray.first_spec line 557
72. def OAI.Superstring.ThreadArray.period line 583
73. theorem OAI.Superstring.ThreadArray.poly_period line 586
74. theorem OAI.Superstring.ThreadArray.test_period line 594
75. theorem OAI.Superstring.ThreadArray.period_spec line 603
76. theorem OAI.Superstring.BitCode.Poly.div line 628