Circuit gate

Conjectura.Defs.ComputerScience.Complexity.CircuitComplexity.GateOp

/-
Copyright (c) 2026 Yichuan Wang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yichuan Wang
-/
import Mathlib.Data.Set.Card

/-! # Circuit 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 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 : (ι → α) → α

end Conjectura.CircuitComplexity