Prove2Me

CookLevin.initialClauseEmitter_polyTime_core_reduction_child

Open

by Rizwan · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

Reduction child lemma for CookLevin.initialClauseEmitter_polyTime_core

Formal statement
import Definitions.Def_CookLevin_Reduction
open CookLevin

theorem CookLevin.initialClauseEmitter_polyTime_core_reduction_child (k G Q cw dw ct dt : Nat) :
    IsPolyTimeComputable (fun x =>
      encodeFormula (startClauses ⟨k, G, Q, tabWidth cw dw ct dt x⟩
        (reductionInit (boolsToSymbols x) (certLen cw dw x)))) := by sorry

View graph