Feedforward circuit

Conjectura.Defs.ComputerScience.Complexity.CircuitComplexity.FeedForward

/-
Copyright (c) 2026 Yichuan Wang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yichuan Wang
-/
import Conjectura.Defs.ComputerScience.Complexity.CircuitComplexity.Gate

/-! # Feedforward circuit

## Source

Adapted for Conjectura from Yichuan Wang's `AC0[2] Circuit Lower Bounds` in the
[UC Berkeley Lean course final projects](https://github.com/ucb-lean-course-sp26/final-projects),
Apache 2.0. Split into one concept per module.
-/

namespace Conjectura.CircuitComplexity

universe u v

/-- 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

end Conjectura.CircuitComplexity