OAI/Computability/FiniteCompiler/Quotients.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

Canonical compiler quotients and effective tested classes for word problems.

  1. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.Alphabet line 17
  2. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.mem_alphabet line 19
  3. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_ne_nil line 23
  4. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.disjoint_infix line 27
  5. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.disjoint_overlap line 32
  6. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table_support line 46
  7. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table_decrease line 53
  8. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table_bounded line 69
  9. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.critical_containment_bound line 82
  10. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.critical_overlap_bound line 95
  11. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.absorption line 122
  12. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.mem_absorption line 126
  13. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.table line 132
  14. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.mem_table line 137
  15. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.absorbs line 144
  16. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.preserves_zero line 153
  17. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.critical line 164

    Source documentation

    All static and absorption critical pairs for the literal two-code base table.

    theorem critical (hC : z ∉ C.Alphabet) (hD : z ∉ D.Alphabet)
    (hdis : Disjoint C.Alphabet D.Alphabet) {n : ℕ}
    (hf : f [] ≠ none) (hg : g [] ≠ none)
    (hfc : Static.Contextual f (n/(C.width+1))) (hfi : Static.ZeroIdeal f (n/(C.width+1)))
    (hgc : Static.Contextual g (n/(D.width+1))) (hgi : Static.ZeroIdeal g (n/(D.width+1))) :
    Critical (table C D wf wg f g z n) n := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.Contextual, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.ZeroIdeal, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Critical, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.table

  18. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.steps_bounded line 230
  19. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.tableNormal line 239

    Source documentation

    The actual partial table-first procedure used at the fixed point.

    def tableNormal (T : ℕ → Part (List (List S × List S))) (w : List S) : Part (List S) :=
…
  20. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.GoodTable line 244

    Source documentation

    A successful table has all the finite mathematical certificates needed by the bounded Newman argument. No totality of the program is part of this.

    def GoodTable (T : ℕ → Part (List (List S × List S))) (n : ℕ) : Prop :=
…
  21. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.tableNormal_at line 247
  22. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.tableNormal_budget line 271

    Source documentation

    This is the whole contextual-induction step, including the table at the shortened contextual endpoint and irreducibility in the larger table.

    theorem tableNormal_budget {T : ℕ → Part (List (List S × List S))} {n : ℕ}
    (wf : WellFounded r) (ht : ∀ k ≤ n,GoodTable (r:=r) T k)
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.GoodTable

  23. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.bootstrap_length_induction line 300

    Source documentation

    The source's simultaneous length induction, for the table builder actually fed to the recursion theorem. build only receives strictly smaller budgets. Thus this lemma never assumes the desired total/contextual program outright.

    theorem bootstrap_length_induction (wf : WellFounded r)
    (T : ℕ → Part (List (List S × List S))) (f : List S → Part (List S))
    (fixed : f=tableNormal T)
    (stable : ∀ k n, k ≤ n → ∀ rk ∈ T k,∀ rn ∈ T n,Selectors.BoundedEq rk rn k)
    (build : ∀ n, (∀ m<n,Compiler.PartialBudget f m) → GoodTable (r:=r) T n) :
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.tableNormal, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.BoundedEq, OAI.FiniteAlgebraicEnvelopes.Compiler.PartialBudget, OAI.FiniteAlgebraicEnvelopes.Bootstrap.GoodTable

  24. theorem OAI.FiniteAlgebraicEnvelopes.Effect.traverse_comp line 326
  25. theorem OAI.FiniteAlgebraicEnvelopes.Effect.traverse_domain line 332
  26. theorem OAI.FiniteAlgebraicEnvelopes.Effect.partrec_traverse_parameter line 345
  27. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.value line 359
  28. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.value_mem line 364
  29. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.compute_domain line 371
  30. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.compute_eq line 383
  31. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Search.partrec_compute_parameter line 390
  32. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.bases line 409
  33. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables line 414
  34. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.bases_eq line 422
  35. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables_eq line 431
  36. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.partrec_bases_parameter line 443
  37. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.partrec_tables_parameter line 458
  38. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.partrec_tableNormal_parameter line 468
  39. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.bounded line 489
  40. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.decrease line 497
  41. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.shapes line 510
  42. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.bases_full line 538
  43. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables_full line 548
  44. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.stable line 557
  45. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.good line 568
  46. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.Rel line 607

    Source documentation

    Literal equations of the stabilized infinite table. Restricting a stage to its own budget removes only premature copies of the fixed absorption rules.

    def Rel (u v : FreeMonoid S) : Prop :=
…
  47. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.Mon line 610
  48. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present line 611
  49. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal line 612
  50. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_nil line 615
  51. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_append line 617
  52. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_step line 620
  53. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_steps line 630
  54. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.budget line 642
  55. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_mem line 645
  56. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_normal line 648
  57. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_context line 654
  58. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_append line 659
  59. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_rel line 666
  60. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normalCon line 684
  61. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_eq_iff line 694
  62. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.computable_normal line 703
  63. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.computable_wordProblem line 711
  64. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_mono line 726
  65. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.selected_mem line 734
  66. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_irreducible line 753
  67. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_idempotent line 760
  68. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_eq_self line 763
  69. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_surjective line 770
  70. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.representative line 775
  71. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_representative line 778
  72. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.representative_injective line 782
  73. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.representative_irreducible line 786
  74. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.irreducible_of_short line 793
  75. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_nil_ne_zero line 802
  76. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_absorbs line 817
  77. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.monoidWithZero line 834
  78. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.representative_avoids_zero line 845
  79. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.tuple_selected line 860

    Source documentation

    Every nonzero irreducible ordered tuple receives its literal selector. The finite processing stage is chosen beyond the complete selector word.

    theorem tuple_selected (a : Markers S) (T : ℕ → Part (List (List S × List S)))
    (bases : ℕ → List (List S × List S))
    (hT : ∀ n,process (a:=a) (bases n) (stages a.zero) n n ∈ T n)
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stages

  80. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.selectors line 913

    Source documentation

    Source selectors for the stabilized quotient, with the distinguished element first in the tuple. Not an extra algebraic assumption on that quotient.

    theorem selectors (a : Selectors.Markers S) (bases : ℕ → List (List S × List S))
    (hT : ∀ n,Selectors.process (a:=a) (bases n) (Selectors.stages a.zero) n n∈T n)
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stages

  81. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table_short line 977
  82. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables_absorb line 997
  83. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables_short line 1009
  84. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables_process line 1028

    Source documentation

    Once bounded induction has proved total tables, their process descriptions are genuine members. No totality of static programs is added here.

    theorem tables_process {t : S → S → Prop}
    (good : ∀ n,GoodTable (r:=t) (tables (r:=r) (s:=s) a C D f g) n) (n : ℕ) :
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.good, OAI.FiniteAlgebraicEnvelopes.Bootstrap.GoodTable, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables

  85. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_surjective line 1048
  86. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_zero_mul line 1055
  87. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_mul_zero line 1069
  88. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.monoidWithZero line 1081
  89. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.computable_normal line 1097
  90. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.computable_wordProblem line 1102
  91. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.representative_mul line 1124
  92. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.rawMap line 1139
  93. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.rawMap_injective line 1156
  94. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.rawMap_ne_one line 1167
  95. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.rawMap_ne_zero line 1178
  96. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.irreducible_of_no_infix line 1198
  97. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table_mono line 1210
  98. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.canonical_no_infix line 1216
  99. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.canonical_irreducible line 1241

    Source documentation

    Rules of the other code and selector/zero rules cannot occur in a pure code.

    theorem canonical_irreducible {rs : List (List S × List S)} {n : ℕ}
    (hiso : ∀ p∈rs,p∈table C wf q z n ∨ ∃ s∈p.1,s∉C.Alphabet)
    (hc : ∀ k,Contextual q k) (hi : ∀ k,ZeroIdeal q k)
    {w : List A} (hw : q w≠none) :
    Irreducible (Step rs) (C.encode (Canonical.least wf q w)) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.Contextual, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.ZeroIdeal, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Irreducible, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Step, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least

  100. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.output_eq_iff line 1252
  101. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_encode line 1289
  102. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_encode_iff line 1307
  103. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.isolate_left line 1324
  104. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_isolate line 1338
  105. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables_isolate line 1364
  106. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables_static line 1376
  107. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.codeHom line 1390
  108. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.descendCode line 1399
  109. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.descendCode_apply line 1413
  110. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.descendCode_injective line 1418
  111. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Separator.prefix_before line 1429
  112. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Separator.infix_split line 1447
  113. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Separator.split_injective line 1462
  114. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.separator_irreducible line 1489
  115. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.separator_literal_injective line 1511
  116. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Base.isolate_separator line 1535
  117. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_isolate_separator line 1551
  118. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Build.tables_isolate_separator line 1577
  119. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.normal_separator line 1606
  120. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_separator_iff line 1629
  121. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present_separator_ne_zero line 1642
  122. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.words line 1667

    Source documentation

    The finite word ball over an explicit finite support.

    def words (letters : List A) : ℕ → List (List A)
  | 0 => [[]]
  | n+1 => [] :: letters.flatMap (fun a => (words letters n).map (a::·))
  123. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.mem_words line 1671
  124. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.words_map line 1693
  125. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.words_specialize line 1700
  126. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.primrec_words line 1703
  127. theorem OAI.FiniteAlgebraicEnvelopes.Effect.computable_map_parameter line 1718

    Source documentation

    Finite traversal of a total computable family is a computable list map.

    theorem computable_map_parameter {f : X → A → B} (hf : Computable₂ f) :
    Computable₂ (fun x (l : List A) => l.map (f x)) := by
…
  128. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.computable_least line 1732

    Source documentation

    Canonical representatives do not require a coding of the semantic class type. Only its word-equivalence test must be algorithmic.

    theorem computable_least (hr : PrimrecRel (List.Shortlex r))
    (hq : ComputablePred (fun p : List A × List A => q p.1=q p.2)) : Computable (least wf q) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least

  129. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_eq_iff line 1768

    Source documentation

    Equality of computed representatives is exactly equality in the semantic quotient, not merely equality of a chosen noncanonical encoding.

    theorem least_eq_iff {u v : List A} : least wf q u=least wf q v ↔ q u=q v := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least

  130. theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.computable_word_equiv line 1780

    Source documentation

    The original word-problem algorithm gives a genuine two-word comparison.

    theorem computable_word_equiv (h : ComputablePred (fun w : Word n => evalWord s w=1)) :
    ComputablePred (fun p : Word n × Word n => evalWord s p.1=evalWord s p.2) := by
…
  131. def OAI.FiniteAlgebraicEnvelopes.WordProblem.letterRel line 1794
  132. theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.letterRel_wf line 1803
  133. theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.primrec_letterShortlex line 1805
  134. def OAI.FiniteAlgebraicEnvelopes.WordProblem.testedClass line 1810
  135. theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.computable_testedClass line 1813
  136. theorem OAI.FiniteAlgebraicEnvelopes.WordProblem.testedClass_eq_iff line 1819