Parity versus finite AC0 formulas -- proof internals

theorem Complexity.AC0Formula.parity_counting_obstruction_internal {N : ℕ} (formula : AC0Formula N) (computes : ∀ (input : BitString N), eval input formula = Schnorr.xorBool N input) (stageCount queryCount q : ℕ) (hdepth : formula.depth ≤ stageCount) (hquery : 2 ≤ queryCount) (hq : 0 < q) : N * ((2 * q + 1) ^ (N - 1)) ^ stageCount * q ^ queryCount ≤ ((2 * q + 1) ^ N) ^ stageCount * queryCount * q ^ queryCount + formula.size * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount * N