Gates with arbitrary scalar activations and mixed capacity costs

Every gate of a real-weight program with arbitrary scalar activations ℝ → Bool forms its own scalar block. Given the values of earlier gates, an input-reading gate j applies its activation (p.lines j).op.activate to t + c in its aggregated weighted input sum t, for a constant c collecting the contributions of earlier gates. When its activation changes at most T j times, the gate's block has capacity cost max 1 (4 * T j), while gates with zero aggregated input weights are constant in the input sum and have cost 1.

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.ActivationOp, Cslib.Circuits.Boolean.WeightedThreshold.activationSignature, Cslib.Circuits.Boolean.WeightedThreshold.activationInterpretation: real-weight gates with arbitrary scalar activations ℝ → Bool.
• Cslib.Circuits.Boolean.WeightedThreshold.ofWeightedThreshold: embedding of the weighted threshold signature into the activation signature.
• Cslib.Circuits.Boolean.WeightedThreshold.activationInputWeight, Cslib.Circuits.Boolean.WeightedThreshold.activationGateWeight, Cslib.Circuits.Boolean.WeightedThreshold.activationInputGates: aggregated wire coefficients and input-reading gates.
• Cslib.Circuits.Boolean.WeightedThreshold.activationBlockDecomposition: gate-by-gate scalar block decomposition.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.cost_activationBlockDecomposition: exact cost ∏ j ∈ activationInputGates p, max 1 (4 * T j).
• Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_activations, Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_activations: the C4 mixed activation capacity bound.

References

• S. Schlesinger, Algebraic circuit formalizations in Complexitylib, Threshold/Internal/Activation

theorem Cslib.ChangesAtMost.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {Ψ : α → β} {T : ℕ} (h : ChangesAtMost Ψ T) (G : β → γ) : ChangesAtMost (fun (t : α) => G (Ψ t)) T

Post-composition preserves a change bound.

structure Cslib.Circuits.Boolean.WeightedThreshold.ActivationOp : Type

A real-weight linear-combination operation with an arbitrary scalar activation.

• arity : ℕ

  The number of argument slots.

• weight : Fin self.arity → ℝ

  The coefficient of each argument slot.

• activate : ℝ → Bool

  The scalar activation applied to the weighted sum.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.WeightedThreshold.activationSignature : Signature

The signature of real-weight gates with arbitrary scalar activations.

def Cslib.Circuits.Boolean.WeightedThreshold.activationInterpretation : Interpretation activationSignature Bool

A gate applies its scalar activation to its weighted sum.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.ofWeightedThresholdOp (op : Op) : ActivationOp

A threshold gate is the activation t ↦ decide (threshold ≤ t).

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.ofWeightedThreshold : signature.Hom activationSignature

The weighted threshold basis embeds gate for gate into the activation basis.

instance Cslib.Circuits.Boolean.WeightedThreshold.preserves_ofWeightedThreshold : ofWeightedThreshold.Preserves interpretation activationInterpretation

Embedding a weighted threshold gate into the activation basis preserves its semantics.

def Cslib.Circuits.Boolean.WeightedThreshold.activationLineWeight {n g : ℕ} (line : Line activationSignature n g) (wire : Wire n g) : ℝ

The combined coefficient of an actual wire in an activation line, summing all slots that read it.

theorem Cslib.Circuits.Boolean.WeightedThreshold.sum_activationLineWeight_mul {n g : ℕ} (line : Line activationSignature n g) (values : Wire n g → ℝ) : ∑ a : Fin line.op.arity, line.op.weight a * values (line.wires a) = ∑ wire : Wire n g, activationLineWeight line wire * values wire

Regrouping argument slots by actual wire preserves their weighted sum.

theorem Cslib.Circuits.Boolean.WeightedThreshold.activationLine_eval_eq {n g : ℕ} (line : Line activationSignature n g) (x : Fin n → Bool) (z : Fin g → Bool) : line.eval activationInterpretation x z = line.op.activate (∑ i : Fin n, activationLineWeight line (Wire.input i) * ↑(x i).toNat + ∑ j : Fin g, activationLineWeight line (Wire.gate j) * ↑(z j).toNat)

An activation line's value splits into its aggregated input and gate contributions.

def Cslib.Circuits.Boolean.WeightedThreshold.activationInputWeight {n g : ℕ} (p : Program activationSignature n g) (gate : Fin g) (input : Fin n) : ℝ

The direct coefficient of an original input in an activation-program gate.

def Cslib.Circuits.Boolean.WeightedThreshold.activationGateWeight {n g : ℕ} (p : Program activationSignature n g) (gate prior : Fin g) : ℝ

The coefficient of an internal gate in another gate of an activation program.

theorem Cslib.Circuits.Boolean.WeightedThreshold.eval_activationGate_eq {n g : ℕ} (p : Program activationSignature n g) (x : Fin n → Bool) (gate : Fin g) : p.eval activationInterpretation x gate = (p.lines gate).op.activate (∑ i : Fin n, activationInputWeight p gate i * ↑(x i).toNat + ∑ j : Fin g, activationGateWeight p gate j * ↑(p.eval activationInterpretation x j).toNat)

A native activation-program gate applies its activation to the sum of its aggregated input and gate contributions.

theorem Cslib.Circuits.Boolean.WeightedThreshold.activationGateWeight_eq_zero_of_le {n g : ℕ} (p : Program activationSignature n g) (gate prior : Fin g) (h : gate ≤ prior) : activationGateWeight p gate prior = 0

A gate has zero coefficient on its own output and on later gate outputs.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.activationInputGates {n g : ℕ} (p : Program activationSignature n g) : Finset (Fin g)

The gates of an activation program with a nonzero aggregated direct-input coefficient.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.mem_activationInputGates {n g : ℕ} (p : Program activationSignature n g) (gate : Fin g) : gate ∈ activationInputGates p ↔ ∃ (i : Fin n), activationInputWeight p gate i ≠ 0

theorem Cslib.Circuits.Boolean.WeightedThreshold.activationInputWeight_eq_zero_of_not_mem {n g : ℕ} (p : Program activationSignature n g) {gate : Fin g} (h : gate ∉ activationInputGates p) (i : Fin n) : activationInputWeight p gate i = 0

Every input coefficient vanishes at a gate outside activationInputGates p.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.activationBlockDecomposition {n g : ℕ} (p : Program activationSignature n g) (readout : (Fin g → Bool) → Bool) (T : Fin g → ℕ) (hT : ∀ j ∈ activationInputGates p, ChangesAtMost (p.lines j).op.activate (T j)) : BlockDecomposition (fun (x : BitString n) => readout (p.eval activationInterpretation x)) (Fin g → Bool)

Revealing the gate evaluation of an activation program one gate at a time gives a scalar block decomposition with per-gate change bounds T.

theorem Cslib.Circuits.Boolean.WeightedThreshold.cost_activationBlockDecomposition {n g : ℕ} (p : Program activationSignature n g) (readout : (Fin g → Bool) → Bool) (T : Fin g → ℕ) (hT : ∀ j ∈ activationInputGates p, ChangesAtMost (p.lines j).op.activate (T j)) : (activationBlockDecomposition p readout T hT).cost = ∏ j ∈ activationInputGates p, max 1 (4 * T j)

Each input-reading gate j costs max 1 (4 * T j), and every other gate costs 1.

theorem Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_of_activations {n g : ℕ} (p : Program activationSignature n g) (readout : (Fin g → Bool) → Bool) {f : BooleanFunction n} {K : ℕ} (T : Fin g → ℕ) (hT : ∀ j ∈ activationInputGates p, ChangesAtMost (p.lines j).op.activate (T j)) (hreadout : ∀ (x : Fin n → Bool), readout (p.eval activationInterpretation x) = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * ∏ j ∈ activationInputGates p, max 1 (4 * T j)

C4: mixed activation gate costs. If an activation program computes f through a Boolean readout of its gate values, and each input-reading gate j has activation changing at most T j times, then 2 ^ n < 4 * K ^ 2 * ∏ j ∈ activationInputGates p, max 1 (4 * T j).

theorem Cslib.Circuits.Boolean.WeightedThreshold.circuit_two_pow_lt_of_activations {n : ℕ} (c : Circuit activationSignature n 1) (houtput : ∃ (gate : Fin c.size), c.outputs 0 = Wire.gate gate) {f : BooleanFunction n} {K : ℕ} (T : Fin c.size → ℕ) (hT : ∀ j ∈ activationInputGates c.program, ChangesAtMost (c.program.lines j).op.activate (T j)) (hcomputes : ∀ (x : Fin n → Bool), c.eval activationInterpretation x 0 = f x) (hf : ∀ (b : Bool), Frontier.RectangleFree {x : Fin n → Bool | f x = b} K) : 2 ^ n < 4 * K ^ 2 * ∏ j ∈ activationInputGates c.program, max 1 (4 * T j)

The C4 mixed-activation bound for a single-output circuit whose output selects a gate.