Bit storage of explicit-table solver instances

Storage charges full binary names and declared arities, row bits, and every list/pair frame. The quantitative bookkeeping here is original. The actual contraction's row/variable bounds come from Observation 26 and Corollary 27 of [KKR18], arXiv:1602.03124v6, printed p. 13. No unit-cost name or table access is used in the bounds.

def Cslib.Complexity.CSP.EdgeSolver.Size.rowCount (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : ℕ

Total number of actual stored rows, retaining duplicate constraints and duplicate rows.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.connector_bits_le (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (B : ℕ) (hB : ∀ v ∈ F.vars, (Turing.MultiTapeTM.encNat v).length ≤ B) (i : Fin (List.length F)) : (Turing.MultiTapeTM.encNat (Logic.PL.CSP.Blossom.connector F i)).length ≤ B + List.length F + 3

A fresh connector increases maximum binary name length additively. The bound depends on the actual constraint count; it never enumerates the interval below an original name.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.contract_name_bits_le (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (B : ℕ) (hB : ∀ v ∈ F.vars, (Turing.MultiTapeTM.encNat v).length ≤ B) (v : ℕ) : v ∈ (Logic.PL.CSP.Blossom.contract f vs).vars → (Turing.MultiTapeTM.encNat v).length ≤ B + List.length F + 3

Every name in the actual child is either an unchanged outside name or one of the actual fresh connectors. This includes arbitrary sparse original names and every framing bit.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.encoded_body_le (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (f : F.OccurrenceLabeling Bool) (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) (B : ℕ) (hB : ∀ v ∈ F.vars, (Turing.MultiTapeTM.encNat v).length ≤ B) : ((encCSP encTable Turing.MultiTapeTM.encNat) F).length ≤ 7 * List.length F + (4 * B + 10) * F.vars.length + 4 * (6 * F.vars.length + 1) * rowCount F

Full framed storage of any valid explicit-table occurrence problem. The bound includes binary declared arities, every stored row and variable-name bit, and all nested list framing. The arities are derived from actual local validity; huge malformed declared widths cannot silently enter this estimate.

inductive Cslib.Complexity.CSP.EdgeSolver.Size.Chain (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : ℕ → Logic.PL.CSP Logic.PL.CSP.Table ℕ → Prop

A finite history of actual whole-instance blossom contractions. Labels and blossoms are the existing mathematical objects, not resource certificates or alternative CSP instances.

• nil {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} : Chain F 0 F

  The original explicit-table problem.

• step {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} {G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (previous : Chain F k G) (f : G.OccurrenceLabeling Bool) (w : G.Walk) (valid : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) (blossom : Logic.PL.CSP.Walk.IsBlossom Logic.PL.CSP.Table.sem f w) : Chain F (k + 1) (Logic.PL.CSP.Blossom.contract f (Logic.PL.CSP.Blossom.internal w))

  One actual valid prepared blossom and its exact constructor.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.edge {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) : G.EdgeInstance

Every body in an actual contraction history retains the original edge model.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.length {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) : List.length G = List.length F + k

Each stored parent contributes exactly one new constraint, including all old nullaries.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.numVars_le {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) : G.numVars ≤ F.numVars

Variable counts do not increase anywhere along the actual contraction history.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.measure_add_le {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) : k + G.contractionMeasure ≤ F.contractionMeasure

Every descent spends the actual concrete measure, including r = b contractions.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.depth_le {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) : k ≤ 2 * F.numVars

All contractions in one improvement have depth at most twice the original variable count.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.rowCount_le {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) : rowCount G ≤ rowCount F + k * F.numVars

The total stored row count grows only additively with descent depth, not multiplicatively.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.name_bits_le {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) (B : ℕ) (hB : ∀ v ∈ F.vars, (Turing.MultiTapeTM.encNat v).length ≤ B) (v : ℕ) : v ∈ G.vars → (Turing.MultiTapeTM.encNat v).length ≤ B + k * (List.length F + 2 * F.numVars + 3)

Full binary original-name storage grows additively along every actual contraction history.

def Cslib.Complexity.CSP.EdgeSolver.Size.nameBudget (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : ℕ

Full binary fresh-name budget across one complete descent. All counts are actual lists; the original complete framed input pays for its maximum original name bit length.

def Cslib.Complexity.CSP.EdgeSolver.Size.rowBudget (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : ℕ

Stored-row budget across one complete descent, including all central one-hot rows.

def Cslib.Complexity.CSP.EdgeSolver.Size.bodyBudget (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : ℕ

Full framed body-storage budget, polynomial in actual original counts and bit lengths.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.original_name_bits_le (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (v : ℕ) : v ∈ F.vars → (Turing.MultiTapeTM.encNat v).length ≤ ((encCSP encTable Turing.MultiTapeTM.encNat) F).length

Every original binary name is charged by the complete original CSP encoding.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.name_budget {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) (v : ℕ) : v ∈ G.vars → (Turing.MultiTapeTM.encNat v).length ≤ nameBudget F

Every actual descended body obeys the original polynomial binary-name budget.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.body_budget {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) (f : G.OccurrenceLabeling Bool) (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) : ((encCSP encTable Turing.MultiTapeTM.encNat) G).length ≤ bodyBudget F

Complete framed bit storage of every actual valid descended body has one fixed original polynomial bound. This includes duplicate/nullary constraints and full binary name lengths.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.encoded_walk_le {H : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : H.Walk) (hw : w.IsWalk) (B : ℕ) (hb : (Turing.MultiTapeTM.encNat w.start).length ≤ B) : (EdgeAugmenting.encWalkCode (EdgeAugmenting.code w)).length ≤ 2 * B + 1 + H.incidenceList.length * (6 * H.incidenceList.length + 3)

The binary-position encoding of any actual trail includes every original start-name bit and every step's two global positions and pair/list framing.

theorem Cslib.Complexity.CSP.EdgeSolver.Size.Chain.width_le {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {k : ℕ} (h : Chain F k G) (hF : F.EdgeInstance) : G.incidenceList.length ≤ 2 * F.vars.length

Every actual descended occurrence buffer fits twice the original actual occurrence count.