Consecutive white-face parity chains #
The actual compiler allocates consecutive blocks by prefix sums of actual boundary lengths. These lemmas compose the checked single-chain semantics while preserving all reserved names.
theorem Cslib.Complexity.CSP.CyclicCompiler.whiteConstraints_cons (edges : ℕ) (scope : List ℕ) (scopes : List (List ℕ)) :
whiteConstraints edges (scope :: scopes) = Logic.PL.CSP.Table.parityChain edges scope ++ whiteConstraints (edges + (scope.length - 3)) scopes
Recursive specification of the actual zip-index/prefix-sum implementation.
theorem Cslib.Complexity.CSP.CyclicCompiler.whiteConstraints_sound (edges : ℕ) (scopes : List (List ℕ)) (σ : ℕ → Bool) (h : Logic.PL.CSP.eval Logic.PL.CSP.Table.sem σ (whiteConstraints edges scopes) = true) (scope : List ℕ) :
scope ∈ scopes → BitString.wordParity (List.map σ scope) = false
Restriction of any satisfying white expansion enforces every original face parity.
theorem Cslib.Complexity.CSP.CyclicCompiler.whiteConstraints_complete (edges : ℕ) (scopes : List (List ℕ)) (σ : ℕ → Bool) (hbound : ∀ scope ∈ scopes, ∀ v ∈ scope, v < edges) (hparity : ∀ scope ∈ scopes, BitString.wordParity (List.map σ scope) = false) :
∃ (τ : ℕ → Bool),
(∀ v < edges, τ v = σ v) ∧ Logic.PL.CSP.eval Logic.PL.CSP.Table.sem τ (whiteConstraints edges scopes) = true
Even boundary assignments extend to the whole actual expansion, preserving every reserved name. Allocation is performed face by face with the exact prefix-sum offsets.
theorem Cslib.Complexity.CSP.CyclicCompiler.count_vars_whiteConstraints (edges : ℕ) (scopes : List (List ℕ)) (v : ℕ) :
List.count v (whiteConstraints edges scopes).vars = List.count v scopes.flatten + if edges ≤ v ∧ v < edges + auxiliaryPrefix scopes scopes.length then 2 else 0
Complete occurrence accounting for consecutive parity-chain blocks.
theorem Cslib.Complexity.CSP.CyclicCompiler.whiteConstraints_scopes_nodup (edges : ℕ) (scopes : List (List ℕ)) (hnd : ∀ scope ∈ scopes, scope.Nodup) (hbound : ∀ scope ∈ scopes, ∀ v ∈ scope, v < edges) (constraint : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) (hc : constraint ∈ whiteConstraints edges scopes) :
constraint.2.Nodup
Every expanded white constraint has a duplicate-free scope when the original white boundaries are distinct and all old edge names precede the auxiliary blocks.