Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.4. NP-Completeness Proofs
  4. 34.4. Cook--Levin infrastructure
  5. 34.4. Verifier circuitization
  6. 34.4. Typed raw-input row families for branch-ending statement results
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionStatementAffineContextBranchRouteSource import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.UnaryFrameMarkedRowDuplicate

Typed raw-input row families for branch-ending statement results

The branch-route source emits one complete marked row per transition seed. This module packages those rows behind the same typed family interface used by normalized linear results.

noncomputable sectionnamespace CLRS.Chapter34.Turing.CookLevinopen PolyBuilder private theorem branchRoute_encodeUnaryFrame_frameEnd_free (values : List Nat) : ∀ symbol ∈ encodeUnaryFrame values, symbol ≠ UnaryFrameSym.frameEnd := by intro symbol hsymbol induction values with | nil => simp [encodeUnaryFrame] at hsymbol | cons value values ih => simp only [encodeUnaryFrame, List.flatMap_cons] at hsymbol rw [List.mem_append] at hsymbol rcases hsymbol with hhead | htail · unfold encodeUnaryFrameBlock at hhead rw [List.mem_append] at hhead rcases hhead with htick | hseparator · have : symbol = UnaryFrameSym.tick := List.eq_of_mem_replicate htick subst symbol decide · have : symbol = UnaryFrameSym.separator := by simpa using hseparator subst symbol decide · exact ih htail

Semantic branch-route rows of one fixed statement context and mux offset.

noncomputable def verifierTransitionStmtBranchRouteFamily {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (labelOffset : TransitionAffineNat) (context : TransitionStmtAffineContext W.machine.tm) (offset : TransitionAffineNat) (input : List Γ) : UnaryFrameMarkedRowFamily := { rows := (verifierTransitionRowSeeds W input).map fun seed => encodeUnaryFrame (transitionStmtBranchRouteValues W.machine.tm seed labelOffset context offset) frameEnd_free := by intro row hrow symbol hsymbol rw [List.mem_map] at hrow rcases hrow with ⟨seed, hseed, rfl⟩ exact branchRoute_encodeUnaryFrame_frameEnd_free _ symbol hsymbol }

The typed family encoding is exactly the concrete affine-segment source stream.

theorem verifierTransitionStmtBranchRouteFamily_encoding_eq {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (input : List Γ) (labelOffset : TransitionAffineNat) (context : TransitionStmtAffineContext W.machine.tm) (offset : TransitionAffineNat) : encodeUnaryFrameMarkedRowFamily (verifierTransitionStmtBranchRouteFamily W labelOffset context offset input) = verifierTransitionStmtBranchRouteFrames W labelOffset context offset input := by rw [verifierTransitionStmtBranchRouteFrames_eq] unfold encodeUnaryFrameMarkedRowFamily verifierTransitionStmtBranchRouteFamily simp [List.flatMap_map]

The typed semantic branch-route family is generated by a concrete fixed polynomial-time TM2 from the original verifier word.

noncomputable def verifierTransitionStmtBranchRouteFamily_computableInPolyTime {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (labelOffset : TransitionAffineNat) (context : TransitionStmtAffineContext W.machine.tm) (offset : TransitionAffineNat) : _root_.Turing.TM2ComputableInPolyTime id encodeUnaryFrameMarkedRowFamily (verifierTransitionStmtBranchRouteFamily W labelOffset context offset) := by let source := verifierTransitionStmtBranchRouteFrames_computableInPolyTime W labelOffset context offset exact { tm := source.tm inputAlphabet := source.inputAlphabet outputAlphabet := source.outputAlphabet time := source.time outputsFun := fun input => by simpa only [id_eq, verifierTransitionStmtBranchRouteFamily_encoding_eq W input labelOffset context offset] using source.outputsFun input }
end CLRS.Chapter34.Turing.CookLevin