Sign changes twisted by powers of -1

Sturm-type counts compare the signs of consecutive entries at +∞ and at -∞. At -∞ a leading sign s of a degree-m polynomial becomes s * (-1) ^ m. For nonzero signs s and t, the sign-change indicator of the twisted pair minus that of the original pair is s * t when m + n is odd and 0 otherwise.

Main results

• SignType.ite_mul_neg_one_pow_sub_ite: the difference of the two sign-change indicators.

theorem SignType.ite_mul_neg_one_pow_sub_ite (m n : ℕ) {s t : SignType} (hs : s ≠ 0) (ht : t ≠ 0) : ↑(if s * (-1) ^ m = t * (-1) ^ n then 0 else 1) - ↑(if s = t then 0 else 1) = if Odd (m + n) then ↑s * ↑t else 0

Comparing the nonzero signs s * (-1) ^ m and t * (-1) ^ n instead of s and t changes the sign-change indicator by s * t exactly when m + n is odd.