Partial evaluation of AC0 circuits

This module rebuilds arbitrary-fan-in AC0 programs after a Boolean partial assignment. Fixed inputs and forced gates are represented as residual Boolean constants, while genuinely live values are represented by wires over the compact namespace of live variables.

The local connective simplifier is deliberately algebraic. An absorbing constant forces an AND or OR gate; otherwise neutral constants are discarded and the remaining wires feed one residual gate. No truth-table search or finite-circuit optimization is involved.

def Algebraic.AC0.Connective.operation : Connective → ℕ → Op

The arbitrary-fan-in operation associated with a connective.

Equations

• Algebraic.AC0.Connective.and.operation = Algebraic.AC0.Op.and
• Algebraic.AC0.Connective.or.operation = Algebraic.AC0.Op.or

def Algebraic.AC0.Connective.neutral : Connective → Bool

The neutral Boolean for a connective.

Equations

• Algebraic.AC0.Connective.and.neutral = true
• Algebraic.AC0.Connective.or.neutral = false

def Algebraic.AC0.Connective.absorbing : Connective → Bool

The Boolean which forces a connective independently of other inputs.

Equations

• Algebraic.AC0.Connective.and.absorbing = false
• Algebraic.AC0.Connective.or.absorbing = true

def Algebraic.AC0.Connective.eval {r : ℕ} (connective : Connective) : (Fin r → Bool) → Bool

Boolean semantics of an arbitrary-fan-in connective.

Equations

• Algebraic.AC0.Connective.and.eval x✝ = Algebraic.AC0.interpretation (Algebraic.AC0.Op.and r) x✝
• Algebraic.AC0.Connective.or.eval x✝ = Algebraic.AC0.interpretation (Algebraic.AC0.Op.or r) x✝

def Algebraic.AC0.Connective.logicalDepth {r : ℕ} (connective : Connective) : (Fin r → ℕ) → ℕ

Source logical depth of an arbitrary-fan-in connective.

Equations

• Algebraic.AC0.Connective.and.logicalDepth x✝ = Algebraic.AC0.logicalDepthInterpretation (Algebraic.AC0.Op.and r) x✝
• Algebraic.AC0.Connective.or.logicalDepth x✝ = Algebraic.AC0.logicalDepthInterpretation (Algebraic.AC0.Op.or r) x✝

@[simp]

theorem Algebraic.AC0.Connective.operation_cost (connective : Connective) (arity : ℕ) : andOrCost (connective.operation arity) = 1

inductive Algebraic.AC0.ResidualValue (n g : ℕ) : Type

A Boolean constant or a wire in a partially evaluated AC0 program.

• constant {n g : ℕ} (value : Bool) : ResidualValue n g
• wire {n g : ℕ} (wire : Wire n g) : ResidualValue n g

def Algebraic.AC0.instDecidableEqResidualValue.decEq {n✝ g✝ : ℕ} (x✝ x✝¹ : ResidualValue n✝ g✝) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.AC0.instDecidableEqResidualValue.decEq (Algebraic.AC0.ResidualValue.constant a) (Algebraic.AC0.ResidualValue.constant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Algebraic.AC0.instDecidableEqResidualValue.decEq (Algebraic.AC0.ResidualValue.constant value) (Algebraic.AC0.ResidualValue.wire wire) = isFalse ⋯
• Algebraic.AC0.instDecidableEqResidualValue.decEq (Algebraic.AC0.ResidualValue.wire wire) (Algebraic.AC0.ResidualValue.constant value) = isFalse ⋯
• Algebraic.AC0.instDecidableEqResidualValue.decEq (Algebraic.AC0.ResidualValue.wire a) (Algebraic.AC0.ResidualValue.wire b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Algebraic.AC0.instDecidableEqResidualValue {n✝ g✝ : ℕ} : DecidableEq (ResidualValue n✝ g✝)

Equations

• Algebraic.AC0.instDecidableEqResidualValue = Algebraic.AC0.instDecidableEqResidualValue.decEq

def Algebraic.AC0.ResidualValue.eval {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) : ResidualValue n g → Bool

Evaluate a residual value in a residual program.

Equations

• Algebraic.AC0.ResidualValue.eval program input (Algebraic.AC0.ResidualValue.constant value) = value
• Algebraic.AC0.ResidualValue.eval program input (Algebraic.AC0.ResidualValue.wire sourceWire) = program.trace Algebraic.AC0.interpretation input sourceWire

def Algebraic.AC0.ResidualValue.mapWires {n g k h : ℕ} (wireMap : Wire n g → Wire k h) : ResidualValue n g → ResidualValue k h

Transport a residual value through a wire map.

Equations

• Algebraic.AC0.ResidualValue.mapWires wireMap (Algebraic.AC0.ResidualValue.constant value) = Algebraic.AC0.ResidualValue.constant value
• Algebraic.AC0.ResidualValue.mapWires wireMap (Algebraic.AC0.ResidualValue.wire sourceWire) = Algebraic.AC0.ResidualValue.wire (wireMap sourceWire)

def Algebraic.AC0.ResidualValue.wire? {n g : ℕ} : ResidualValue n g → Option (Wire n g)

Return the represented wire, if the value is nonconstant.

Equations

• (Algebraic.AC0.ResidualValue.constant value).wire? = none
• (Algebraic.AC0.ResidualValue.wire sourceWire).wire? = some sourceWire

def Algebraic.AC0.ResidualValue.logicalDepth {n g : ℕ} (program : Program signature n g) : ResidualValue n g → ℕ

Logical depth of a residual value, assigning depth zero to constants.

Equations

• Algebraic.AC0.ResidualValue.logicalDepth program (Algebraic.AC0.ResidualValue.constant value) = 0
• Algebraic.AC0.ResidualValue.logicalDepth program (Algebraic.AC0.ResidualValue.wire sourceWire) = program.trace Algebraic.AC0.logicalDepthInterpretation (fun (x : Fin n) => 0) sourceWire

@[simp]

theorem Algebraic.AC0.ResidualValue.eval_constant {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) (value : Bool) : eval program input (constant value) = value

@[simp]

theorem Algebraic.AC0.ResidualValue.eval_wire {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) (wire : Wire n g) : eval program input (ResidualValue.wire wire) = program.trace interpretation input wire

@[simp]

theorem Algebraic.AC0.ResidualValue.mapWires_constant {n g k h : ℕ} (wireMap : Wire n g → Wire k h) (value : Bool) : mapWires wireMap (constant value) = constant value

@[simp]

theorem Algebraic.AC0.ResidualValue.mapWires_wire {n g k h : ℕ} (wireMap : Wire n g → Wire k h) (wire : Wire n g) : mapWires wireMap (ResidualValue.wire wire) = ResidualValue.wire (wireMap wire)

theorem Algebraic.AC0.ResidualValue.eval_mapWires {n g h : ℕ} (value : ResidualValue n g) (wireMap : Wire.Renaming n g h) (source : Program signature n g) (result : Program signature n h) (input : Fin n → Bool) (preserves : ∀ (sourceWire : Wire n g), result.trace interpretation input (wireMap.apply sourceWire) = source.trace interpretation input sourceWire) : eval result input (mapWires wireMap.apply value) = eval source input value

Mapping residual wires preserves evaluation when the wire map preserves the preceding program trace.

theorem Algebraic.AC0.ResidualValue.logicalDepth_mapWires {n g h : ℕ} (value : ResidualValue n g) (wireMap : Wire.Renaming n g h) (source : Program signature n g) (result : Program signature n h) (preserves : ∀ (sourceWire : Wire n g), result.trace logicalDepthInterpretation (fun (x : Fin n) => 0) (wireMap.apply sourceWire) = source.trace logicalDepthInterpretation (fun (x : Fin n) => 0) sourceWire) : logicalDepth result (mapWires wireMap.apply value) = logicalDepth source value

Mapping residual wires preserves logical depth when the wire map preserves the preceding depth trace.

def Algebraic.AC0.residualWires {r n g : ℕ} (values : Fin r → ResidualValue n g) : List (Wire n g)

The nonconstant arguments of a gate, in their original order.

Equations

• Algebraic.AC0.residualWires values = List.filterMap Algebraic.AC0.ResidualValue.wire? (List.ofFn values)

@[simp]

theorem Algebraic.AC0.mem_residualWires {r n g : ℕ} (values : Fin r → ResidualValue n g) (wire : Wire n g) : wire ∈ residualWires values ↔ ∃ (argument : Fin r), values argument = ResidualValue.wire wire

def Algebraic.AC0.residualLine {n g : ℕ} (connective : Connective) (wires : List (Wire n g)) : Line signature n g

A connective gate whose constant arguments have been removed.

Equations

• Algebraic.AC0.residualLine Algebraic.AC0.Connective.and wires = { op := Algebraic.AC0.Op.and wires.length, wires := wires.get }
• Algebraic.AC0.residualLine Algebraic.AC0.Connective.or wires = { op := Algebraic.AC0.Op.or wires.length, wires := wires.get }

inductive Algebraic.AC0.GateReduction (n g : ℕ) : Type

Result of locally simplifying one charged connective gate.

• value {n g : ℕ} (result : ResidualValue n g) : GateReduction n g
• line {n g : ℕ} (result : Line signature n g) : GateReduction n g

def Algebraic.AC0.GateReduction.eval {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) : GateReduction n g → Bool

Evaluate a local gate reduction against its preceding program.

Equations

• Algebraic.AC0.GateReduction.eval program input (Algebraic.AC0.GateReduction.value result) = Algebraic.AC0.ResidualValue.eval program input result
• Algebraic.AC0.GateReduction.eval program input (Algebraic.AC0.GateReduction.line result) = result.eval Algebraic.AC0.interpretation input (program.eval Algebraic.AC0.interpretation input)

def Algebraic.AC0.GateReduction.cost {n g : ℕ} : GateReduction n g → ℕ

Whether the reduction retains one charged gate.

Equations

• (Algebraic.AC0.GateReduction.value result).cost = 0
• (Algebraic.AC0.GateReduction.line result).cost = 1

def Algebraic.AC0.GateReduction.chargedCost {n g : ℕ} : GateReduction n g → ℕ

Charged AND/OR cost contributed by a local gate reduction.

Equations

• (Algebraic.AC0.GateReduction.value result).chargedCost = 0
• (Algebraic.AC0.GateReduction.line result).chargedCost = Algebraic.AC0.andOrCost result.op

def Algebraic.AC0.GateReduction.logicalDepth {n g : ℕ} (program : Program signature n g) : GateReduction n g → ℕ

Logical depth contributed by a local gate reduction.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.GateReduction.logicalDepth program (Algebraic.AC0.GateReduction.value result) = Algebraic.AC0.ResidualValue.logicalDepth program result

@[simp]

theorem Algebraic.AC0.GateReduction.cost_le_one {n g : ℕ} (result : GateReduction n g) : result.cost ≤ 1

noncomputable def Algebraic.AC0.simplifyConnective {r n g : ℕ} (connective : Connective) (values : Fin r → ResidualValue n g) : GateReduction n g

Simplify one arbitrary-fan-in AND or OR from already restricted arguments.

Equations

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

theorem Algebraic.AC0.argument_eval_eq_neutral_of_not_forced_of_not_wire {r n g : ℕ} (connective : Connective) (values : Fin r → ResidualValue n g) (program : Program signature n g) (input : Fin n → Bool) (notForced : ¬∃ (argument : Fin r), values argument = ResidualValue.constant connective.absorbing) (argument : Fin r) (notWire : ¬∃ (sourceWire : Wire n g), values argument = ResidualValue.wire sourceWire) : ResidualValue.eval program input (values argument) = connective.neutral

If a gate is not forced, every constant argument is its connective's neutral value.

theorem Algebraic.AC0.residualLine_eval_of_not_forced {r n g : ℕ} (connective : Connective) (values : Fin r → ResidualValue n g) (program : Program signature n g) (input : Fin n → Bool) (notForced : ¬∃ (argument : Fin r), values argument = ResidualValue.constant connective.absorbing) : (residualLine connective (residualWires values)).eval interpretation input (program.eval interpretation input) = connective.eval fun (argument : Fin r) => ResidualValue.eval program input (values argument)

Removing neutral constants from a non-forced connective preserves its Boolean value.

theorem Algebraic.AC0.connective_eval_eq_absorbing_of_forced {r n g : ℕ} (connective : Connective) (values : Fin r → ResidualValue n g) (program : Program signature n g) (input : Fin n → Bool) (forced : ∃ (argument : Fin r), values argument = ResidualValue.constant connective.absorbing) : (connective.eval fun (argument : Fin r) => ResidualValue.eval program input (values argument)) = connective.absorbing

An absorbing residual constant forces the original connective.

theorem Algebraic.AC0.connective_eval_eq_neutral_of_no_wires {r n g : ℕ} (connective : Connective) (values : Fin r → ResidualValue n g) (program : Program signature n g) (input : Fin n → Bool) (notForced : ¬∃ (argument : Fin r), values argument = ResidualValue.constant connective.absorbing) (noWires : residualWires values = []) : (connective.eval fun (argument : Fin r) => ResidualValue.eval program input (values argument)) = connective.neutral

If no argument is a wire and the connective is not forced, all arguments are neutral and so is the gate output.

theorem Algebraic.AC0.simplifyConnective_eval {r n g : ℕ} (connective : Connective) (values : Fin r → ResidualValue n g) (program : Program signature n g) (input : Fin n → Bool) : GateReduction.eval program input (simplifyConnective connective values) = connective.eval fun (argument : Fin r) => ResidualValue.eval program input (values argument)

The local simplifier exactly preserves the value of an arbitrary-fan-in AND or OR gate.

theorem Algebraic.AC0.simplifyConnective_chargedCost_le {r n g : ℕ} (connective : Connective) (values : Fin r → ResidualValue n g) : (simplifyConnective connective values).chargedCost ≤ 1

Local connective simplification never contributes more than one charged gate.

theorem Algebraic.AC0.simplifyConnective_logicalDepth_le {r n g : ℕ} (connective : Connective) (values : Fin r → ResidualValue n g) (program : Program signature n g) (sourceDepths : Fin r → ℕ) (bounds : ∀ (argument : Fin r), ResidualValue.logicalDepth program (values argument) ≤ sourceDepths argument) : GateReduction.logicalDepth program (simplifyConnective connective values) ≤ connective.logicalDepth sourceDepths

Local connective simplification does not increase logical depth when each residual argument is no deeper than its source argument.

def Algebraic.AC0.simplifyNot {n g : ℕ} (value : ResidualValue n g) : GateReduction n g

A unary NOT gate on a residual value: constants are folded and wires retain one zero-cost NOT line.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.simplifyNot (Algebraic.AC0.ResidualValue.constant value_1) = Algebraic.AC0.GateReduction.value (Algebraic.AC0.ResidualValue.constant !value_1)

@[simp]

theorem Algebraic.AC0.simplifyNot_eval {n g : ℕ} (value : ResidualValue n g) (program : Program signature n g) (input : Fin n → Bool) : GateReduction.eval program input (simplifyNot value) = !ResidualValue.eval program input value

@[simp]

theorem Algebraic.AC0.simplifyNot_logicalDepth {n g : ℕ} (value : ResidualValue n g) (program : Program signature n g) : GateReduction.logicalDepth program (simplifyNot value) = ResidualValue.logicalDepth program value

noncomputable def Algebraic.AC0.simplifyLine {n g k h : ℕ} (line : Line signature n g) : (Wire n g → ResidualValue k h) → GateReduction k h

Simplify an AC0 line after assigning a residual value to every wire it reads.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.simplifyLine { op := Algebraic.AC0.Op.not, wires := wires } x✝ = Algebraic.AC0.simplifyNot (x✝ (wires 0))

theorem Algebraic.AC0.simplifyLine_eval {n g k h : ℕ} (line : Line signature n g) (values : Wire n g → ResidualValue k h) (program : Program signature k h) (input : Fin k → Bool) : GateReduction.eval program input (simplifyLine line values) = interpretation line.op fun (argument : Fin (signature.Arity line.op)) => ResidualValue.eval program input (values (line.wires argument))

Line simplification preserves the operation's value under the residual wire valuation.

theorem Algebraic.AC0.simplifyLine_chargedCost_le {n g k h : ℕ} (line : Line signature n g) (values : Wire n g → ResidualValue k h) : (simplifyLine line values).chargedCost ≤ andOrCost line.op

A simplified line costs no more charged gates than its source line.

theorem Algebraic.AC0.simplifyLine_logicalDepth_le {n g k h : ℕ} (source : Program signature n g) (line : Line signature n g) (values : Wire n g → ResidualValue k h) (result : Program signature k h) (bounds : ∀ (sourceWire : Wire n g), ResidualValue.logicalDepth result (values sourceWire) ≤ source.trace logicalDepthInterpretation (fun (x : Fin n) => 0) sourceWire) : GateReduction.logicalDepth result (simplifyLine line values) ≤ line.eval logicalDepthInterpretation (fun (x : Fin n) => 0) (source.eval logicalDepthInterpretation fun (x : Fin n) => 0)

A simplified line is no deeper than its source line when every represented wire is no deeper than the corresponding source wire.

Whole-program restriction

noncomputable def Algebraic.AC0.inputResidual {n : ℕ} (rho : PartialAssignment n) (sourceInput : Fin n) : ResidualValue rho.liveCount 0

The residual representation of one original input.

Equations

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

@[simp]

theorem Algebraic.AC0.inputResidual_eval {n : ℕ} (rho : PartialAssignment n) (sourceInput : Fin n) (input : Fin rho.liveCount → Bool) : ResidualValue.eval Program.empty input (inputResidual rho sourceInput) = rho.toLiveInputSubstitution.apply input sourceInput

structure Algebraic.AC0.ProgramRestriction {n g : ℕ} (source : Program signature n g) (rho : PartialAssignment n) : Type

A proof-carrying partial evaluation of every wire in an AC0 program.

• gateCount : ℕ

  Number of gates in the residual program.

• result : Program signature rho.liveCount self.gateCount

  Residual program over exactly the live variables.

• values : Wire n g → ResidualValue rho.liveCount self.gateCount

  Constant-or-wire representation of every source wire.

• trace_eq (input : Fin rho.liveCount → Bool) (sourceWire : Wire n g) : ResidualValue.eval self.result input (self.values sourceWire) = source.trace interpretation (rho.toLiveInputSubstitution.apply input) sourceWire

  Every represented wire has its exact restricted semantics.

• logicalDepth_le (sourceWire : Wire n g) : ResidualValue.logicalDepth self.result (self.values sourceWire) ≤ source.trace logicalDepthInterpretation (fun (x : Fin n) => 0) sourceWire

  Every residual wire is no deeper than the source wire it represents.

• gateCount_le : self.gateCount ≤ g

  Partial evaluation does not increase the total gate count.

• cost_le : Program.cost andOrCost self.result ≤ Program.cost andOrCost source

  Partial evaluation does not increase charged AND/OR cost.

noncomputable def Algebraic.AC0.ProgramRestriction.empty {n : ℕ} (rho : PartialAssignment n) : ProgramRestriction Program.empty rho

Restriction of the empty program compactly reindexes its live inputs.

Equations

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

theorem Algebraic.AC0.ProgramRestriction.line_eval {n g : ℕ} {source : Program signature n g} {rho : PartialAssignment n} (restriction : ProgramRestriction source rho) (line : Line signature n g) (input : Fin rho.liveCount → Bool) : line.eval interpretation (rho.toLiveInputSubstitution.apply input) (source.eval interpretation (rho.toLiveInputSubstitution.apply input)) = interpretation line.op fun (argument : Fin (signature.Arity line.op)) => ResidualValue.eval restriction.result input (restriction.values (line.wires argument))

Evaluate a source line through a restriction of its preceding program.

def Algebraic.AC0.ProgramRestriction.reuseLast {n g : ℕ} {source : Program signature n g} {rho : PartialAssignment n} (prior : ProgramRestriction source rho) (line : Line signature n g) (value : ResidualValue rho.liveCount prior.gateCount) (value_eq : ∀ (input : Fin rho.liveCount → Bool), ResidualValue.eval prior.result input value = line.eval interpretation (rho.toLiveInputSubstitution.apply input) (source.eval interpretation (rho.toLiveInputSubstitution.apply input))) (logicalDepthBound : ResidualValue.logicalDepth prior.result value ≤ line.eval logicalDepthInterpretation (fun (x : Fin n) => 0) (source.eval logicalDepthInterpretation fun (x : Fin n) => 0)) : ProgramRestriction (source.gate line) rho

Delete the new last source gate because its residual value is already available.

Equations

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

def Algebraic.AC0.ProgramRestriction.retainLast {n g : ℕ} {source : Program signature n g} {rho : PartialAssignment n} (prior : ProgramRestriction source rho) (line : Line signature n g) (residualLine : Line signature rho.liveCount prior.gateCount) (line_eq : ∀ (input : Fin rho.liveCount → Bool), residualLine.eval interpretation input (prior.result.eval interpretation input) = line.eval interpretation (rho.toLiveInputSubstitution.apply input) (source.eval interpretation (rho.toLiveInputSubstitution.apply input))) (logicalDepthBound : residualLine.eval logicalDepthInterpretation (fun (x : Fin rho.liveCount) => 0) (prior.result.eval logicalDepthInterpretation fun (x : Fin rho.liveCount) => 0) ≤ line.eval logicalDepthInterpretation (fun (x : Fin n) => 0) (source.eval logicalDepthInterpretation fun (x : Fin n) => 0)) (costBound : andOrCost residualLine.op ≤ andOrCost line.op) : ProgramRestriction (source.gate line) rho

Retain the new last source gate as one residual line. Earlier residual wires are embedded into the extended program.

Equations

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

noncomputable def Algebraic.AC0.ProgramRestriction.append {n g : ℕ} {source : Program signature n g} {rho : PartialAssignment n} (prior : ProgramRestriction source rho) (line : Line signature n g) : ProgramRestriction (source.gate line) rho

Simplify and append one source line to a restricted prefix.

Equations

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

noncomputable def Algebraic.AC0.restrictProgram {n g : ℕ} (rho : PartialAssignment n) (source : Program signature n g) : ProgramRestriction source rho

Partially evaluate every gate of an AC0 program under rho, rebuilding it over exactly the live input coordinates.

Equations

• Algebraic.AC0.restrictProgram rho Cslib.Circuits.Program.empty = Algebraic.AC0.ProgramRestriction.empty rho
• Algebraic.AC0.restrictProgram rho (source.gate line) = (Algebraic.AC0.restrictProgram rho source).append line

Residual circuits

structure Algebraic.AC0.ResidualCircuit (n g m : ℕ) : Type

An AC0 program whose designated outputs may be Boolean constants. Keeping constants explicit is necessary for exact cost monotonicity: restricting a zero-gate projection can produce a constant function.

• program : Program signature n g

  Internal residual program.

• outputs : Fin m → ResidualValue n g

  Constant-or-wire representative of each designated output.

def Algebraic.AC0.ResidualCircuit.eval {n g m : ℕ} (circuit : ResidualCircuit n g m) (input : Fin n → Bool) : Fin m → Bool

Evaluate all designated residual outputs.

Equations

• circuit.eval input output = Algebraic.AC0.ResidualValue.eval circuit.program input (circuit.outputs output)

def Algebraic.AC0.ResidualCircuit.cost {n g m : ℕ} (circuit : ResidualCircuit n g m) : ℕ

Charged AND/OR cost of a residual circuit.

Equations

• circuit.cost = Cslib.Circuits.Program.cost Algebraic.AC0.andOrCost circuit.program

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

Logical depth of every residual output, with constant outputs at depth zero.

Equations

• circuit.logicalOutputDepths output = Algebraic.AC0.ResidualValue.logicalDepth circuit.program (circuit.outputs output)

def Algebraic.AC0.ResidualCircuit.logicalDepth {n g m : ℕ} (circuit : ResidualCircuit n g m) : ℕ

Maximum logical depth of a residual output.

Equations

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

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

A one-output residual circuit's depth is its sole output depth.

structure Algebraic.AC0.CircuitRestriction {n m : ℕ} (source : Circuit signature n m) (rho : PartialAssignment n) : Type

A circuit-level partial evaluation over the compact namespace of live variables.

• gateCount : ℕ

  Number of gates in the residual circuit.

• result : ResidualCircuit rho.liveCount self.gateCount m

  Residual circuit, including explicit constant outputs.

• eval_eq (input : Fin rho.liveCount → Bool) : self.result.eval input = source.eval interpretation (rho.toLiveInputSubstitution.apply input)

  Exact pointwise semantics under the compact input substitution.

• logicalOutputDepths_le (output : Fin m) : self.result.logicalOutputDepths output ≤ Circuit.logicalOutputDepths source output

  Every residual output is no deeper than its source output.

• gateCount_le : self.gateCount ≤ source.size

  Partial evaluation does not increase total gate count.

• cost_le : self.result.cost ≤ source.cost andOrCost

  Partial evaluation does not increase charged AND/OR cost.

noncomputable def Algebraic.AC0.restrictCircuit {n m : ℕ} (source : Circuit signature n m) (rho : PartialAssignment n) : CircuitRestriction source rho

Partially evaluate an arbitrary-output AC0 circuit under rho.

Equations

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

theorem Algebraic.AC0.CircuitRestriction.logicalDepth_le {n m : ℕ} {source : Circuit signature n m} {rho : PartialAssignment n} (restriction : CircuitRestriction source rho) : restriction.result.logicalDepth ≤ Circuit.logicalDepth source

Exact residual-circuit restriction does not increase logical depth.

theorem Algebraic.AC0.restrictCircuit_eval_projectLive {n m : ℕ} (source : Circuit signature n m) (rho : PartialAssignment n) (input : Fin n → Bool) : (restrictCircuit source rho).result.eval (rho.projectLive input) = source.eval interpretation (rho.apply input)

The compact residual circuit also realizes the original same-width restriction after projecting a complete input to its live coordinates.

Materializing a one-output residual circuit

def Algebraic.AC0.constantLine {n g : ℕ} (value : Bool) : Line signature n g

A nullary gate realizing a Boolean constant.

Equations

• Algebraic.AC0.constantLine false = { op := Algebraic.AC0.Op.or 0, wires := Fin.elim0 }
• Algebraic.AC0.constantLine true = { op := Algebraic.AC0.Op.and 0, wires := Fin.elim0 }

@[simp]

theorem Algebraic.AC0.constantLine_eval {n g : ℕ} (value : Bool) (program : Program signature n g) (input : Fin n → Bool) : (constantLine value).eval interpretation input (program.eval interpretation input) = value

structure Algebraic.AC0.ResidualCircuit.Materialization {n g : ℕ} (source : ResidualCircuit n g 1) : Type

Materializing the sole output of a residual circuit as an ordinary wire requires at most one nullary constant gate.

• result : Circuit signature n 1

  Ordinary one-output circuit.

• eval_eq (input : Fin n → Bool) : self.result.eval interpretation input = source.eval input

  Materialization preserves the residual output.

• logicalDepth_le : Circuit.logicalDepth self.result ≤ source.logicalDepth + 1

  Materializing a constant output adds at most one logical level.

• gateCount_le : self.result.size ≤ g + 1

  At most one gate is added.

• cost_le : self.result.cost andOrCost ≤ source.cost + 1

  At most one charged constant gate is added.

@[reducible, inline]

abbrev Algebraic.AC0.ResidualCircuit.Materialization.gateCount {n g : ℕ} {source : ResidualCircuit n g 1} (materialization : source.Materialization) : ℕ

Gate count of the ordinary circuit.

Equations

• materialization.gateCount = materialization.result.size

def Algebraic.AC0.ResidualCircuit.materialize {n g : ℕ} (source : ResidualCircuit n g 1) : source.Materialization

Convert a one-output residual circuit into an ordinary circuit. Wire outputs are free; constant outputs receive one nullary AND or OR gate.

Equations

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

structure Algebraic.AC0.OrdinaryCircuitRestriction {n : ℕ} (source : Circuit signature n 1) (rho : PartialAssignment n) : Type

An ordinary one-output circuit obtained by partial evaluation. The single unit of possible overhead is exactly the cost of materializing a constant output as a wire.

• result : Circuit signature rho.liveCount 1

  Ordinary circuit over exactly the live variables.

• eval_eq (input : Fin rho.liveCount → Bool) : self.result.eval interpretation input = source.eval interpretation (rho.toLiveInputSubstitution.apply input)

  Exact pointwise semantics under the compact input substitution.

• logicalDepth_le : Circuit.logicalDepth self.result ≤ Circuit.logicalDepth source + 1

  Restriction plus constant-output materialization adds at most one logical level.

• gateCount_le : self.result.size ≤ source.size + 1

  Restriction and output materialization add at most one gate overall.

• cost_le : self.result.cost andOrCost ≤ source.cost andOrCost + 1

  Charged AND/OR cost grows by at most the one constant-output gate.

@[reducible, inline]

abbrev Algebraic.AC0.OrdinaryCircuitRestriction.gateCount {n : ℕ} {source : Circuit signature n 1} {rho : PartialAssignment n} (restriction : OrdinaryCircuitRestriction source rho) : ℕ

Gate count of the materialized restricted circuit.

Equations

• restriction.gateCount = restriction.result.size

noncomputable def Algebraic.AC0.restrictOneOutputCircuit {n : ℕ} (source : Circuit signature n 1) (rho : PartialAssignment n) : OrdinaryCircuitRestriction source rho

Partially evaluate a one-output AC0 circuit and materialize its output as an ordinary circuit wire.

Equations

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

theorem Algebraic.AC0.restrictOneOutputCircuit_eval_projectLive {n : ℕ} (source : Circuit signature n 1) (rho : PartialAssignment n) (input : Fin n → Bool) : (restrictOneOutputCircuit source rho).result.eval interpretation (rho.projectLive input) = source.eval interpretation (rho.apply input)

Same-width semantics of the materialized restricted circuit.