OAI/Combinatorics/HoneycombChords/RowExchange.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Monodromy row exchange and fusion

Formalized from Uniform marked polygon estimates and sharp finite bridge moments (OpenAI, September 26, 2026).

  1. abbrev OAI.CriticalHoneycomb.Transfer.RowExchange.Spin line 17
  2. abbrev OAI.CriticalHoneycomb.Transfer.RowExchange.Local line 18
  3. abbrev OAI.CriticalHoneycomb.Transfer.RowExchange.Space line 19
  4. def OAI.CriticalHoneycomb.Transfer.RowExchange.block line 20
  5. def OAI.CriticalHoneycomb.Transfer.RowExchange.row line 23
  6. def OAI.CriticalHoneycomb.Transfer.RowExchange.forward line 26
  7. def OAI.CriticalHoneycomb.Transfer.RowExchange.backward line 28
  8. def OAI.CriticalHoneycomb.Transfer.RowExchange.localForward line 30
  9. def OAI.CriticalHoneycomb.Transfer.RowExchange.localBackward line 32
  10. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.sum_space_succ line 34
  11. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.forward_succ line 40
  12. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.backward_succ line 49
  13. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.row_exchange line 59
  14. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.row_fusion line 75
  15. theorem OAI.CriticalHoneycomb.Transfer.RowExchange.row_quotient_fusion line 86
  16. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.block_conjTranspose line 103
  17. lemma OAI.CriticalHoneycomb.Transfer.RowExchange.localBackward_conjTranspose line 107