The unbounded-fan-in AC0 basis

This module models the source convention used by Hastad's small-depth lower bound. AND and OR gates have arbitrary finite fan-in. NOT is explicit in the generic circuit syntax, but the source-facing cost charges only AND/OR gates and the source-facing logical depth gives NOT zero delay. The checked class presentation requires every NOT to read an original input. A stronger Circuit.NormalForm predicate additionally records alternation of adjacent AND/OR gates.

inductive Algebraic.AC0.Op : Type

Operations in the arbitrary-fan-in AND/OR/NOT basis. Zero-ary AND and OR serve as the Boolean constants true and false.

• not : Op
• and (arity : ℕ) : Op
• or (arity : ℕ) : Op

def Algebraic.AC0.instDecidableEqOp.decEq (x✝ x✝¹ : Op) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.AC0.instDecidableEqOp.decEq Algebraic.AC0.Op.not Algebraic.AC0.Op.not = isTrue ⋯
• Algebraic.AC0.instDecidableEqOp.decEq Algebraic.AC0.Op.not (Algebraic.AC0.Op.and arity) = isFalse ⋯
• Algebraic.AC0.instDecidableEqOp.decEq Algebraic.AC0.Op.not (Algebraic.AC0.Op.or arity) = isFalse ⋯
• Algebraic.AC0.instDecidableEqOp.decEq (Algebraic.AC0.Op.and arity) Algebraic.AC0.Op.not = isFalse ⋯
• Algebraic.AC0.instDecidableEqOp.decEq (Algebraic.AC0.Op.and a) (Algebraic.AC0.Op.and b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Algebraic.AC0.instDecidableEqOp.decEq (Algebraic.AC0.Op.and arity) (Algebraic.AC0.Op.or arity_1) = isFalse ⋯
• Algebraic.AC0.instDecidableEqOp.decEq (Algebraic.AC0.Op.or arity) Algebraic.AC0.Op.not = isFalse ⋯
• Algebraic.AC0.instDecidableEqOp.decEq (Algebraic.AC0.Op.or arity) (Algebraic.AC0.Op.and arity_1) = isFalse ⋯
• Algebraic.AC0.instDecidableEqOp.decEq (Algebraic.AC0.Op.or a) (Algebraic.AC0.Op.or b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Algebraic.AC0.instDecidableEqOp : DecidableEq Op

Equations

• Algebraic.AC0.instDecidableEqOp = Algebraic.AC0.instDecidableEqOp.decEq

@[reducible]

def Algebraic.AC0.arity : Op → ℕ

Arity of an AC0 operation.

Equations

• Algebraic.AC0.arity Algebraic.AC0.Op.not = 1
• Algebraic.AC0.arity (Algebraic.AC0.Op.and n) = n
• Algebraic.AC0.arity (Algebraic.AC0.Op.or n) = n

@[reducible, inline]

abbrev Algebraic.AC0.signature : Signature

Signature of the arbitrary-fan-in Boolean basis.

Equations

• Algebraic.AC0.signature = { Op := Algebraic.AC0.Op, Arity := Algebraic.AC0.arity }

def Algebraic.AC0.interpretation : Interpretation signature Bool

Standard Boolean semantics. Empty conjunction is true and empty disjunction is false.

Equations

• Algebraic.AC0.interpretation Algebraic.AC0.Op.not input = !input 0
• Algebraic.AC0.interpretation (Algebraic.AC0.Op.and arity) input = decide (∀ (k : Fin (Algebraic.AC0.signature.Arity (Algebraic.AC0.Op.and arity))), input k = true)
• Algebraic.AC0.interpretation (Algebraic.AC0.Op.or arity) input = decide (∃ (k : Fin (Algebraic.AC0.signature.Arity (Algebraic.AC0.Op.or arity))), input k = true)

@[simp]

theorem Algebraic.AC0.interpretation_not (input : Fin 1 → Bool) : interpretation Op.not input = !input 0

@[simp]

theorem Algebraic.AC0.interpretation_and_eq_true {n : ℕ} (input : Fin n → Bool) : interpretation (Op.and n) input = true ↔ ∀ (k : Fin n), input k = true

@[simp]

theorem Algebraic.AC0.interpretation_or_eq_true {n : ℕ} (input : Fin n → Bool) : interpretation (Op.or n) input = true ↔ ∃ (k : Fin n), input k = true

@[simp]

theorem Algebraic.AC0.interpretation_and_zero : interpretation (Op.and 0) Fin.elim0 = true

@[simp]

theorem Algebraic.AC0.interpretation_or_zero : interpretation (Op.or 0) Fin.elim0 = false

def Algebraic.AC0.andOrCost : OperationCost signature

Hastad's size convention: count AND and OR gates, not input negations.

Equations

• Algebraic.AC0.andOrCost Algebraic.AC0.Op.not = 0
• Algebraic.AC0.andOrCost (Algebraic.AC0.Op.and arity) = 1
• Algebraic.AC0.andOrCost (Algebraic.AC0.Op.or arity) = 1

@[simp]

theorem Algebraic.AC0.andOrCost_not : andOrCost Op.not = 0

@[simp]

theorem Algebraic.AC0.andOrCost_and (n : ℕ) : andOrCost (Op.and n) = 1

@[simp]

theorem Algebraic.AC0.andOrCost_or (n : ℕ) : andOrCost (Op.or n) = 1

inductive Algebraic.AC0.Connective : Type

The two connectives whose adjacent levels are merged in normal form.

• and : Connective
• or : Connective

@[instance_reducible]

instance Algebraic.AC0.instDecidableEqConnective : DecidableEq Connective

Equations

• Algebraic.AC0.instDecidableEqConnective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Algebraic.AC0.Op.connective : Op → Option Connective

Forget fan-in while retaining whether an operation is AND or OR.

Equations

• Algebraic.AC0.Op.not.connective = none
• (Algebraic.AC0.Op.and n).connective = some Algebraic.AC0.Connective.and
• (Algebraic.AC0.Op.or n).connective = some Algebraic.AC0.Connective.or

def Algebraic.AC0.Line.NegationAtInput {n g : ℕ} : Line signature n g → Prop

A NOT line is a source literal precisely when it reads an original input.

Equations

• Algebraic.AC0.Line.NegationAtInput { op := Algebraic.AC0.Op.not, wires := wires } = ∃ (input : Fin n), wires 0 = Cslib.Circuits.Wire.input input
• Algebraic.AC0.Line.NegationAtInput { op := Algebraic.AC0.Op.and arity, wires := wires } = True
• Algebraic.AC0.Line.NegationAtInput { op := Algebraic.AC0.Op.or arity, wires := wires } = True

def Algebraic.AC0.Line.AlternatesAfter {n g : ℕ} (program : Program signature n g) (line : Line signature n g) : Prop

Every direct AND/OR predecessor has the opposite connective. NOT lines are treated as input literals and impose no connective condition.

Equations

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

def Algebraic.AC0.Program.NegationsAtInputs {n g : ℕ} (program : Program signature n g) : Prop

Every NOT gate in a program reads an original input.

Equations

• Algebraic.AC0.Program.NegationsAtInputs Cslib.Circuits.Program.empty = True
• Algebraic.AC0.Program.NegationsAtInputs (program.gate line) = (Algebraic.AC0.Program.NegationsAtInputs program ∧ Algebraic.AC0.Line.NegationAtInput line)

def Algebraic.AC0.Program.Alternating {n g : ℕ} (program : Program signature n g) : Prop

No AND gate directly reads an AND gate and no OR gate directly reads an OR gate.

Equations

• Algebraic.AC0.Program.Alternating Cslib.Circuits.Program.empty = True
• Algebraic.AC0.Program.Alternating (program.gate line) = (Algebraic.AC0.Program.Alternating program ∧ Algebraic.AC0.Line.AlternatesAfter program line)

def Algebraic.AC0.logicalDepthInterpretation : Interpretation signature ℕ

Arrival-time semantics for source gate levels. Input negations are literal annotations and therefore have zero delay; AND and OR add one level.

Equations

• Algebraic.AC0.logicalDepthInterpretation Algebraic.AC0.Op.not input = input 0
• Algebraic.AC0.logicalDepthInterpretation (Algebraic.AC0.Op.and n) input = (Fin.foldl n (fun (depth : ℕ) (argument : Fin n) => max depth (input argument)) 0).succ
• Algebraic.AC0.logicalDepthInterpretation (Algebraic.AC0.Op.or n) input = (Fin.foldl n (fun (depth : ℕ) (argument : Fin n) => max depth (input argument)) 0).succ

@[simp]

theorem Algebraic.AC0.logicalDepthInterpretation_not_zero : (logicalDepthInterpretation Op.not fun (x : Fin (signature.Arity Op.not)) => 0) = 0

@[simp]

theorem Algebraic.AC0.logicalDepthInterpretation_and_zero (n : ℕ) : (logicalDepthInterpretation (Op.and n) fun (x : Fin (signature.Arity (Op.and n))) => 0) = 1

@[simp]

theorem Algebraic.AC0.logicalDepthInterpretation_or_zero (n : ℕ) : (logicalDepthInterpretation (Op.or n) fun (x : Fin (signature.Arity (Op.or n))) => 0) = 1

def Algebraic.AC0.Circuit.NegationsAtInputs {n m : ℕ} (circuit : Circuit signature n m) : Prop

Every NOT gate in the circuit is an input literal.

Equations

• Algebraic.AC0.Circuit.NegationsAtInputs circuit = Algebraic.AC0.Program.NegationsAtInputs circuit.program

def Algebraic.AC0.Circuit.logicalOutputDepths {n m : ℕ} (circuit : Circuit signature n m) : Fin m → ℕ

Logical depth of each designated output in Hastad's convention.

Equations

• Algebraic.AC0.Circuit.logicalOutputDepths circuit = circuit.eval Algebraic.AC0.logicalDepthInterpretation fun (x : Fin n) => 0

def Algebraic.AC0.Circuit.logicalDepth {n m : ℕ} (circuit : Circuit signature n m) : ℕ

Maximum number of AND/OR levels on a designated input-output path.

Equations

• Algebraic.AC0.Circuit.logicalDepth circuit = Fin.foldl m (fun (depth : ℕ) (output : Fin m) => max depth (Algebraic.AC0.Circuit.logicalOutputDepths circuit output)) 0

theorem Algebraic.AC0.Circuit.logicalDepth_one_output {n : ℕ} (circuit : Circuit signature n 1) : logicalDepth circuit = logicalOutputDepths circuit 0

A one-output circuit's logical depth is the depth of its unique output.

def Algebraic.AC0.Circuit.NormalForm {n m : ℕ} (circuit : Circuit signature n m) : Prop

Source-facing normal form: negations are input literals and consecutive AND/OR gates alternate.

Equations

• Algebraic.AC0.Circuit.NormalForm circuit = (Algebraic.AC0.Circuit.NegationsAtInputs circuit ∧ Algebraic.AC0.Program.Alternating circuit.program)

theorem Algebraic.AC0.Circuit.NormalForm.negationsAtInputs {n m : ℕ} {circuit : Circuit signature n m} (normal : NormalForm circuit) : NegationsAtInputs circuit

Strong normal form in particular places every negation at an input.

def Algebraic.AC0.Family.logicalDepth {m : ℕ} (family : Circuit.Family signature m) (n : ℕ) : ℕ

Logical depth as a resource function of a nonuniform family.

Equations

• Algebraic.AC0.Family.logicalDepth family n = Algebraic.AC0.Circuit.logicalDepth (family.circuit n)

def Algebraic.AC0.Family.NormalForm {m : ℕ} (family : Circuit.Family signature m) : Prop

Every member of the family is in the source-facing normal form.

Equations

• Algebraic.AC0.Family.NormalForm family = ∀ (n : ℕ), Algebraic.AC0.Circuit.NormalForm (family.circuit n)

def Algebraic.AC0.Family.NegationsAtInputs {m : ℕ} (family : Circuit.Family signature m) : Prop

Every family member has only input-level negations.

Equations

• Algebraic.AC0.Family.NegationsAtInputs family = ∀ (n : ℕ), Algebraic.AC0.Circuit.NegationsAtInputs (family.circuit n)

theorem Algebraic.AC0.Family.NormalForm.negationsAtInputs {m : ℕ} {family : Circuit.Family signature m} (normal : NormalForm family) : NegationsAtInputs family

Strong family normal form implies the input-negation invariant used by the switching-lemma development.

def Algebraic.AC0.Family.HasConstantLogicalDepth {m : ℕ} (family : Circuit.Family signature m) : Prop

One source-level depth bound works at every input width.

Equations

• Algebraic.AC0.Family.HasConstantLogicalDepth family = Cslib.Circuits.Circuit.Resource.ConstantlyBounded (Algebraic.AC0.Family.logicalDepth family)

def Algebraic.AC0.Family.IsRawSmallDepth (family : Circuit.Family signature 1) : Prop

An unrestricted small-depth family has polynomial AND/OR cost and constant logical depth. Internal NOT gates are allowed in this raw presentation.

Equations

• Algebraic.AC0.Family.IsRawSmallDepth family = (family.HasPolynomialCost Algebraic.AC0.andOrCost ∧ Algebraic.AC0.Family.HasConstantLogicalDepth family)

def Algebraic.AC0.Family.IsSmallDepth (family : Circuit.Family signature 1) : Prop

A checked AC0 family has polynomial AND/OR cost, constant logical depth, and only input-level negations. Alternation is available separately through Family.NormalForm but is not needed for the class definition.

Equations

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

theorem Algebraic.AC0.Family.IsSmallDepth.raw {family : Circuit.Family signature 1} (smallDepth : IsSmallDepth family) : IsRawSmallDepth family

Forgetting the input-negation invariant yields a raw small-depth family.

def Algebraic.AC0.Computable (target : Target.Family Bool 1) : Prop

Nonuniform AC0 computability of a one-output Boolean target family.

Equations

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

def Algebraic.AC0.RawComputable (target : Target.Family Bool 1) : Prop

Raw nonuniform AC0 computability, allowing NOT gates at arbitrary internal wires. Dual-rail normalization proves this presentation equivalent to Computable.

Equations

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