The component bound for threshold programs with input fan-in two #
Combining the split lemma with the component split: if every gate reads at most two inputs and
f is two-sided K-rectangle-free with K ≤ 2 ^ L, then n < s_in + 2 L.
theorem
Algebraic.Threshold.card_filter_subset_add_card_filter_subset_compl_le
{n s : ℕ}
(C : Program n s)
(U : Finset (Fin n))
:
Gates with nonempty support inside U and inside Uᶜ are disjoint, so together they number
at most the input-reading gates.
theorem
Algebraic.Threshold.TwoSidedRectangleFree.lt_of_support_card_le_two_internal
{n s : ℕ}
{f : Cslib.BooleanFunction n}
{K : ℕ}
(hf : TwoSidedRectangleFree f K)
{C : Program n s}
(hC : C.Computes f)
(h2 : ∀ (j : Fin s), (C.support j).card ≤ 2)
{L : ℕ}
(hK : K ≤ 2 ^ L)
:
The component bound. If every gate reads at most two inputs and the program computes
a two-sided K-rectangle-free function with K ≤ 2 ^ L, then n < s_in + 2 L.