Iterated switching for AC0 formulas -- proof internals

theorem Complexity.RandomRestriction.card_stageSeed_internal (N q stageCount : ℕ) : Fintype.card (StageSeed N q stageCount) = ((2 * q + 1) ^ N) ^ stageCount

theorem Complexity.RandomRestriction.stageFreeSum_internal (N q stageCount : ℕ) : stageFreeSum N q stageCount = N * ((2 * q + 1) ^ (N - 1)) ^ stageCount

Exact first moment of the number of coordinates surviving every sparse restriction stage.

theorem Complexity.AC0Formula.depth_baseDecisionTree_le_one_internal {N : ℕ} (formula : AC0Formula N) : formula.baseDecisionTree.depth ≤ 1

theorem Complexity.AC0Formula.eval_stagedDecisionTree_internal {N : ℕ} (stageCount : ℕ) (stages : Switching.RestrictionStages N stageCount) (formula : AC0Formula N) (hdepth : formula.depth ≤ stageCount) (input : BitString N) : DecisionTree.On.eval input (stagedDecisionTree stageCount stages formula) = eval ((Switching.RestrictionStages.cumulative stageCount stages).applyTo input) formula

theorem Complexity.AC0Formula.depth_stagedDecisionTree_const_le_one_internal {N : ℕ} (stageCount : ℕ) (stages : Switching.RestrictionStages N stageCount) (value : Bool) : (stagedDecisionTree stageCount stages (const value)).depth ≤ 1

theorem Complexity.AC0Formula.depth_stagedDecisionTree_lit_le_one_internal {N : ℕ} (stageCount : ℕ) (stages : Switching.RestrictionStages N stageCount) (literal : Literal N) : (stagedDecisionTree stageCount stages (lit literal)).depth ≤ 1

theorem Complexity.AC0Formula.stageEventCount_stagedBad_mul_pow_le_internal {N : ℕ} (formula : AC0Formula N) (stageCount queryCount q : ℕ) (hdepth : formula.depth ≤ stageCount) (hquery : 2 ≤ queryCount) : RandomRestriction.stageEventCount q (formula.stagedBad queryCount) * q ^ queryCount ≤ formula.size * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount

theorem Complexity.AC0Formula.exists_shallow_stagedDecisionTree_internal {N : ℕ} (formula : AC0Formula N) (stageCount queryCount q : ℕ) (haverage : ((2 * q + 1) ^ N) ^ stageCount * queryCount + RandomRestriction.stageEventCount q (formula.stagedBad queryCount) * N < RandomRestriction.stageFreeSum N q stageCount) : ∃ (seeds : RandomRestriction.StageSeed N q stageCount), (stagedDecisionTree stageCount (RandomRestriction.decodeStages seeds) formula).depth < queryCount ∧ queryCount ≤ (RandomRestriction.finalRestriction seeds).freeVariables.card

theorem Complexity.AC0Formula.exists_shallow_stagedDecisionTree_of_counting_internal {N : ℕ} (formula : AC0Formula N) (stageCount queryCount q : ℕ) (hdepth : formula.depth ≤ stageCount) (hquery : 2 ≤ queryCount) (hq : 0 < q) (hnumeric : ((2 * q + 1) ^ N) ^ stageCount * queryCount * q ^ queryCount + formula.size * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount * N < N * ((2 * q + 1) ^ (N - 1)) ^ stageCount * q ^ queryCount) : ∃ (seeds : RandomRestriction.StageSeed N q stageCount), (stagedDecisionTree stageCount (RandomRestriction.decodeStages seeds) formula).depth < queryCount ∧ queryCount ≤ (RandomRestriction.finalRestriction seeds).freeVariables.card