feat(circuits): tighten iterated switching union bound to gate count

[SamuelSchlesinger]

Only AND/OR nodes can fail to switch, so the union bound in the iterated switching theorem needs one advice slot per gate, not one per syntax-tree node. Leaves (constants and literals) compile to depth-≤1 decision trees and provably contribute no bad events, yet size charged them anyway — for a width-w bottom gate the old bound overcharged by roughly a factor of w.

Changes

• Add AC0Formula.gateCount / forestGateCount (leaves cost zero, every gate costs one) with gateCount_le_size, and forestGateCount_ofList_internal.
• Strengthen stageEventCount_stagedBad_mul_pow_le, exists_shallow_stagedDecisionTree_of_counting, and parity_counting_obstruction to charge gateCount instead of size. The internal induction is unchanged in structure: the 1 + pays for the top gate's switching event and the forest sum covers the children.
• Any size-based form remains derivable in one step via gateCount_le_size.

Verification

• lake build --wfail plus both Validation executables
• python3 scripts/lint_style.py clean
• lake exe runLinter Complexitylib clean
• lake env lean scripts/AxiomGuard.lean: 42,920 declarations (31,285 theorems) on standard axioms only

Downstream note: circuit-nondet pins this commit and restates its iterated_switching_count, sensitivity_depth_reduction, and avgSensitivity_le_of_switching_budget with the tightened measure.