OAI/Computability/WLIdentification/DimensionDecider.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.DimensionDecider.matrix line 9
  2. def OAI.WLIdentification.DimensionDecider.bits line 10
  3. def OAI.WLIdentification.DimensionDecider.valid line 11
  4. def OAI.WLIdentification.DimensionDecider.identifies line 15
  5. def OAI.WLIdentification.DimensionDecider.atOrder line 20
  6. def OAI.WLIdentification.DimensionDecider.decideWord line 24
  7. def OAI.WLIdentification.DimensionDecider.budget line 27
  8. theorem OAI.WLIdentification.NumericGraph.ofWord_matrixWord line 33
  9. theorem OAI.WLIdentification.NumericGraph.mate_simple line 38
  10. theorem OAI.WLIdentification.NumericGraph.ofWord_mate line 44
  11. theorem OAI.WLIdentification.NumericGraph.matrixWord_ofWord line 48
  12. theorem OAI.WLIdentification.equivalent_order line 65

    Source documentation

    Positive-dimensional equivalence always fixes the order, even for the ordinary-neighbor dimension-one convention.

    theorem equivalent_order {G H : Graph} {k : ℕ} (hk : 0<k) (h : Equivalent k G H) : G.order=H.order := by
…

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Equivalent

  13. theorem OAI.WLIdentification.identifies_iff_masks line 75

    Source documentation

    Exhaustive masks suffice for all mates because order equality is proved, not inserted as an extra hypothesis in identification.

    theorem identifies_iff_masks (G : Graph) (k : ℕ) (hk : 0<k) : Identifies k G ↔
    ∀ x<2^(G.order*G.order), Equivalent k G (NumericGraph.mateGraph G.order x) →
      Isomorphic G (NumericGraph.mateGraph G.order x) := by
…

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Identifies, OAI.WLIdentification.Equivalent, OAI.WLIdentification.NumericGraph.mateGraph, OAI.WLIdentification.Isomorphic

  14. theorem OAI.WLIdentification.DimensionDecider.valid_iff line 97
  15. theorem OAI.WLIdentification.DimensionDecider.binaryValue_leading_pos line 108
  16. theorem OAI.WLIdentification.DimensionDecider.input_valid line 118
  17. theorem OAI.WLIdentification.DimensionDecider.input_extract line 132
  18. theorem OAI.WLIdentification.DimensionDecider.reconstruct line 140
  19. theorem OAI.WLIdentification.DimensionDecider.budget_bounds line 156
  20. theorem OAI.WLIdentification.NumericWL.equivalent_correct line 200
  21. theorem OAI.WLIdentification.DimensionDecider.identifies_correct line 211
  22. theorem OAI.WLIdentification.DimensionDecider.capped_identifies line 226
  23. theorem OAI.WLIdentification.DimensionDecider.decideWord_correct line 233
  24. theorem OAI.WLIdentification.DimensionDecider.matrix_poly line 266
  25. theorem OAI.WLIdentification.DimensionDecider.bits_poly line 270
  26. theorem OAI.WLIdentification.DimensionDecider.valid_poly line 274
  27. theorem OAI.WLIdentification.DimensionDecider.identifies_poly line 282
  28. theorem OAI.WLIdentification.DimensionDecider.identifies_poly_of line 301
  29. theorem OAI.WLIdentification.DimensionDecider.atOrder_poly line 308
  30. theorem OAI.WLIdentification.DimensionDecider.decideWord_poly line 314
  31. theorem OAI.WLIdentification.dimensionLanguage_inEXPTIME line 322

    Source documentation

    Membership for the literal parser, all-mates identification, and finite-alphabet tape model.

    theorem dimensionLanguage_inEXPTIME : InEXPTIME dimensionLanguage := by
…

    Mentions: OAI.WLIdentification.InEXPTIME, OAI.WLIdentification.dimensionLanguage