Combinatorial and encoded compiler bounds

M is the actual original occurrence count and C the actual constraint count. White boundaries partition exactly M edge positions; auxiliary blocks have at most M names. The bounds refer to actual emitted constraints and dense binary names, independently of original label magnitude. Full framed encoded output polynomiality is polyBounded_length_compile, derived from the ordinary native program certificate, not from a unit-cost combinatorial-size proxy.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_encTable_differenceTable_le {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : (encTable (Logic.PL.CSP.Table.differenceTable arity sem r)).length ≤ 2 * (Turing.MultiTapeTM.encNat (arity r)).length + 1 + 2 ^ arity r * (6 * arity r + 1)

Full static black-table encoding bound, including binary arity, Boolean row framing and row-list framing. Its exponential arity factor is a constant only for a fixed language.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_encTable_evenTable_le {n : ℕ} (hn : n ≤ 3) : (encTable (Logic.PL.CSP.Table.evenTable n)).length ≤ 81

Each emitted white table has at most 81 fully framed bits, independent of face length.

theorem Cslib.Complexity.CSP.CyclicCompiler.whiteScope_nonempty {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (edge : ℕ) (hedge : edge < F.occurrences.length) : 0 < (whiteScope F cert edge).length

Nonempty raw boundary scans include their starting edge whenever it is in range.

theorem Cslib.Complexity.CSP.CyclicCompiler.whiteScopes_nonempty {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (scope : List ℕ) : scope ∈ whiteScopes F cert → 0 < scope.length

Every emitted white face has a genuine nonempty boundary, including raw certificates.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_flatten_whiteScopes {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) : (whiteScopes F cert).flatten.length = F.occurrences.length

The complete white boundary length is exactly the original occurrence count.

theorem Cslib.Complexity.CSP.CyclicCompiler.auxiliaryPrefix_all_le (scopes : List (List ℕ)) : auxiliaryPrefix scopes scopes.length ≤ scopes.flatten.length

Fresh auxiliary allocation is bounded by the actual total white boundary length.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_whiteConstraints_le (edges : ℕ) (scopes : List (List ℕ)) (hpos : ∀ scope ∈ scopes, 0 < scope.length) : List.length (whiteConstraints edges scopes) ≤ scopes.flatten.length

At most one chain constraint per original boundary edge for nonempty faces.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_body_le {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) : List.length (body arity sem F cert) ≤ List.length F + F.occurrences.length

The body contains at most C + M constraints, including retained original positions.

theorem Cslib.Complexity.CSP.CyclicCompiler.body_names_lt {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (v : ℕ) (hv : v ∈ (body arity sem F cert).vars) : v < 2 * F.occurrences.length

Every body variable lies in the consecutive old-edge-plus-auxiliary interval.

theorem Cslib.Complexity.CSP.CyclicCompiler.vars_toFinset_body {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) : (body arity sem F cert).vars.toFinset = Finset.range (F.occurrences.length + auxiliaryPrefix (whiteScopes F cert) (whiteScopes F cert).length)

The body's variable set is exactly one dense interval; unused auxiliary names are not allocated. Source names and nullary constraint positions introduce no holes.

theorem Cslib.Complexity.CSP.CyclicCompiler.numVars_body {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) : (body arity sem F cert).numVars = F.occurrences.length + auxiliaryPrefix (whiteScopes F cert) (whiteScopes F cert).length

Exact dense variable count, before the fixed rejection branch.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_vars_body_le {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) : (body arity sem F cert).vars.length ≤ 4 * F.occurrences.length

Exactly two actual ports per dense target variable, and at most 4M emitted ports.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_compile_le {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) : List.length (compile arity sem input) ≤ List.length input.1 + input.1.occurrences.length + 2

Every raw compiler output has at most C + M + 2 constraints. Rejection uses two pins.

theorem Cslib.Complexity.CSP.CyclicCompiler.compile_names_lt {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) (v : ℕ) (hv : v ∈ (compile arity sem input).vars) : v < 2 * input.1.occurrences.length + 1

Binary output names are bounded by 2M, with the fixed rejecting name included.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_vars_compile_le {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) : (compile arity sem input).vars.length ≤ 4 * input.1.occurrences.length + 2

Every raw compiler output has at most 4M + 2 actual ports, including rejection.