OAI/Combinatorics/StripMass/StepComplete.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.GraphRealizes.boundary_used_iff line 16
  2. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_compatible line 36
  3. theorem OAI.CriticalStrip.Diagram.Pairing.cutGraph_profile_ne_none line 47
  4. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_iff line 59
  5. theorem OAI.CriticalStrip.Diagram.Pairing.stepWiring_out_used line 76
  6. def OAI.CriticalStrip.Diagram.Pairing.stepSupport line 96
  7. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_support line 99
  8. def OAI.CriticalStrip.Diagram.Graph.BoundaryEquiv.ofEquiv line 117
  9. abbrev OAI.CriticalStrip.Diagram.GateExterior line 134
  10. def OAI.CriticalStrip.Diagram.gateWiring line 136
  11. def OAI.CriticalStrip.Diagram.gateInput line 142
  12. def OAI.CriticalStrip.Diagram.stepVertexEquiv line 145
  13. theorem OAI.CriticalStrip.Diagram.gateInput_eq_box line 157
  14. theorem OAI.CriticalStrip.Diagram.gateInput_eq_out line 161
  15. theorem OAI.CriticalStrip.Diagram.Pairing.stepWiring_glued line 167
  16. def OAI.CriticalStrip.Diagram.Pairing.stepGluedEquiv line 186
  17. theorem OAI.CriticalStrip.Diagram.graph_gate_step_iff line 196
  18. def OAI.CriticalStrip.Diagram.Graph.DrainsBoundary line 213
  19. theorem OAI.CriticalStrip.Diagram.Graph.BoundaryEquiv.drains line 216
  20. theorem OAI.CriticalStrip.Diagram.Graph.BoundaryEquiv.drains_iff line 227
  21. theorem OAI.CriticalStrip.Diagram.Graph.drains_glued_exterior_iff line 231
  22. theorem OAI.CriticalStrip.Diagram.Graph.glued_drains_local line 245
  23. theorem OAI.CriticalStrip.Diagram.GraphRealizes.drainsBoundary line 258
  24. theorem OAI.CriticalStrip.Diagram.GraphRealizes.substitute_drains_iff line 264
  25. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_ne_none_of_drains line 274
  26. theorem OAI.CriticalStrip.Diagram.graph_gate_step_exists line 292
  27. structure OAI.CriticalStrip.Diagram.Gate line 310
  28. inductive OAI.CriticalStrip.Diagram.Circuit line 316
  29. def OAI.CriticalStrip.Diagram.Circuit.Vertex line 323
  30. def OAI.CriticalStrip.Diagram.Circuit.boundary line 327
  31. def OAI.CriticalStrip.Diagram.Circuit.support line 331
  32. def OAI.CriticalStrip.Diagram.Circuit.wiring line 336
  33. def OAI.CriticalStrip.Diagram.Circuit.Compatible line 341
  34. def OAI.CriticalStrip.Diagram.Circuit.eval line 347
  35. theorem OAI.CriticalStrip.Diagram.Circuit.eval_sound line 351
  36. theorem OAI.CriticalStrip.Diagram.Circuit.eval_exists line 382
  37. theorem OAI.CriticalStrip.Diagram.Circuit.eval_iff line 405
  38. structure OAI.CriticalStrip.Diagram.Position line 426
  39. def OAI.CriticalStrip.Diagram.Position.gate line 431
  40. def OAI.CriticalStrip.Diagram.optionMatrix line 434
  41. theorem OAI.CriticalStrip.Diagram.optionMatrix_mul line 437
  42. def OAI.CriticalStrip.Diagram.localR line 453
  43. inductive OAI.CriticalStrip.Diagram.Program line 456
  44. def OAI.CriticalStrip.Diagram.Program.Choices line 463
  45. instance OAI.CriticalStrip.Diagram.Program.choicesFinite line 467
  46. def OAI.CriticalStrip.Diagram.Program.circuit line 472
  47. def OAI.CriticalStrip.Diagram.Program.weight line 476
  48. def OAI.CriticalStrip.Diagram.Program.matrix line 480
  49. lemma OAI.CriticalStrip.Diagram.Program.matrix_expansion line 484
  50. lemma OAI.CriticalStrip.Diagram.Program.matrix_apply line 507