(1) interpolation / triangle check: True
(2a) F_k^n formula on truncation: True
(2b) witness pair in F_{k'}^m o F_k, outside K when k < m+1: True
