CLRS-Lean
Chapter 34. NP-Completeness
34.4. NP-Completeness Proofs
34.4. Cook--Levin infrastructure
34.4. Verifier circuitization
34.4. Continuous arithmetic row-validity generation

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorValidityStack
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.ValidityRow

Continuous arithmetic row-validity generation

This module instantiates the fixed whole-row controller with the exact arithmetic one-hot, halted-agreement, stack-canonicality, and final-conjunction data of one Cook--Levin tableau row.

              namespace CLRS.Chapter34.Turing.CookLevinopen PolyBuilderopen StateTransitionnoncomputable section

Exact runtime frame for all validity phases of one arithmetic tableau row.

noncomputable def arithmeticValidityRowFrame
    (tm : _root_.Turing.FinTM2) (H start rowBase : Nat) :
    AffineValidityRowFrame :=
  { oneHotFrames := arithmeticRawOneHotFrames tm H start rowBase
    haltedStart := arithmeticHaltedMatchStart tm H start
    haltedLeft := rowBase
    haltedRight := arithmeticNoneLabelWire tm rowBase
    tailFrame := arithmeticValidityTailFrame tm H start rowBase }

Interpreting the complete runtime frame yields byte-for-byte the canonical semantic validity stream of the arithmetic row.


theorem arithmeticValidityRowGateStream_eq_semantic
    (tm : _root_.Turing.FinTM2) (H start rowBase : Nat) :
    affineValidityRowGateStream
        (arithmeticValidityRowFrame tm H start rowBase) =
      validityRowGateStreamAt tm H start rowBase := by
  rw [validityRowGateStreamAt_eq_rawOneHot_append_post,
    arithmeticValidityPostOneHot_eq_haltedMatch_append_post]
  unfold arithmeticValidityRowFrame affineValidityRowGateStream
  rw [arithmeticRawOneHotFrames_gateStream,
    arithmeticValidityTailGateStream_eq_postHaltedMatch]
  simp [This simp argument is unused:
  arithmeticValidityRowFrame

Hint: Omit it from the simp argument list.
  simp [̵a̵r̵i̵t̵h̵m̵e̵t̵i̵c̵V̵a̵l̵i̵d̵i̵t̵y̵R̵o̵w̵F̵r̵a̵m̵e̵,̵ ̵a̵r̵i̵t̵h̵m̵e̵t̵i̵c̵H̵a̵l̵t̵e̵d̵M̵a̵t̵c̵h̵G̵a̵t̵e̵S̵t̵r̵e̵a̵m̵,̵[̲a̲r̲i̲t̲h̲m̲e̲t̲i̲c̲H̲a̲l̲t̲e̲d̲M̲a̲t̲c̲h̲G̲a̲t̲e̲S̲t̲r̲e̲a̲m̲,̲ List.append_assoc]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`arithmeticValidityRowFrame, arithmeticHaltedMatchGateStream,
    List.append_assoc]

One fixed program executes the complete canonical validity suffix for one arithmetic row, with no intermediate halt.

noncomputable def arithmeticValidityRowRev_runFrom
    (tm : _root_.Turing.FinTM2) (H start rowBase : Nat)
    (output : List CircuitSym) :
    EvalsToInTime (step affineValidityRowRevProgram)
      (affineValidityRowLoopCfg
        (encodeAffineValidityRowFrame
          (arithmeticValidityRowFrame tm H start rowBase)) output)
      (some (haltCfg affineValidityRowRevProgram
        ((validityRowGateStreamAt tm H start rowBase).reverse ++ output)))
      (affineValidityRowRevSteps
        (arithmeticValidityRowFrame tm H start rowBase)) := by
  simpa [arithmeticValidityRowGateStream_eq_semantic] using
    affineValidityRow_run
      (arithmeticValidityRowFrame tm H start rowBase) output

The concrete arithmetic row inherits the controller's explicit quadratic bound in its exact delimiter-bearing runtime frame.

theorem arithmeticValidityRowRev_steps_le
    (tm : _root_.Turing.FinTM2) (H start rowBase : Nat) :
    affineValidityRowRevSteps
        (arithmeticValidityRowFrame tm H start rowBase) ≤
      2500 * (encodeAffineValidityRowFrame
        (arithmeticValidityRowFrame tm H start rowBase)).length ^ 2 + 20 :=
  affineValidityRowRev_steps_le _

endend CLRS.Chapter34.Turing.CookLevin