Asymptotic lower bounds for bounded direct input support

The random-cut estimate gives a coefficient 1 / (2 * (1 - 2⁻ᵈ)) for input-reading gates whose aggregated support on original inputs has size at most the fixed positive integer d. The two Boolean fibers must be rectangle-free at a threshold with sublinear binary logarithm. Internal predecessor fan-in, depth, fan-out, and real weights remain unrestricted.

For d = 3, incidence layouts improve the coefficient to 2 / 3. The separate support-at-most-two theorem gives the stronger coefficient 1 when d = 2.

This follows from the finite support bound. It does not construct an explicit family with the required rectangle-freeness property.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.eventually_lt_inputGates_of_inputSupport_card_le: the asymptotic bound for native programs and any fixed Boolean readout of their gate values.
• Cslib.Circuits.Boolean.WeightedThreshold.eventually_lt_inputGates_of_inputSupport_card_le_three: the coefficient 2 / 3 for direct support of size at most three.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eventually_lt_inputGates_of_inputSupport_card_le {d : ℕ} (hd : 0 < d) {f : (n : ℕ) → BooleanFunction n} {K k : ℕ → ℕ} (hf : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f n x = b} (K n)) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ 2 ^ k n) (hk : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (g : ℕ) (p : Program signature n g) (readout : (Fin g → Bool) → Bool), (∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f n x) → (∀ (gate : Fin g), (inputSupport p gate).card ≤ d) → (1 / (2 * (1 - (1 / 2) ^ d)) - ε) * ↑n < ↑(inputGates p).card

A family with both fibers K(n)-rectangle-free, with K(n) ≤ 2 ^ k(n) and k(n) = o(n), requires more than (1 / (2 * (1 - 2⁻ᵈ)) - ε) n input-reading gates for every ε > 0 and all sufficiently large n, when each gate directly reads at most d > 0 original inputs.

The readout may be any Boolean function of the gate values. Internal predecessor fan-in, depth, fan-out, and real coefficients are unrestricted.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eventually_lt_inputGates_of_inputSupport_card_le_three {f : (n : ℕ) → BooleanFunction n} {K k : ℕ → ℕ} (hf : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f n x = b} (K n)) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ 2 ^ k n) (hk : (fun (n : ℕ) => ↑(k n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (g : ℕ) (p : Program signature n g) (readout : (Fin g → Bool) → Bool), (∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f n x) → (∀ (gate : Fin g), (inputSupport p gate).card ≤ 3) → (2 / 3 - ε) * ↑n < ↑(inputGates p).card

For direct support of size at most three, incidence layouts force more than (2 / 3 - ε) n input-reading gates for all sufficiently large input lengths.