OAI/Combinatorics/HoneycombChords/YangBaxterDefinitions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Local numerator matrices for the honeycomb Yang–Baxter identity.

This development follows the finite strip transfer calculation for critical honeycomb walks in the companion paper on uniform marked polygon estimates.

  1. def OAI.CriticalHoneycomb.Transfer.YangBaxter.numerator line 14
  2. def OAI.CriticalHoneycomb.Transfer.YangBaxter.leftComponent line 42
  3. def OAI.CriticalHoneycomb.Transfer.YangBaxter.rightComponent line 49
  4. abbrev OAI.CriticalHoneycomb.Transfer.YangBaxter.complexAdd line 56
  5. abbrev OAI.CriticalHoneycomb.Transfer.YangBaxter.complexMul line 57
  6. abbrev OAI.CriticalHoneycomb.Transfer.YangBaxter.complexPow line 58
  7. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.finThreeTwo line 59