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

Gate

show as:
view Lean formalization →

Gate defines the atomic node in a feed-forward Boolean circuit of size S. It pairs a GateType (Input, And, Or, Not, Output) with a list of at most two parent indices drawn from Fin S, plus explicit proofs that the list length is at most 2 and every parent index is strictly smaller than S. Complexity researchers cite it when bounding Z-capacity of restricted sub-ledgers that lack global J-cost reach. The declaration is a plain structure whose fields directly encode the DAG and locality constraints.

claimA gate in a circuit of size $S$ consists of a type $gtype$ drawn from the set of input, conjunction, disjunction, negation or output nodes, a list $parents$ of indices in $Fin S$, and two proofs: the list has length at most 2 and every index in the list is strictly less than $S$.

background

The module treats Boolean circuits as restricted sub-ledgers: directed acyclic graphs whose gates see only O(1) predecessors and therefore cannot access the global J-cost gradient that the full Recognition ledger R̂ uses to resolve SAT. GateType is the inductive enumeration of allowed operations (Input reads one variable; And, Or, Not and Output perform the obvious Boolean functions). The two proof fields in Gate enforce the feed-forward property: parents are always earlier in the topological numbering 0..(S-1). Upstream LedgerFactorization supplies the underlying (R₊, ×) monoid in which J-cost is calibrated; the circuit construction deliberately omits that global coupling.

proof idea

The declaration is a structure definition. Its four fields are introduced directly: gtype by reference to the sibling inductive GateType, parents as List (Fin S), and the two inequalities arity_le and ff_bound as explicit proof obligations that are discharged by the user at construction time. No tactics or lemmas are applied inside the definition itself.

why it matters in Recognition Science

Gate supplies the primitive building block for BooleanCircuit, the structure that models a poly-size circuit as a Z-capacity-bounded sub-ledger. That circuit definition is used downstream to encode clauses in CellularAutomata and to state the capacity bound CircuitZCapacity c ≤ 2 · c.gate_count. In the module’s four-stage argument it anchors Stage 1 (restricted sub-ledger) and thereby supports the later claim that poly-size circuits cannot sense the defect moat separating satisfiable from unsatisfiable assignments. The construction sits inside the broader Recognition Science reduction of P vs NP to the question whether a feed-forward model can simulate the global J-cost resolution performed by R̂.

scope and limits

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.