Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.5. NP-Complete Problems
  4. 34.5. HAM-CYCLE
  5. 34.5. HAM-CYCLE fixed verifier machinery
  6. 34.5. HAM-CYCLE cycle-adjacency verifier
  7. 34.5. HAM-CYCLE cycle-adjacency raw streams
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.VerifierMachine.CyclePairs import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.VerifierMachine.AdjacencyPipeline.RawStreams

HAM-CYCLE verifier: raw cycle-query and graph streams

The existing total certificate/graph canonicalizers are reused unchanged. Only the CLIQUE all-pairs branch is replaced by the verified HAM consecutive- and-closing pair generator.

noncomputable sectionnamespace CLRS.Chapter34.Turing.HamiltonianCycle.VerifierMachine.CycleAdjacencyopen PolyBuilderopen _root_.Turingabbrev RawInput := GeneralCliqueVerifier.AdjacencyPipeline.RawInputdef rawEncoding (input : RawInput) : List (Option CliqueSym) := GeneralCliqueVerifier.AdjacencyPipeline.rawEncoding inputdef rawVertices (input : RawInput) : List Nat := GeneralCliqueVerifier.AdjacencyPipeline.rawVertices inputdef rawInstance (input : RawInput) : CliqueInstance := GeneralCliqueVerifier.AdjacencyPipeline.rawInstance input

Consecutive path pairs and the closing pair from the total decoded certificate.

def rawCyclePairs (input : RawInput) : List (Nat × Nat) := CyclePairs.cyclePairs (rawVertices input)

Canonically oriented cycle-edge queries.

def rawQueries (input : RawInput) : List (Nat × Nat) := (rawCyclePairs input).map GeneralCliqueVerifier.QueryNormalizer.normalizeQuery
def rawQueryStream (input : RawInput) : List CliqueSym := (rawQueries input).flatMap encodeCliqueEdgedef rawGraphStream (input : RawInput) : List CliqueSym := encodeCliqueInstance (rawInstance input)noncomputable def rawCyclePairsComputableInPolyTime : TM2ComputableInPolyTime rawEncoding (fun pairs : List (Nat × Nat) => pairs.flatMap encodeCliqueEdge) rawCyclePairs := by let composed := TM2Comp.TM2ComputableInPolyTime.comp_scratch GeneralCliqueVerifier.AdjacencyPipeline.rawVerticesComputableInPolyTime CyclePairs.pairsComputableInPolyTime change TM2ComputableInPolyTime rawEncoding (fun pairs : List (Nat × Nat) => pairs.flatMap encodeCliqueEdge) (fun input => CyclePairs.cyclePairs (rawVertices input)) exact Classical.choice composednoncomputable def rawQueriesComputableInPolyTime : TM2ComputableInPolyTime rawEncoding (fun pairs : List (Nat × Nat) => pairs.flatMap encodeCliqueEdge) rawQueries := by let composed := TM2Comp.TM2ComputableInPolyTime.comp_scratch rawCyclePairsComputableInPolyTime GeneralCliqueVerifier.QueryNormalizer.normalizer_computableInPolyTime change TM2ComputableInPolyTime rawEncoding (fun pairs : List (Nat × Nat) => pairs.flatMap encodeCliqueEdge) (fun input => (rawCyclePairs input).map GeneralCliqueVerifier.QueryNormalizer.normalizeQuery) simpa [Function.comp_def] using Classical.choice composednoncomputable def rawQueryStreamComputableInPolyTime : TM2ComputableInPolyTime rawEncoding id rawQueryStream := by let queries := rawQueriesComputableInPolyTime exact { tm := queries.tm inputAlphabet := queries.inputAlphabet outputAlphabet := queries.outputAlphabet time := queries.time outputsFun := fun input => by simpa [rawQueryStream] using queries.outputsFun input }noncomputable def rawGraphStreamComputableInPolyTime : TM2ComputableInPolyTime rawEncoding id rawGraphStream := by let graph := GeneralCliqueVerifier.AdjacencyPipeline.rawGraphStreamComputableInPolyTime exact { tm := graph.tm inputAlphabet := graph.inputAlphabet outputAlphabet := graph.outputAlphabet time := graph.time outputsFun := fun input => by simpa [rawEncoding, rawGraphStream, rawInstance, GeneralCliqueVerifier.AdjacencyPipeline.rawGraphStream] using graph.outputsFun input }def queryPairLeft (input : RawInput) : List (Option CliqueSym) := OptionPairLeft.format (rawQueryStream input)def graphPairRight (input : RawInput) : List (Option CliqueSym) := (rawGraphStream input).map somenoncomputable def queryPairLeftComputableInPolyTime : TM2ComputableInPolyTime rawEncoding id queryPairLeft := by let composed := TM2Comp.TM2ComputableInPolyTime.comp_scratch rawQueryStreamComputableInPolyTime (OptionPairLeft.computableInPolyTime CliqueSym) change TM2ComputableInPolyTime rawEncoding id (fun input => OptionPairLeft.format (rawQueryStream input)) exact Classical.choice composednoncomputable def graphPairRightComputableInPolyTime : TM2ComputableInPolyTime rawEncoding id graphPairRight := by let composed := TM2Comp.TM2ComputableInPolyTime.comp_scratch rawGraphStreamComputableInPolyTime (GeneralCliqueVerifier.AdjacencyPipeline.someMapComputableInPolyTime CliqueSym) change TM2ComputableInPolyTime rawEncoding id (fun input => (rawGraphStream input).map some) exact Classical.choice composeddef batchInputStream (input : RawInput) : List (Option CliqueSym) := pairEncoding (rawQueryStream input) (rawGraphStream input)

A fixed polynomial-time TM2 assembles the normalized cycle queries and canonical graph into the shared batch-lookup input format.

noncomputable def batchInputStreamComputableInPolyTime : TM2ComputableInPolyTime rawEncoding id batchInputStream := by let joined := fixedPairSameInputConcat_computableInPolyTime GeneralCliqueVerifier.AdjacencyPipeline.encodeOptionCliqueSymPair GeneralCliqueVerifier.AdjacencyPipeline.decodeOptionCliqueSymPair GeneralCliqueVerifier.AdjacencyPipeline.decode_encodeOptionCliqueSymPair queryPairLeftComputableInPolyTime graphPairRightComputableInPolyTime have machine : TM2ComputableInPolyTime rawEncoding id (fun input => queryPairLeft input ++ graphPairRight input) := joined exact { tm := machine.tm inputAlphabet := machine.inputAlphabet outputAlphabet := machine.outputAlphabet time := machine.time outputsFun := fun input => by have output := machine.outputsFun input have heq : queryPairLeft input ++ graphPairRight input = batchInputStream input := by simp [queryPairLeft, graphPairRight, batchInputStream, OptionPairLeft.format, pairEncoding, List.append_assoc] rw [heq] at output simpa using output }
end CLRS.Chapter34.Turing.HamiltonianCycle.VerifierMachine.CycleAdjacency