The quantitative theorem, one determinant from Deligne-only

The sector bound is a theorem given the negated square Schur nonvanishing, so the quantitative Regts–Sevenster statement rests on Deligne's theorem and one binomial determinant.

theorem RS.regts_sevenster_quant_of_detPos (H : SquareBinomialDetPos) (hDeligne : DeligneTheoremStatement) : RegtsSevensterStatementQuant

THE QUANTITATIVE REGTS–SEVENSTER THEOREM, CONDITIONAL ON DELIGNE AND THE BINOMIAL DETERMINANT.

theorem RS.regts_sevenster_quant_deligne_only (hDeligne : DeligneTheoremStatement) : RegtsSevensterStatementQuant

THE QUANTITATIVE REGTS–SEVENSTER THEOREM, CONDITIONAL ON DELIGNE ALONE: the binomial determinant is a theorem (Lindström–Gessel–Viennot), so every graph parameter with edge-connection rank at most R ^ t is the mixed partition function of a functional with both dimensions at most ⌊2eR⌋, assuming only Deligne's theorem on tensor categories.