Browse chapters

Imports

import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.SyntaxNormalizer
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.WellFormedGuard
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.RawWellFormed
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.PairStream
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.NonedgeFilter
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.Header
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.TypedComplement
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.GuardSelector
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.VertexCover.ComplementMachine.Total

VERTEX-COVER complement-machine components

The raw graph syntax-normalizer is closed at semantic and fixed linear-time TM2 layers. The target/order/endpoint conjunction is also closed as a fixed polynomial-time guard on the established empty-certificate pair encoding. The graph-pair formatter and composition theorem close the entire original-raw- input to exact well-formedness-verdict pipeline. A new graph-to-range- certificate controller composes with the verified general-CLIQUE positional- pair generator, closing the original canonical graph to exact normalized-pair stream as a fixed polynomial-time TM2. Repeated lookup and the nonedge selector compute the exact complement edge table. The transformed n, n-k header is generated by an independent linear-time controller, then joined to that table. Finally, the raw syntax/invariant verdict selects either the complete complement or the canonical no-instance. Thus the public total CLIQUE-to-VERTEX-COVER map is now computed exactly by one fixed polynomial-time TM2 on every raw word.