CLRS-Lean
Chapter 34. NP-Completeness
34.4. NP-Completeness Proofs
34.4. Cook--Levin infrastructure
34.4. Verifier circuitization
34.4. Concrete compiler for the canonical transition-family input

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionCompleteQuotedSource
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.UnaryFrameMarkedRowsUnquoteRuntime

Concrete compiler for the canonical transition-family input

The complete quoted row source is followed by the verified multi-row decoder. The result is the exact unary byte stream consumed by the established transition-family controller, not an extensionally equivalent script oracle.

              noncomputable sectionnamespace CLRS.Chapter34.Turing.CookLevinopen PolyBuilder

Decoding the complete marked row source yields the canonical unary transition-family input byte-for-byte.


theorem verifierTransitionCompleteQuotedFamily_unquote_eq_target
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (input : List Γ) :
    unquoteUnaryFrameMarkedRows
        (encodeUnaryFrameMarkedRowFamily
          (verifierTransitionCompleteQuotedFamily W input)) =
      verifierTransitionFamilyUnaryInputTarget W input := by
  rw [verifierTransitionFamilyUnaryInputTarget_eq_flatMap]
  unfold encodeUnaryFrameMarkedRowFamily
  rw [verifierTransitionCompleteQuotedFamily_rows]
  simp only [List.flatMap_map]
  let payload : TransitionRowSeed → List UnaryFrameSym := fun seed =>
    .frameEnd ::
      (encodeAffineStmtControllerScript
          (transitionDispatchScriptFromSeed W.machine.tm seed) ++
        affineStmtTransitionBoundaryCode ++
        encodeAffineTransitionTail
          (transitionScriptFromSeed W.machine.tm seed
            (seed.rowBase + cfgBitCount W.machine.tm seed.height)))
  have decoded := unquoteUnaryFrameMarkedRows_encode_family
    ((verifierTransitionRowSeeds W input).map payload)
  simp only [List.flatMap_map] at decoded
  change unquoteUnaryFrameMarkedRows
      ((verifierTransitionRowSeeds W input).flatMap fun seed =>
        quoteUnaryFrameStream (payload seed) ++ [.frameEnd]) = _
  rw [decoded]
  apply List.flatMap_congr
  intro seed _hseed
  unfold payload transitionSeedLocalUnaryInput
    encodeAffineTransitionLocalUnary transitionScriptFromSeed
    transitionScriptOfDecomposition transitionScriptDecompositionFromSeed
  rfl

Fixed polynomial-time TM2 from the raw verifier word to the exact unary input of the transition-family controller.


noncomputable def
    verifierTransitionFamilyUnaryInputTarget_computableInPolyTime
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L) :
    _root_.Turing.TM2ComputableInPolyTime id id
      (verifierTransitionFamilyUnaryInputTarget W) := by
  let quoted :=
    verifierTransitionCompleteQuotedFamily_computableInPolyTime W
  let quotedRaw : _root_.Turing.TM2ComputableInPolyTime id id
      (fun input => encodeUnaryFrameMarkedRowFamily
        (verifierTransitionCompleteQuotedFamily W input)) :=
    { tm := quoted.tm
      inputAlphabet := quoted.inputAlphabet
      outputAlphabet := quoted.outputAlphabet
      time := quoted.time
      outputsFun := fun input => by
        simpa only [id_eq] using quoted.outputsFun input }
  let composed :=
    _root_.Turing.TM2Comp.TM2ComputableInPolyTime.comp_scratch quotedRaw
      unaryFrameMarkedRowsUnquote_computableInPolyTime
  let result := Classical.choice composed
  exact
    { tm := result.tm
      inputAlphabet := result.inputAlphabet
      outputAlphabet := result.outputAlphabet
      time := result.time
      outputsFun := fun input => by
        have run := result.outputsFun input
        simpa only [Function.comp_def, id_eq,
          verifierTransitionCompleteQuotedFamily_unquote_eq_target W input]
          using run }

Fixed polynomial-time compiler for the exact typed controller input.

noncomputable def
    verifierTransitionFamilyInputTarget_computableInPolyTime
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L) :
    _root_.Turing.TM2ComputableInPolyTime id id
      (verifierTransitionFamilyInputTarget W) :=
  verifierTransitionFamilyInputTarget_computableInPolyTime_of_unaryCompiler W
    (verifierTransitionFamilyUnaryInputTarget_computableInPolyTime W)

The complete semantic transition-gate stream is now generated by one fixed polynomial-time TM2 from the raw verifier input.

noncomputable def verifierTransitionGateStream_computableInPolyTime
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L) :
    _root_.Turing.TM2ComputableInPolyTime id id
      (verifierTransitionGateStream W) :=
  verifierTransitionGateStream_computableInPolyTime_of_inputCompiler W
    (verifierTransitionFamilyInputTarget_computableInPolyTime W)

end CLRS.Chapter34.Turing.CookLevin