OAI/Combinatorics/StripMass/HoneycombDictionary.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.HoneycombAssignment.ext line 17
  2. lemma OAI.CriticalStrip.HoneycombAssignment.ext_graph_boundary line 22
  3. def OAI.CriticalStrip.WireConfiguration.physicalTile line 73
  4. lemma OAI.CriticalStrip.WireConfiguration.physicalTile_spec line 81
  5. def OAI.CriticalStrip.WireConfiguration.toAssignment line 109
  6. lemma OAI.CriticalStrip.WireConfiguration.toAssignment_up line 135
  7. theorem OAI.CriticalStrip.WireConfiguration.toAssignment_graph line 156
  8. lemma OAI.CriticalStrip.WireConfiguration.toAssignment_bottom line 179
  9. lemma OAI.CriticalStrip.WireConfiguration.toAssignment_top line 184
  10. structure OAI.CriticalStrip.HoneycombConfiguration line 194
  11. lemma OAI.CriticalStrip.HoneycombConfiguration.ext line 203
  12. def OAI.CriticalStrip.HoneycombConfiguration.toWire line 208
  13. def OAI.CriticalStrip.HoneycombConfiguration.ofWire line 224
  14. lemma OAI.CriticalStrip.HoneycombConfiguration.toWire_ofWire line 234
  15. lemma OAI.CriticalStrip.HoneycombConfiguration.ofWire_toWire line 239
  16. def OAI.CriticalStrip.HoneycombConfiguration.equivWires line 251
  17. def OAI.CriticalStrip.HoneycombConfiguration.equivPaths line 258
  18. lemma OAI.CriticalStrip.HoneycombConfiguration.path_spec line 262
  19. lemma OAI.CriticalStrip.Diagram.physicalWeights_two_lambda line 277
  20. lemma OAI.CriticalStrip.Diagram.Tile.nonvacant_iff_used line 294
  21. lemma OAI.CriticalStrip.Diagram.Tile.upperUsed_internal line 298
  22. lemma OAI.CriticalStrip.Diagram.Tile.lowerUsed_internal line 303
  23. lemma OAI.CriticalStrip.HoneycombAssignment.up_support_iff line 313
  24. lemma OAI.CriticalStrip.HoneycombAssignment.down_support_iff line 333
  25. def OAI.CriticalStrip.HoneycombAssignment.tileSupport line 353
  26. lemma OAI.CriticalStrip.HoneycombAssignment.tileSupport_eq_image line 355
  27. lemma OAI.CriticalStrip.HoneycombAssignment.support_ncard_eq line 374
  28. lemma OAI.CriticalStrip.HoneycombConfiguration.tileSupport_finite line 432
  29. def OAI.CriticalStrip.HoneycombConfiguration.weight line 439
  30. lemma OAI.CriticalStrip.HoneycombConfiguration.finite_weight_support line 442
  31. theorem OAI.CriticalStrip.HoneycombConfiguration.weight_eq_wire line 451
  32. lemma OAI.CriticalStrip.HoneycombConfiguration.weight_eq_path line 476
  33. lemma OAI.CriticalStrip.HoneycombConfiguration.countable line 480
  34. theorem OAI.CriticalStrip.HoneycombConfiguration.summable_weight_iff line 485
  35. lemma OAI.CriticalStrip.HoneycombConfiguration.tsum_weight line 494
  36. theorem OAI.CriticalStrip.HoneycombConfiguration.arch_sum line 501
  37. theorem OAI.CriticalStrip.HoneycombConfiguration.arch_summable line 506
  38. theorem OAI.CriticalStrip.HoneycombConfiguration.bridge_sum line 511
  39. theorem OAI.CriticalStrip.HoneycombConfiguration.bridge_summable line 516