GateType

formal source

  70/-! ## Part 1: Boolean Circuit as a Restricted Sub-Ledger -/
  71
  72/-- Gate types in a Boolean circuit. -/
  73inductive GateType
  74  | Input  : GateType   -- leaf node; reads one input variable
  75  | And    : GateType   -- binary conjunction
  76  | Or     : GateType   -- binary disjunction
  77  | Not    : GateType   -- unary negation
  78  | Output : GateType   -- circuit output gate
  79
  80/-- A single gate with its type and parent wire indices.
  81    Wires are numbered 0..(gate_count-1) in topological order,
  82    so parents always have strictly smaller index → DAG guarantee. -/
  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. -/
  96structure BooleanCircuit (n : ℕ) where
  97  /-- Total number of gates (inputs + internal + output) -/
  98  gate_count : ℕ
  99  /-- The gates in topological order -/
 100  gates : Fin gate_count → Gate gate_count
 101  /-- Input gates each reference one variable in {0,..,n-1} -/
 102  input_var : ∀ i : Fin gate_count,
 103    (gates i).gtype = GateType.Input → ∃ _v : Fin n, True