Documentation

Complexitylib.Algebraic.Basis.DeMorgan.Complexity

Boolean circuit complexity on the truth-table cube #

Every Boolean function has a De Morgan circuit. Its minimum internal gate count is therefore a natural number, agreeing with the generic extended- natural Circuit.gateComplexity. Constants and identities count as gates; designated output wires remain free.

Changing one truth-table entry costs at most 2 * n gates. Consequently the complexity measure is 2 * n Lipschitz for unnormalized Hamming distance and crosses every attainable threshold with overshoot at most 2 * n.

source
noncomputable def Algebraic.DeMorgan.minimumCircuit {n : ℕ} (function : ScalarFunction Bool n) :
Circuit.Minimum OperationCost.unit interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input

A minimum-size circuit chosen by well-ordering. This is a classical proof witness, not an executable circuit optimizer.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.DeMorgan.complexity {n : ℕ} (function : ScalarFunction Bool n) :
    ℕ

    Minimum number of internal gates in a scalar De Morgan circuit.

    Equations
    Instances For
      source
      theorem Algebraic.DeMorgan.complexity_eq_gateComplexity {n : ℕ} (function : ScalarFunction Bool n) :
      ↑(complexity function) = Circuit.gateComplexity interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input

      The natural-valued Boolean measure agrees with generic gate complexity.

      source
      theorem Algebraic.DeMorgan.complexity_le {n : ℕ} (circuit : Circuit signature n 1) {function : ScalarFunction Bool n} (computes : circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input) :
      complexity function ≤ circuit.size

      Any concrete circuit upper-bounds minimum internal gate count.

      source
      theorem Algebraic.DeMorgan.complexity_constant_le (n : ℕ) (value : Bool) :
      (complexity fun (x : Fin n → Bool) => value) ≤ 1

      The constant functions have one-gate implementations at every width.

      source
      theorem Algebraic.DeMorgan.gateHard_iff {n : ℕ} (function : ScalarFunction Bool n) (budget : ℕ) :
      (Circuit.GateHard interpretation budget fun (input : Fin n → Bool) (x : Fin 1) => function input) ↔ budget < complexity function

      Gate hardness is exactly a strict lower bound on the natural minimum.

      source
      theorem Algebraic.DeMorgan.complexity_update_le {n : ℕ} (function : ScalarFunction Bool n) (point : Fin n → Bool) (value : Bool) :
      complexity (Function.update function point value) ≤ complexity function + 2 * n

      Changing one truth-table entry adds at most twice the input width.

      source
      theorem Algebraic.DeMorgan.complexity_le_add_hammingDist {n : ℕ} (left right : ScalarFunction Bool n) :
      complexity right ≤ complexity left + 2 * n * hammingDist left right

      One-sided Hamming Lipschitz bound on Boolean circuit complexity.

      source
      theorem Algebraic.DeMorgan.complexity_dist_le {n : ℕ} (left right : ScalarFunction Bool n) :
      (complexity left).dist (complexity right) ≤ 2 * n * hammingDist left right

      Boolean circuit complexity is 2 * n Lipschitz on the truth-table cube.

      source
      theorem Algebraic.DeMorgan.exists_complexity_between {n : ℕ} (threshold : ℕ) (positive : 1 ≤ threshold) (hard : ScalarFunction Bool n) (above : threshold < complexity hard) :
      ∃ (function : ScalarFunction Bool n), threshold < complexity function ∧ complexity function ≤ threshold + 2 * n

      Every threshold above the constant-function cost and below an attained complexity is crossed with overshoot at most 2 * n.