OAI/Combinatorics/HoneycombChords/YangBaxter.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The honeycomb Yang–Baxter identity in the sine parametrization.

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

  1. theorem OAI.CriticalHoneycomb.Transfer.YangBaxter.numerator_yang_baxter line 22
  2. theorem OAI.CriticalHoneycomb.Transfer.YangBaxter.source_yang_baxter line 56