RankBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_le_nine_quarters line 18
Source documentation
The polynomial inequalities bound the actual exact-rank exponent.
```
theorem exactRankExponent_le_nine_quarters : exactRankExponent ≤ (9 : ℝ) / 4 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent