Simultaneous switching for finite formula collections -- proof internals

theorem Complexity.DNF.switchingAnyBad_width_encoding_bound_internal {formulaCount N : ℕ} (formulas : Fin formulaCount → DNF N) (hconsistent : ∀ (index : Fin formulaCount), (formulas index).Consistent) (width : ℕ) (hwidth : ∀ (index : Fin formulaCount), (formulas index).width ≤ width) (q queryCount : ℕ) : RandomRestriction.eventCount q (switchingAnyBad formulas queryCount) * q ^ queryCount ≤ formulaCount * ((2 * q + 1) ^ N * (4 * (width + 1)) ^ queryCount)

theorem Complexity.DNF.switchingAnyBad_consistentParts_width_encoding_bound_internal {formulaCount N : ℕ} (formulas : Fin formulaCount → DNF N) (width : ℕ) (hwidth : ∀ (index : Fin formulaCount), (formulas index).width ≤ width) (q queryCount : ℕ) : RandomRestriction.eventCount q (switchingAnyBad (consistentParts formulas) queryCount) * q ^ queryCount ≤ formulaCount * ((2 * q + 1) ^ N * (4 * (width + 1)) ^ queryCount)

theorem Complexity.CNF.switchingAnyBad_width_encoding_bound_internal {formulaCount N : ℕ} (formulas : Fin formulaCount → CNF N) (hconsistent : ∀ (index : Fin formulaCount), (formulas index).Consistent) (width : ℕ) (hwidth : ∀ (index : Fin formulaCount), (formulas index).width ≤ width) (q queryCount : ℕ) : RandomRestriction.eventCount q (switchingAnyBad formulas queryCount) * q ^ queryCount ≤ formulaCount * ((2 * q + 1) ^ N * (4 * (width + 1)) ^ queryCount)

theorem Complexity.CNF.switchingAnyBad_consistentParts_width_encoding_bound_internal {formulaCount N : ℕ} (formulas : Fin formulaCount → CNF N) (width : ℕ) (hwidth : ∀ (index : Fin formulaCount), (formulas index).width ≤ width) (q queryCount : ℕ) : RandomRestriction.eventCount q (switchingAnyBad (consistentParts formulas) queryCount) * q ^ queryCount ≤ formulaCount * ((2 * q + 1) ^ N * (4 * (width + 1)) ^ queryCount)