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. Exact-polynomial sources for canonical `EqFin` frames
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionEqFrames import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.ExactPolynomialAffineUnaryTripleProgression import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.UnaryFrameSameInputConcat

Exact-polynomial sources for canonical EqFin frames

This module packages a recurring Cook--Levin source pattern. Seven fixed polynomials describe a row-major progression of triples (previous, left, right). The established affine-map and delimiter controllers turn each triple into the exact runtime encoding of one AffineEqFinPairFrame.

The construction is independent of transition semantics and is reused by the post-transition initial and accepting boundaries.

noncomputable sectionnamespace CLRS.Chapter34.Turing.CookLevinopen PolyBuilder

Repackage every row of a triple progression for the generic affine map.

def eqFinProgressionSeeds (progression : AffineUnaryTripleProgression) : List AffineUnaryTripleSeed := (affineUnaryTripleProgressionRows progression).map transitionEqCoordinateSeed

Interpret (previous, left, right) triples as canonical equality frames.

def eqFinProgressionFrames (progression : AffineUnaryTripleProgression) : List AffineEqFinPairFrame := (eqFinProgressionSeeds progression).map transitionEqCoordinateFrame

The progression controller's output is literally the generic seed-family encoding expected by the affine-map controller.

theorem affineUnaryTripleProgressionFrameStream_eq_eqFinSeeds (progression : AffineUnaryTripleProgression) : affineUnaryTripleProgressionFrameStream progression = encodeAffineUnaryTripleSeedFamily (eqFinProgressionSeeds progression) := by unfold affineUnaryTripleProgressionFrameStream eqFinProgressionSeeds generalize affineUnaryTripleProgressionRows progression = rows induction rows with | nil => rfl | cons row rest ih => rcases row with ⟨first, second, third⟩ simp only [List.flatMap_cons, List.map_cons, encodeAffineUnaryTripleSeedFamily] rw [ih] rfl

Fixed delimiter materialization for an arbitrary equality-frame family.

theorem eqFinInvocationDelimiter_frames (frames : List AffineEqFinPairFrame) : encodeUnaryFrameWithDelimiterCycle transitionEqInvocationDelimiterTable transitionEqInvocationDelimiterTable_nonempty (frames.flatMap fun frame => [0, frame.eqStart, frame.left, frame.right, 0, frame.matched, 0, frame.previous, 0]) = encodeAffineEqFinFrames frames := by induction frames with | nil => rfl | cons frame frames ih => simp [encodeUnaryFrameWithDelimiterCycle, encodeUnaryFrameWithDelimiterCycleFrom, transitionEqInvocationDelimiterTable, unaryFrameDelimiterNext, encodeAffineEqFinFrames, encodeAffineEqFinPairFrame, encodeUnaryFrame, encodeUnaryFrameBlock, List.append_assoc] change encodeUnaryFrameWithDelimiterCycle transitionEqInvocationDelimiterTable transitionEqInvocationDelimiterTable_nonempty (frames.flatMap fun frame => [0, frame.eqStart, frame.left, frame.right, 0, frame.matched, 0, frame.previous, 0]) = encodeAffineEqFinFrames frames exact ih

The fixed nine-symbol delimiter cycle materializes the exact encoding of every equality frame generated by a triple progression.

theorem eqFinProgression_delimiter_eq_frames (progression : AffineUnaryTripleProgression) : rewriteUnaryFrameDelimiters transitionEqInvocationDelimiterTable transitionEqInvocationDelimiterTable_nonempty (encodeUnaryFrame (affineUnaryTripleMapFamily transitionEqInvocationForms (eqFinProgressionSeeds progression))) = encodeAffineEqFinFrames (eqFinProgressionFrames progression) := by rw [rewriteUnaryFrameDelimiters_encodeUnaryFrame] unfold eqFinProgressionFrames affineUnaryTripleMapFamily generalize eqFinProgressionSeeds progression = seeds have hvalues : seeds.flatMap (affineUnaryTripleMap transitionEqInvocationForms) = seeds.flatMap fun seed => let frame := transitionEqCoordinateFrame seed [0, frame.eqStart, frame.left, frame.right, 0, frame.matched, 0, frame.previous, 0] := by apply List.flatMap_congr intro seed _hseed exact transitionEqInvocationForms_value seed rw [hvalues] simpa only [List.flatMap_map] using eqFinInvocationDelimiter_frames (seeds.map transitionEqCoordinateFrame)

Exact runtime equality frames whose three source coordinates are fixed polynomials of the raw input length and the row index.

def exactPolynomialAffineEqFinFrames {Γ : Type} (basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count : Polynomial Nat) (input : List Γ) : List AffineEqFinPairFrame := eqFinProgressionFrames (exactPolynomialAffineUnaryTripleProgression basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count input)

Pointwise closed form of an exact-polynomial equality progression.

theorem exactPolynomialAffineEqFinFrames_eq_ofFn {Γ : Type} (basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count : Polynomial Nat) (input : List Γ) : exactPolynomialAffineEqFinFrames basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count input = List.ofFn fun index : Fin (count.eval input.length) => { eqStart := basePrevious.eval input.length + index.val * stepPrevious.eval input.length + 1 left := baseLeft.eval input.length + index.val * stepLeft.eval input.length right := baseRight.eval input.length + index.val * stepRight.eval input.length matched := basePrevious.eval input.length + index.val * stepPrevious.eval input.length + 5 previous := basePrevious.eval input.length + index.val * stepPrevious.eval input.length } := by unfold exactPolynomialAffineEqFinFrames eqFinProgressionFrames eqFinProgressionSeeds rw [affineUnaryTripleProgressionRows_eq_ofFn, List.map_ofFn, List.map_ofFn] apply List.ofFn_inj.mpr funext index simp [exactPolynomialAffineUnaryTripleProgression, transitionEqCoordinateSeed, transitionEqCoordinateFrame]

Byte-exact input consumed by the established EqFin controller.

def exactPolynomialAffineEqFinInput {Γ : Type} (basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count : Polynomial Nat) (input : List Γ) : List UnaryFrameSym := encodeAffineEqFinFrames (exactPolynomialAffineEqFinFrames basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count input)

A fixed polynomial-time TM2 emits the exact canonical equality frames described by seven fixed natural polynomials.

noncomputable def exactPolynomialAffineEqFinInput_computableInPolyTime {Γ : Type} [Fintype Γ] (basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count : Polynomial Nat) : _root_.Turing.TM2ComputableInPolyTime id id (@exactPolynomialAffineEqFinInput Γ basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count) := by let progressionSource := exactPolynomialAffineUnaryTripleProgressionFrameStream_computableInPolyTime (Γ := Γ) basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count let progressionStructured : _root_.Turing.TM2ComputableInPolyTime id encodeAffineUnaryTripleSeedFamily (fun input : List Γ => eqFinProgressionSeeds (exactPolynomialAffineUnaryTripleProgression basePrevious baseLeft baseRight stepPrevious stepLeft stepRight count input)) := { tm := progressionSource.tm inputAlphabet := progressionSource.inputAlphabet outputAlphabet := progressionSource.outputAlphabet time := progressionSource.time outputsFun := fun input => by have run := progressionSource.outputsFun input simp only [id_eq, exactPolynomialAffineUnaryTripleProgressionFrameStream] at run rw [affineUnaryTripleProgressionFrameStream_eq_eqFinSeeds] at run simpa only [id_eq] using run } let mappedExists := _root_.Turing.TM2Comp.TM2ComputableInPolyTime.comp_scratch progressionStructured (affineUnaryTripleMapFamily_computableInPolyTime transitionEqInvocationForms) let mapped := Classical.choice mappedExists let delimitedExists := _root_.Turing.TM2Comp.TM2ComputableInPolyTime.comp_scratch mapped (unaryFrameDelimiterMap_computableInPolyTime transitionEqInvocationDelimiterTable transitionEqInvocationDelimiterTable_nonempty) let result := Classical.choice delimitedExists exact { tm := result.tm inputAlphabet := result.inputAlphabet outputAlphabet := result.outputAlphabet time := result.time outputsFun := fun input => by have run := result.outputsFun input simp only [Function.comp_def, id_eq] at run rw [eqFinProgression_delimiter_eq_frames] at run simpa only [id_eq, exactPolynomialAffineEqFinInput, exactPolynomialAffineEqFinFrames] using run }

Fixed finite families of polynomial segments

Seven polynomial coordinates describing one contiguous equality segment.

structure PolynomialAffineEqFinSpec where basePrevious : Polynomial Nat baseLeft : Polynomial Nat baseRight : Polynomial Nat stepPrevious : Polynomial Nat stepLeft : Polynomial Nat stepRight : Polynomial Nat count : Polynomial Nat

Exact equality input generated by one polynomial segment specification.

def polynomialAffineEqFinSpecInput {Γ : Type} (spec : PolynomialAffineEqFinSpec) (input : List Γ) : List UnaryFrameSym := exactPolynomialAffineEqFinInput spec.basePrevious spec.baseLeft spec.baseRight spec.stepPrevious spec.stepLeft spec.stepRight spec.count input

Concatenate a fixed finite list of equality segments in semantic order.

def polynomialAffineEqFinFamilyInput {Γ : Type} (specs : List PolynomialAffineEqFinSpec) (input : List Γ) : List UnaryFrameSym := specs.flatMap fun spec => polynomialAffineEqFinSpecInput spec input

A fixed finite family of exact-polynomial equality segments is itself compiled by one fixed polynomial-time TM2.

noncomputable def polynomialAffineEqFinFamilyInput_computableInPolyTime {Γ : Type} [Fintype Γ] (specs : List PolynomialAffineEqFinSpec) : _root_.Turing.TM2ComputableInPolyTime id id (@polynomialAffineEqFinFamilyInput Γ specs) := by induction specs with | nil => let empty := exactPolynomialAffineEqFinInput_computableInPolyTime (Γ := Γ) 0 0 0 0 0 0 0 exact { tm := empty.tm inputAlphabet := empty.inputAlphabet outputAlphabet := empty.outputAlphabet time := empty.time outputsFun := fun input => by have run := empty.outputsFun input simpa [polynomialAffineEqFinFamilyInput, exactPolynomialAffineEqFinInput, exactPolynomialAffineEqFinFrames, eqFinProgressionFrames, eqFinProgressionSeeds, exactPolynomialAffineUnaryTripleProgression, affineUnaryTripleProgressionRows, affineUnaryTripleProgressionRowsFrom, encodeAffineEqFinFrames] using run } | cons spec rest ih => let head := exactPolynomialAffineEqFinInput_computableInPolyTime (Γ := Γ) spec.basePrevious spec.baseLeft spec.baseRight spec.stepPrevious spec.stepLeft spec.stepRight spec.count let combined := unaryFrameSameInputConcat_computableInPolyTime head ih exact { tm := combined.tm inputAlphabet := combined.inputAlphabet outputAlphabet := combined.outputAlphabet time := combined.time outputsFun := fun input => by have run := combined.outputsFun input simpa [polynomialAffineEqFinFamilyInput, polynomialAffineEqFinSpecInput] using run }
end CLRS.Chapter34.Turing.CookLevin