Wired gate

Gatestructure

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

Builds on

Circuit gate

Used by

Feedforward circuit

import Conjectura.Defs.ComputerScience.Complexity.CircuitComplexity.Gate · 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