Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
SamuelSchlesinger wants to merge 1 commit into
base: dev
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 9 additions & 6 deletions Complexitylib/Circuits/AC0/Iteration.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 : ℕ)
Expand All @@ -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
Expand All @@ -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) *
Expand Down
48 changes: 24 additions & 24 deletions Complexitylib/Circuits/AC0/Iteration/Internal.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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 :
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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 :
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand Down Expand Up @@ -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) *
Expand Down
41 changes: 41 additions & 0 deletions Complexitylib/Circuits/AC0/NormalForm/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 8 additions & 0 deletions Complexitylib/Circuits/AC0/NormalForm/Internal.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions Complexitylib/Circuits/AC0/Parity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
-/

Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Complexitylib/Circuits/AC0/Parity/Internal.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down