Scalar-block and direction-run capacity of native weighted threshold programs

A native program gives a block decomposition by revealing its gate values in topological order. The history is its existing gate evaluation, masked to the gates already processed. Each gate with a nonzero effective coefficient on an original input has capacity cost four. Every other gate has cost one, even when its output changes with earlier gate values. Repeated argument wires are counted through their aggregated coefficients, so cancelling input weights do not create an input-reading block.

More generally, when the gates are partitioned into B consecutive runs along single input directions (DirectionRuns), for each fixed valuation of the gates in preceding runs, run i with rᵢ input-reading gates has at most 2 ^ rᵢ pieces as a function of its shared directional projection (piecesAtMost_evalFrom), forming a one-dimensional block with at most 2 ^ rᵢ - 1 changes and cost at most 4 · 2 ^ rᵢ. This yields 2 ^ n < 16 * K ^ 2 * 2 ^ |inputGates| (C2) and the B-run bound 2 ^ n < 4 * K ^ 2 * 4 ^ B * 2 ^ |inputGates| (C3), alongside the multilevel threshold transition bound 2 ^ n < 4 * K ^ 2 * max 1 (4 * T) (C2′).

The resulting capacity bounds apply to any fixed Boolean readout of the gate values. The single-output circuit corollaries require that the output wire selects a gate: an original-input wire is not part of this readout.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.blockDecomposition: a native program as scalar blocks.
• Cslib.Circuits.Boolean.WeightedThreshold.evalFrom: gate evaluation with fixed overrides and parametric input contributions.
• Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns: a partition of the gates into consecutive runs along single input directions, with DirectionRuns.toBlockDecomposition.
• Cslib.Circuits.Boolean.WeightedThreshold.multilevelDecomposition: a multilevel threshold representation F (∑ i, w i * (x i).toNat) as a single scalar block.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.cost_blockDecomposition: exact cost 4 ^ |inputGates|.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_four_pow_inputGates, Cslib.Circuits.Boolean.WeightedThreshold.lt_two_mul_add_two_mul_inputGates: the C1 bounds.
• Cslib.Circuits.Boolean.WeightedThreshold.piecesAtMost_evalFrom, Cslib.Circuits.Boolean.WeightedThreshold.changesAtMost_evalFrom: Lemma 2 (at most 2 ^ r pieces and 2 ^ r - 1 changes for a directional run of r active gates with fixed prior gates).
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_direction, Cslib.Circuits.Boolean.WeightedThreshold.lt_of_direction: the C2 single-direction bounds.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_runs, Cslib.Circuits.Boolean.WeightedThreshold.lt_of_runs: the C3 direction-run bounds.
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_multilevel, Cslib.Circuits.Boolean.WeightedThreshold.two_pow_sub_lt_of_multilevel: the C2′ multilevel threshold bounds.

References

• S. Schlesinger, Algebraic circuit formalizations in Complexitylib, Threshold and its internal lemmas

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.blockDecomposition {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) : BlockDecomposition (fun (x : BitString n) => readout (p.eval interpretation x)) (Fin g → Bool)

Revealing the existing gate evaluation one gate at a time gives a scalar block decomposition. The output may be any fixed Boolean readout of the gate values.

theorem Cslib.Circuits.Boolean.WeightedThreshold.cost_blockDecomposition {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) : (blockDecomposition p readout).cost = 4 ^ (inputGates p).card

Every effective input-reading gate costs four, and every other gate costs one.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_four_pow_inputGates {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) : 2 ^ n < 4 * K ^ 2 * 4 ^ (inputGates p).card

C1 capacity bound. Any Boolean readout of a weighted program's gate values computing a function whose two fibers are K-rectangle-free satisfies this input-reading-gate bound.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_mul_four_pow_inputGates {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) : 2 ^ n < 4 * K ^ 2 * 4 ^ (inputGates c.program).card

The C1 bound for a single-output circuit whose output selects a gate.

Parametric gate evaluation and piece bounds (Lemma 2)

@[irreducible]

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.evalFrom {n g : ℕ} (p : Program signature n g) (fixed : Finset (Fin g)) (η : Fin g → Bool) (z : Fin g → ℝ) (gate : Fin g) : Bool

The gate values when every gate in fixed takes the value given by η, and every other gate gate receives the real input contribution z gate in place of its weighted input sum.

theorem Cslib.Circuits.Boolean.WeightedThreshold.evalFrom_eq {n g : ℕ} (p : Program signature n g) (fixed : Finset (Fin g)) (η : Fin g → Bool) (z : Fin g → ℝ) (gate : Fin g) : evalFrom p fixed η z gate = if gate ∈ fixed then η gate else decide ((p.lines gate).op.threshold ≤ z gate + ∑ prior : Fin g, if prior < gate then gateWeight p gate prior * ↑(evalFrom p fixed η z prior).toNat else 0)

theorem Cslib.Circuits.Boolean.WeightedThreshold.evalFrom_eq_eval {n g : ℕ} (p : Program signature n g) {fixed : Finset (Fin g)} {η : Fin g → Bool} {z : Fin g → ℝ} {x : Fin n → Bool} (gate : Fin g) (hfix : ∀ prior ≤ gate, prior ∈ fixed → η prior = p.eval interpretation x prior) (hz : ∀ prior ≤ gate, prior ∉ fixed → z prior = ∑ i : Fin n, inputWeight p prior i * ↑(x i).toNat) : evalFrom p fixed η z gate = p.eval interpretation x gate

Overriding gates by their true values and feeding the other gates their true weighted input sums recovers the ordinary evaluation, gate by gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.piecesAtMost_evalFrom {n g : ℕ} (p : Program signature n g) (fixed : Finset (Fin g)) (η : Fin g → Bool) (slope : Fin g → ℝ) : PiecesAtMost (fun (t : ℝ) => evalFrom p fixed η fun (gate : Fin g) => slope gate * t) (2 ^ {gate : Fin g | gate ∉ fixed ∧ slope gate ≠ 0}.card)

Lemma 2 (pieces of a run). If every gate outside fixed receives the input contribution slope gate * t, and the gates in fixed are set by η, the gate values have at most 2 ^ r pieces as functions of t, where r counts the gates outside fixed with a nonzero slope.

theorem Cslib.Circuits.Boolean.WeightedThreshold.changesAtMost_evalFrom {n g : ℕ} (p : Program signature n g) (fixed : Finset (Fin g)) (η : Fin g → Bool) (slope : Fin g → ℝ) : ChangesAtMost (fun (t : ℝ) => evalFrom p fixed η fun (gate : Fin g) => slope gate * t) (2 ^ {gate : Fin g | gate ∉ fixed ∧ slope gate ≠ 0}.card - 1)

Lemma 2, change form. The same run of gates changes at most 2 ^ r - 1 times.

Direction runs and block decompositions

structure Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns {n g : ℕ} (p : Program signature n g) (B : ℕ) : Type

A split of the gates into B consecutive runs, numbered by the monotone map run, such that every gate of run i reads the inputs along the direction dir i: its input weight vector is a real multiple of dir i. A gate that reads no input fits every direction.

• run : Fin g → ℕ

  The run of each gate.

• monotone : Monotone self.run

  Runs are consecutive in the gate order.

• run_lt (gate : Fin g) : self.run gate < B

  There are at most B runs.

• dir : ℕ → Fin n → ℝ

  The direction of each run.

• along (gate : Fin g) : ∃ (c : ℝ), inputWeight p gate = c • self.dir (self.run gate)

  Every gate reads the inputs along the direction of its run.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns.size {n g : ℕ} {p : Program signature n g} {B : ℕ} (R : DirectionRuns p B) (i : ℕ) : ℕ

The number of input-reading gates in run i.

theorem Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns.sum_size {n g : ℕ} {p : Program signature n g} {B : ℕ} (R : DirectionRuns p B) : ∑ i ∈ Finset.range B, R.size i = (inputGates p).card

def Cslib.Circuits.Boolean.WeightedThreshold.gateRuns {n g : ℕ} (p : Program signature n g) : DirectionRuns p g

The split of the gates into single-gate runs, each along its own input weight vector.

def Cslib.Circuits.Boolean.WeightedThreshold.singleRun {n g : ℕ} (p : Program signature n g) (w : Fin n → ℝ) (along : ∀ (gate : Fin g), ∃ (c : ℝ), inputWeight p gate = c • w) : DirectionRuns p 1

The single run of a program whose input weight vectors are all multiples of w.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns.slope {n g : ℕ} {p : Program signature n g} {B : ℕ} (R : DirectionRuns p B) (i : ℕ) (gate : Fin g) : ℝ

The slope of a gate of run i along the direction of the run, and zero elsewhere.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns.toBlockDecomposition {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {B : ℕ} (R : DirectionRuns p B) : BlockDecomposition (fun (x : BitString n) => readout (p.eval interpretation x)) (Fin g → Bool)

The block decomposition of a program along a split into direction runs: the history after i blocks holds the values of the gates of the first i runs, and the output applies readout to the complete gate valuation.

theorem Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns.cost_toBlockDecomposition {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {B : ℕ} (R : DirectionRuns p B) : (toBlockDecomposition p readout R).cost = ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost

Capacity and logarithmic corollaries (C1, C2, C3, C2′)

theorem Cslib.Circuits.Boolean.WeightedThreshold.cost_oneDim_le_four_pow (r : ℕ) : (BlockKind.oneDim (2 ^ r - 1)).cost ≤ 4 ^ r

theorem Cslib.Circuits.Boolean.WeightedThreshold.cost_oneDim_le_four_mul (r : ℕ) : (BlockKind.oneDim (2 ^ r - 1)).cost ≤ 4 * 2 ^ r

theorem Cslib.Circuits.Boolean.WeightedThreshold.cost_oneDim_eq_max (T : ℕ) : (BlockKind.oneDim T).cost = max 1 (4 * T)

theorem Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns.prod_cost_le_four_pow {n g : ℕ} {p : Program signature n g} {B : ℕ} (R : DirectionRuns p B) : ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost ≤ 4 ^ (inputGates p).card

theorem Cslib.Circuits.Boolean.WeightedThreshold.DirectionRuns.prod_cost_le_four_pow_mul {n g : ℕ} {p : Program signature n g} {B : ℕ} (R : DirectionRuns p B) : ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost ≤ 4 ^ B * 2 ^ (inputGates p).card

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_directionRuns {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {B : ℕ} (R : DirectionRuns p B) {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) : 2 ^ n < 4 * K ^ 2 * ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost

Theorem U for threshold programs. Split the gates of a threshold program into B consecutive runs along single directions, with rᵢ input-reading gates in run i. Then 2 ^ n < 4 * K ^ 2 * ∏ i, cᵢ, where cᵢ = 4 * (2 ^ rᵢ - 1) if rᵢ ≥ 1 and cᵢ = 1 otherwise.

theorem Cslib.Circuits.Boolean.WeightedThreshold.lt_two_mul_add_two_mul_inputGates {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K k : ℕ} (hK : K ≤ 2 ^ 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) : n < 2 * k + 2 + 2 * (inputGates p).card

C1, logarithmic form. With K ≤ 2 ^ k, every threshold program computing f has n < 2 * k + 2 + 2 * |inputGates p|.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_two_mul_add_two_mul_inputGates {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {f : BooleanFunction n} {K k : ℕ} (hK : K ≤ 2 ^ 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) : n < 2 * k + 2 + 2 * (inputGates c.program).card

The logarithmic C1 bound for a single-output circuit whose output selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_direction {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (w : Fin n → ℝ) (along : ∀ (gate : Fin g), ∃ (c : ℝ), inputWeight p gate = c • w) {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) : 2 ^ n < 16 * K ^ 2 * 2 ^ (inputGates p).card

C2: one direction. If every input weight vector of a threshold program computing f is a real multiple of one vector w, then 2 ^ n < 16 * K ^ 2 * 2 ^ |inputGates p|.

theorem Cslib.Circuits.Boolean.WeightedThreshold.lt_of_direction {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) (w : Fin n → ℝ) (along : ∀ (gate : Fin g), ∃ (c : ℝ), inputWeight p gate = c • w) {f : BooleanFunction n} {K k : ℕ} (hK : K ≤ 2 ^ 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) : n < 2 * k + 4 + (inputGates p).card

C2, logarithmic form. With K ≤ 2 ^ k, a threshold program computing f whose input weight vectors are all multiples of one vector has n < 2 * k + 4 + |inputGates p|.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_direction {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (w : Fin n → ℝ) (along : ∀ (gate : Fin c.size), ∃ (a : ℝ), inputWeight c.program gate = a • w) {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) : 2 ^ n < 16 * K ^ 2 * 2 ^ (inputGates c.program).card

The C2 single-direction bound for a single-output circuit whose output selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_of_direction {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) (w : Fin n → ℝ) (along : ∀ (gate : Fin c.size), ∃ (a : ℝ), inputWeight c.program gate = a • w) {f : BooleanFunction n} {K k : ℕ} (hK : K ≤ 2 ^ 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) : n < 2 * k + 4 + (inputGates c.program).card

The logarithmic C2 single-direction bound for a single-output circuit whose output selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_runs {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {B : ℕ} (R : DirectionRuns p B) {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) : 2 ^ n < 4 * K ^ 2 * 4 ^ B * 2 ^ (inputGates p).card

C3: direction runs. If the gates of a threshold program computing f split into B consecutive runs along single directions, then 2 ^ n < 4 * K ^ 2 * 4 ^ B * 2 ^ |inputGates p|.

theorem Cslib.Circuits.Boolean.WeightedThreshold.lt_of_runs {n g : ℕ} (p : Program signature n g) (readout : (Fin g → Bool) → Bool) {B : ℕ} (R : DirectionRuns p B) {f : BooleanFunction n} {K k : ℕ} (hK : K ≤ 2 ^ 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) : n < 2 * k + 2 + 2 * B + (inputGates p).card

C3, logarithmic form. With K ≤ 2 ^ k and B direction runs, n < 2 * k + 2 + 2 * B + |inputGates p|.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_runs {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {B : ℕ} (R : DirectionRuns c.program B) {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) : 2 ^ n < 4 * K ^ 2 * 4 ^ B * 2 ^ (inputGates c.program).card

The C3 direction-run bound for a single-output circuit whose output selects a gate.

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_lt_of_runs {n : ℕ} (c : Circuit signature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {B : ℕ} (R : DirectionRuns c.program B) {f : BooleanFunction n} {K k : ℕ} (hK : K ≤ 2 ^ 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) : n < 2 * k + 2 + 2 * B + (inputGates c.program).card

The logarithmic C3 direction-run bound for a single-output circuit whose output selects a gate.

def Cslib.Circuits.Boolean.WeightedThreshold.multilevelDecomposition {n : ℕ} {f : BooleanFunction n} (w : Fin n → ℝ) (F : ℝ → Bool) {T : ℕ} (hF : ChangesAtMost F T) (hfF : ∀ (x : BitString n), f x = F (∑ i : Fin n, w i * ↑(x i).toNat)) : BlockDecomposition f Bool

The one-block decomposition of a multilevel threshold function F (∑ i, w i * (x i).toNat).

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_multilevel {n : ℕ} {f : BooleanFunction n} {K : ℕ} (w : Fin n → ℝ) (F : ℝ → Bool) {T : ℕ} (hF : ChangesAtMost F T) (hfF : ∀ (x : BitString n), f x = F (∑ i : Fin n, w i * ↑(x i).toNat)) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * max 1 (4 * T)

C2′: multilevel threshold representations. If f x = F (∑ i, w i * (x i).toNat) for a function F changing at most T times, then 2 ^ n < 4 * K ^ 2 * max 1 (4 * T).

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_sub_lt_of_multilevel {n : ℕ} {f : BooleanFunction n} {K k : ℕ} (hK : K ≤ 2 ^ k) (w : Fin n → ℝ) (F : ℝ → Bool) {T : ℕ} (hF : ChangesAtMost F T) (hfF : ∀ (x : BitString n), f x = F (∑ i : Fin n, w i * ↑(x i).toNat)) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (hn : 2 * k + 4 ≤ n) : 2 ^ (n - (2 * k + 4)) < T

C2′, logarithmic form. With K ≤ 2 ^ k and 2 * k + 4 ≤ n, a multilevel threshold representation f x = F (∑ i, w i * (x i).toNat) needs more than 2 ^ (n - (2 * k + 4)) transitions.