The exact-rank exponent bound

Detecting characters exist by Appendix A. The determinant and three-sector polynomial constructions bound the sum of their dot-product exponents by 9/4. Integer rounding then gives the same bound for the exact-rank exponent.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_le_nine_quarters {K : Type} [Field K] [IsAlgClosed K] : exactRankExponent K ≤ 9 / 4

The polynomial inequalities bound the actual exact-rank exponent.