CLRS-Lean
Chapter 34. NP-Completeness
34.4. NP-Completeness Proofs
34.4. Cook--Levin infrastructure
34.4. Verifier circuitization
34.4. Canonical affine disjunction families

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionAffineOrGroups

Canonical affine disjunction families

The OR-family controller expects the tail-first coordinates generated by CircuitBuilder.disjunctionGateTrace. This module constructs those frames symbolically from affine wire forms and proves that evaluation commutes with both the single-disjunction recursion and the running-start family recursion.

              noncomputable sectionnamespace CLRS.Chapter34.Turing.CookLevinopen PolyBuilder

Tail-first canonical OR frames over symbolic affine wires.

def transitionAffineOrCanonicalFrameForms
    (start : AffineUnaryTripleForm) :
    List AffineUnaryTripleForm → List TransitionAffineOrPairForm
  | [] => []
  | wire :: rest =>
      transitionAffineOrCanonicalFrameForms start rest ++
        [{ left := wire
           right := transitionAffineFormAddConst start rest.length }]

private theorem transitionDisjunctionGateTrace_wire_eq_start_add_length
    (start : Nat) : ∀ wires : List CircuitBuilder.Wire,
    (CircuitBuilder.disjunctionGateTrace start wires).wire =
      start + wires.length := by
  intro wires
  induction wires with
  | nil => rfl
  | cons wire rest ih =>
      simp [CircuitBuilder.disjunctionGateTrace,
        CircuitBuilder.disjunctionGateTrace_length]

Evaluating symbolic canonical frames gives the literal concrete tail-first frame list.


theorem transitionAffineOrCanonicalFrameForms_eval
    (start : AffineUnaryTripleForm)
    (wires : List AffineUnaryTripleForm)
    (seed : AffineUnaryTripleSeed) :
    (transitionAffineOrCanonicalFrameForms start wires).map
        (fun frame => frame.eval seed) =
      affineOrFinCanonicalFrames
        (affineUnaryTripleFormValue start seed)
        (wires.map fun wire => affineUnaryTripleFormValue wire seed) := by
  induction wires with
  | nil => rfl
  | cons wire rest ih =>
      simp only [transitionAffineOrCanonicalFrameForms,
        List.map_append, List.map_cons, List.map_nil,
        affineOrFinCanonicalFrames]
      rw [ih]
      congr 2
      simp only [TransitionAffineOrPairForm.eval]
      congr 1
      rw [transitionAffineFormAddConst_value]
      rw [transitionDisjunctionGateTrace_wire_eq_start_add_length]
      simp

Symbolic canonical groups with the running gate start advanced by the exact fixed size of every preceding source fiber.

def transitionAffineOrCanonicalGroupFormsFrom :
    AffineUnaryTripleForm → List (List AffineUnaryTripleForm) →
      List TransitionAffineOrGroupForm
  | _, [] => []
  | start, wires :: rest =>
      transitionAffineOrCanonicalFrameForms start wires ::
        transitionAffineOrCanonicalGroupFormsFrom
          (transitionAffineFormAddConst start (wires.length + 1)) rest

theorem transitionAffineOrCanonicalGroupFormsFrom_nonempty
    (start : AffineUnaryTripleForm)
    {families : List (List AffineUnaryTripleForm)}
    (hnonempty : families ≠ []) :
    transitionAffineOrCanonicalGroupFormsFrom start families ≠ [] := by
  cases families with
  | nil => exact (hnonempty rfl).elim
  | cons wires rest => simp [transitionAffineOrCanonicalGroupFormsFrom]

Evaluation commutes with the complete running-start group recursion.


theorem transitionAffineOrCanonicalGroupFormsFrom_eval
    (start : AffineUnaryTripleForm)
    (families : List (List AffineUnaryTripleForm))
    (seed : AffineUnaryTripleSeed) :
    (transitionAffineOrCanonicalGroupFormsFrom start families).map
        (fun group => group.map fun frame => frame.eval seed) =
      affineOrFinCanonicalGroupsFrom
        (affineUnaryTripleFormValue start seed)
        (families.map fun wires =>
          wires.map fun wire => affineUnaryTripleFormValue wire seed) := by
  induction families generalizing start with
  | nil => rfl
  | cons wires rest ih =>
      simp only [transitionAffineOrCanonicalGroupFormsFrom,
        List.map_cons, affineOrFinCanonicalGroupsFrom]
      rw [transitionAffineOrCanonicalFrameForms_eval]
      congr 1
      rw [ih]
      rw [transitionAffineFormAddConst_value]
      rw [CircuitBuilder.disjunctionGateTrace_length]
      simp

Raw-input target for a fixed symbolic canonical disjunction family.

noncomputable def verifierTransitionAffineCanonicalOrGroups
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (start : AffineUnaryTripleForm)
    (families : List (List AffineUnaryTripleForm))
    (hnonempty : families ≠ []) (input : List Γ) : List UnaryFrameSym :=
  verifierTransitionAffineOrGroups W
    (transitionAffineOrCanonicalGroupFormsFrom start families)
    (transitionAffineOrCanonicalGroupFormsFrom_nonempty start hnonempty)
    input

The raw-input compiler emits the exact concrete canonical family at every transition row seed.


theorem verifierTransitionAffineCanonicalOrGroups_eq_rows
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (start : AffineUnaryTripleForm)
    (families : List (List AffineUnaryTripleForm))
    (hnonempty : families ≠ []) (input : List Γ) :
    verifierTransitionAffineCanonicalOrGroups W start families hnonempty
        input =
      (verifierTransitionRowSeeds W input).flatMap fun seed =>
        encodeAffineOrFinGroups
          (affineOrFinCanonicalGroupsFrom
            (affineUnaryTripleFormValue start
              (transitionTailAffineSeed seed))
            (families.map fun wires => wires.map fun wire =>
              affineUnaryTripleFormValue wire
                (transitionTailAffineSeed seed))) := by
  unfold verifierTransitionAffineCanonicalOrGroups
  rw [verifierTransitionAffineOrGroups_eq_rows]
  apply List.flatMap_congr
  intro seed hseed
  rw [transitionAffineOrCanonicalGroupFormsFrom_eval]

One fixed polynomial-time TM2 emits the exact canonical symbolic disjunction family directly from the original verifier input.

noncomputable def
    verifierTransitionAffineCanonicalOrGroups_computableInPolyTime
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (start : AffineUnaryTripleForm)
    (families : List (List AffineUnaryTripleForm))
    (hnonempty : families ≠ []) :
    _root_.Turing.TM2ComputableInPolyTime id id
      (verifierTransitionAffineCanonicalOrGroups W start families
        hnonempty) :=
  verifierTransitionAffineOrGroups_computableInPolyTime W
    (transitionAffineOrCanonicalGroupFormsFrom start families)
    (transitionAffineOrCanonicalGroupFormsFrom_nonempty start hnonempty)

end CLRS.Chapter34.Turing.CookLevin