Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Model

Elementary semantics of the signed gate model #

Parity commutes with pointwise XOR. The sixteen binary Boolean operations have arity-preserving signed affine or conjunction normal forms, so the model contains the full binary basis without increasing gate count.

source
theorem Algebraic.Aggregate.Geometry.xorSum_xor {r : ℕ} (x y : Fin r → Bool) :
(xorSum fun (i : Fin r) => x i ^^ y i) = (xorSum x ^^ xorSum y)

Parity of pointwise XOR is the XOR of the two parities.

source
def Algebraic.Aggregate.Geometry.binaryOp (f : Bool → Bool → Bool) :
Op

A binary operation in signed affine/conjunction normal form.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.Aggregate.Geometry.binaryOp_arity (f : Bool → Bool → Bool) :
    (binaryOp f).arity = 2

    Binary normalization retains both ordered argument slots.

    source
    def Algebraic.Aggregate.Geometry.binaryLine {n g : ℕ} (line : Line Binary.signature n g) :
    Line signature n g

    A binary line translated into a single signed gate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.Aggregate.Geometry.interpretation_binaryOp (f : Bool → Bool → Bool) (x : Fin 2 → Bool) :
      (interpretation (binaryOp f) fun (i : Fin (signature.Arity (binaryOp f))) => x (Fin.cast ⋯ i)) = f (x 0) (x 1)

      Every one-gate binary normalization computes the original truth table.

      source
      def Algebraic.Aggregate.Geometry.binaryProgram {n g : ℕ} :
      Program Binary.signature n g → Program signature n g

      Replace each binary gate by its one-gate signed normal form.

      Equations
      Instances For
        source
        theorem Algebraic.Aggregate.Geometry.eval_binaryProgram {n g : ℕ} (p : Program Binary.signature n g) (x : Fin n → Bool) :
        (binaryProgram p).eval interpretation x = p.eval Binary.interpretation x

        Binary normalization preserves the complete gate trace.

        source
        def Algebraic.Aggregate.Geometry.binaryCircuit {n m : ℕ} (c : Circuit Binary.signature n m) :
        Circuit signature n m

        Normalize a binary circuit without changing any gate or output index.

        Equations
        Instances For
          source
          @[simp]
          theorem Algebraic.Aggregate.Geometry.size_binaryCircuit {n m : ℕ} (c : Circuit Binary.signature n m) :
          (binaryCircuit c).size = c.size

          The translation charges exactly one gate per original binary gate.

          source
          @[simp]
          theorem Algebraic.Aggregate.Geometry.eval_binaryCircuit {n m : ℕ} (c : Circuit Binary.signature n m) (x : Fin n → Bool) :
          (binaryCircuit c).eval interpretation x = c.eval Binary.interpretation x

          The normalized circuit has identical Boolean outputs.