Median-cut and coordinate-split restrictions for weighted threshold programs

This module proves the coordinate-split and median-cut rectangle-extraction lemmas for weighted threshold programs. Given a coordinate split U : Finset (Fin n) and subsets A ⊆ U and B ⊆ Uᶜ of inputs fixed to false, we restrict the remaining coordinates P ⊆ (U → Bool) and Q ⊆ (↥Uᶜ → Bool) gate by gate in topological order so that every gate of the program becomes constant on the induced combinatorial rectangle:

• If a gate's active input support meets both U \ A and Uᶜ \ B, we cut both P and Q at the medians of their half-sums (exists_median), halving each side at most once.
• If a gate's active input support meets only one side, its threshold condition depends only on that side, so we halve only that side.
• If a gate's input support is contained in A ∪ B, its weighted input sum vanishes on P × Q, and neither side is shrunk.

Specializing A = ∅ and B = ∅ gives the general median-cut rectangle lemma (exists_rectangle_of_cut), the cut theorem (lt_of_split), and the balanced cut-weight bound n ≤ 2 * ((inputGates p).card + k) (le_two_mul_add). Specializing to gates that do not cross U gives the coordinate-split restriction (exists_rectangle_of_split).

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.inputSupport: the set of original inputs with nonzero aggregated weight at a gate.
• Cslib.Circuits.Boolean.WeightedThreshold.glue: combines partial assignments on U and Uᶜ into a full input Fin n → Bool.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.exists_median: every finite set of points with a real-valued weight function has a median threshold splitting at least half the points to each side.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_rectangle_of_cut_with_fixed: unified median-cut and coordinate-fixing rectangle extraction.
• Cslib.Circuits.Boolean.WeightedThreshold.exists_rectangle_of_cut, Cslib.Circuits.Boolean.WeightedThreshold.exists_rectangle_of_split: median-cut and unsplit-gate rectangle extraction.
• Cslib.Circuits.Boolean.WeightedThreshold.lt_of_split, Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_of_split: the cut theorem.
• Cslib.Circuits.Boolean.WeightedThreshold.le_two_mul_add, Cslib.Circuits.Boolean.WeightedThreshold.circuit_le_two_mul_add: the balanced cut bound.

References

• S. Schlesinger, Algebraic circuit formalizations in Complexitylib, Threshold/Internal/Cut and Split

Aggregated input support

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.inputSupport {n g : ℕ} (p : Program signature n g) (gate : Fin g) : Finset (Fin n)

The original inputs with nonzero aggregated coefficient at gate.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_inputSupport {n g : ℕ} (p : Program signature n g) (gate : Fin g) (i : Fin n) : i ∈ inputSupport p gate ↔ inputWeight p gate i ≠ 0

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_inputGates_iff_inputSupport_nonempty {n g : ℕ} (p : Program signature n g) (gate : Fin g) : gate ∈ inputGates p ↔ (inputSupport p gate).Nonempty

A gate belongs to inputGates p iff its aggregated input support is nonempty.

theorem Cslib.Circuits.Boolean.WeightedThreshold.inputSupport_ne_empty_iff {n g : ℕ} (p : Program signature n g) (gate : Fin g) : inputSupport p gate ≠ ∅ ↔ gate ∈ inputGates p

A gate's aggregated input support is nonempty iff it belongs to inputGates p.

Gluing across a coordinate split

def Cslib.Circuits.Boolean.WeightedThreshold.glue {n : ℕ} (U : Finset (Fin n)) (p : ↥U → Bool) (q : ↥Uᶜ → Bool) : Fin n → Bool

Combine partial assignments on U and Uᶜ into a total input on Fin n.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_lt_or_card_lt_of_rectangleFree {n : ℕ} {f : BooleanFunction n} {K : ℕ} (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (U : Finset (Fin n)) (P : Finset (↥U → Bool)) (Q : Finset (↥Uᶜ → Bool)) (b : Bool) (hconst : ∀ p ∈ P, ∀ q ∈ Q, f (glue U p q) = b) : P.card < K ∨ Q.card < K

If f is monochromatic on the rectangle glue U '' (P × Q) and two-sided K-rectangle-free, then P.card < K or Q.card < K.

Weighted sums and gluing

theorem Cslib.Circuits.Boolean.WeightedThreshold.weightedSum_glue {n : ℕ} (U : Finset (Fin n)) (w : Fin n → ℝ) (p : ↥U → Bool) (q : ↥Uᶜ → Bool) : weightedSum w (glue U p q) = weightedSum w (glue U p fun (x : ↥Uᶜ) => false) + weightedSum w (glue U (fun (x : ↥U) => false) q)

Medians and halving

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_median {α : Type u_1} (P : Finset α) (f : α → ℝ) : ∃ (μ : ℝ), P.card ≤ 2 * {p ∈ P | f p ≤ μ}.card ∧ P.card ≤ 2 * {p ∈ P | μ ≤ f p}.card

Every finite set P equipped with a real-valued function f has a threshold μ such that at least half of P satisfies f x ≤ μ and at least half satisfies μ ≤ f x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.le_card_of_pow_le {m card t k K : ℕ} (hpow : 2 ^ m ≤ card * 2 ^ t) (hm : t + k ≤ m) (hK : K ≤ 2 ^ k) : K ≤ card

Convert a multiplicative power-of-two bound 2 ^ m ≤ card * 2 ^ t with t + k ≤ m and K ≤ 2 ^ k into K ≤ card.

Initial subcubes with fixed coordinates

Unified median-cut and coordinate-fixing invariant

Rectangle extraction and cut bounds

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_rectangle_of_cut_with_fixed {n g : ℕ} (p : Program signature n g) (U A B : Finset (Fin n)) (hA : A ⊆ U) (hB : B ⊆ Uᶜ) : ∃ (P : Finset (↥U → Bool)) (Q : Finset (↥Uᶜ → Bool)) (v : Fin g → Bool), (∀ x ∈ P, ∀ y ∈ Q, p.eval interpretation (glue U x y) = v) ∧ 2 ^ (U.card - A.card) ≤ P.card * 2 ^ {j : Fin g | ¬inputSupport p j ∩ U ⊆ A}.card ∧ 2 ^ (Uᶜ.card - B.card) ≤ Q.card * 2 ^ {j : Fin g | ¬inputSupport p j ∩ Uᶜ ⊆ B}.card

Unified median-cut and coordinate-fixing rectangle extraction. For any split U and sets A ⊆ U and B ⊆ Uᶜ of coordinates fixed to false on U and Uᶜ, there is a combinatorial rectangle P × Q on which the entire gate-evaluation vector p.eval interpretation is constant, with P losing at most |A| coordinates initially and one factor of 2 per gate whose support on U is not contained in A (and symmetrically for Q).

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_rectangle_of_cut {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (U : Finset (Fin n)) : ∃ (P : Finset (↥U → Bool)) (Q : Finset (↥Uᶜ → Bool)) (b : Bool), (∀ x ∈ P, ∀ y ∈ Q, f (glue U x y) = b) ∧ 2 ^ U.card ≤ P.card * 2 ^ {j : Fin g | (inputSupport p j ∩ U).Nonempty}.card ∧ 2 ^ Uᶜ.card ≤ Q.card * 2 ^ {j : Fin g | (inputSupport p j ∩ Uᶜ).Nonempty}.card

The cut lemma. For every coordinate split U, there is a rectangle P × Q on which f is constant, with 2 ^ |U| ≤ |P| · 2 ^ #{j : inputSupport p j ∩ U ≠ ∅} and symmetrically for Uᶜ.

theorem Cslib.Circuits.Boolean.WeightedThreshold.exists_rectangle_of_split {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (U A B : Finset (Fin n)) (hA : A ⊆ U) (hB : B ⊆ Uᶜ) (hsplit : ∀ (j : Fin g), inputSupport p j ⊆ U ∨ inputSupport p j ⊆ Uᶜ) : ∃ (P : Finset (↥U → Bool)) (Q : Finset (↥Uᶜ → Bool)) (b : Bool), (∀ x ∈ P, ∀ y ∈ Q, f (glue U x y) = b) ∧ 2 ^ (U.card - A.card) ≤ P.card * 2 ^ {j : Fin g | inputSupport p j ⊆ U ∧ ¬inputSupport p j ⊆ A}.card ∧ 2 ^ (Uᶜ.card - B.card) ≤ Q.card * 2 ^ {j : Fin g | inputSupport p j ⊆ Uᶜ ∧ ¬inputSupport p j ⊆ B}.card

Coordinate-split rectangle extraction. When every gate's input support is contained in U or in Uᶜ, fixing A ⊆ U and B ⊆ Uᶜ to false yields a monochromatic rectangle P × Q that loses at most one factor of 2 per gate on U with support not contained in A (and symmetrically for Uᶜ and B).

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_filter_inter_nonempty_le_card_inputGates {n g : ℕ} (p : Program signature n g) (S : Finset (Fin n)) : {j : Fin g | (inputSupport p j ∩ S).Nonempty}.card ≤ (inputGates p).card

Gates whose input support meets S belong to inputGates p.

theorem Cslib.Circuits.Boolean.WeightedThreshold.lt_of_split {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (U : Finset (Fin n)) {k : ℕ} (hK : K ≤ 2 ^ k) : U.card < {j : Fin g | (inputSupport p j ∩ U).Nonempty}.card + k ∨ Uᶜ.card < {j : Fin g | (inputSupport p j ∩ Uᶜ).Nonempty}.card + k

The cut theorem. If p computes a two-sided K-rectangle-free function f through readout with K ≤ 2 ^ k, then for every coordinate split U, one side has fewer than k more coordinates than gates whose input support meets that side.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_of_split {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (U : Finset (Fin n)) {k : ℕ} (hK : K ≤ 2 ^ k) : U.card < {j : Fin c.size | (inputSupport c.program j ∩ U).Nonempty}.card + k ∨ Uᶜ.card < {j : Fin c.size | (inputSupport c.program j ∩ Uᶜ).Nonempty}.card + k

The cut theorem for a single-output weighted threshold circuit whose output selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.le_two_mul_add {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K : ℕ} (hreadout : ∀ (x : Fin n → Bool), readout (p.eval interpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) {k : ℕ} (hK : K ≤ 2 ^ k) : n ≤ 2 * ((inputGates p).card + k)

The balanced cut bound. If p computes a two-sided K-rectangle-free function f through readout with K ≤ 2 ^ k, then n ≤ 2 * ((inputGates p).card + k).

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_le_two_mul_add {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {f : BooleanFunction n} {K : ℕ} (hcomputes : ∀ (x : Fin n → Bool), c.eval interpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) {k : ℕ} (hK : K ≤ 2 ^ k) : n ≤ 2 * ((inputGates c.program).card + k)

The balanced cut bound for a single-output weighted threshold circuit whose output selects a gate.