Encoding faithfulness: the completeness direction

Reflect/Encode.lean provides soundness: every clause satisfied $\\Longrightarrow$ the semantic condition holds. Is that enough to turn "the solver reports unsatisfiable" into "there is no light logical operator"? No. What is missing is the converse direction: the encoding does not over-constrain, so that whenever the semantic condition holds there exists an assignment of the auxiliary variables under which all clauses are true. Only the two together give "satisfiable if and only if a light logical operator exists", and "a UNSAT verdict implies a distance lower bound" is exactly the forward direction of that equivalence.

This module supplies the converse direction. Each of the four components comes with a constructive lemma:

component	construction
xorChain	the auxiliary variables take the prefix parity: at counter c + i the value is

`acc ⊕ σ x₀ ⊕ ⋯ ⊕ σ xᵢ` |

| prodClauses | the product variables take σ x ∧ σ w | | atMostK | slot (i,j) takes "at least j of the first i variables are true" | | buildPair | the four segments are concatenated, see buildPair_complete |

Why the construction is written segment by segment rather than as a single function

The encoder allocates the auxiliary variable numbers sequentially (c1Of/c2Of/c3Of are determined by the exit point of the preceding segment), so building the assignment segment by segment matches that order and avoids counting arithmetic of the form c1Of = 2n + Σ(|r| - 1). The interface for the concatenation is the pair of properties of chainAssign: below the counter it agrees with the input, and above the counter it reads only the current segment, so the assignment of a later segment leaves the ground of an earlier one untouched.

What "light logical operator" means in this module

Here a light logical operator is still only a semantic condition (a weight bound, kernels on the two sides, and a pairing equal to 1); the step that turns it into a statement about binary matrices and Hamming weight is proved in Reflect/Distance.lean.

1. Completeness of the Tseitin chain

def QECCertificates.LRAT.chainFill (σ : Assign) : List ℕ → Bool → ℕ → ℕ → Bool

The fill value of a chain: rest allocates the auxiliary variables starting from the counter c, and acc is the value of the accumulator on entering this segment.

At t = c the value is acc ⊕ σ x₀, and at t = c + i it is acc ⊕ σ x₀ ⊕ ⋯ ⊕ σ xⱼ (where j is the i-th element); outside the allocated range it is false (those variable numbers should never be referenced anyway).

Note that it does not read σ at t < c, which is the source of "a later segment does not overwrite an earlier one" during concatenation.

Equations

• QECCertificates.LRAT.chainFill σ [] x✝² x✝¹ x✝ = false
• QECCertificates.LRAT.chainFill σ (x_4 :: rest) x✝² x✝¹ x✝ = if x✝ = x✝¹ then x✝² ^^ σ x_4 else QECCertificates.LRAT.chainFill σ rest (x✝² ^^ σ x_4) (x✝¹ + 1) x✝

theorem QECCertificates.LRAT.chainFill_nil (σ : Assign) (acc : Bool) (c t : ℕ) : chainFill σ [] acc c t = false

theorem QECCertificates.LRAT.chainFill_cons (σ : Assign) (x : ℕ) (rest : List ℕ) (acc : Bool) (c t : ℕ) : chainFill σ (x :: rest) acc c t = if t = c then acc ^^ σ x else chainFill σ rest (acc ^^ σ x) (c + 1) t

theorem QECCertificates.LRAT.chainFill_self (σ : Assign) (x : ℕ) (rest : List ℕ) (acc : Bool) (c : ℕ) : chainFill σ (x :: rest) acc c c = (acc ^^ σ x)

The fill value at the counter is the xor of this step.

theorem QECCertificates.LRAT.chainFill_succ (σ : Assign) (x : ℕ) (rest : List ℕ) (acc : Bool) (c t : ℕ) (h : t ≠ c) : chainFill σ (x :: rest) acc c t = chainFill σ rest (acc ^^ σ x) (c + 1) t

One step past the counter: the part after c is the chain with the accumulator updated and the counter incremented.

theorem QECCertificates.LRAT.chainFill_eq_false_of_lt (σ : Assign) (rest : List ℕ) (acc : Bool) (c t : ℕ) : t < c → chainFill σ rest acc c t = false

Below the counter the input is not read: the fill value is always false.

theorem QECCertificates.LRAT.chainFill_congr {σ σ' : Assign} (rest : List ℕ) (acc acc' : Bool) (c : ℕ) (hacc : acc = acc') (h : ∀ (t : ℕ), t ∈ rest → σ t = σ' t) (t : ℕ) : chainFill σ rest acc c t = chainFill σ' rest acc' c t

The fill value reads only the elements of rest and the initial accumulator; the compatibility needed for concatenation rests on this.

def QECCertificates.LRAT.chainAssign (σ : Assign) (rest : List ℕ) (acc : Bool) (c : ℕ) : Assign

The complete assignment of a chain: below the counter c it keeps σ, above it it takes the fill value of the chain.

Equations

• QECCertificates.LRAT.chainAssign σ rest acc c t = if t < c then σ t else QECCertificates.LRAT.chainFill σ rest acc c t

theorem QECCertificates.LRAT.chainAssign_of_lt {σ : Assign} {rest : List ℕ} {acc : Bool} {c t : ℕ} (h : t < c) : chainAssign σ rest acc c t = σ t

theorem QECCertificates.LRAT.chainAssign_succ (σ : Assign) (x : ℕ) (rest : List ℕ) (acc : Bool) (c t : ℕ) (h : c < t) : chainAssign σ (x :: rest) acc c t = chainAssign σ rest (acc ^^ σ x) (c + 1) t

One step past the counter (the chainAssign version).

theorem QECCertificates.LRAT.chainAssign_self (σ : Assign) (x : ℕ) (rest : List ℕ) (acc : Bool) (c : ℕ) : chainAssign σ (x :: rest) acc c c = (acc ^^ σ x)

The value of chainAssign at the counter.

theorem QECCertificates.LRAT.chainAssign_congr {σ σ' : Assign} {rest : List ℕ} {acc acc' : Bool} {c : ℕ} (hacc : acc = acc') (hlt : ∀ (t : ℕ), t < c → σ t = σ' t) (h : ∀ (t : ℕ), t ∈ rest → σ t = σ' t) (t : ℕ) : chainAssign σ rest acc c t = chainAssign σ' rest acc' c t

Compatibility of chainAssign: if the two assignments agree below the counter according to hlt and on rest according to h, then they are equal.

theorem QECCertificates.LRAT.chainAssign_tail (σ : Assign) (x : ℕ) (rest : List ℕ) (acc : Bool) (c : ℕ) (hrest : ∀ (t : ℕ), t ∈ rest → t < c) (t : ℕ) : chainAssign (chainAssign σ (x :: rest) acc c) rest (chainAssign σ (x :: rest) acc c c) (c + 1) t = chainAssign σ (x :: rest) acc c t

Feeding the assignment of one segment of a chain on into its tail yields the same assignment: the concatenation lemma.

Note that the two agree exactly at t = c (the left side takes the new accumulator acc ⊕ σ x, the right side takes the value of chainFill at the counter), which is precisely why chainFill does not read below the counter.

theorem QECCertificates.LRAT.xorStepClauses_sat_of {τ : Assign} {cur x nxt : ℕ} (h : τ nxt = (τ cur ^^ τ x)) (C : Clause) : C ∈ xorStepClauses cur x nxt → SatClause τ C

Completeness of one step: if the values satisfy the xor relation, all four clauses are true.

theorem QECCertificates.LRAT.xorChainAux_complete (rest : List ℕ) (want : Bool) (cur c : ℕ) (σ : Assign) : cur < c → (∀ (t : ℕ), t ∈ rest → t < c) → dotS σ (cur :: rest) = want → ∀ (C : Clause), C ∈ (xorChainAux rest want cur c).fst → SatClause (chainAssign σ rest (σ cur) c) C

Completeness of a chain: if the semantic condition holds and every input variable read by the chain lies below the counter c, then chainAssign satisfies all the clauses of the chain.

2. Concatenation: one chain per row

chainsFrom turns each row into a chain and allocates the variable numbers end to end. Completeness has to concatenate segment by segment: the assignment of a later segment must leave the ground of an earlier one untouched, and the interface is the "agrees with the input below the counter" property of chainAssign.

Two bookkeeping lemmas are needed for this: the exit counter of a chain (the new variable numbers reach exactly c + rest.length) and the variable bound of the chain clauses (all of them lie below the exit counter).

theorem QECCertificates.LRAT.xorChainAux_snd (rest : List ℕ) (want : Bool) (cur c : ℕ) : (xorChainAux rest want cur c).snd = c + rest.length

The exit counter of a chain: one number is allocated per variable processed.

theorem QECCertificates.LRAT.xorStepClauses_vars {cur x nxt : ℕ} {C : Clause} (hC : C ∈ xorStepClauses cur x nxt) (l : Lit) : l ∈ C → l.fst = cur ∨ l.fst = x ∨ l.fst = nxt

A variable in a step clause can only occupy one of three positions.

theorem QECCertificates.LRAT.xorChainAux_vars_lt (rest : List ℕ) (want : Bool) (cur c : ℕ) : cur < c → (∀ (t : ℕ), t ∈ rest → t < c) → ∀ (C : Clause), C ∈ (xorChainAux rest want cur c).fst → ∀ (l : Lit), l ∈ C → l.fst < c + rest.length

The variable bound of the chain clauses: all of them lie below the exit counter.

theorem QECCertificates.LRAT.satClause_of_agree {σ τ : Assign} {C : Clause} {c : ℕ} (h : ∀ (t : ℕ), t < c → τ t = σ t) (hvars : ∀ (l : Lit), l ∈ C → l.fst < c) (hC : SatClause σ C) : SatClause τ C

Chain clauses are preserved between assignments that agree below the counter.

theorem QECCertificates.LRAT.chainsFrom_complete {f : ℕ → ℕ} {rows : List (List ℕ)} (hne : ∀ (r : List ℕ), r ∈ rows → r ≠ []) (c : ℕ) (σ : Assign) : (∀ (r : List ℕ), r ∈ rows → ∀ (t : ℕ), t ∈ r → f t < c) → (∀ (r : List ℕ), r ∈ rows → dotS (fun (t : ℕ) => σ (f t)) r = false) → ∃ (τ : Assign), (∀ (t : ℕ), t < c → τ t = σ t) ∧ ∀ (C : Clause), C ∈ (chainsFrom f rows c).fst → SatClause τ C

Completeness of a sequence of chains: if the dot product of every row is false, then there exists an assignment that satisfies all the chain clauses at once and agrees with the input below the counter c.

3. Completeness of the product block

prodClauses c n carries x_j ∧ w_j in the variable c + j (x_j is variable j and w_j is variable n + j). Completeness consists in assigning c + j directly to the conjunction.

def QECCertificates.LRAT.prodFill (σ : Assign) (c n : ℕ) : Assign

The assignment of the product block: the range c..c+n-1 takes the pointwise conjunction and the rest is kept as it is.

Equations

• QECCertificates.LRAT.prodFill σ c n t = if c ≤ t ∧ t < c + n then σ (t - c) && σ (n + (t - c)) else σ t

theorem QECCertificates.LRAT.prodFill_at (σ : Assign) (c n j : ℕ) (hj : j < n) : prodFill σ c n (c + j) = (σ j && σ (n + j))

The value at a product variable is the conjunction of the two factors.

theorem QECCertificates.LRAT.prodClauses_three_sat {τ : Assign} {a x w : ℕ} (h : τ a = (τ x && τ w)) (C : Clause) : C ∈ [[(a, false), (x, true)], [(a, false), (w, true)], [(a, true), (x, false), (w, false)]] → SatClause τ C

The semantics of the three product-block clauses: if the conjunction relation holds, all three of them are true.

theorem QECCertificates.LRAT.prodFill_of_lt {σ : Assign} {c n t : ℕ} (h : t < c) : prodFill σ c n t = σ t

The product block does not touch the input variables (c lies above them).

theorem QECCertificates.LRAT.prodClauses_complete {c n : ℕ} {σ : Assign} (hc : 2 * n ≤ c) (C : Clause) : C ∈ prodClauses c n → SatClause (prodFill σ c n) C

Completeness of the product block.

4. Completeness of the sequential counter (Sinz)

The soundness of atMostK is "all clauses true implies at most k variables are true" (Reflect/Encode.lean). The converse direction assigns slot (i,j) to "at least j of the first i variables are true" and verifies the four clauses row by row.

Three preliminaries are needed: the recursion for slotBase (the block before row i+1 has min i (k + 1) slots more than the block before row i, namely those of row i), a characterization of the value of slotVar, and a few lemmas that bridge the clause criterion from Bool back to a proposition.

theorem QECCertificates.LRAT.slotBase_succ (k i : ℕ) : slotBase k (i + 1) = slotBase k i + min i (k + 1)

The block before row i+1 has min i (k + 1) slots more than the block before row i, namely those of row i.

theorem QECCertificates.LRAT.slotBase_mono (k : ℕ) {i i' : ℕ} (h : i ≤ i') : slotBase k i ≤ slotBase k i'

The slot base is monotone.

theorem QECCertificates.LRAT.slotBase_pred {k i : ℕ} (hi : 1 ≤ i) : slotBase k i = slotBase k (i - 1) + min (i - 1) (k + 1)

The "previous index" form of slotBase, with the hypothesis stated on the index itself.

theorem QECCertificates.LRAT.slotVar_of_le {c k i j : ℕ} (h1 : 1 ≤ j) (h2 : j ≤ min i (k + 1)) : slotVar c k i j = some (c + slotBase k i + (j - 1))

slotVar takes a definite value on a valid slot.

theorem QECCertificates.LRAT.slotVar_eq_none {c k i j : ℕ} (h : ¬(1 ≤ j ∧ j ≤ min i (k + 1))) : slotVar c k i j = none

slotVar takes none on an invalid slot.

The Bool bridge at the clause level

Each of the four clauses says that one Bool implies another, so the criterion can be stated as an implication between values, with no need to unfold decide again and again.

theorem QECCertificates.LRAT.decide_imp {P Q : Prop} [Decidable P] [Decidable Q] (h : P → Q) : decide P = true → decide Q = true

theorem QECCertificates.LRAT.decide_imp2 {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] (h : P → Q → R) : decide P = true → decide Q = true → decide R = true

theorem QECCertificates.LRAT.sat_two_of_imp {τ : Assign} {p q : ℕ} {bp bq : Bool} (hp : τ p = bp) (hq : τ q = bq) (h : bp = true → bq = true) : SatClause τ [(p, false), (q, true)]

Binary clause ¬p ∨ q: given by bp = true → bq = true.

theorem QECCertificates.LRAT.sat_three_of_imp {τ : Assign} {a x s : ℕ} {ba bx bs : Bool} (ha : τ a = ba) (hx : τ x = bx) (hs : τ s = bs) (h : ba = true → bx = true → bs = true) : SatClause τ [(a, false), (x, false), (s, true)]

Ternary clause ¬a ∨ ¬x ∨ s: given by (a ∧ x) → s.

theorem QECCertificates.LRAT.sat_three_of_imp2 {τ : Assign} {s a x : ℕ} {bs ba bx : Bool} (hs : τ s = bs) (ha : τ a = ba) (hx : τ x = bx) (h : bs = true → ba = false → bx = true) : SatClause τ [(s, false), (a, true), (x, true)]

Ternary clause ¬s ∨ a ∨ x: given by (s ∧ ¬a) → x.

theorem QECCertificates.LRAT.sat_three_of_imp3 {τ : Assign} {s a b : ℕ} {bs ba bb : Bool} (hs : τ s = bs) (ha : τ a = ba) (hb : τ b = bb) (h : bs = true → ba = false → bb = true) : SatClause τ [(s, false), (a, true), (b, true)]

Ternary clause ¬s ∨ a ∨ b: given by (s ∧ ¬a) → b.

The four branches of slotClauses as explicit equations

The scrutinee of the match in slotClauses consists of three Option values. A rw on the slot in the goal does not move it, because the slot is a function argument; the three values are therefore first written as hypotheses, and the match then reduces.

theorem QECCertificates.LRAT.slotClauses_eq_some_some {s : ℕ → ℕ → Option ℕ} {i j x a b si : ℕ} (ha : s (i - 1) j = some a) (hb : s (i - 1) (j - 1) = some b) (hs : s i j = some si) : slotClauses s i j x = [[(a, false), (si, true)], [(b, false), (x, false), (si, true)], [(si, false), (a, true), (x, true)], [(si, false), (a, true), (b, true)]]

theorem QECCertificates.LRAT.slotClauses_eq_some_none {s : ℕ → ℕ → Option ℕ} {i j x a si : ℕ} (ha : s (i - 1) j = some a) (hb : s (i - 1) (j - 1) = none) (hs : s i j = some si) : slotClauses s i j x = [[(a, false), (si, true)], [(x, false), (si, true)], [(si, false), (a, true), (x, true)]]

theorem QECCertificates.LRAT.slotClauses_eq_none_some {s : ℕ → ℕ → Option ℕ} {i j x b si : ℕ} (ha : s (i - 1) j = none) (hb : s (i - 1) (j - 1) = some b) (hs : s i j = some si) : slotClauses s i j x = [[(b, false), (x, false), (si, true)], [(si, false), (x, true)], [(si, false), (b, true)]]

theorem QECCertificates.LRAT.slotClauses_eq_none_none {s : ℕ → ℕ → Option ℕ} {i j x si : ℕ} (ha : s (i - 1) j = none) (hb : s (i - 1) (j - 1) = none) (hs : s i j = some si) : slotClauses s i j x = [[(x, false), (si, true)], [(si, false), (x, true)]]

Completeness of one row

Row i processes the i-th variable, and the value of slot (i,j) is determined by "at least j of the first i variables are true". Here cnt' is the number of true values among the first i-1 variables, cnt that among the first i, and bx the value of the i-th variable; hprev/hcur state the slot values of the previous row and of this row as hypotheses, so this lemma only performs the verification at the level of Bool.

The four cases are separated by whether the slots (i-1,j) and (i-1,j-1) of the previous row are valid, which is the branch condition of the match in slotClauses.

theorem QECCertificates.LRAT.rowClauses_complete {c k i cnt' cnt x : ℕ} {τ : Assign} {bx : Bool} (hx : τ x = bx) (hcnt : cnt = cnt' + if bx = true then 1 else 0) (hmin : cnt' ≤ min (i - 1) (k + 1)) (hprev : ∀ (j : ℕ), 1 ≤ j → j ≤ min (i - 1) (k + 1) → τ (c + slotBase k (i - 1) + (j - 1)) = decide (j ≤ cnt')) (hcur : ∀ (j : ℕ), 1 ≤ j → j ≤ min i (k + 1) → τ (c + slotBase k i + (j - 1)) = decide (j ≤ cnt)) (C : Clause) : C ∈ rowClauses (slotVar c k) k i x → SatClause τ C

Filling row by row, and the main theorem

Write the slot block of row i into the assignment. The block boundaries are pinned down by slotBase: row i occupies [c + slotBase k i, c + slotBase k (i+1)), and slotBase k (i+1) = slotBase k i + min i (k + 1) (slotBase_succ) says that the two blocks meet end to end without overlapping. In the induction, "later rows leave the slots already filled by earlier rows alone" is exactly this, and it chains the segment-by-segment construction together without having to recover the row index from a variable number.

def QECCertificates.LRAT.rowFill (τ : Assign) (c k i cnt : ℕ) : Assign

Write the slot block of row i into the assignment: inside the block it takes "at least j of the first i variables are true", outside the block it is kept as it is.

Equations

• One or more equations did not get rendered due to their size.

theorem QECCertificates.LRAT.rowFill_at {τ : Assign} {c k i cnt j : ℕ} (hj : j < min i (k + 1)) : rowFill τ c k i cnt (c + slotBase k i + j) = decide (j + 1 ≤ cnt)

The value of the j-th slot inside the block.

theorem QECCertificates.LRAT.rowFill_of_notMem {τ : Assign} {c k i cnt t : ℕ} (h : ¬(c + slotBase k i ≤ t ∧ t < c + slotBase k i + min i (k + 1))) : rowFill τ c k i cnt t = τ t

Outside the block the assignment is kept as it is.

theorem QECCertificates.LRAT.rowFill_prev {τ : Assign} {c k i cnt j : ℕ} (hi : 1 ≤ i) (hj : j < min (i - 1) (k + 1)) : rowFill τ c k i cnt (c + slotBase k (i - 1) + j) = τ (c + slotBase k (i - 1) + j)

Filling row i leaves the block of row i-1 untouched (the two blocks meet end to end without overlapping).

theorem QECCertificates.LRAT.atMostK_complete {k c : ℕ} {xs : List ℕ} {σ : Assign} (hc : ∀ (t : ℕ), t ∈ xs → t < c) (hcnt : cntS σ xs ≤ k) : ∃ (τ : Assign), (∀ (t : ℕ), t < c → τ t = σ t) ∧ ∀ (C : Clause), C ∈ atMostK (slotVar c k) k xs → SatClause τ C

Completeness of the sequential counter: if at most k variables are true, then there exists an assignment satisfying all the counter clauses that agrees with the given assignment on the input variables.

The induction follows the traversal of atMostKAux (pre is the prefix already processed and suf the remainder), writing the slot block of that row into the assignment at each step. The returned assignment has two properties that the outer argument uses: it agrees with the original assignment below c + slotBase k (pre.length + 1) (the slots filled by earlier rows are not overwritten by later ones), and it characterizes the slot values of the last row (the next step uses this as its hprev).

5. Assembly: completeness of buildPair

The assignments of the four segments are concatenated segment by segment. The assembly has to move "the clauses of a segment are satisfied by that segment's assignment" to the final assignment, and it rests on two facts: the counters only increase (the threshold of a later segment is never lower than that of an earlier one), and the variables of each segment's clauses lie below its own exit counter.

The segments and counters of buildPair (Reflect/Encode.lean): the kernel constraints start at 2n, the pairing constraints at c1Of, the product block at c2Of, the chain for x·w at c2Of + n, and the counter at c3Of.

theorem QECCertificates.LRAT.xorChain_snd_ge (xs : List ℕ) (w : Bool) (c : ℕ) : c ≤ (xorChain xs w c).snd

The exit counter of a chain never decreases.

theorem QECCertificates.LRAT.chainsFrom_snd_ge {f : ℕ → ℕ} (rows : List (List ℕ)) (c : ℕ) : c ≤ (chainsFrom f rows c).snd

The exit counter of a sequence of chains never decreases.

theorem QECCertificates.LRAT.chainsFrom_vars_lt {f : ℕ → ℕ} {rows : List (List ℕ)} {c : ℕ} (hne : ∀ (r : List ℕ), r ∈ rows → r ≠ []) (hlt : ∀ (r : List ℕ), r ∈ rows → ∀ (t : ℕ), t ∈ r → f t < c) (C : Clause) : C ∈ (chainsFrom f rows c).fst → ∀ (l : Lit), l ∈ C → l.fst < (chainsFrom f rows c).snd

The clause variables of a sequence of chains all lie below the exit counter of that segment.

theorem QECCertificates.LRAT.prodClauses_vars_lt {c n : ℕ} (hc : n ≤ c) (C : Clause) : C ∈ prodClauses c n → ∀ (l : Lit), l ∈ C → l.fst < c + n

The variables of the product-block clauses all lie below c + n (and when n ≤ c the input variables are among them).

theorem QECCertificates.LRAT.xorChain_vars_lt {xs : List ℕ} {w : Bool} {c : ℕ} (hne : xs ≠ []) (hlt : ∀ (t : ℕ), t ∈ xs → t < c) (C : Clause) : C ∈ (xorChain xs w c).fst → ∀ (l : Lit), l ∈ C → l.fst < (xorChain xs w c).snd

The clause variables of a single chain all lie below the exit counter of its segment.

theorem QECCertificates.LRAT.satFormula_of_agree {σ τ : Assign} {F : CNF} {c : ℕ} (h : ∀ (t : ℕ), t < c → τ t = σ t) (hF : ∀ (C : Clause), C ∈ F → ∀ (l : Lit), l ∈ C → l.fst < c) (hσ : SatFormula σ F) : SatFormula τ F

A set of clauses is preserved between assignments that agree below the threshold.

theorem QECCertificates.LRAT.agree_le_trans {σ τ υ : Assign} {a b : ℕ} (h1 : ∀ (t : ℕ), t < b → τ t = σ t) (h2 : ∀ (t : ℕ), t < a → υ t = τ t) (h : a ≤ b) (t : ℕ) : t < a → υ t = σ t

Agreement below c is transitive, and the threshold may be lowered.

theorem QECCertificates.LRAT.xorChain_complete {xs : List ℕ} {w : Bool} {c : ℕ} {σ : Assign} (hne : xs ≠ []) (hlt : ∀ (t : ℕ), t ∈ xs → t < c) (h : dotS σ xs = w) : ∃ (τ : Assign), (∀ (t : ℕ), t < c → τ t = σ t) ∧ ∀ (C : Clause), C ∈ (xorChain xs w c).fst → SatClause τ C

Completeness of a single chain (the nonempty form).

theorem QECCertificates.LRAT.buildPair_complete {Rker Rpair : List (List ℕ)} {n k : ℕ} {σ : Assign} (hn : 0 < n) (hne₁ : ∀ (r : List ℕ), r ∈ Rker → r ≠ []) (hne₂ : ∀ (r : List ℕ), r ∈ Rpair → r ≠ []) (hcol₁ : ∀ (r : List ℕ), r ∈ Rker → ∀ (t : ℕ), t ∈ r → t < n) (hcol₂ : ∀ (r : List ℕ), r ∈ Rpair → ∀ (t : ℕ), t ∈ r → t < n) (hwt : cntS σ (List.range n) ≤ k) (hker : ∀ (r : List ℕ), r ∈ Rker → dotS σ r = false) (hpair : ∀ (r : List ℕ), r ∈ Rpair → dotS (fun (t : ℕ) => σ (n + t)) r = false) (hxw : dotS (fun (t : ℕ) => σ t && σ (n + t)) (List.range n) = true) : ∃ (τ : Assign), (∀ (t : ℕ), t < 2 * n → τ t = σ t) ∧ SatFormula τ (buildPair Rker Rpair n k)

Completeness of buildPair: when the four semantic conditions hold, the encoding is satisfiable — with the witness pinned down on the input variables.

Together with buildPair_sat of Reflect/Encode.lean (soundness) this composes into an equivalence with the Boolean semantic conditions. Reflect/Distance.lean bridges these conditions to binary matrices and Hamming weight. Composing that bridge with the soundness theorem of Reflect/LRAT.lean gives a matrix-level distance lower bound.

The agreement clause ∀ t, t < 2 * n → τ t = σ t is what an assembly needs and what a bare "there exists a model" cannot supply: the base part is followed by other clause blocks, and to carry a model of the base part past those blocks one has to know that the base model reads the input variables — that is, the ones a lexicographic comparator compares — exactly as the semantic data does. It costs nothing here, since the whole proof is already built out of extensions that agree below their own starting point: the first segment agrees below 2 * n, and every later segment agrees with the previous one below a number that is at least 2 * n (hge1).