OAI/Combinatorics/StripMass/VacuumClosure.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.Graph.closure_drains_local line 13
  2. def OAI.CriticalStrip.Diagram.Pairing.join line 31
  3. instance OAI.CriticalStrip.Diagram.Pairing.join_symm line 33
  4. def OAI.CriticalStrip.Diagram.Pairing.GluesAt line 38
  5. lemma OAI.CriticalStrip.Diagram.Pairing.GluesAt.symm line 41
  6. lemma OAI.CriticalStrip.Diagram.GraphRealizes.closure_reach line 53
  7. lemma OAI.CriticalStrip.Diagram.GraphRealizes.closure_drains_iff line 84
  8. def OAI.CriticalStrip.Diagram.Tile.transpose line 106
  9. def OAI.CriticalStrip.Diagram.Tile.transposePort line 113
  10. lemma OAI.CriticalStrip.Diagram.Tile.transpose_transpose line 115
  11. lemma OAI.CriticalStrip.Diagram.Tile.transposePort_involutive line 116
  12. lemma OAI.CriticalStrip.Diagram.Tile.transpose_adj line 118
  13. lemma OAI.CriticalStrip.Diagram.Tile.transpose_occupied line 121
  14. lemma OAI.CriticalStrip.Diagram.Tile.weight_transpose line 124
  15. def OAI.CriticalStrip.Diagram.Tile.transposeEquiv line 127
  16. def OAI.CriticalStrip.Diagram.Pairing.GateCompatible line 135
  17. def OAI.CriticalStrip.Diagram.Pairing.flipStep line 139
  18. lemma OAI.CriticalStrip.Diagram.Pairing.flipStep_involutive line 144
  19. lemma OAI.CriticalStrip.Diagram.Pairing.GateCompatible.transpose line 147
  20. def OAI.CriticalStrip.Diagram.Pairing.closedStep line 169
  21. lemma OAI.CriticalStrip.Diagram.Pairing.closedStep_flip line 172
  22. lemma OAI.CriticalStrip.Diagram.Pairing.glues_tile_iff_closedStep line 227
  23. lemma OAI.CriticalStrip.Diagram.Pairing.glues_tile_flip line 253
  24. theorem OAI.CriticalStrip.Diagram.Pairing.glues_tile_adjoint line 270
  25. lemma OAI.CriticalStrip.Diagram.Pairing.gluesAt_comm line 282
  26. def OAI.CriticalStrip.Diagram.glueMatrix line 289
  27. lemma OAI.CriticalStrip.Diagram.glueMatrix_transpose line 293
  28. lemma OAI.CriticalStrip.Diagram.mul_optionMatrix_apply line 298
  29. lemma OAI.CriticalStrip.Diagram.transpose_optionMatrix_mul_apply line 305
  30. lemma OAI.CriticalStrip.Diagram.tileMatrix_glue_adjoint line 312
  31. theorem OAI.CriticalStrip.Diagram.localR_glue_adjoint line 337
  32. def OAI.CriticalStrip.Diagram.sourceBlock line 355
  33. lemma OAI.CriticalStrip.Diagram.LastMatrix.source_mulVec line 359
  34. lemma OAI.CriticalStrip.Diagram.LastMatrix.source_coeff line 373
  35. lemma OAI.CriticalStrip.Diagram.northNumerator_covariance line 381
  36. lemma OAI.CriticalStrip.Diagram.northNumerator_parity line 394
  37. lemma OAI.CriticalStrip.Diagram.LastDegree.occupied_mul_top line 403
  38. lemma OAI.CriticalStrip.Diagram.isEmpty_source_zero line 414