Simultaneous switching for finite formula collections

The exact finite union bound turns the width-sensitive switching theorem into a simultaneous bound for any Fin formulaCount-indexed collection. These collections are finite nonuniform objects; no generator or uniformity assumption is involved.

theorem Complexity.DNF.switchingAnyBad_width_encoding_bound {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)

Simultaneous width-sensitive switching bound for a finite collection of consistent DNFs.

theorem Complexity.DNF.switchingAnyBad_consistentParts_width_encoding_bound {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)

Simultaneous switching bound for arbitrary DNFs after semantics-preserving cleanup, under a common original-width bound.

theorem Complexity.CNF.switchingAnyBad_width_encoding_bound {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)

Simultaneous width-sensitive switching bound for a finite collection of consistent CNFs.

theorem Complexity.CNF.switchingAnyBad_consistentParts_width_encoding_bound {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)

Simultaneous switching bound for arbitrary CNFs after semantics-preserving cleanup, under a common original-width bound.