DetLow: the theorems lowestUnit : LowestUnit and lowestBound : LowestBound #
lowestUnit is Lemma 3.3 of the paper; lowestBound is Lemma 3.4 and Lemma 3.6.
Lemma 3.3 of the paper: multiplying by a polynomial with constant coefficient 1 does not
change the monomials of least total degree.
theorem
AaronsonAmbainis.DetLow.degreeOf_cofactor_le
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(g : Cube ι → Bool)
(j : ι)
(R : MvPolynomial ι ℤ)
(hR : (agMatrix g).det = (1 - MvPolynomial.X j ^ 2) ^ (Up g j).card * R)
:
The cofactor R of (1 - s_j^2)^(e_j) has degree at most b_j(g) in s_j (proof of
Lemma 3.6 of the paper).
Lemma 3.4 and Lemma 3.6 of the paper: the determinant of the agreement matrix is nonzero, and
each of its monomials of least total degree has exponent at most b_j(g) in every variable
s_j.