Native bit complexity of unweighted matching

The certificates use the complete framed encGraph input and encMatching output. Retained vertex/name bits, explicit one-hot table rows, scope positions, every intermediate solver state and the output edge list enter ordinary native multitape polynomial composition. No graph validity, degree bound, finite relation language or runtime provider is an input.

For framed input length L, there are at most L distinct vertices and normalized edges. Writing these counts as n and m, each choice table has at most m + 1 rows of width m + 1, and each pin has one unary row. Thus choice-row storage is bounded by n * (m + 1) ^ 2 Boolean entries, before the explicitly charged framing and binary scope names. Tagging a retained vertex name by 2 * v + 1 adds at most one binary digit; original edge names are tagged list positions. Solver storage growth is charged by the all-raw explicit-table optimizer certificate used in the composition.

theorem Cslib.Complexity.Graph.computableInPolyTime_matchingScope : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × ℕ) => p.1.matchingScope p.2) (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

The nonempty choice scope is built in polynomial time, retaining binary names.

theorem Cslib.Complexity.Graph.computableInPolyTime_matchingInstance : Turing.MultiTapeTM.ComputableInPolyTime matchingInstance encGraph (encCSP CSP.encTable Turing.MultiTapeTM.encNat)

The complete generated explicit-table instance is native polynomial-time on every graph.

theorem Cslib.Complexity.Graph.computableInPolyTime_selectedBit : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool) × ℕ) => selectedBit p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair CSP.EdgeAugmenting.encBuffer Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Reading mutual selection scans only actual occurrence records and their bit buffer.

theorem Cslib.Complexity.Graph.computableInPolyTime_matchingPositions : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × List Bool) => p.1.matchingPositions p.2) encMatchingBuffer (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

The selected original position list is native polynomial-time.

theorem Cslib.Complexity.Graph.computableInPolyTime_edgesAtPositions : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × List ℕ) => p.1.edgesAtPositions p.2) (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) encMatching

Converting positions to actual original endpoint pairs is native polynomial-time.

theorem Cslib.Complexity.Graph.computableInPolyTime_maximumMatching : Turing.MultiTapeTM.ComputableInPolyTime maximumMatching encGraph encMatching

The graph-only maximum matching endpoint has an ordinary native polynomial certificate.

theorem Cslib.Complexity.Graph.computableInPolyTime_coversVertices : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × List (ℕ × ℕ)) => p.1.coversVertices p.2) (Turing.MultiTapeTM.encPair encGraph encMatching) Turing.MultiTapeTM.encBool

Checking full vertex coverage scans the actual lists of vertices and selected edges.

theorem Cslib.Complexity.Graph.computableInPolyTime_perfectMatching : Turing.MultiTapeTM.ComputableInPolyTime perfectMatching encGraph (Turing.MultiTapeTM.encOption encMatching)

Constructive perfect-matching search is native polynomial-time on complete raw graphs.

theorem Cslib.Complexity.Graph.computableInPolyTime_decidePerfectMatching : Turing.MultiTapeTM.ComputableInPolyTime decidePerfectMatching encGraph Turing.MultiTapeTM.encBool

Full perfect-matching decision is native polynomial-time on complete raw graphs.