OAI/Combinatorics/StripMass/ColumnSweep.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.PartialColumn.baseProject line 18
  2. lemma OAI.CriticalStrip.Diagram.PartialColumn.base_edge line 22
  3. lemma OAI.CriticalStrip.Diagram.PartialColumn.base_used line 28
  4. def OAI.CriticalStrip.Diagram.PartialColumn.baseEquiv line 35
  5. lemma OAI.CriticalStrip.Diagram.PartialColumn.base_realizes line 48
  6. def OAI.CriticalStrip.Diagram.PartialColumn.gate line 52
  7. def OAI.CriticalStrip.Diagram.PartialColumn.circuit line 55
  8. lemma OAI.CriticalStrip.Diagram.PartialColumn.circuit_support line 59
  9. lemma OAI.CriticalStrip.Diagram.PartialColumn.circuit_sound line 72
  10. lemma OAI.CriticalStrip.Diagram.PartialColumn.circuit_exists line 102
  11. lemma OAI.CriticalStrip.Diagram.PartialColumn.circuit_iff line 145
  12. def OAI.CriticalStrip.Diagram.PartialColumn.inputCompatible line 162
  13. lemma OAI.CriticalStrip.Diagram.PartialColumn.circuit_compatible_iff line 166
  14. structure OAI.CriticalStrip.Diagram.PartialColumn.InputConditions line 186
  15. lemma OAI.CriticalStrip.Diagram.PartialColumn.all_input_iff line 191
  16. lemma OAI.CriticalStrip.Diagram.PartialColumn.full_compatible_iff line 211
  17. lemma OAI.CriticalStrip.Diagram.PartialColumn.fullBoundary_injective line 220
  18. lemma OAI.CriticalStrip.Diagram.PartialColumn.east_used line 225
  19. lemma OAI.CriticalStrip.Diagram.PartialColumn.north_isolated line 233
  20. lemma OAI.CriticalStrip.Diagram.PartialColumn.graph_of_realizes line 242
  21. lemma OAI.CriticalStrip.Diagram.PartialColumn.realizes_of_graph line 277
  22. lemma OAI.CriticalStrip.Diagram.PartialColumn.realizes_graph_iff line 301
  23. lemma OAI.CriticalStrip.Diagram.PartialColumn.column_eval_iff line 307
  24. def OAI.CriticalStrip.Diagram.PartialColumn.position line 317
  25. def OAI.CriticalStrip.Diagram.PartialColumn.program line 319
  26. def OAI.CriticalStrip.Diagram.PartialColumn.choicesEquiv line 323
  27. lemma OAI.CriticalStrip.Diagram.PartialColumn.circuit_congr line 333
  28. lemma OAI.CriticalStrip.Diagram.PartialColumn.choices_circuit line 344
  29. lemma OAI.CriticalStrip.Diagram.PartialColumn.choices_weight line 365
  30. lemma OAI.CriticalStrip.Diagram.PartialColumn.program_column line 382