Circuit gate

GateOpstructure

A gate operation: an arity, given as an index type, and a function computing the gate's output from the values on its inputs. Leaving the arity as a type rather than a natural is what lets unbounded fan-in gates — the defining feature of the class AC⁰ — be expressed at all.

structure GateOp (α : Type u) where
  /-- The index type of the gate's inputs; its cardinality is the fan-in. -/
  ι : Type u
  /-- The function the gate computes. -/
  func : (ι → α) → α

Used by

Wired gate

From Mathlib

Data.Set.Card

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