3.2. Use the resource certificates
The input encoding Cslib.Complexity.encGraph charges both complete framed lists,
including binary names. The output encoding Cslib.Complexity.Graph.encMatching is a
framed list of binary endpoint pairs. No model, degree bound, perfect solver, or runtime witness
is supplied by the caller.
example : ComputableInPolyTime maximumMatching encGraph encMatching :=
computableInPolyTime_maximumMatching
example : ComputableInPolyTime perfectMatching encGraph
(encOption encMatching) :=
computableInPolyTime_perfectMatching
example : perfectMatchingProblem ∈ P encGraph := perfectMatchingProblem_mem_P
The implementation specializes the Kazda–Kolmogorov–Rolinek even-delta-matroid solver. Each vertex chooses an incident edge or a private unmatched port, whose other end is pinned false. Mutually true original edges form a matching; the exact defect identity makes minimum defect equivalent to maximum cardinality. All generated table rows, their widths, retained name bits, intermediate solver states and output bits enter polynomial composition. Loops enumerate only actual lists, including for sparse binary names. These certificates do not assert a tight classical Edmonds operation bound or solve weighted/min-cost matching. Typed encoded inputs also do not by themselves provide a parser for malformed bit strings.