Weighted threshold programs and one-dimensional capacity

This file fixes the definitions of the one-dimensional capacity method for threshold circuits of unbounded depth.

Rectangles

TwoSidedRectangleFree f K says that under every split of the coordinates into U and its complement, every rectangle P × Q on which f is constant (with either value) has a side with fewer than K elements. The one-sided Cutwidth.RectangleFree only excludes rectangles on which f is identically 1.

Change counts

ChangesAtMost Ψ T is the discrete form of "Ψ : ℝ → β has at most T + 1 interval pieces": along every nondecreasing sequence of reals, the value of Ψ changes at most T times. A threshold function t ↦ [λ t + c ≥ 0] changes at most once, and a multilevel threshold function with T transitions changes at most T times. PiecesAtMost Φ M is the constructive form used for runs of threshold gates: Φ is constant on the level sets of a monotone rank function with fewer than M values.

Threshold programs

Program n s is a straight-line program of s weighted threshold gates on n Boolean inputs, with arbitrary real weights, arbitrary depth, and arbitrary fan-in and fan-out. Gate j reads every input x i with weight inputWeight j i and every earlier gate k < j with weight gateWeight j k, and outputs 1 exactly when its weighted sum plus bias j is nonnegative. Integer weights are a special case. Booleans enter the sums as 0 and 1. A gate is input-reading when its input weight vector is nonzero (Program.inputGates); gates that read only other gates are not counted by the bounds of this development.

Program.evalFrom evaluates the gates when some gates are overridden by given values and the other gates receive arbitrary real input contributions in place of their weighted input sums; the ordinary evaluation Program.eval overrides nothing and uses the true weighted sums. The override form expresses a run of gates as a function of one real parameter.

ActivationProgram n s replaces the threshold of each gate by an arbitrary activation ℝ → Bool applied to the weighted sum of its inputs and earlier gates. A threshold gate is the activation t ↦ [t + bias ≥ 0], which changes once; exact-threshold, interval, symmetric, and modular gates on weighted sums change finitely often, at mixed costs.

Block decompositions

A BlockDecomposition f H presents f as the output of a sequence of histories history i : {0,1}ⁿ → H, starting from a constant one. Each step is one-dimensional (the next history is a function of the previous one and of a single weighted sum ⟨w, x⟩, with at most T changes in the weighted sum for each previous history) or a summary (under every split, the next history depends on the first side only through a value with at most V possibilities). Its cost multiplies 4T over the one-dimensional steps with T ≥ 1 and V over the summary steps.

def Algebraic.Threshold.TwoSidedRectangleFree {n : ℕ} (f : Cslib.BooleanFunction n) (K : ℕ) : Prop

f is two-sided K-rectangle-free when, under every split of the coordinates into U and its complement, every rectangle P × Q on which f is constant has a side with fewer than K elements.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Threshold.ChangesAtMost {β : Type u_1} (Ψ : ℝ → β) (T : ℕ) : Prop

Ψ changes at most T times: along every nondecreasing sequence z of reals, every set of positions i with Ψ (z i) ≠ Ψ (z (i + 1)) has at most T elements. This is the discrete form of having at most T + 1 interval pieces.

Equations

• Algebraic.Threshold.ChangesAtMost Ψ T = ∀ (z : ℕ → ℝ), Monotone z → ∀ (S : Finset ℕ), (∀ i ∈ S, Ψ (z i) ≠ Ψ (z (i + 1))) → S.card ≤ T

def Algebraic.Threshold.PiecesAtMost {β : Type u_1} (Φ : ℝ → β) (M : ℕ) : Prop

Φ has at most M pieces: it is constant on the level sets of a monotone rank function π : ℝ → ℕ with values below M. The level sets are intervals.

Equations

• Algebraic.Threshold.PiecesAtMost Φ M = ∃ (π : ℝ → ℕ), Monotone π ∧ (∀ (t : ℝ), π t < M) ∧ ∀ (t t' : ℝ), π t = π t' → Φ t = Φ t'

def Algebraic.Threshold.weightedSum {n : ℕ} (w : Fin n → ℝ) (x : Fin n → Bool) : ℝ

The real weighted sum ∑ i, w i * x i of the bits of x, read as 0 and 1.

Equations

• Algebraic.Threshold.weightedSum w x = ∑ i : Fin n, w i * ↑(x i).toNat

structure Algebraic.Threshold.Program (n s : ℕ) : Type

A weighted real threshold straight-line program with n inputs and s gates. Gate j reads every input and every earlier gate, with arbitrary real weights; depth and fan-out are unrestricted.

• inputWeight : Fin s → Fin n → ℝ

  The weight of input i in gate j (inputWeight j i).

• gateWeight : Fin s → Fin s → ℝ

  The weight of gate k in gate j (gateWeight j k); only the entries with k < j are read.

• bias : Fin s → ℝ

  The bias of gate j.

• output : Fin s

  The output gate.

@[irreducible]

noncomputable def Algebraic.Threshold.Program.evalFrom {n s : ℕ} (C : Program n s) (fixed : Finset (Fin s)) (η : Fin s → Bool) (z : Fin s → ℝ) (j : Fin s) : Bool

The gate values when every gate in fixed takes the value given by η, and every other gate j receives the real input contribution z j in place of its weighted input sum: such a gate is 1 exactly when z j + ∑_{k < j} gateWeight j k * (gate k) + bias j ≥ 0.

Equations

• C.evalFrom fixed η z j = if j ∈ fixed then η j else decide (0 ≤ (z j + ∑ k : Fin s, if _h : k < j then C.gateWeight j k * ↑(C.evalFrom fixed η z k).toNat else 0) + C.bias j)

noncomputable def Algebraic.Threshold.Program.eval {n s : ℕ} (C : Program n s) (x : Fin n → Bool) : Fin s → Bool

The gate values of the program on the input x: gate j is 1 exactly when ∑ i, inputWeight j i * x i + ∑_{k < j} gateWeight j k * (gate k) + bias j ≥ 0.

Equations

• C.eval x = C.evalFrom ∅ (fun (x : Fin s) => false) fun (j : Fin s) => Algebraic.Threshold.weightedSum (C.inputWeight j) x

def Algebraic.Threshold.Program.Computes {n s : ℕ} (C : Program n s) (f : Cslib.BooleanFunction n) : Prop

The program computes f at its output gate.

Equations

• C.Computes f = ∀ (x : Fin n → Bool), C.eval x C.output = f x

noncomputable def Algebraic.Threshold.Program.inputGates {n s : ℕ} (C : Program n s) : Finset (Fin s)

The input-reading gates: those with a nonzero input weight vector.

Equations

• C.inputGates = {j : Fin s | C.inputWeight j ≠ 0}

structure Algebraic.Threshold.Program.DirectionRuns {n s : ℕ} (C : Program n s) (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 s → ℕ

  The run of each gate.

• monotone : Monotone self.run

  Runs are consecutive in the gate order.

• run_lt (j : Fin s) : self.run j < B

  There are at most B runs.

• dir : ℕ → Fin n → ℝ

  The direction of each run.

• along (j : Fin s) : ∃ (c : ℝ), C.inputWeight j = c • self.dir (self.run j)

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

noncomputable def Algebraic.Threshold.Program.DirectionRuns.size {n s : ℕ} {C : Program n s} {B : ℕ} (R : C.DirectionRuns B) (i : ℕ) : ℕ

The number of input-reading gates in run i.

Equations

• R.size i = {j ∈ C.inputGates | R.run j = i}.card

structure Algebraic.Threshold.ActivationProgram (n s : ℕ) : Type

A straight-line program of s gates with arbitrary activations on n Boolean inputs: gate j outputs activation j (∑ i, inputWeight j i * x i + ∑_{k < j} gateWeight j k * (gate k)). Weights are arbitrary reals; depth and fan-out are unrestricted.

• inputWeight : Fin s → Fin n → ℝ

  The weight of input i in gate j (inputWeight j i).

• gateWeight : Fin s → Fin s → ℝ

  The weight of gate k in gate j (gateWeight j k); only the entries with k < j are read.

• activation : Fin s → ℝ → Bool

  The activation of gate j, applied to its weighted sum.

• output : Fin s

  The output gate.

@[irreducible]

noncomputable def Algebraic.Threshold.ActivationProgram.eval {n s : ℕ} (C : ActivationProgram n s) (x : Fin n → Bool) (j : Fin s) : Bool

The gate values of the program on the input x.

Equations

• C.eval x j = C.activation j (Algebraic.Threshold.weightedSum (C.inputWeight j) x + ∑ k : Fin s, if _h : k < j then C.gateWeight j k * ↑(C.eval x k).toNat else 0)

def Algebraic.Threshold.ActivationProgram.Computes {n s : ℕ} (C : ActivationProgram n s) (f : Cslib.BooleanFunction n) : Prop

The program computes f at its output gate.

Equations

• C.Computes f = ∀ (x : Fin n → Bool), C.eval x C.output = f x

noncomputable def Algebraic.Threshold.ActivationProgram.inputGates {n s : ℕ} (C : ActivationProgram n s) : Finset (Fin s)

The input-reading gates: those with a nonzero input weight vector.

Equations

• C.inputGates = {j : Fin s | C.inputWeight j ≠ 0}

inductive Algebraic.Threshold.BlockKind : Type

The kind of a block in a block decomposition.

• oneDim (T : ℕ) : BlockKind

  A one-dimensional block whose value changes at most T times along its weighted sum.

• summary (V : ℕ) : BlockKind

  A summary block, depending on the first side of every split through at most V values.

def Algebraic.Threshold.BlockKind.cost : BlockKind → ℕ

The capacity cost of a block: 4T for a one-dimensional block with T ≥ 1 changes, 1 for one without changes, and V for a summary block.

Equations

• (Algebraic.Threshold.BlockKind.oneDim T).cost = if T = 0 then 1 else 4 * T
• (Algebraic.Threshold.BlockKind.summary V).cost = V

def Algebraic.Threshold.BlockKind.Step {n : ℕ} {H : Type u_1} : BlockKind → ((Fin n → Bool) → H) → ((Fin n → Bool) → H) → Prop

A step of kind κ from the history prev to the history next.

• One-dimensional with T changes: for some weight vector w and some Φ, next x = Φ (prev x) ⟨w, x⟩, where every Φ η changes at most T times.
• Summary with V values: for every split U, some σ on the first side with V values and some Φ satisfy next (glue U p q) = Φ (prev (glue U p q)) (σ p) q.

Equations

• One or more equations did not get rendered due to their size.

structure Algebraic.Threshold.BlockDecomposition {n : ℕ} (f : Cslib.BooleanFunction n) (H : Type u_1) : Type u_1

A decomposition of f into blocks: histories history 0, …, history length, the first constant, each obtained from the previous one by a step of the given kind, and f read off the last history.

• length : ℕ

  The number of blocks.

• kind : ℕ → BlockKind

  The kind of each block.

• history : ℕ → (Fin n → Bool) → H

  The history after the first i blocks.

• output : H → Bool

  The output read from the final history.

• history_zero (x y : Fin n → Bool) : self.history 0 x = self.history 0 y

  Before any block, the history is constant.

• step (i : ℕ) : i < self.length → (self.kind i).Step (self.history i) (self.history (i + 1))

  Each block is a step of its kind.

• output_history (x : Fin n → Bool) : self.output (self.history self.length x) = f x

  The final history determines f.

def Algebraic.Threshold.BlockDecomposition.cost {n : ℕ} {f : Cslib.BooleanFunction n} {H : Type u_1} (D : BlockDecomposition f H) : ℕ

The capacity cost of a block decomposition: the product of the costs of its blocks.

Equations

• D.cost = ∏ i ∈ Finset.range D.length, (D.kind i).cost