Threshold circuits -- proof internals

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

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

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

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

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

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

def Complexity.Basis.andOrToThresholdHomInternal : unboundedAndOr.Hom threshold

Proof-internal exact embedding of unbounded AND/OR into threshold gates.

Equations

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