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.RuntimeFixed 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.