Feedforward circuit

FeedForwardstructure

A layered feedforward circuit: a depth, a type of nodes at each layer, and a Gate for every node above the input layer reading only from the layer below. Acyclicity is structural rather than a side condition, which is what makes induction over the layers available.

structure FeedForward (α : Type u) (inp : Type v) (out : Type v) where
  /-- Number of gate layers above the inputs. -/
  depth : ℕ
  /-- The nodes at each layer; layer `0` is the input layer. -/
  nodes : Fin (depth + 1) → Type v
  /-- Every node above layer zero is a gate reading from the layer below it. -/
  gates : (d : Fin depth) → nodes d.succ → Gate α (nodes d.castSucc)
  /-- Layer zero is the circuit's input. -/
  nodes_zero : nodes 0 = inp
  /-- The top layer is the circuit's output. -/
  nodes_last : nodes (Fin.last depth) = out

Builds on

Wired gate

import Conjectura.Defs.ComputerScience.Complexity.CircuitComplexity.FeedForward · maintainer — open · raw source

Adapted for Conjectura from Yichuan Wang's `AC0[2] Circuit Lower Bounds` in the UC Berkeley Lean course final projects, Apache 2.0. Split into one concept per module.

Copyright (c) 2026 Yichuan Wang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yichuan Wang

Full credits