Capacity of scalar blocks and finite summaries

A block decomposition describes a Boolean function through successive histories. A scalar block updates the history from a real weighted sum, with a uniform bound on changes. A summary block depends on the first side of every coordinate split through finitely many summary values. This semantic decomposition uses no separate circuit representation or evaluator.

The capacity cost multiplies the costs of the blocks: 4T for a scalar block with T > 0 changes, 1 for zero changes, and V for a summary with V values. If both Boolean fibers are K-rectangle-free for every coordinate split, then 2 ^ n < 4 * K ^ 2 * cost.

The proof preserves a rectangle where history depends only on the second side. Sorted grouping shrinks its sides by 2T and 2 for a changing scalar block; a summary keeps a largest fiber. Zero-change blocks shrink neither side. The final Boolean output costs at most another factor of two on the second side. Integer division is retained at every step.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.BlockKind: scalar and finite-summary blocks.
• Cslib.Circuits.Boolean.WeightedThreshold.BlockDecomposition: a semantic block decomposition.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.BlockDecomposition.two_pow_lt_mul_cost: the capacity lower bound for a function with two rectangle-free Boolean fibers.

References

• [S. Schlesinger, Algebraic circuit formalization, Threshold/Defs and Internal/Capacity] [Sch26a]

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.WeightedThreshold.weightedSum {n : ℕ} (w : Fin n → ℝ) (x : Fin n → Bool) : ℝ

The weighted sum ∑ i, w i * (x i).toNat of a Boolean input x with real weights w.

inductive Cslib.Circuits.Boolean.WeightedThreshold.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 Cslib.Circuits.Boolean.WeightedThreshold.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.

def Cslib.Circuits.Boolean.WeightedThreshold.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. Here glue denotes the inverse of Equiv.piEquivPiSubtypeProd for the split.

structure Cslib.Circuits.Boolean.WeightedThreshold.BlockDecomposition {n : ℕ} (f : 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 Cslib.Circuits.Boolean.WeightedThreshold.BlockDecomposition.cost {n : ℕ} {f : 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.

theorem Cslib.Circuits.Boolean.WeightedThreshold.BlockDecomposition.two_pow_lt_mul_cost {n : ℕ} {f : BooleanFunction n} {H : Type u_1} {K : ℕ} (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) (D : BlockDecomposition f H) : 2 ^ n < 4 * K ^ 2 * D.cost

Theorem U (one-dimensional capacity). If f is two-sided K-rectangle-free, every block decomposition of f has 2ⁿ < 4 K² · cost.