Constructive row witnesses for table contraction

Section 5.3 of [KKR18], arXiv:1602.03124v6, printed pp. 12–13, retains rows with at most one changed internal coordinate. The witness routine below scans the actual original rows. Zero and one deviations respectively give equality and a unique changed actual port, including at unbounded finite arity.

def Cslib.Logic.PL.CSP.Table.contractWitness (table : Table) (reference : List Bool) (positions : List ℕ) (row : List Bool) : Option (List Bool)

Recover a local original-row witness by scanning the explicit stored table.

theorem Cslib.Logic.PL.CSP.Table.contractWitness_spec {table : Table} {reference row : List Bool} {positions : List ℕ} (hc : table.canContract reference positions = true) (hr : (table.contract reference positions).sem row = true) : ∃ (old : List Bool), table.contractWitness reference positions row = some old ∧ old ∈ table.rows ∧ deviations reference old positions ≤ 1 ∧ project old (outsidePositions reference.length positions) ++ [decide (deviations reference old positions = 1)] = row

Every accepted contracted row has an executable original stored-row witness.

theorem Cslib.Logic.PL.CSP.Table.deviations_eq_zero_iff (reference row : List Bool) (positions : List ℕ) : deviations reference row positions = 0 ↔ ∀ j ∈ positions, row.getD j false = reference.getD j false

Zero internal deviations means agreement at every selected original coordinate.

theorem Cslib.Logic.PL.CSP.Table.deviations_eq_one {reference row : List Bool} {positions : List ℕ} (h : deviations reference row positions = 1) : ∃ j ∈ positions, row.getD j false ≠ reference.getD j false ∧ ∀ k ∈ positions, k ≠ j → row.getD k false = reference.getD k false

Exactly one deviation gives a unique changed original coordinate; all other selected coordinates agree. This uses the actual position list, not an interval of variable names.

theorem Cslib.Logic.PL.CSP.Table.project_getD_idxOf (row : List Bool) (positions : List ℕ) {j : ℕ} (hj : j ∈ positions) : (project row positions).getD (List.idxOf j positions) false = row.getD j false

Reading a projected coordinate at its actual index recovers the original bit.

theorem Cslib.Logic.PL.CSP.Table.eq_of_project_eq_of_eqOn {reference row : List Bool} {positions : List ℕ} (hl : row.length = reference.length) (hp : project row (outsidePositions reference.length positions) = project reference (outsidePositions reference.length positions)) (hi : ∀ j ∈ positions, row.getD j false = reference.getD j false) : row = reference

A full-width row is determined by its outside projection and its internal bits.

theorem Cslib.Logic.PL.CSP.Table.contractWitness_projection {table : Table} {reference current : List Bool} {positions : List ℕ} {bit : Bool} (hc : table.canContract reference positions = true) (hr : (table.contract reference positions).sem (project current (outsidePositions reference.length positions) ++ [bit]) = true) : ∃ (old : List Bool), table.contractWitness reference positions (project current (outsidePositions reference.length positions) ++ [bit]) = some old ∧ table.sem old = true ∧ deviations reference old positions = bit.toNat ∧ project old (outsidePositions reference.length positions) = project current (outsidePositions reference.length positions)

The actual last connector bit determines the exact number of internal deviations in the computed row witness; its outside projection is precisely the supplied finite row.

theorem Cslib.Logic.PL.CSP.Table.sem_contract_zero_iff {table : Table} {reference current : List Bool} {positions : List ℕ} (hc : table.canContract reference positions = true) (hl : current.length = reference.length) (hi : ∀ j ∈ positions, current.getD j false = reference.getD j false) : (table.contract reference positions).sem (project current (outsidePositions reference.length positions) ++ [false]) = true ↔ table.sem current = true

At connector zero, contraction preserves exactly the feasible rows with the reference internal bits. All outside coordinates may change arbitrarily.