Finite-buffer whole-instance contraction

Native list operations implement the existing whole-instance constructor. All old constraints, including nullaries, keep their positions. Selected internal coordinates are gathered once per original constraint, surviving coordinates keep their order, and one central exactly-one table is appended. Local rows and positions are funded by actual scopes, not declared binary arities.

Original names and fresh connectors remain binary. The maximum scan traverses only occurring names; no interval below a name is enumerated. The source construction is Section 5.3 of [KKR18], arXiv:1602.03124v6, printed pp. 12–13.

def Cslib.Complexity.CSP.EdgeSolver.Contraction.rows (input : EdgeForest.Input) : List (List Bool)

Actual local rows, in original constraint and argument order, read from the existing buffer.

def Cslib.Complexity.CSP.EdgeSolver.Contraction.freshBase (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : ℕ

A fresh binary base, obtained by one scan of actual original names.

def Cslib.Complexity.CSP.EdgeSolver.Contraction.connectors (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (vs : List ℕ) : List ℕ

Actual fresh connectors, one per touched original constraint and in original order.

def Cslib.Complexity.CSP.EdgeSolver.Contraction.constraint (input : EdgeForest.Input) (vs : List ℕ) (c : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) (i : ℕ) : Logic.PL.Constraint Logic.PL.CSP.Table ℕ

Replace all selected positions of one original constraint in a single local contraction.

def Cslib.Complexity.CSP.EdgeSolver.Contraction.contract (input : EdgeForest.Input) (vs : List ℕ) : Logic.PL.CSP Logic.PL.CSP.Table ℕ

Total finite whole-instance contraction on arbitrary raw table and buffer inputs.

def Cslib.Complexity.CSP.EdgeSolver.Contraction.referenceRows (input : EdgeForest.Input) (vs : List ℕ) : List (List Bool)

The honest contracted reference: zero old connector bits, followed by one central one-hot row. The central row is paid for by the actual connector list.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.freshBase_eq (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : freshBase F = Logic.PL.CSP.Blossom.freshBase F

The fresh-name scan agrees with the original constructor's maximum scan.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.rows_eq (input : EdgeForest.Input) : rows input = List.ofFn fun (i : Fin (List.length input.body)) => Logic.PL.CSP.localTuple (EdgeAugmenting.labeling input.body input.labels) i

Every raw-buffer row is exactly the original positional local tuple; no width premise is needed, since both readers default identically on missing occurrence bits.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.connectors_eq (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (vs : List ℕ) : connectors F vs = Logic.PL.CSP.Blossom.connectors F vs

Fresh connectors are precisely those of the original whole-instance constructor.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.contract_eq (input : EdgeForest.Input) (vs : List ℕ) : contract input vs = Logic.PL.CSP.Blossom.contract (EdgeAugmenting.labeling input.body input.labels) vs

Exact native whole-instance contraction on every raw buffer, without semantic premises.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.referenceRows_eq (input : EdgeForest.Input) (vs : List ℕ) : referenceRows input vs = Logic.PL.CSP.Blossom.referenceRows (EdgeAugmenting.labeling input.body input.labels) vs

Exact actual reference rows, including the central one-hot row.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.flatten_referenceRows {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (Logic.PL.CSP.Blossom.referenceRows f vs).flatten = List.map (Logic.PL.CSP.Blossom.reference f vs) (Logic.PL.CSP.Blossom.contract f vs).incidenceList

Flattening the actual constructor's reference rows gives precisely its occurrence buffer. Every row has the actual scope width, including the appended central row and all nullaries.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_positionsWith {α : Type} {e : α ↪ List Bool} {vs scope : α → List ℕ} (hv : Turing.MultiTapeTM.ComputableInPolyTime vs e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hs : Turing.MultiTapeTM.ComputableInPolyTime scope e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => Logic.PL.CSP.Blossom.positions (vs x) (scope x)) e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Native composition on actual lists with binary names and positions.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_nameReadWith {α : Type} {e : α ↪ List Bool} {scope : α → List ℕ} {index : α → ℕ} (hs : Turing.MultiTapeTM.ComputableInPolyTime scope e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hi : Turing.MultiTapeTM.ComputableInPolyTime index e Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => (scope a).getD (index a) 0) e Turing.MultiTapeTM.encNat

Native composition on actual lists with binary names and positions.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_outsideWith {α : Type} {e : α ↪ List Bool} {width : α → ℕ} {positions : α → List ℕ} (hw : Turing.MultiTapeTM.ComputableInPolyTime width e Turing.MultiTapeTM.encUnary) (hp : Turing.MultiTapeTM.ComputableInPolyTime positions e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => Logic.PL.CSP.Table.outsidePositions (width a) (positions a)) e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Native composition on actual lists with binary names and positions.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.Contraction.encConnectorArgs : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List ℕ ↪ List Bool

Framed original body followed by the framed list of selected original binary names.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_connectors : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List ℕ) => connectors p.1 p.2) encConnectorArgs (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Fresh binary connector names are computed by bounded scans of actual scopes.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_connectorsWith {α : Type} {e : α ↪ List Bool} {F : α → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {vs : α → List ℕ} (hF : Turing.MultiTapeTM.ComputableInPolyTime F e (encCSP encTable Turing.MultiTapeTM.encNat)) (hv : Turing.MultiTapeTM.ComputableInPolyTime vs e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => connectors (F a) (vs a)) e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Compose connector construction with computed finite inputs, charging their full encodings.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_contract : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeForest.Input × List ℕ) => contract p.1 p.2) (Turing.MultiTapeTM.encPair EdgeForest.encInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (encCSP encTable Turing.MultiTapeTM.encNat)

Whole-instance contraction is ordinary native polynomial-time on all raw inputs. The certificate scans actual rows and scopes and includes binary fresh-name arithmetic.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_referenceRows : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : EdgeForest.Input × List ℕ) => referenceRows p.1 p.2) (Turing.MultiTapeTM.encPair EdgeForest.encInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))

The honest reference rows are native polynomial-time, including all row/list framing.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_contractWith {α : Type} {e : α ↪ List Bool} {input : α → EdgeForest.Input} {vs : α → List ℕ} (hi : Turing.MultiTapeTM.ComputableInPolyTime input e EdgeForest.encInput) (hv : Turing.MultiTapeTM.ComputableInPolyTime vs e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => contract (input a) (vs a)) e (encCSP encTable Turing.MultiTapeTM.encNat)

Compose the native finite operation with computed inputs, charging their full encodings.

theorem Cslib.Complexity.CSP.EdgeSolver.Contraction.computableInPolyTime_referenceRowsWith {α : Type} {e : α ↪ List Bool} {input : α → EdgeForest.Input} {vs : α → List ℕ} (hi : Turing.MultiTapeTM.ComputableInPolyTime input e EdgeForest.encInput) (hv : Turing.MultiTapeTM.ComputableInPolyTime vs e (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => referenceRows (input a) (vs a)) e (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))

Compose honest reference-row construction with computed finite inputs.