Skip to content
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.Header import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.WidgetEdges.Formatter import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.NondegeneratePrefix import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.SelectorClique.Formatter import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.Incidence.Scanner.Runtime import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.Incidence.Chain.Runtime import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.Incidence.Endpoints.Runtime import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.SelectorEndpoints.Formatter import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.Ordinary.Runtime import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.Ordinary.Semantics import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.BranchClassifier.Runtime import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.BranchSelector.Runtime import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.TypedTotal.Runtime import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.TypedTotal.Semantics import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.RawTotal.Runtime import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.ReductionMachine.Runtime

Fixed VERTEX-COVER to HAM-CYCLE reduction machinery

Exports the verified fixed-machine stages used to compute the total raw reduction. The nondegenerate target header, all fourteen internal gadget edges per source-edge occurrence, and the complete selector clique are now generated by fixed polynomial-time TM2s. The shared incidence stage now also has a fixed polynomial-time scanner from the raw VERTEX-COVER encoding to the canonical per-vertex occurrence rows and formats those rows into every successive incidence-chain edge. A second fixed pipeline extracts the two gadget ports at the ends of every nonempty incidence row, repeats them for every selector, and formats the complete selector-endpoint edge multiset. These four edge families are assembled into one exact serialized ordinary target. A fixed branch classifier and selector now totalize that construction over all typed instances, including the two degenerate textbook branches. The selected target has exact encoding semantics, is well formed, has target size equal to its vertex count, and is equivalent to the textbook construction. Finally, the reused raw parser/well-formedness guard selects either this target or a fixed no-instance. The resulting all-input map has exact language semantics and is computed by one fixed polynomial-time TM2.