Explicit parity chains

The chain replaces an EVEN constraint by tables of width at most three. It has k - 2 constraints and k - 3 fresh variables when k ≥ 4; smaller scopes retain one table. Fresh names begin at the supplied offset. Construction traverses the actual scope, never an unchecked binary arity. The chain is an original implementation detail for the difference reduction of [DK15], Section 3, Lemma 5, Corollary 4 and Theorem 2, printed pp. 439–440. No geometric realization of the expansion is asserted or needed.

Main definitions

• Cslib.Logic.PL.CSP.Table.evenTable: explicit even-parity rows.
• Cslib.Logic.PL.CSP.Table.parityChain: the actual width-three expansion.

def Cslib.Logic.PL.CSP.Table.evenTable (width : ℕ) : Table

Explicit even-parity table. Only widths zero through three are generated at runtime by parityChain; larger tables are a mathematical API, with no uniform polynomial claim.

@[simp]

theorem Cslib.Logic.PL.CSP.Table.arity_evenTable (width : ℕ) : (evenTable width).arity = width

theorem Cslib.Logic.PL.CSP.Table.wellFormed_evenTable (width : ℕ) : (evenTable width).wellFormed = true

Every row has exactly the declared width, including the nullary row.

theorem Cslib.Logic.PL.CSP.Table.sem_evenTable (width : ℕ) (row : List Bool) : (evenTable width).sem row = true ↔ row.length = width ∧ BitString.wordParity row = false

The table includes the exact-arity guard even for malformed supplied rows.

theorem Cslib.Logic.PL.CSP.Table.booleanRelation_evenTable (width : ℕ) : booleanRelation arity sem (evenTable width) = {x : Fin width → Bool | parityOn Finset.univ x = false}

Explicit tables denote the existing parity relation, without a second Boolean model.

theorem Cslib.Logic.PL.CSP.Table.isEvenDeltaMatroid_evenTable (width : ℕ) : BitString.IsEvenDeltaMatroid (booleanRelation arity sem (evenTable width))

All parity tables used by a chain are nonempty even delta-matroids.

def Cslib.Logic.PL.CSP.Table.parityChainTail (fresh first : ℕ) : List ℕ → CSP Table ℕ

Chain tail with the accumulated parity variable first. Each recursive step consumes one actual boundary entry and allocates one fresh binary name.

def Cslib.Logic.PL.CSP.Table.parityChain (fresh : ℕ) (scope : List ℕ) : CSP Table ℕ

Width-three expansion, retaining the original boundary order. Names below fresh are reserved for the caller; an empty boundary is the true nullary parity table.

theorem Cslib.Logic.PL.CSP.Table.length_parityChainTail (fresh first : ℕ) (rest : List ℕ) : List.length (parityChainTail fresh first rest) = max 1 (rest.length - 1)

Exactly the requested number of chain constraints.

theorem Cslib.Logic.PL.CSP.Table.length_parityChain (fresh : ℕ) (scope : List ℕ) : List.length (parityChain fresh scope) = max 1 (scope.length - 2)

Linear constraint count, including empty and short boundaries.

theorem Cslib.Logic.PL.CSP.Table.parityChainTail_width (fresh first : ℕ) (rest : List ℕ) (c : Constraint Table ℕ) (hc : c ∈ parityChainTail fresh first rest) : c.1.arity = c.2.length ∧ c.2.length ≤ 3 ∧ ∃ n ≤ 3, c.1 = evenTable n

Every output table and scope has matching width at most three.

theorem Cslib.Logic.PL.CSP.Table.parityChain_tables (fresh : ℕ) (scope : List ℕ) (c : Constraint Table ℕ) (hc : c ∈ parityChain fresh scope) : c.1.arity = c.2.length ∧ c.2.length ≤ 3 ∧ BitString.IsEvenDeltaMatroid (booleanRelation arity sem c.1)

The actual expansion uses only nonempty even delta-matroid relations.

theorem Cslib.Logic.PL.CSP.Table.parityChainTail_sound (fresh first : ℕ) (rest : List ℕ) (σ : ℕ → Bool) (h : eval sem σ (parityChainTail fresh first rest) = true) : BitString.wordParity (List.map σ (first :: rest)) = false

Every satisfying chain assignment has even boundary parity. This direction needs no freshness or distinctness assumption, so repeated boundary names cause no semantic shortcut.

theorem Cslib.Logic.PL.CSP.Table.parityChain_sound (fresh : ℕ) (scope : List ℕ) (σ : ℕ → Bool) (h : eval sem σ (parityChain fresh scope) = true) : BitString.wordParity (List.map σ scope) = false

A satisfying expansion enforces even parity on its original boundary, including zero and one ports.

theorem Cslib.Logic.PL.CSP.Table.parityChainTail_complete (fresh first : ℕ) (rest : List ℕ) (σ : ℕ → Bool) (hbound : ∀ v ∈ first :: rest, v < fresh) (hparity : BitString.wordParity (List.map σ (first :: rest)) = false) : ∃ (τ : ℕ → Bool), (∀ (v : ℕ), v < fresh ∨ fresh + (rest.length - 2) ≤ v → τ v = σ v) ∧ eval sem τ (parityChainTail fresh first rest) = true

Extend any even boundary assignment using only the consecutive allocated auxiliary block. Names outside that block are preserved, including arbitrary large binary names.

theorem Cslib.Logic.PL.CSP.Table.parityChain_complete (fresh : ℕ) (scope : List ℕ) (σ : ℕ → Bool) (hbound : ∀ v ∈ scope, v < fresh) (hparity : BitString.wordParity (List.map σ scope) = false) : ∃ (τ : ℕ → Bool), (∀ (v : ℕ), v < fresh ∨ fresh + (scope.length - 3) ≤ v → τ v = σ v) ∧ eval sem τ (parityChain fresh scope) = true

Exact existential semantics of the actual chain with its allocated names.

theorem Cslib.Logic.PL.CSP.Table.count_vars_parityChainTail (fresh first : ℕ) (rest : List ℕ) (v : ℕ) : List.count v (parityChainTail fresh first rest).vars = List.count v (first :: rest) + if fresh ≤ v ∧ v < fresh + (rest.length - 2) then 2 else 0

Exactly two occurrences of each allocated auxiliary, and the original multiplicity of all boundary names. This equality does not assume that the caller chose fresh names.

theorem Cslib.Logic.PL.CSP.Table.count_vars_parityChain (fresh : ℕ) (scope : List ℕ) (v : ℕ) : List.count v (parityChain fresh scope).vars = List.count v scope + if fresh ≤ v ∧ v < fresh + (scope.length - 3) then 2 else 0

Every old boundary occurrence is retained once, and every new auxiliary occurs twice.

theorem Cslib.Logic.PL.CSP.Table.mem_vars_parityChain (fresh : ℕ) (scope : List ℕ) (v : ℕ) : v ∈ (parityChain fresh scope).vars ↔ v ∈ scope ∨ fresh ≤ v ∧ v < fresh + (scope.length - 3)

Output names are boundary names or precisely the allocated consecutive auxiliary interval.

theorem Cslib.Logic.PL.CSP.Table.parityChain_names_lt (fresh : ℕ) (scope : List ℕ) (hbound : ∀ v ∈ scope, v < fresh) (v : ℕ) (hv : v ∈ (parityChain fresh scope).vars) : v < fresh + (scope.length - 3)

The entire output lies below the first unused name when all boundary names are reserved.

theorem Cslib.Logic.PL.CSP.Table.parityChainTail_scopes_nodup (fresh first : ℕ) (rest : List ℕ) (hnd : (first :: rest).Nodup) (hbound : ∀ v ∈ first :: rest, v < fresh) (constraint : Constraint Table ℕ) (hc : constraint ∈ parityChainTail fresh first rest) : constraint.2.Nodup

No scope repeats a name when the original boundary is distinct and auxiliaries are fresh.

theorem Cslib.Logic.PL.CSP.Table.parityChain_scopes_nodup (fresh : ℕ) (scope : List ℕ) (hnd : scope.Nodup) (hbound : ∀ v ∈ scope, v < fresh) (constraint : Constraint Table ℕ) (hc : constraint ∈ parityChain fresh scope) : constraint.2.Nodup

Fresh parity expansion satisfies the target's no-repeat-within-one-scope convention.