module module high

`IndisputableMonolith.Complexity.CircuitLedger`

This module defines gate types, Boolean circuits with evaluation, bond counts, capacity bounds, and defect moats as the structural ledger for circuit analysis in Recognition Science. Researchers on circuit lower bounds and the P vs NP program cite it to track J-frustration and topological obstructions in SAT instances. It consists of definitions and elementary lemmas with no deep proofs.

claimThe module introduces gate types (AND, OR, NOT, etc.), Boolean circuits as DAGs of gates, evaluation maps, bond-count functions, capacity bounds, and defect moats, all equipped with the J-symmetry ledger structure.

background

Recognition Science models complexity via the J-operator and R̂ SAT encoding. Upstream, LedgerForcing shows that J-symmetry forces double-entry ledger structure, while RSatEncoding states that R̂ reaches zero J-cost in O(n) steps for satisfiable k-CNF and produces a non-contractible obstruction for unsatisfiable instances. Constants fix the RS time quantum as τ₀ = 1 tick. The module supplies the concrete circuit objects on which these J-cost and frustration quantities are defined.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The structures feed CircuitLowerBound, which states that high J-frustration implies super-polynomial circuit size, and PvsNPAssembly, which assembles the conditional P ≠ NP path via UniformTopologicalObstructionHyp and the three-phase argument from J-frustration to exponential size. It also supports Core.Complexity. The module closes the structural gap between the abstract J-forcing chain and concrete circuit instances used in the Recognition Science P vs NP program.

scope and limits

Does not prove any circuit-size lower bounds.
Does not compute J-cost or frustration values.
Does not address satisfiability or R̂ directly.
Does not treat quantum or other non-Boolean models.
Does not contain the full P vs NP assembly.

used by (3)

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

IndisputableMonolith.Complexity.CircuitLowerBound module_import
IndisputableMonolith.Complexity.PvsNPAssembly module_import
IndisputableMonolith.Core.Complexity module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Complexity.BalancedParityHidden module_import
IndisputableMonolith.Complexity.RSatEncoding module_import
IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.LedgerForcing module_import

declarations in this module (23)

inductive GateType L73
structure Gate L83
structure BooleanCircuit L96
structure BooleanCircuitWithEval L114
def CircuitWithEvalDecides L120
def CircuitDecides L128
def CircuitBondCount L136
theorem circuit_bond_count_le L140
def CircuitZCapacity L154
theorem circuit_capacity_bound L162
theorem poly_circuit_poly_capacity L167
def DefectMoat L179
theorem moat_width_unsat L185
theorem moat_zero_sat L191
theorem defect_moat_zero_iff_sat L196
theorem circuit_cannot_sense_moat L215
theorem no_sublinear_universal_decoder L226
structure CircuitSeparation L239
theorem circuitSeparation L260
structure SpectralTuringBridgeHypothesis L294
theorem conditional_separation L307
structure CircuitLedgerCert L320
def circuitLedgerCert L337