Pending-bias state simulation and input-summary lower bounds for threshold circuits

A weighted threshold program of size g has a layered finite-state representation across any gate cut k. After the first k gates have been evaluated to a Boolean prefix u : Fin k → Bool, their entire effect on the remaining g - k gates is captured by the pending-bias vector pendingBias p k u : Fin (g - k) → ℝ collecting the internal weighted sums contributed by the prefix to each future gate. The layered evolution pendingBiasTrace computes these states recursively by evaluating each gate from its direct input sum and the first coordinate of the current pending-bias vector, then shifting the state and adding the new gate's outgoing internal weights (Theorem 6.1).

Bounding the syntactic state space pendingBiasStates p k yields finite-state width bounds under bounded fan-in (2 ^ k), bounded integer internal weights on a row basis (∏ i ∈ rows, (1 + ∑ j, |w i j|) and (1 + k * W) ^ rows.card), or column-constant internal weights (k + 1).

On the input side, the complete gate valuation is determined by the direct input summary inputSummary p x. Whenever a threshold program computes a two-party function f : X → Y → Bool, any summary map on X that determines inputSummary for every y : Y must take at least as many values as there are distinct rows of f (Proposition 9.1), forcing (1 + |ι| * W) ^ r ≥ 2 ^ |ι| for rank-r integer summaries of the Hadamard inner-product code. Under phased input access across cut k (gates < k reading only X, gates ≥ k reading only Y, and readout depending only on gates ≥ k), the pending-bias state at cut k is a deterministic one-way message from X to Y, forcing (pendingBiasStates p k).card to be at least the number of distinct rows of f.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.gateThreshold: the threshold of a program gate.
• Cslib.Circuits.Boolean.WeightedThreshold.pendingBias: the pending internal bias vector at cut k from a Boolean prefix u : Fin k → Bool.
• Cslib.Circuits.Boolean.WeightedThreshold.pendingBiasTrace: the layered pending-bias state evolution on input x.
• Cslib.Circuits.Boolean.WeightedThreshold.pendingBiasStates: the syntactic set of pending-bias states at cut k.
• Cslib.Circuits.Boolean.WeightedThreshold.inputSummary: the direct input-weighted sum vector of a program on input x.
• Cslib.Circuits.Boolean.WeightedThreshold.intSummary: the integer linear summary u ↦ R u of a Boolean input u : ι → Bool.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.pendingBiasTrace_eq_pendingBias, Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_decide_pendingBiasTrace: Theorem 6.1, exact pending-bias state simulation.
• Cslib.Circuits.Boolean.WeightedThreshold.card_pendingBiasStates_le_two_pow, Cslib.Circuits.Boolean.WeightedThreshold.card_pendingBiasStates_le_prod_intWeight, Cslib.Circuits.Boolean.WeightedThreshold.card_pendingBiasStates_le_pow_intWeight, Cslib.Circuits.Boolean.WeightedThreshold.card_pendingBiasStates_le_add_one_of_row_const: Section 6.1 state-space bounds.
• Cslib.Circuits.Boolean.WeightedThreshold.card_rows_le_card_summaries, Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_card_summaries_of_hadamardCode, Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_pow_intSummary_of_hadamardCode: Proposition 9.1 input-summary and rank-precision lower bounds.
• Cslib.Circuits.Boolean.WeightedThreshold.card_rows_le_card_pendingBiasStates_of_phased, Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_card_pendingBiasStates_of_phased_hadamardCode: Section 9 phased-access cut lower bounds.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Sections 6 and 9] [26]

Helper lemmas for finite-image and integer-box cardinality bounds

Section 6: Pending-bias state simulation and state-set bounds

def Cslib.Circuits.Boolean.WeightedThreshold.gateThreshold {n g : ℕ} (p : Program signature n g) (gate : Fin g) : ℝ

The threshold of a gate in a weighted threshold program.

def Cslib.Circuits.Boolean.WeightedThreshold.pendingBias {n g : ℕ} (p : Program signature n g) (k : ℕ) (u : Fin k → Bool) (i : Fin (g - k)) : ℝ

At cut k, the pending internal bias accumulated at future gate k + i from the first k gate outputs u : Fin k → Bool.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.pendingBias_zero {n g : ℕ} (p : Program signature n g) (u : Fin 0 → Bool) (i : Fin (g - 0)) : pendingBias p 0 u i = 0

At cut 0, the pending internal bias is identically zero.

theorem Cslib.Circuits.Boolean.WeightedThreshold.pendingBias_succ {n g : ℕ} (p : Program signature n g) (k : ℕ) (u : Fin (k + 1) → Bool) (i : Fin (g - (k + 1))) : have this := ⋯; pendingBias p (k + 1) u i = pendingBias p k (fun (j : Fin k) => u j.castSucc) ⟨↑i + 1, ⋯⟩ + gateWeight p ⟨k + 1 + ↑i, ⋯⟩ ⟨k, ⋯⟩ * ↑(u (Fin.last k)).toNat

Stepping from cut k to cut k + 1 shifts the remaining-gate index by one and adds the new gate's internal-weight contribution.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_decide_pendingBias {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (gate : Fin g) : p.eval interpretation x gate = decide (gateThreshold p gate ≤ ∑ a : Fin n, inputWeight p gate a * ↑(x a).toNat + pendingBias p (↑gate) (fun (j : Fin ↑gate) => p.eval interpretation x ⟨↑j, ⋯⟩) ⟨0, ⋯⟩)

The output of gate is determined by its direct input-weighted sum and the first coordinate of the pending-bias vector at cut gate.val.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.pendingBiasTrace {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (k : ℕ) : Fin (g - k) → ℝ

The layered pending-bias state evolution along the gates of p on input x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.pendingBiasTrace_eq_pendingBias {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (k : ℕ) : pendingBiasTrace p x k = pendingBias p k fun (j : Fin k) => if hj : ↑j < g then p.eval interpretation x ⟨↑j, hj⟩ else false

Theorem 6.1 (Pending-bias state simulation). At every layer k, the recursively updated state pendingBiasTrace p x k equals the syntactic pending-bias vector of the actual gate prefix evaluated on x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_decide_pendingBiasTrace {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (gate : Fin g) : p.eval interpretation x gate = decide (gateThreshold p gate ≤ ∑ a : Fin n, inputWeight p gate a * ↑(x a).toNat + pendingBiasTrace p x ↑gate ⟨0, ⋯⟩)

Theorem 6.1 (Pending-bias query rule). Each gate's evaluation is a single linear threshold query on x shifted by the first coordinate of the recursive pending-bias state.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.pendingBiasStates {n g : ℕ} (p : Program signature n g) (k : ℕ) : Finset (Fin (g - k) → ℝ)

The syntactic set of pending-bias states at cut k, ranging over all Boolean prefixes u : Fin k → Bool.

theorem Cslib.Circuits.Boolean.WeightedThreshold.pendingBias_mem_pendingBiasStates {n g : ℕ} (p : Program signature n g) (k : ℕ) (u : Fin k → Bool) : pendingBias p k u ∈ pendingBiasStates p k

Every Boolean prefix produces a state in pendingBiasStates p k.

theorem Cslib.Circuits.Boolean.WeightedThreshold.pendingBiasTrace_mem_pendingBiasStates {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (k : ℕ) : pendingBiasTrace p x k ∈ pendingBiasStates p k

The reachable state pendingBiasTrace p x k belongs to pendingBiasStates p k.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_pendingBiasStates_le_two_pow {n g : ℕ} (p : Program signature n g) (k : ℕ) : (pendingBiasStates p k).card ≤ 2 ^ k

At cut k, there are at most 2 ^ k pending-bias states.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_pendingBiasStates_le_prod_intWeight {n g : ℕ} (p : Program signature n g) (k : ℕ) (rows : Finset (Fin (g - k))) (hrows : ∀ (u v : Fin k → Bool), (∀ i ∈ rows, pendingBias p k u i = pendingBias p k v i) → pendingBias p k u = pendingBias p k v) (w : Fin (g - k) → Fin k → ℤ) (hw : ∀ i ∈ rows, ∀ (j : Fin k), gateWeight p ⟨k + ↑i, ⋯⟩ ⟨↑j, ⋯⟩ = ↑(w i j)) : (pendingBiasStates p k).card ≤ ∏ i ∈ rows, (1 + ∑ j : Fin k, (w i j).natAbs)

Section 6.1 (Integer-weight box bound for pending-bias states). If a subset rows of remaining gates determines the entire pending-bias vector at cut k, and the internal weights into rows from the first k gates are integers w i j, then the number of pending-bias states is at most ∏ i ∈ rows, (1 + ∑ j : Fin k, (w i j).natAbs).

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_pendingBiasStates_le_pow_intWeight {n g : ℕ} (p : Program signature n g) (k W : ℕ) (rows : Finset (Fin (g - k))) (hrows : ∀ (u v : Fin k → Bool), (∀ i ∈ rows, pendingBias p k u i = pendingBias p k v i) → pendingBias p k u = pendingBias p k v) (w : Fin (g - k) → Fin k → ℤ) (hw : ∀ i ∈ rows, ∀ (j : Fin k), gateWeight p ⟨k + ↑i, ⋯⟩ ⟨↑j, ⋯⟩ = ↑(w i j)) (hW : ∀ i ∈ rows, ∀ (j : Fin k), (w i j).natAbs ≤ W) : (pendingBiasStates p k).card ≤ (1 + k * W) ^ rows.card

Section 6.1, equation (9) (Rank-precision bound for pending-bias states). Under the hypotheses of card_pendingBiasStates_le_prod_intWeight, if every selected integer internal weight has magnitude at most W, then (pendingBiasStates p k).card ≤ (1 + k * W) ^ rows.card.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_pendingBiasStates_le_add_one_of_row_const {n g : ℕ} (p : Program signature n g) (k : ℕ) (β : Fin (g - k) → ℝ) (hβ : ∀ (i : Fin (g - k)) (j : Fin k), gateWeight p ⟨k + ↑i, ⋯⟩ ⟨↑j, ⋯⟩ = β i) : (pendingBiasStates p k).card ≤ k + 1

Section 6.1 (Column-constant internal weights). If every future gate k + i assigns a single weight β i to all k earlier gates, the pending-bias state depends only on the Hamming weight of the prefix and has at most k + 1 values.

Section 9: Input summaries and phased-access cut lower bounds

def Cslib.Circuits.Boolean.WeightedThreshold.inputSummary {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (gate : Fin g) : ℝ

The direct input-weighted sum at each gate of p on input x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_inputSummary_eq_lt {n g : ℕ} (p : Program signature n g) {x y : Fin n → Bool} (b : ℕ) (h : ∀ (gate : Fin g), ↑gate < b → inputSummary p x gate = inputSummary p y gate) (gate : Fin g) : ↑gate < b → p.eval interpretation x gate = p.eval interpretation y gate

Agreement of direct input summaries on all gates below b forces agreement of gate evaluations below b.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_inputSummary_eq {n g : ℕ} (p : Program signature n g) {x y : Fin n → Bool} (h : inputSummary p x = inputSummary p y) : p.eval interpretation x = p.eval interpretation y

Equal direct input summaries produce identical complete gate valuations.

theorem Cslib.Circuits.Boolean.WeightedThreshold.f_eq_of_summary_eq {n g : ℕ} {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Program signature n g) (enc : X → Y → Fin n → Bool) (readout : (Fin g → Bool) → Bool) (f : X → Y → Bool) (summary : X → α) (hcomp : ∀ (x : X) (y : Y), readout (p.eval interpretation (enc x y)) = f x y) (hsum : ∀ (x₁ x₂ : X) (y : Y), summary x₁ = summary x₂ → inputSummary p (enc x₁ y) = inputSummary p (enc x₂ y)) {x₁ x₂ : X} (h : summary x₁ = summary x₂) : f x₁ = f x₂

If summary x determines the direct input summary of enc x y for every y, then equal summaries force identical row functions f x₁ = f x₂.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_rows_le_card_summaries {n g : ℕ} {X : Type u_1} {Y : Type u_2} {α : Type u_3} [Fintype X] [DecidableEq (Y → Bool)] [DecidableEq α] (p : Program signature n g) (enc : X → Y → Fin n → Bool) (readout : (Fin g → Bool) → Bool) (f : X → Y → Bool) (summary : X → α) (hcomp : ∀ (x : X) (y : Y), readout (p.eval interpretation (enc x y)) = f x y) (hsum : ∀ (x₁ x₂ : X) (y : Y), summary x₁ = summary x₂ → inputSummary p (enc x₁ y) = inputSummary p (enc x₂ y)) : (Finset.image f Finset.univ).card ≤ (Finset.image summary Finset.univ).card

Proposition 9.1 (Distinct communication rows force distinct input summaries). If f is computed by a threshold program p via enc and readout, any summary of the left input X that determines inputSummary p (enc x y) for every y takes at least as many values as there are distinct rows of f.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_card_summaries_of_hadamardCode {n g : ℕ} {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq α] (p : Program signature n g) (enc : (ι → Bool) → (ι → Bool) → Fin n → Bool) (readout : (Fin g → Bool) → Bool) (summary : (ι → Bool) → α) (hcomp : ∀ (x y : ι → Bool), readout (p.eval interpretation (enc x y)) = BitString.hadamardCode x y) (hsum : ∀ (x₁ x₂ y : ι → Bool), summary x₁ = summary x₂ → inputSummary p (enc x₁ y) = inputSummary p (enc x₂ y)) : 2 ^ Fintype.card ι ≤ (Finset.image summary Finset.univ).card

Proposition 9.1 (Hadamard input-summary lower bound). Any summary of x : ι → Bool that determines the direct input weights of a threshold program computing hadamardCode has at least 2 ^ Fintype.card ι distinct values.

def Cslib.Circuits.Boolean.WeightedThreshold.intSummary {ι : Type u_1} [Fintype ι] {r : ℕ} (R : Fin r → ι → ℤ) (u : ι → Bool) : Fin r → ℤ

The integer linear summary u ↦ R u of a Boolean input u : ι → Bool by an integer matrix R : Fin r → ι → ℤ.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_intSummary_le_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (R : Fin r → ι → ℤ) : (Finset.image (intSummary R) Finset.univ).card ≤ ∏ a : Fin r, (1 + ∑ i : ι, (R a i).natAbs)

Each row a of intSummary R takes at most 1 + ∑ i, (R a i).natAbs values on the Boolean cube.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_intSummary_le_pow {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r W : ℕ} (R : Fin r → ι → ℤ) (hW : ∀ (a : Fin r) (i : ι), (R a i).natAbs ≤ W) : (Finset.image (intSummary R) Finset.univ).card ≤ (1 + Fintype.card ι * W) ^ r

If all entries of R : Fin r → ι → ℤ have magnitude at most W, then intSummary R takes at most (1 + Fintype.card ι * W) ^ r values on the Boolean cube.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_prod_intSummary_of_hadamardCode {n g : ℕ} {ι : Type u_1} [Fintype ι] {r : ℕ} (p : Program signature n g) (enc : (ι → Bool) → (ι → Bool) → Fin n → Bool) (readout : (Fin g → Bool) → Bool) (R : Fin r → ι → ℤ) (hcomp : ∀ (x y : ι → Bool), readout (p.eval interpretation (enc x y)) = BitString.hadamardCode x y) (hsum : ∀ (x₁ x₂ y : ι → Bool), intSummary R x₁ = intSummary R x₂ → inputSummary p (enc x₁ y) = inputSummary p (enc x₂ y)) : 2 ^ Fintype.card ι ≤ ∏ a : Fin r, (1 + ∑ i : ι, (R a i).natAbs)

Proposition 9.1 (Integer summary product bound for inner product). If an integer matrix R : Fin r → ι → ℤ determines the direct input weights of a threshold program computing hadamardCode, the product of its row ranges is at least 2 ^ Fintype.card ι.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_pow_intSummary_of_hadamardCode {n g : ℕ} {ι : Type u_1} [Fintype ι] {r W : ℕ} (p : Program signature n g) (enc : (ι → Bool) → (ι → Bool) → Fin n → Bool) (readout : (Fin g → Bool) → Bool) (R : Fin r → ι → ℤ) (hW : ∀ (a : Fin r) (i : ι), (R a i).natAbs ≤ W) (hcomp : ∀ (x y : ι → Bool), readout (p.eval interpretation (enc x y)) = BitString.hadamardCode x y) (hsum : ∀ (x₁ x₂ y : ι → Bool), intSummary R x₁ = intSummary R x₂ → inputSummary p (enc x₁ y) = inputSummary p (enc x₂ y)) : 2 ^ Fintype.card ι ≤ (1 + Fintype.card ι * W) ^ r

Proposition 9.1, equation (20) (Rank-precision bound for inner product). If an integer matrix R : Fin r → ι → ℤ with entries bounded in magnitude by W determines the direct input weights of a threshold program computing hadamardCode, then 2 ^ Fintype.card ι ≤ (1 + Fintype.card ι * W) ^ r.

theorem Cslib.Circuits.Boolean.WeightedThreshold.f_eq_of_pendingBiasTrace_eq_of_phased {n g : ℕ} {X : Type u_1} {Y : Type u_2} (p : Program signature n g) (enc : X → Y → Fin n → Bool) (readout : (Fin g → Bool) → Bool) (f : X → Y → Bool) (k : ℕ) (y₀ : Y) (hcomp : ∀ (x : X) (y : Y), readout (p.eval interpretation (enc x y)) = f x y) (hpref : ∀ (j : Fin k) (hj : ↑j < g) (x : X) (y : Y), inputSummary p (enc x y) ⟨↑j, hj⟩ = inputSummary p (enc x y₀) ⟨↑j, hj⟩) (hsuff : ∀ (i : Fin (g - k)) (x₁ x₂ : X) (y : Y), inputSummary p (enc x₁ y) ⟨k + ↑i, ⋯⟩ = inputSummary p (enc x₂ y) ⟨k + ↑i, ⋯⟩) (hread : ∀ (z₁ z₂ : Fin g → Bool), (∀ (i : Fin (g - k)), z₁ ⟨k + ↑i, ⋯⟩ = z₂ ⟨k + ↑i, ⋯⟩) → readout z₁ = readout z₂) {x₁ x₂ : X} (htrace : pendingBiasTrace p (enc x₁ y₀) k = pendingBiasTrace p (enc x₂ y₀) k) : f x₁ = f x₂

Under phased input access across cut k, the pending-bias state pendingBiasTrace p (enc x y₀) k at a reference right input y₀ determines the entire row f x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.card_rows_le_card_pendingBiasStates_of_phased {n g : ℕ} {X : Type u_1} {Y : Type u_2} [Fintype X] [DecidableEq (Y → Bool)] (p : Program signature n g) (enc : X → Y → Fin n → Bool) (readout : (Fin g → Bool) → Bool) (f : X → Y → Bool) (k : ℕ) (y₀ : Y) (hcomp : ∀ (x : X) (y : Y), readout (p.eval interpretation (enc x y)) = f x y) (hpref : ∀ (j : Fin k) (hj : ↑j < g) (x : X) (y : Y), inputSummary p (enc x y) ⟨↑j, hj⟩ = inputSummary p (enc x y₀) ⟨↑j, hj⟩) (hsuff : ∀ (i : Fin (g - k)) (x₁ x₂ : X) (y : Y), inputSummary p (enc x₁ y) ⟨k + ↑i, ⋯⟩ = inputSummary p (enc x₂ y) ⟨k + ↑i, ⋯⟩) (hread : ∀ (z₁ z₂ : Fin g → Bool), (∀ (i : Fin (g - k)), z₁ ⟨k + ↑i, ⋯⟩ = z₂ ⟨k + ↑i, ⋯⟩) → readout z₁ = readout z₂) : (Finset.image f Finset.univ).card ≤ (pendingBiasStates p k).card

Section 9 (Phased-access pending-bias cut bound). If gates before cut k read only the left input X, gates from k onward read only the right input Y, and the readout depends only on gates from k onward, then (pendingBiasStates p k).card is at least the number of distinct rows of f.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_le_card_pendingBiasStates_of_phased_hadamardCode {n g : ℕ} {ι : Type u_1} [Fintype ι] (p : Program signature n g) (enc : (ι → Bool) → (ι → Bool) → Fin n → Bool) (readout : (Fin g → Bool) → Bool) (k : ℕ) (hcomp : ∀ (x y : ι → Bool), readout (p.eval interpretation (enc x y)) = BitString.hadamardCode x y) (hpref : ∀ (j : Fin k) (hj : ↑j < g) (x y : ι → Bool), inputSummary p (enc x y) ⟨↑j, hj⟩ = inputSummary p (enc x fun (x : ι) => false) ⟨↑j, hj⟩) (hsuff : ∀ (i : Fin (g - k)) (x₁ x₂ y : ι → Bool), inputSummary p (enc x₁ y) ⟨k + ↑i, ⋯⟩ = inputSummary p (enc x₂ y) ⟨k + ↑i, ⋯⟩) (hread : ∀ (z₁ z₂ : Fin g → Bool), (∀ (i : Fin (g - k)), z₁ ⟨k + ↑i, ⋯⟩ = z₂ ⟨k + ↑i, ⋯⟩) → readout z₁ = readout z₂) : 2 ^ Fintype.card ι ≤ (pendingBiasStates p k).card

Section 9 (Phased-access pending-bias bound for inner product). Under phased input access across cut k, any threshold program computing hadamardCode has at least 2 ^ Fintype.card ι pending-bias states at cut k.