OAI/Computability/WLIdentification/GraphEnumeration.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WLIdentification.NumericGraph.edge line 10

   Source documentation

   Row-major access, with a total default outside the matrix.

   def edge (n : ℕ) (W : Word) (i j : ℕ) : Bool := W[i*n+j]?.getD false

   Mentions: OAI.WLIdentification.Word

2. def OAI.WLIdentification.NumericGraph.simple line 12
3. def OAI.WLIdentification.NumericGraph.iso line 16
4. def OAI.WLIdentification.NumericGraph.mateEdge line 24

   Source documentation

   A canonically normalized mate: every simple graph occurs among these masks, while diagonal/asymmetric mask bits do not admit malformed graphs.

   def mateEdge (n mask i j : ℕ) : Bool :=
   …

5. def OAI.WLIdentification.NumericGraph.mate line 27
6. theorem OAI.WLIdentification.WordExpressions.BoolPoly.eqtest line 34
7. theorem OAI.WLIdentification.WordExpressions.BoolPoly.propEq line 41
8. theorem OAI.WLIdentification.NumericGraph.edge_poly line 52
9. theorem OAI.WLIdentification.NumericGraph.simple_poly line 57
10. theorem OAI.WLIdentification.NumericGraph.iso_poly line 66
11. theorem OAI.WLIdentification.NumericGraph.mateEdge_poly line 84
12. theorem OAI.WLIdentification.NumericGraph.mate_poly line 92
13. theorem OAI.WLIdentification.NumericGraph.rows_entry line 103

    Source documentation

    Entries of a rectangular row-major serialization.

    theorem rows_entry (n m : ℕ) (f : Fin n → Fin m → Bool) (i : Fin n) (j : Fin m) :
        (((List.ofFn fun a => List.ofFn (f a)).flatten)[i.val*m+j.val]?).getD false = f i j := by
    …

14. theorem OAI.WLIdentification.NumericGraph.edge_matrixWord line 118
15. theorem OAI.WLIdentification.NumericGraph.simple_true line 121
16. abbrev OAI.WLIdentification.NumericGraph.ofWord line 132
17. theorem OAI.WLIdentification.NumericGraph.simple_matrixWord line 138
18. def OAI.WLIdentification.NumericGraph.mateGraph line 142
19. theorem OAI.WLIdentification.NumericGraph.edge_mate line 148
20. def OAI.WLIdentification.NumericGraph.number line 157

    Source documentation

    Little-endian packing, used solely for proving exhaustive mask coverage.

    def number : Word → ℕ
      | [] => 0
      | b::w => Nat.bit b (number w)

    Mentions: OAI.WLIdentification.Word

21. theorem OAI.WLIdentification.NumericGraph.number_lt line 161
22. theorem OAI.WLIdentification.NumericGraph.testBit_number line 168
23. theorem OAI.WLIdentification.NumericGraph.mateGraph_covers line 177
24. theorem OAI.WLIdentification.NumericGraph.iso_correct line 192