Gate
plain-language theorem explainer
A structure that encodes one gate inside a circuit of size S, with a type drawn from the five-element set of input, binary, and unary operations together with a list of at most two strictly earlier parent indices. Complexity theorists comparing Boolean circuits to the global J-cost gradient in Recognition Science cite this when they need the local DAG constraint that separates restricted sub-ledgers from the full Z³ ledger. The definition is purely structural: its four fields directly embed the arity and feed-forward conditions with no separate
Claim. A gate in a circuit of size $S$ consists of a type $g$ belonging to the set {Input, And, Or, Not, Output}, a list $p$ of parent indices satisfying $|p|≤2$, and the two predicates that every index in $p$ is strictly less than $S$ and that the list length is at most two.
background
The CircuitLedger module treats Boolean circuits as feed-forward sub-ledgers: directed acyclic graphs whose nodes see only O(1) predecessors and therefore lack the global J-cost coupling that the full Recognition ledger R̂ maintains across the Z³ lattice. GateType enumerates the five possible operations: Input reads one variable, And and Or perform binary conjunction and disjunction, Not performs unary negation, and Output marks the circuit result. The module doc states that this construction is Stage 1 of the four-stage argument that reduces the P-vs-NP gap in Recognition Science to the question whether a poly-size circuit can simulate the global recognition steps that resolve SAT.
proof idea
This is a structural definition whose fields directly encode the required locality and topological-order constraints; no lemmas are applied and the body is empty.
why it matters
Gate supplies the atomic node type for the BooleanCircuit structure that appears in downstream results such as CellularAutomata encodings and the circuit-capacity bound. It realizes the first stage of the module’s separation argument: a restricted sub-ledger whose Z-capacity is bounded by twice the gate count, thereby setting up the defect-moat comparison proved in RSatEncoding. The definition therefore sits inside the larger chain that asks whether poly-size circuits can cross the J-cost moat without exponential depth overhead.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.