Circuits for comparison with a fixed numerical threshold

The first input bit is the most significant bit. An interior threshold on n bits has a constant-free AND/OR expression with at most n - 1 gates. The two endpoint thresholds are represented by Boolean constants.

def Algebraic.DeMorgan.inputRank {n : ℕ} : (Fin n → Bool) → ℕ

Interpret a Boolean input as a natural number, most significant bit first.

Equations

• Algebraic.DeMorgan.inputRank x_2 = 0
• Algebraic.DeMorgan.inputRank input = (if input 0 = true then 2 ^ n else 0) + Algebraic.DeMorgan.inputRank (Fin.tail input)

theorem Algebraic.DeMorgan.inputRank_lt {n : ℕ} (input : Fin n → Bool) : inputRank input < 2 ^ n

Input ranks lie below the number of truth-table coordinates.

theorem Algebraic.DeMorgan.inputRank_injective {n : ℕ} : Function.Injective inputRank

The numerical ordering distinguishes all input assignments.

def Algebraic.DeMorgan.thresholdExpression (n threshold : ℕ) : Expression n

A comparison with a fixed threshold, simplifying constant subexpressions.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.DeMorgan.thresholdExpression 0 x✝ = Algebraic.DeMorgan.Expression.constant (decide (x✝ = 0))

theorem Algebraic.DeMorgan.thresholdExpression_eval {n : ℕ} (threshold : ℕ) (input : Fin n → Bool) : Expression.eval input (thresholdExpression n threshold) = decide (threshold ≤ inputRank input)

The threshold expression tests the input's numerical rank.

theorem Algebraic.DeMorgan.thresholdExpression_gateCount_le {n : ℕ} (threshold : ℕ) (positive : 0 < threshold) (interior : threshold < 2 ^ n) : (thresholdExpression n threshold).gateCount + 1 ≤ n

An interior threshold needs at most one fewer gate than input bits.