OAI/Combinatorics/PolynomialVacuum/Bridge/PrimitiveCounterexample.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzagVertices line 9
  2. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.upperZigzagWord line 13
  3. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzagWord line 17
  4. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.column line 21
  5. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_bounds line 25
  6. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_nodup line 37
  7. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_first line 48
  8. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_last_up line 50
  9. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_step_up2 line 58
  10. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_step_up0 line 60
  11. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_step_down_false line 62
  12. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_step_down_true line 64
  13. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.upperZigzag_trace line 67
  14. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_trace line 78
  15. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag line 89
  16. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.height_one_primitive line 102
  17. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_primitive line 116
  18. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.CylinderSafe line 118
  19. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.zigzag_unsafe line 121