OAI/Combinatorics/HoneycombChords/YangBaxterWeights.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Sine parametrization and phase normalization of the honeycomb transfer weights.

The formulas follow the finite strip transfer calculation in the companion paper on uniform marked polygon estimates.

  1. def OAI.CriticalHoneycomb.Transfer.YangBaxter.angle line 19
  2. def OAI.CriticalHoneycomb.Transfer.YangBaxter.sine2 line 20
  3. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.cos_two_angle line 22
  4. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.sine2_sq line 27
  5. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.sin_angle_sq line 33
  6. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.cos_angle_eq line 38
  7. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.trig_constraints line 49
  8. def OAI.CriticalHoneycomb.Transfer.YangBaxter.denominator line 65
  9. def OAI.CriticalHoneycomb.Transfer.YangBaxter.phase line 67
  10. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.sin_three_angle line 69
  11. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.cos_three_angle line 71
  12. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.denominator_eq line 74
  13. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.phase_eq line 84
  14. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.phase_sq line 90
  15. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.phase_ne_zero line 99
  16. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.phase_inverse line 101
  17. def OAI.CriticalHoneycomb.Transfer.YangBaxter.sourceR line 108
  18. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.h_plus line 136
  19. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.h_minus line 142
  20. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.c_minus line 147
  21. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.c_plus line 152
  22. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.sourceR_eq_numerator line 156
  23. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.physical_left_sum line 168
  24. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.physical_right_sum line 190