Wired gate

Conjectura.Defs.ComputerScience.Complexity.CircuitComplexity.Gate

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

/-! # Wired gate

## 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 **gate** is a `GateOp` together with the wiring that says where each of its
inputs comes from. -/
structure Gate (α : Type u) (domain : Type v) where
  /-- The operation this gate performs. -/
  op : GateOp α
  /-- Where each input is read from. -/
  inputs : op.ι → domain

end Conjectura.CircuitComplexity