pith. sign in
module module high

IndisputableMonolith.Complexity.CircuitLedger

show as:
view Lean formalization →

The CircuitLedger module supplies foundational type definitions for Boolean circuits, gates, evaluation, bond counts, and capacity in the Recognition Science complexity setting. Researchers on circuit lower bounds or the P vs NP program cite these structures to model computation with J-frustration. It consists entirely of definitions and basic lemmas with no deep proofs.

claimThe module introduces GateType (gate kinds), Gate, BooleanCircuit, BooleanCircuitWithEval, CircuitBondCount, CircuitZCapacity, and DefectMoat as the basic objects for circuit modeling.

background

This module belongs to the Complexity domain. It imports LedgerForcing, whose doc states it proves that J-symmetry forces double-entry ledger structure, and RSatEncoding, whose doc describes the R̂ operator as a non-natural polytime certifier for SAT with J-cost reaching zero in O(n) steps for satisfiable instances. Constants supplies the RS time quantum τ₀ = 1 tick. Sibling declarations define GateType as gate types in a Boolean circuit, BooleanCircuit as the circuit structure, CircuitBondCount and circuit_capacity_bound for size measures, and DefectMoat for topological features.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions feed CircuitLowerBound, whose doc states it formalizes that high J-frustration implies super-polynomial circuit size, and PvsNPAssembly, whose doc assembles the conditional P ≠ NP path via J-frustration being non-natural and implying exponential size. The module supplies the circuit objects required for the three-step argument in the Recognition Science treatment of complexity.

scope and limits

used by (3)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (23)