Padded circuit satisfiability

The ruler in a query fixes the exact satisfying-assignment width. The resulting language belongs to NP, using the verified serialized circuit evaluator as its deterministic witness checker.

theorem Complexity.CircuitSAT.witness_pair_iff (code ruler witness : List Bool) : Witness (pair code ruler) witness ↔ witness.length = ruler.length ∧ CircuitCode.evalFamilyCode code witness = some true

On a canonical query, witnesses have the ruler's exact width and make the tagged circuit code evaluate to true.

theorem Complexity.CircuitSAT.pair_mem_language_iff (code ruler : List Bool) : pair code ruler ∈ language ↔ ∃ (witness : List Bool), witness.length = ruler.length ∧ CircuitCode.evalFamilyCode code witness = some true

A canonical padded circuit query is accepted exactly when it has a satisfying assignment of the ruler's exact width.

theorem Complexity.CircuitSAT.witness_length_le (query witness : List Bool) (h : Witness query witness) : witness.length ≤ query.length + 1

Every valid circuit-satisfiability witness is linearly bounded by its query length.

theorem Complexity.CircuitSAT.pairLang_witness_mem_P : pairLang Witness ∈ P

The paired verifier language is polynomial-time decidable.

theorem Complexity.CircuitSAT.language_mem_NP : language ∈ NP

Padded circuit satisfiability belongs to NP.

theorem Complexity.CircuitSAT.extensionWitness_pair_iff (code fixedPrefix ruler witness : List Bool) : ExtensionWitness (pair code (pair fixedPrefix ruler)) witness ↔ witness.length = ruler.length ∧ CircuitCode.evalFamilyCode code (fixedPrefix ++ witness) = some true

On a canonical extension query, witnesses have the ruler's exact width and make the circuit accept when appended to the fixed public prefix.

theorem Complexity.CircuitSAT.pair_mem_extensionLanguage_iff (code fixedPrefix ruler : List Bool) : pair code (pair fixedPrefix ruler) ∈ extensionLanguage ↔ ∃ (witness : List Bool), witness.length = ruler.length ∧ CircuitCode.evalFamilyCode code (fixedPrefix ++ witness) = some true

A canonical extension query is accepted exactly when the circuit has an accepting suffix of the ruler's exact width.

theorem Complexity.CircuitSAT.extensionWitness_length_le (query witness : List Bool) (h : ExtensionWitness query witness) : witness.length ≤ query.length + 1

Every valid extension witness is linearly bounded by its query length.

theorem Complexity.CircuitSAT.pairLang_extensionWitness_mem_P : pairLang ExtensionWitness ∈ P

The paired extension verifier language is polynomial-time decidable.

theorem Complexity.CircuitSAT.extensionLanguage_mem_NP : extensionLanguage ∈ NP

Exact-width existential circuit extension belongs to NP.