Padded circuit satisfiability -- proof internals

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

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

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

theorem Complexity.CircuitSAT.pairLang_witness_mem_P_internal : pairLang Witness ∈ P

theorem Complexity.CircuitSAT.language_mem_NP_internal : language ∈ NP

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

theorem Complexity.CircuitSAT.pair_mem_extensionLanguage_iff_internal (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

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

theorem Complexity.CircuitSAT.pairLang_extensionWitness_mem_P_internal : pairLang ExtensionWitness ∈ P

theorem Complexity.CircuitSAT.extensionLanguage_mem_NP_internal : extensionLanguage ∈ NP