Documentation

Complexitylib.Circuits.Threshold

Threshold circuits #

Basis.threshold consists of unbounded-fan-in unweighted threshold gates. Cutoff zero is constant true, cutoff one is disjunction, cutoff equal to fan-in is conjunction, and cutoff n / 2 + 1 is strict majority.

The exact basis map Basis.andOrToThresholdHom shows that every unbounded AND/OR circuit becomes a threshold circuit without changing wiring, size, depth, negation flags, or semantics.

source
theorem Complexity.ThresholdOp.trueCount_le_arity {n : ℕ} (inputs : BitString n) :
trueCount inputs ≤ n

A true-input count never exceeds gate arity.

source
theorem Complexity.ThresholdOp.eval_conjunction (n : ℕ) (inputs : BitString n) :
(conjunction n).eval n inputs = AndOrOp.and.eval n inputs

Cutoff equal to fan-in computes conjunction.

source
theorem Complexity.ThresholdOp.eval_disjunction (n : ℕ) (inputs : BitString n) :
disjunction.eval n inputs = AndOrOp.or.eval n inputs

Cutoff one computes disjunction, including false at arity zero.

source
theorem Complexity.ThresholdOp.eval_majority (n : ℕ) (inputs : BitString n) :
(majority n).eval n inputs = decide (n / 2 < Fin.countP inputs)

The designated majority operation is strict majority: more than half of the inputs must be true.

source
theorem Complexity.ThresholdOp.eval_zero (n : ℕ) (inputs : BitString n) :
{ cutoff := 0 }.eval n inputs = true

Cutoff zero is the constant-true operation.

source
theorem Complexity.ThresholdOp.eval_of_arity_lt {cutoff n : ℕ} (hcutoff : n < cutoff) (inputs : BitString n) :
{ cutoff := cutoff }.eval n inputs = false

A cutoff strictly larger than arity is constant false.

source
def Complexity.Basis.andOrToThresholdHom :
unboundedAndOr.Hom threshold

Exact, arity-dependent embedding of unbounded AND/OR into threshold gates.

Equations
Instances For