OAI/Combinatorics/HoneycombCorridor/Basic.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PolynomialVacuumBridge.Corridor.Vertex line 9

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:7 (same declaration text).

  2. def OAI.PolynomialVacuumBridge.Corridor.position line 14

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:12 (same declaration text).

  3. def OAI.PolynomialVacuumBridge.Corridor.adjacent line 20

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:18 (same declaration text).

  4. def OAI.PolynomialVacuumBridge.Corridor.criticalActivity line 27

    Also declared: ComparatorChallenges/HoneycombBridgeFiniteness.lean:25 (same declaration text).

  5. def OAI.PolynomialVacuumBridge.Corridor.neighbor line 29
  6. abbrev OAI.PolynomialVacuumBridge.Corridor.Germ line 36
  7. def OAI.PolynomialVacuumBridge.Corridor.outgoingSlot line 38
  8. def OAI.PolynomialVacuumBridge.Corridor.advance line 41
  9. def OAI.PolynomialVacuumBridge.Corridor.Stopped line 44
  10. def OAI.PolynomialVacuumBridge.Corridor.leaves line 48
  11. def OAI.PolynomialVacuumBridge.Corridor.turnAngle line 56
  12. def OAI.PolynomialVacuumBridge.Corridor.stepWeight line 59
  13. def OAI.PolynomialVacuumBridge.Corridor.wordWeight line 62
  14. def OAI.PolynomialVacuumBridge.Corridor.traced line 64
  15. def OAI.PolynomialVacuumBridge.Corridor.terminalGerm line 68
  16. def OAI.PolynomialVacuumBridge.Corridor.explorationTotal line 72
  17. theorem OAI.PolynomialVacuumBridge.Corridor.neighbor_neighbor line 75
  18. theorem OAI.PolynomialVacuumBridge.Corridor.adjacent_neighbor line 79
  19. theorem OAI.PolynomialVacuumBridge.Corridor.neighbor_injective line 82
  20. theorem OAI.PolynomialVacuumBridge.Corridor.advance_adjacent line 86
  21. theorem OAI.PolynomialVacuumBridge.Corridor.advance_not_backtracking line 89
  22. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_nil line 96
  23. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_cons line 97
  24. theorem OAI.PolynomialVacuumBridge.Corridor.critical_cos_pos line 100
  25. theorem OAI.PolynomialVacuumBridge.Corridor.stepWeight_sum line 104
  26. theorem OAI.PolynomialVacuumBridge.Corridor.mem_leaves_iff line 121
  27. theorem OAI.PolynomialVacuumBridge.Corridor.stopped_traced line 133
  28. theorem OAI.PolynomialVacuumBridge.Corridor.traced_length line 152
  29. theorem OAI.PolynomialVacuumBridge.Corridor.trace_chain line 157
  30. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_physical line 168
  31. theorem OAI.PolynomialVacuumBridge.Corridor.sum_cons_image line 179
  32. theorem OAI.PolynomialVacuumBridge.Corridor.disjoint_cons_images line 187
  33. theorem OAI.PolynomialVacuumBridge.Corridor.leaf_balance line 195
  34. theorem OAI.PolynomialVacuumBridge.Corridor.visit_exploration_balance line 208
  35. def OAI.PolynomialVacuumBridge.Corridor.complexPosition line 212
  36. theorem OAI.PolynomialVacuumBridge.Corridor.exp_turnAngle line 215
  37. theorem OAI.PolynomialVacuumBridge.Corridor.advance_rotation line 223