pith. machine review for the scientific record. sign in
structure definition def or abbrev

Gate

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  83structure Gate (S : ℕ) where
  84  /-- Gate type -/
  85  gtype    : GateType
  86  /-- Parent gate indices (at most 2 for binary gates) -/
  87  parents  : List (Fin S)
  88  /-- Locality: at most 2 parents (no gate sees more than 2 predecessors) -/
  89  arity_le : parents.length ≤ 2
  90  /-- Feed-forward: all parent indices are strictly less than this gate's index -/
  91  ff_bound : ∀ p ∈ parents, (p : ℕ) < S
  92
  93/-- A Boolean circuit of size S over n input variables.
  94    This is a *restricted sub-ledger*: feed-forward, locally deterministic,
  95    no global coupling across the Z³ lattice. -/

used by (27)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.