Documentation

LeanPool.RegtsSevenster.RS.QuantSector

Assembly of the quantitative theorem #

The quantitative Regts–Sevenster statement, assembled against the sector bound. The sector bound (SquareSectorBound) is the model half of the dichotomy: when the super permutation action kills the square block idempotent, both sector dimensions of the standard model lie below the side. It is discharged as squareSectorBound_of_detPos in RS/Classical/Interfaces/SectorDischarge.lean (sector intertwining together with the square Schur nonvanishing); this file holds the tower half of the dichotomy and the assembly.

source
def RS.SquareSectorBound :
Prop

The sector bound: super-level death of the square block idempotent forces both dimensions of the standard model below the side. Discharged as squareSectorBound_of_detPos in RS/Classical/Interfaces/SectorDischarge.lean.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem RS.regts_sevenster_quant_of_sector (HSB : SquareSectorBound) (hDeligne : DeligneTheoremStatement) :
    RegtsSevensterStatementQuant

    THE QUANTITATIVE REGTS–SEVENSTER THEOREM, CONDITIONAL ON DELIGNE AND THE SECTOR BOUND: 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⌋.