Linear combinatorial size of fixed-gadget replacement

Relabeling preserves constraint counts and variable-occurrence counts. Each input constraint therefore contributes exactly the fixed size of its chosen template. The number of distinct output variables is at most the number of output occurrences. For a finite source alphabet, the guarded compiler has a uniform linear bound on output variables plus constraints, including malformed inputs and the empty instance.

These are combinatorial counts, not binary encoding lengths. Fresh variable names contain constraint indices, so the binary encoding may incur an additional logarithmic factor.

Main results

• Cslib.Logic.PL.CSP.length_replaceGadgets: exact output constraint count.
• Cslib.Logic.PL.CSP.vars_length_replaceGadgets: exact output occurrence count.
• Cslib.Logic.PL.CSP.exists_linear_bound_replaceGadgetsGuarded: the guarded linear bound.

theorem Cslib.Logic.PL.CSP.length_replaceGadgets {Src Rel : Type} (B : ℕ) (templates : Src → CSP Rel (Bool × ℕ)) (F : CSP Src ℕ) : List.length (replaceGadgets B templates F) = (List.map (fun (c : Constraint Src ℕ) => List.length (templates c.1)) F).sum

Each source constraint contributes exactly the constraints in its fixed template.

theorem Cslib.Logic.PL.CSP.vars_length_replaceGadgets {Src Rel : Type} (B : ℕ) (templates : Src → CSP Rel (Bool × ℕ)) (F : CSP Src ℕ) : (replaceGadgets B templates F).vars.length = (List.map (fun (c : Constraint Src ℕ) => (templates c.1).vars.length) F).sum

Relabeling template ports preserves their occurrence count, even when ports coincide.

theorem Cslib.Logic.PL.CSP.numVars_add_length_replaceGadgets_le {Src Rel : Type} (B : ℕ) (templates : Src → CSP Rel (Bool × ℕ)) (K : ℕ) (hK : ∀ (r : Src), (templates r).vars.length + List.length (templates r) ≤ K) (F : CSP Src ℕ) : (replaceGadgets B templates F).numVars + List.length (replaceGadgets B templates F) ≤ K * List.length F

A bound on template occurrences plus constraints bounds distinct output variables plus constraints. No freshness or well-formedness assumption is needed for this size inequality.

theorem Cslib.Logic.PL.CSP.exists_linear_bound_replaceGadgetsGuarded {Src Rel : Type} [Finite Src] (srcArity : Src → ℕ) (B : ℕ) (templates : Src → CSP Rel (Bool × ℕ)) (reject : CSP Rel ℕ) : ∃ (C : ℕ), ∀ (F : CSP Src ℕ), (replaceGadgetsGuarded srcArity B templates reject F).numVars + List.length (replaceGadgetsGuarded srcArity B templates reject F) ≤ C * List.length F

Fixed finite template lookup and a fixed malformed-input reject instance give a linear bound on distinct output variables plus constraints, for every raw input. The constant is independent of the input and of its numeric variable labels.