Sector discharge: the last gap of the quantitative Regts–Sevenster theorem

Given SquareBinomialDetPos (the Lindström–Gessel–Viennot core: the binomial Toeplitz determinant for squareDiagram s at −m is nonzero whenever 1 ≤ s ≤ m), we discharge SquareSectorBound: when the super permutation action kills the square-block idempotent at every side s' ≥ s, both sector dimensions k (even) and 2l (odd) of the standard model stdSuperPair k l lie strictly below s.

The proof transports the abstract superPermAction on superPow (strandImage f P) n to the model action modelPermMap on superPow (stdSuperPair k l) n via the iterated iso built from the standard-model extraction (e, e'), then feeds the sector traces evenSectorTr / oddSectorTr through sector_bound_of_dead / sector_bound_of_dead_signed.

Main result

• squareSectorBound_of_detPos — the last gap of the quantitative theorem.

Transport identification

The iterated standard-model transport stdToOmega ≫ omegaPowInv conjugates superPermAction to modelPermMap.

Even sector bound

Even (s²) is equivalent to even s

The main theorem

theorem RS.squareSectorBound_of_detPos (H : SquareBinomialDetPos) : SquareSectorBound

Discharge of SquareSectorBound: the last gap of the quantitative Regts–Sevenster theorem.

Given SquareBinomialDetPos (the binomial determinant nonvanishing), we show that when superPermAction kills the square-block idempotent at every side s' ≥ s with 1 ≤ s, both sector dimensions k (even) and 2l (odd) of the standard model lie below s.