diff --git a/Complexitylib/Circuits/AC0/Iteration.lean b/Complexitylib/Circuits/AC0/Iteration.lean index aebf08ab..c229441e 100644 --- a/Complexitylib/Circuits/AC0/Iteration.lean +++ b/Complexitylib/Circuits/AC0/Iteration.lean @@ -65,10 +65,13 @@ theorem eval_stagedDecisionTree formula. For `queryCount ≥ 2`, the bad staged seeds, amplified by -`q ^ queryCount`, are bounded by the formula tree size, the full staged sample -space, and the width-switching advice factor. The formula may have arbitrary -unbounded fan-in: width at each stage comes from the depth of the child -decision trees, not from the original gate arity. -/ +`q ^ queryCount`, are bounded by the formula gate count, the full staged +sample space, and the width-switching advice factor. Only AND/OR nodes can +fail to switch, so the union bound is over `formula.gateCount`, not the +(strictly larger) syntax-tree `size`; `gateCount_le_size` recovers the +size-based form. The formula may have arbitrary unbounded fan-in: width at +each stage comes from the depth of the child decision trees, not from the +original gate arity. -/ theorem stageEventCount_stagedBad_mul_pow_le (formula : AC0Formula N) (stageCount queryCount q : ℕ) @@ -78,7 +81,7 @@ theorem stageEventCount_stagedBad_mul_pow_le (stagedBad (stageCount := stageCount) formula queryCount) * q ^ queryCount ≤ - formula.size * + formula.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount := stageEventCount_stagedBad_mul_pow_le_internal @@ -99,7 +102,7 @@ theorem exists_shallow_stagedDecisionTree_of_counting (hnumeric : (((2 * q + 1) ^ N) ^ stageCount * queryCount) * q ^ queryCount + - formula.size * + formula.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount * N < (N * ((2 * q + 1) ^ (N - 1)) ^ stageCount) * diff --git a/Complexitylib/Circuits/AC0/Iteration/Internal.lean b/Complexitylib/Circuits/AC0/Iteration/Internal.lean index 4794a978..6207a8c8 100644 --- a/Complexitylib/Circuits/AC0/Iteration/Internal.lean +++ b/Complexitylib/Circuits/AC0/Iteration/Internal.lean @@ -512,7 +512,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal (stagedBad (stageCount := stageCount) formula queryCount) * q ^ queryCount ≤ - formula.size * + formula.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount := by classical @@ -598,7 +598,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal have hchild : Switching.finiteEventCount childBad * q ^ queryCount ≤ - forestSize children * + forestGateCount children * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount := by calc @@ -615,7 +615,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal q ^ queryCount).sum := by rw [List.sum_map_mul_right] _ ≤ (children.toList.map fun child => - child.size * + child.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount).sum := by @@ -629,25 +629,25 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal RandomRestriction.stageEventCount, Switching.finiteEventCount] using ih child hchildDepth - _ = forestSize children * + _ = forestGateCount children * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount := by rw [show (children.toList.map fun child => - child.size * + child.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount).sum = - (children.toList.map size).sum * + (children.toList.map gateCount).sum * (((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount) by simpa [Nat.mul_assoc] using - List.sum_map_mul_right children.toList size + List.sum_map_mul_right children.toList gateCount (((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount)] - rw [← forestSize_ofList_internal, + rw [← forestGateCount_ofList_internal, AC0Forest.ofList_toList] simp [Nat.mul_assoc] let trees : @@ -740,7 +740,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal have hprefix : Switching.finiteEventCount prefixPair * q ^ queryCount ≤ - forestSize children * + forestGateCount children * ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount := by @@ -796,7 +796,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal switchGood pair.1 pair.2) change Switching.finiteEventCount rootEvent * q ^ queryCount ≤ - (1 + forestSize children) * + (1 + forestGateCount children) * ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount calc @@ -819,13 +819,13 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal switchGood pair.1 pair.2) * q ^ queryCount := by rw [Nat.add_mul] - _ ≤ forestSize children * + _ ≤ forestGateCount children * ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount + ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount := Nat.add_le_add hprefix hswitch - _ = (1 + forestSize children) * + _ = (1 + forestGateCount children) * ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount := by simp [Nat.add_mul, Nat.mul_assoc, Nat.add_comm] @@ -854,7 +854,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal have hchild : Switching.finiteEventCount childBad * q ^ queryCount ≤ - forestSize children * + forestGateCount children * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount := by calc @@ -871,7 +871,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal q ^ queryCount).sum := by rw [List.sum_map_mul_right] _ ≤ (children.toList.map fun child => - child.size * + child.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount).sum := by @@ -885,25 +885,25 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal RandomRestriction.stageEventCount, Switching.finiteEventCount] using ih child hchildDepth - _ = forestSize children * + _ = forestGateCount children * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount := by rw [show (children.toList.map fun child => - child.size * + child.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount).sum = - (children.toList.map size).sum * + (children.toList.map gateCount).sum * (((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount) by simpa [Nat.mul_assoc] using - List.sum_map_mul_right children.toList size + List.sum_map_mul_right children.toList gateCount (((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount)] - rw [← forestSize_ofList_internal, + rw [← forestGateCount_ofList_internal, AC0Forest.ofList_toList] simp [Nat.mul_assoc] let trees : @@ -996,7 +996,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal have hprefix : Switching.finiteEventCount prefixPair * q ^ queryCount ≤ - forestSize children * + forestGateCount children * ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount := by @@ -1052,7 +1052,7 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal switchGood pair.1 pair.2) change Switching.finiteEventCount rootEvent * q ^ queryCount ≤ - (1 + forestSize children) * + (1 + forestGateCount children) * ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount calc @@ -1075,13 +1075,13 @@ theorem stageEventCount_stagedBad_mul_pow_le_internal switchGood pair.1 pair.2) * q ^ queryCount := by rw [Nat.add_mul] - _ ≤ forestSize children * + _ ≤ forestGateCount children * ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount + ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount := Nat.add_le_add hprefix hswitch - _ = (1 + forestSize children) * + _ = (1 + forestGateCount children) * ((2 * q + 1) ^ N) ^ (stageCount + 1) * (4 * (queryCount + 1)) ^ queryCount := by simp [Nat.add_mul, Nat.mul_assoc, Nat.add_comm] @@ -1139,7 +1139,7 @@ theorem exists_shallow_stagedDecisionTree_of_counting_internal (hnumeric : (((2 * q + 1) ^ N) ^ stageCount * queryCount) * q ^ queryCount + - formula.size * + formula.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount * N < (N * ((2 * q + 1) ^ (N - 1)) ^ stageCount) * diff --git a/Complexitylib/Circuits/AC0/NormalForm/Defs.lean b/Complexitylib/Circuits/AC0/NormalForm/Defs.lean index f46ad231..6b07f507 100644 --- a/Complexitylib/Circuits/AC0/NormalForm/Defs.lean +++ b/Complexitylib/Circuits/AC0/NormalForm/Defs.lean @@ -138,6 +138,47 @@ end mutual +/-- Number of unbounded gates. Leaves are free and every AND/OR node costs +one. Only gates incur switching failures, so this is the sharp union-bound +measure for iterated switching; `gateCount_le_size` recovers any bound +previously stated with `size`. -/ +def gateCount : AC0Formula N → ℕ + | .const _ => 0 + | .lit _ => 0 + | .and children => 1 + forestGateCount children + | .or children => 1 + forestGateCount children + +/-- Sum of the gate counts of every formula in a forest. -/ +def forestGateCount : AC0Forest N → ℕ + | .nil => 0 + | .cons formula formulas => gateCount formula + forestGateCount formulas + +end + +mutual + +/-- Gate count never exceeds tree size. -/ +theorem gateCount_le_size : (formula : AC0Formula N) → + formula.gateCount ≤ formula.size + | .const _ => Nat.zero_le _ + | .lit _ => Nat.zero_le _ + | .and children => + Nat.add_le_add_left (forestGateCount_le_forestSize children) 1 + | .or children => + Nat.add_le_add_left (forestGateCount_le_forestSize children) 1 + +/-- Forest gate count never exceeds forest size. -/ +theorem forestGateCount_le_forestSize : (formulas : AC0Forest N) → + forestGateCount formulas ≤ forestSize formulas + | .nil => Nat.le_refl 0 + | .cons formula formulas => + Nat.add_le_add (gateCount_le_size formula) + (forestGateCount_le_forestSize formulas) + +end + +mutual + /-- Formula depth. Leaves have depth zero and every unbounded gate adds one. -/ def depth : AC0Formula N → ℕ | .const _ => 0 diff --git a/Complexitylib/Circuits/AC0/NormalForm/Internal.lean b/Complexitylib/Circuits/AC0/NormalForm/Internal.lean index f3ec79a3..e70bfbbd 100644 --- a/Complexitylib/Circuits/AC0/NormalForm/Internal.lean +++ b/Complexitylib/Circuits/AC0/NormalForm/Internal.lean @@ -118,6 +118,14 @@ theorem forestSize_ofList_internal (formulas : List (AC0Formula N)) : simp only [AC0Forest.ofList, forestSize, List.map_cons, List.sum_cons, ih] +theorem forestGateCount_ofList_internal (formulas : List (AC0Formula N)) : + forestGateCount (.ofList formulas) = (formulas.map gateCount).sum := by + induction formulas with + | nil => rfl + | cons formula formulas ih => + simp only [AC0Forest.ofList, forestGateCount, List.map_cons, + List.sum_cons, ih] + theorem forestDepth_ofList_internal (formulas : List (AC0Formula N)) : forestDepth (.ofList formulas) = formulas.foldr (fun formula rest => max formula.depth rest) 0 := by diff --git a/Complexitylib/Circuits/AC0/Parity.lean b/Complexitylib/Circuits/AC0/Parity.lean index 5c1bee8a..e5a3928c 100644 --- a/Complexitylib/Circuits/AC0/Parity.lean +++ b/Complexitylib/Circuits/AC0/Parity.lean @@ -15,12 +15,12 @@ negation-normal unbounded AND/OR formula computing parity. It combines: * exact semantics of iterated restrictions; * the width switching lemma at every connective level; -* a union bound over all nodes in the finite formula tree; +* a union bound over the AND/OR gates of the finite formula tree; * the exact first moment of variables surviving all stages; and * the decision-tree depth lower bound for restricted parity. No uniformity assumption occurs. The remaining family-level step is purely -arithmetic: instantiate the parameters against a polynomial formula-size +arithmetic: instantiate the parameters against a polynomial gate-count bound and a fixed depth. -/ @@ -49,7 +49,7 @@ theorem parity_counting_obstruction q ^ queryCount ≤ (((2 * q + 1) ^ N) ^ stageCount * queryCount) * q ^ queryCount + - formula.size * + formula.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount * N := parity_counting_obstruction_internal diff --git a/Complexitylib/Circuits/AC0/Parity/Internal.lean b/Complexitylib/Circuits/AC0/Parity/Internal.lean index dc48fd3a..c7aeff96 100644 --- a/Complexitylib/Circuits/AC0/Parity/Internal.lean +++ b/Complexitylib/Circuits/AC0/Parity/Internal.lean @@ -30,7 +30,7 @@ theorem parity_counting_obstruction_internal q ^ queryCount ≤ (((2 * q + 1) ^ N) ^ stageCount * queryCount) * q ^ queryCount + - formula.size * + formula.gateCount * ((2 * q + 1) ^ N) ^ stageCount * (4 * (queryCount + 1)) ^ queryCount * N := by apply Nat.le_of_not_gt