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. Source compilation for the first validity row's halted frame
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorValidityRows import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.ExactPolynomialUnaryFrameFamily

Source compilation for the first validity row's halted frame

This module turns the three unary operands of the first Cook--Levin validity row's halted/none-label equality phase into an actual source-to-script compiler. Unlike the row controller's conditional interface, its input is the raw verifier word. The fixed verifier witness determines three exact natural polynomials, and a concrete polynomial-time TM2 emits their complete delimiter-bearing unary encoding.

noncomputable sectionnamespace CLRS.Chapter34.Turing.CookLevinopen _root_.Turingopen PolyBuilder

Exact arithmetic operands

Exact affine polynomial for the number of gates emitted by the raw one-hot phase of one validity row.

noncomputable def rawOneHotGatePolynomial (tm : _root_.Turing.FinTM2) : Polynomial Nat := by letI : Fintype tm.K := tm.kFin exact Polynomial.C ((3 * (labelCount tm + 1) + 4) + (3 * stateCount tm + 4) + 7 * Fintype.card tm.K) + Polynomial.C (∑ k : tm.K, (3 * ((reachableAlphabet tm k).card + 1) + 7)) * Polynomial.X

The affine polynomial agrees exactly with the arithmetic raw-one-hot gate count used by the concrete row controller.

@[simp] theorem rawOneHotGatePolynomial_eval (tm : _root_.Turing.FinTM2) (H : Nat) : (rawOneHotGatePolynomial tm).eval H = arithmeticRawOneHotGateCount tm H := by letI : Fintype tm.K := tm.kFin simp only [rawOneHotGatePolynomial, Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_X] unfold arithmeticRawOneHotGateCount rw [show (∑ k : tm.K, ((3 * (H + 1) + 4) + H * (3 * ((reachableAlphabet tm k).card + 1) + 4))) = 7 * Fintype.card tm.K + H * (∑ k : tm.K, (3 * ((reachableAlphabet tm k).card + 1) + 7)) by calc _ = ∑ k : tm.K, (7 + H * (3 * ((reachableAlphabet tm k).card + 1) + 7)) := by apply Finset.sum_congr rfl intro k _ ring _ = 7 * Fintype.card tm.K + H * (∑ k : tm.K, (3 * ((reachableAlphabet tm k).card + 1) + 7)) := by rw [Finset.sum_add_distrib] congr 1 · simp [Nat.mul_comm] · exact (Finset.mul_sum Finset.univ (fun k : tm.K => 3 * ((reachableAlphabet tm k).card + 1) + 7) H).symm] ring

Exact polynomial for the first validity row's initial fresh-gate index.

def verifierFirstValidityRowStartPolynomial {Γ : Type} {L : Language Γ} (W : VerifierWitness L) : Polynomial Nat := verifierTableauInputPolynomial W + 2

The three exact input-length polynomials consumed by the halted/none-label equality phase of the first validity row.

noncomputable def verifierFirstValidityHaltedPolynomials {Γ : Type} {L : Language Γ} (W : VerifierWitness L) : List (Polynomial Nat) := [verifierFirstValidityRowStartPolynomial W + (rawOneHotGatePolynomial W.machine.tm).comp (verifierHeight W), 0, Polynomial.C (labelCount W.machine.tm + 1)]

Concrete source-to-script compiler

Delimiter-bearing runtime operands for the first row's halted/none-label equality controller, computed solely from the raw verifier input.

noncomputable def verifierFirstValidityHaltedFrame {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (input : List Γ) : List UnaryFrameSym := exactPolynomialUnaryFrames (verifierFirstValidityHaltedPolynomials W) input

The generated operands are the closed arithmetic halted-start, halted wire, and none-label wire of the first tableau row.

theorem verifierFirstValidityHaltedFrame_eq_arithmetic {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (input : List Γ) : verifierFirstValidityHaltedFrame W input = encodeUnaryFrame [arithmeticHaltedMatchStart W.machine.tm ((verifierHeight W).eval input.length) (tableauInputCount W.machine.tm ((verifierHeight W).eval input.length) ((verifierHorizon W).eval input.length) + 2), 0, arithmeticNoneLabelWire W.machine.tm 0] := by simp [verifierFirstValidityHaltedFrame, verifierFirstValidityHaltedPolynomials, exactPolynomialUnaryFrames, verifierFirstValidityRowStartPolynomial, arithmeticHaltedMatchStart, arithmeticNoneLabelWire, Polynomial.eval_add, Polynomial.eval_comp]

The generated byte stream agrees field-for-field with the actual AffineValidityRowFrame passed to the first row controller.

theorem verifierFirstValidityHaltedFrame_eq_rowFields {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (input : List Γ) : let H := (verifierHeight W).eval input.length let T := (verifierHorizon W).eval input.length let frame := arithmeticValidityRowFrame W.machine.tm H (tableauInputCount W.machine.tm H T + 2) 0 verifierFirstValidityHaltedFrame W input = encodeUnaryFrame [frame.haltedStart, frame.haltedLeft, frame.haltedRight] := by simpa [arithmeticValidityRowFrame] using verifierFirstValidityHaltedFrame_eq_arithmetic W input

The arithmetic row used above is literally the head of the runtime frame family supplied to the complete validity-row controller.

theorem verifierValidityRowFramesByLength_head {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (inputLength : Nat) : (verifierValidityRowFramesByLength W inputLength).head? = some (arithmeticValidityRowFrame W.machine.tm ((verifierHeight W).eval inputLength) (tableauInputCount W.machine.tm ((verifierHeight W).eval inputLength) ((verifierHorizon W).eval inputLength) + 2) 0) := by simp [verifierValidityRowFramesByLength, arithmeticValidityRowFrames, tableauRowCount]

In the actual first-row runtime encoding, the compiled byte stream is exactly the middle operand frame between the one-hot and tail delimiters.

theorem encodeFirstValidityRowFrame_eq_compiledHalted {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (input : List Γ) : let H := (verifierHeight W).eval input.length let T := (verifierHorizon W).eval input.length let frame := arithmeticValidityRowFrame W.machine.tm H (tableauInputCount W.machine.tm H T + 2) 0 encodeAffineValidityRowFrame frame = encodeAffineExactlyOneFamily frame.oneHotFrames ++ .frameEnd :: (verifierFirstValidityHaltedFrame W input ++ .frameEnd :: encodeAffineValidityTailFrame frame.tailFrame) := by dsimp only rw [encodeAffineValidityRowFrame, verifierFirstValidityHaltedFrame_eq_rowFields]

A fixed polynomial-time TM2 compiles the raw verifier word directly into the actual halted/none-label operand frame of its first validity row.

noncomputable def verifierFirstValidityHaltedFrame_computableInPolyTime {Γ : Type} {L : Language Γ} (W : VerifierWitness L) : TM2ComputableInPolyTime id id (verifierFirstValidityHaltedFrame W) := by letI : Fintype Γ := W.alphabetFintype exact exactPolynomialUnaryFrames_computableInPolyTime (verifierFirstValidityHaltedPolynomials W)
end CLRS.Chapter34.Turing.CookLevin