Documentation

Complexitylib.Circuits.Majority

Strict-majority circuits #

This module packages the unary threshold fragment as a typed fan-in-two AND/OR circuit. On n inputs it uses exactly 3 + 2 * n * (n / 2 + 1) gates and returns true exactly when strictly more than half of its inputs are true.

source
theorem Complexity.CircuitCode.strictMajorityThreshold_le (inputCount : ℕ) [NeZero inputCount] :
strictMajorityThreshold inputCount ≤ inputCount

A strict-majority threshold never exceeds a positive input count.

source
@[simp]
theorem Complexity.CircuitCode.length_strictMajorityRawCircuit (inputCount : ℕ) :
List.length (strictMajorityRawCircuit inputCount) = 3 + 2 * inputCount * strictMajorityThreshold inputCount

Exact raw gate count for the strict-majority construction.

source
theorem Complexity.CircuitCode.strictMajorityRawCircuit_wellFormed (inputCount : ℕ) [NeZero inputCount] :
RawCircuit.WellFormed inputCount (strictMajorityRawCircuit inputCount)

The raw strict-majority construction is a valid single-output circuit at every positive input arity.

source
noncomputable def Complexity.Circuit.strictMajority (inputCount : ℕ) [NeZero inputCount] :
Circuit Basis.andOr2 inputCount 1 (List.length (CircuitCode.strictMajorityRawCircuit inputCount) - 1)

Typed fan-in-two strict-majority circuit reconstructed from the verified raw threshold fragment.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.Circuit.size_strictMajority (inputCount : ℕ) [NeZero inputCount] :
    (strictMajority inputCount).size = 3 + 2 * inputCount * CircuitCode.strictMajorityThreshold inputCount

    Exact size of the typed strict-majority circuit.

    source
    theorem Complexity.Circuit.eval_strictMajority (inputCount : ℕ) [NeZero inputCount] (input : BitString inputCount) :
    (strictMajority inputCount).eval input 0 = decide (CircuitCode.strictMajorityThreshold inputCount ≤ Fin.countP input)

    The typed circuit returns the unary-count strict-majority predicate.