GateType
plain-language theorem explainer
GateType enumerates the five operations permitted in a Boolean circuit modeled as a restricted sub-ledger in Recognition Science. Researchers formalizing the P versus NP gap cite it when constructing feed-forward DAGs that lack global J-cost coupling across the Z³ lattice. The inductive definition lists Input for variable reads, And and Or for binary operations, Not for negation, and Output for the result.
Claim. The inductive type of gate types consists of the five constructors Input (leaf node reading one variable), And (binary conjunction), Or (binary disjunction), Not (unary negation), and Output (circuit result).
background
The CircuitLedger module treats Boolean circuits as feed-forward sub-ledgers inside the Recognition Science framework. Each circuit of size S forms a DAG in which wires are indexed 0 to S-1 in topological order, so every parent index is strictly smaller than its gate index. GateType supplies the allowed operations at each node: reading an input variable, performing conjunction or disjunction on two parents, negating a single parent, or emitting the final output.
proof idea
This is an inductive definition that introduces the five constructors directly. No lemmas are applied; the declaration itself supplies the type whose inhabitants are later used inside the Gate structure.
why it matters
GateType anchors Stage 1 of the module by supplying the node labels for the BooleanCircuit structure. That structure in turn supports the capacity bound CircuitZCapacity c ≤ 2 * c.gate_count and the defect-moat argument that poly-size circuits cannot sense the full J-cost separation proved in RSatEncoding. The definition therefore participates in the reduction of P versus NP to the question whether a feed-forward circuit can simulate the global recognition operator R̂.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.