Encoding fidelity: a model of the CNF is a light logical operator

Reflect/LRAT.lean turns successful kernel replay into unsatisfiability of a CNF. This module supplies Boolean semantic soundness of the encoder; Reflect/Complete proves the converse, and Reflect/Distance connects these semantics to binary matrices and Hamming weight. Concrete solver output and replay data are outside this import.

What the encoder asserts is (see the module note of the external encoder)

exists x, w  with  x in ker(Hker),  w in ker(Hpair),  x.w = 1,  wt(x) <= k

The three parts are each realised by one class of clauses, and for each class this module establishes soundness ("all clauses satisfied implies that the semantics holds"):

part	clauses	soundness
xorChain	a Tseitin chain plus one fixing clause	dotS σ xs = want (dotS is the GF(2)

dot product over a support set) |

| atMostK | a sequential counter (Sinz) | cntS σ xs ≤ k |

The product variables (a Tseitin conjunction of three clauses) are given in a later section of this same file. The fact that "x is not in the row space of Hpair" follows from x.w = 1 together with w ∈ ker(Hpair): if x = Σ c_r r is a combination of rows, then x.w = Σ c_r (r.w) = 0, contradicting x.w = 1. This step uses only the one half row space ⊆ (ker)⊥; the converse inclusion (ker)⊥ ⊆ row is not needed.

The GF(2) dot product over a support set, and the support size

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

The GF(2) dot product Σ_{j ∈ s} σ j over the support set s (with XOR of Bool as the addition).

Equations

• QECCertificates.LRAT.dotS σ [] = false
• QECCertificates.LRAT.dotS σ (j :: s) = (σ j ^^ QECCertificates.LRAT.dotS σ s)

@[simp]

theorem QECCertificates.LRAT.dotS_nil (σ : Assign) : dotS σ [] = false

@[simp]

theorem QECCertificates.LRAT.dotS_cons (σ : Assign) (j : ℕ) (s : List ℕ) : dotS σ (j :: s) = (σ j ^^ dotS σ s)

theorem QECCertificates.LRAT.dotS_append (σ : Assign) (s t : List ℕ) : dotS σ (s ++ t) = (dotS σ s ^^ dotS σ t)

The concatenation law: the dot product is additive under concatenation of support sets.

def QECCertificates.LRAT.cntS (σ : Assign) (l : List ℕ) : ℕ

The support size: the number of variables that σ assigns true.

Equations

• QECCertificates.LRAT.cntS σ l = (List.filter (fun (t : ℕ) => σ t) l).length

@[simp]

theorem QECCertificates.LRAT.cntS_nil (σ : Assign) : cntS σ [] = 0

theorem QECCertificates.LRAT.cntS_append (σ : Assign) (l₁ l₂ : List ℕ) : cntS σ (l₁ ++ l₂) = cntS σ l₁ + cntS σ l₂

theorem QECCertificates.LRAT.cntS_singleton_true (σ : Assign) (x : ℕ) (h : σ x = true) : cntS σ [x] = 1

theorem QECCertificates.LRAT.cntS_singleton_false (σ : Assign) (x : ℕ) (h : σ x = false) : cntS σ [x] = 0

theorem QECCertificates.LRAT.cntS_le_length (σ : Assign) (l : List ℕ) : cntS σ l ≤ l.length

General clause lemmas

theorem QECCertificates.LRAT.sat_two {σ : Assign} {a b : Lit} (h : SatClause σ [a, b]) : σ a.fst = a.snd ∨ σ b.fst = b.snd

The semantics of a two-literal clause.

theorem QECCertificates.LRAT.sat_three {σ : Assign} {a b c : Lit} (h : SatClause σ [a, b, c]) : σ a.fst = a.snd ∨ σ b.fst = b.snd ∨ σ c.fst = c.snd

The semantics of a three-literal clause.

Tseitin chain: Σ xs = want

def QECCertificates.LRAT.xorStepClauses (cur x nxt : ℕ) : List Clause

The four clauses of one Tseitin step, pinning nxt = cur ⊕ x.

The polarities of the four clauses must not be swapped: dropping the negation of nxt in the first two leaves the chain computing an equivalence rather than an XOR, which detaches the UNSAT result from the physical assertion (a self-check on a small example in the external encoder guards against exactly this).

Equations

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

theorem QECCertificates.LRAT.xorStep_sat {σ : Assign} {cur x nxt : ℕ} (h : ∀ (C : Clause), C ∈ xorStepClauses cur x nxt → SatClause σ C) : σ nxt = (σ cur ^^ σ x)

Soundness of one step: all four clauses true implies that nxt takes the value cur ⊕ x.

def QECCertificates.LRAT.xorChainAux : List ℕ → Bool → ℕ → ℕ → List Clause × ℕ

The chain: starting from cur, XOR in each variable of rest in turn, with the new variables numbered consecutively from c.

The final clause (emitted once rest is exhausted) pins the result of the chain to want.

Equations

• One or more equations did not get rendered due to their size.
• QECCertificates.LRAT.xorChainAux [] x✝² x✝¹ x✝ = ([[(x✝¹, x✝²)]], x✝)

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

Soundness of the chain: all clauses true implies dotS σ (cur :: rest) = want.

def QECCertificates.LRAT.xorChain (xs : List ℕ) (want : Bool) (start : ℕ) : List Clause × ℕ

The complete chain (xs nonempty; an empty list can only come from an empty support set, in which case no clause is emitted at all, since the encoder never produces an empty support set and a [-start] clause would create a constraint out of nothing).

Equations

• QECCertificates.LRAT.xorChain [] want start = ([], start)
• QECCertificates.LRAT.xorChain (j :: s) want start = QECCertificates.LRAT.xorChainAux s want j start

theorem QECCertificates.LRAT.xorChain_sat {σ : Assign} {x₀ : ℕ} {rest : List ℕ} {want : Bool} {start : ℕ} (h : ∀ (C : Clause), C ∈ (xorChainAux rest want x₀ start).fst → SatClause σ C) : dotS σ (x₀ :: rest) = want

Soundness of the chain (the nonempty form).

theorem QECCertificates.LRAT.xorChain_sat' {σ : Assign} {xs : List ℕ} {want : Bool} {start : ℕ} (hne : xs ≠ []) (h : ∀ (C : Clause), C ∈ (xorChain xs want start).fst → SatClause σ C) : dotS σ xs = want

Soundness of the chain for an arbitrary nonempty list of variables; used when a definition such as prodVars does not reduce syntactically.

Sequential counter: wt ≤ k

def QECCertificates.LRAT.SlotOK (s : ℕ → ℕ → Option ℕ) (k : ℕ) : Prop

The slot convention: s i j is the variable number meaning "at least j of the first i variables are true"; none marks the slot as a constant (true when j = 0, false when j > min i (k + 1)).

The external encoder writes 0 for those two constant slots, and it must discharge them before emitting clauses: 0 is the clause terminator in DIMACS, so writing it out would split one clause into two.

Equations

• QECCertificates.LRAT.SlotOK s k = ∀ (i j : ℕ), s i j = none ↔ ¬(1 ≤ j ∧ j ≤ min i (k + 1))

theorem QECCertificates.LRAT.SlotOK.some_of {s : ℕ → ℕ → Option ℕ} {k : ℕ} (hok : SlotOK s k) {i j : ℕ} (h1 : 1 ≤ j) (h2 : j ≤ min i (k + 1)) : ∃ (v : ℕ), s i j = some v

theorem QECCertificates.LRAT.SlotOK.none_of {s : ℕ → ℕ → Option ℕ} {k : ℕ} (hok : SlotOK s k) {i j : ℕ} (h : ¬(1 ≤ j ∧ j ≤ min i (k + 1))) : s i j = none

def QECCertificates.LRAT.slotClauses (s : ℕ → ℕ → Option ℕ) (i j x : ℕ) : List Clause

The three or four clauses of the slot (i,j), transcribed verbatim from the encoder none slots are discharged as constants (always false or always true).

Equations

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

def QECCertificates.LRAT.rowClauses (s : ℕ → ℕ → Option ℕ) (k i x : ℕ) : List Clause

All clauses of the i-th row (which processes the variable x), expanded over j = 1..min i (k + 1).

Equations

• QECCertificates.LRAT.rowClauses s k i x = List.flatMap (fun (j' : ℕ) => QECCertificates.LRAT.slotClauses s i (j' + 1) x) (List.range (min i (k + 1)))

def QECCertificates.LRAT.atMostKAux (s : ℕ → ℕ → Option ℕ) (k : ℕ) (pre suf : List ℕ) : List Clause

The sequential counter: pre holds the variables already processed (the slot numbers are computed from its length) and suf the remaining ones. When k+1 ≤ pre.length, that is on reaching the last row, one further clause is emitted pinning s n (k + 1) to false.

Equations

• QECCertificates.LRAT.atMostKAux s k pre [] = if k + 1 ≤ pre.length then match s pre.length (k + 1) with | some v => [[(v, false)]] | none => [] else []
• QECCertificates.LRAT.atMostKAux s k pre (j :: s_1) = QECCertificates.LRAT.rowClauses s k (pre.length + 1) j ++ QECCertificates.LRAT.atMostKAux s k (pre ++ [j]) s_1

def QECCertificates.LRAT.atMostK (s : ℕ → ℕ → Option ℕ) (k : ℕ) (xs : List ℕ) : List Clause

All clauses of the counter (starting from an empty prefix).

Equations

• QECCertificates.LRAT.atMostK s k xs = QECCertificates.LRAT.atMostKAux s k [] xs

theorem QECCertificates.LRAT.mem_rowClauses {s : ℕ → ℕ → Option ℕ} {k i j x : ℕ} {C : Clause} (h1 : 1 ≤ j) (h2 : j ≤ min i (k + 1)) (hC : C ∈ slotClauses s i j x) : C ∈ rowClauses s k i x

Membership for the row clauses: for 1 ≤ j ≤ min i (k + 1), the clauses of the slot (i,j) all occur in the i-th row.

theorem QECCertificates.LRAT.atMostKAux_sat {σ : Assign} {s : ℕ → ℕ → Option ℕ} {k : ℕ} (hok : SlotOK s k) (pre suf : List ℕ) : (∀ (j : ℕ), 1 ≤ j → j ≤ min pre.length (k + 1) → j ≤ cntS σ pre → ∃ (v : ℕ), s pre.length j = some v ∧ σ v = true) → (∀ (C : Clause), C ∈ atMostKAux s k pre suf → SatClause σ C) → cntS σ (pre ++ suf) ≤ k

Soundness of the counter: all clauses satisfied implies that the number of true variables is at most k.

The invariant is: at least j of the first i variables are true implies that the slot (i,j) is true. The induction runs along the list of variables (pre is the prefix already processed and suf the remainder), so the step needs only List.filter_append and not the index bookkeeping of List.take.

theorem QECCertificates.LRAT.atMostK_sat {σ : Assign} {s : ℕ → ℕ → Option ℕ} {k : ℕ} (hok : SlotOK s k) {xs : List ℕ} (h : ∀ (C : Clause), C ∈ atMostK s k xs → SatClause σ C) : cntS σ xs ≤ k

Soundness of the counter (the prefix-free form): the existence of a σ satisfying all clauses implies that the number of true variables is at most k.

Assembly, matching build_pair of the external encoder

theorem QECCertificates.LRAT.satFormula_append {σ : Assign} {A B : CNF} : SatFormula σ (A ++ B) ↔ SatFormula σ A ∧ SatFormula σ B

theorem QECCertificates.LRAT.SatFormula.forall {σ : Assign} {F : CNF} (h : SatFormula σ F) (C : Clause) : C ∈ F → SatClause σ C

SatFormula is a def and does not unfold automatically at implicit transparency; use this to obtain the ∀ C ∈ F form.

theorem QECCertificates.LRAT.dotS_map (σ : Assign) (f : ℕ → ℕ) (l : List ℕ) : dotS σ (List.map f l) = dotS (fun (t : ℕ) => σ (f t)) l

theorem QECCertificates.LRAT.dotS_congr {σ τ : Assign} {l : List ℕ} (h : ∀ (j : ℕ), j ∈ l → σ j = τ j) : dotS σ l = dotS τ l

theorem QECCertificates.LRAT.cntS_map (σ : Assign) (f : ℕ → ℕ) (l : List ℕ) : cntS σ (List.map f l) = cntS (fun (t : ℕ) => σ (f t)) l

The invariance of the support size under a map, exchanging a list of variable numbers for an assignment indexed by column.

def QECCertificates.LRAT.prodClauses (c n : ℕ) : List Clause

The block of product variables: a_j ↔ x_j ∧ w_j, with three clauses each.

Equations

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

theorem QECCertificates.LRAT.prod_sat {σ : Assign} {a x w : ℕ} (h1 : SatClause σ [(a, false), (x, true)]) (h2 : SatClause σ [(a, false), (w, true)]) (h3 : SatClause σ [(a, true), (x, false), (w, false)]) : σ a = (σ x && σ w)

The three clauses of the product block imply a = x ∧ w.

theorem QECCertificates.LRAT.prodClauses_sat {σ : Assign} {c n : ℕ} (h : ∀ (C : Clause), C ∈ prodClauses c n → SatClause σ C) (j : ℕ) : j < n → σ (c + j) = (σ j && σ (n + j))

All of the product block satisfied implies that every product variable takes the value of the conjunction.

def QECCertificates.LRAT.chainsFrom (f : ℕ → ℕ) : List (List ℕ) → ℕ → List Clause × ℕ

A sequence of xorChains, one per row, returning the clauses and the next variable number.

Equations

• One or more equations did not get rendered due to their size.
• QECCertificates.LRAT.chainsFrom f [] x✝ = ([], x✝)

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

def QECCertificates.LRAT.slotBase (k i : ℕ) : ℕ

The slot base: the number of slots allocated before the i-th row (agreeing with the row-major allocation order of the encoder).

Equations

• QECCertificates.LRAT.slotBase k i = (List.map (fun (i' : ℕ) => min i' (k + 1)) (List.range i)).sum

def QECCertificates.LRAT.slotVar (c k i j : ℕ) : Option ℕ

The slot variable numbers of the sequential counter (none marks a constant slot).

Equations

• QECCertificates.LRAT.slotVar c k i j = if 1 ≤ j ∧ j ≤ min i (k + 1) then some (c + QECCertificates.LRAT.slotBase k i + (j - 1)) else none

theorem QECCertificates.LRAT.slotVar_ok (c k : ℕ) : SlotOK (slotVar c k) k

def QECCertificates.LRAT.kerClauses (Rker : List (List ℕ)) (n : ℕ) : List Clause

The kernel-constraint section (the rows of x, with variable number = column + 1), together with the counter that follows it.

Equations

• QECCertificates.LRAT.kerClauses Rker n = (QECCertificates.LRAT.chainsFrom (fun (j : ℕ) => j) Rker (2 * n)).fst

def QECCertificates.LRAT.c1Of (Rker : List (List ℕ)) (n : ℕ) : ℕ

First unused auxiliary variable after the kernel constraints.

Equations

• QECCertificates.LRAT.c1Of Rker n = (QECCertificates.LRAT.chainsFrom (fun (j : ℕ) => j) Rker (2 * n)).snd

def QECCertificates.LRAT.pairClauses (Rker Rpair : List (List ℕ)) (n : ℕ) : List Clause

The pairing-constraint section (the rows of w, with variable number = n + column + 1).

Equations

• QECCertificates.LRAT.pairClauses Rker Rpair n = (QECCertificates.LRAT.chainsFrom (fun (j : ℕ) => n + j) Rpair (QECCertificates.LRAT.c1Of Rker n)).fst

def QECCertificates.LRAT.c2Of (Rker Rpair : List (List ℕ)) (n : ℕ) : ℕ

First unused auxiliary variable after the pairing constraints.

Equations

• QECCertificates.LRAT.c2Of Rker Rpair n = (QECCertificates.LRAT.chainsFrom (fun (j : ℕ) => n + j) Rpair (QECCertificates.LRAT.c1Of Rker n)).snd

def QECCertificates.LRAT.prodVars (Rker Rpair : List (List ℕ)) (n : ℕ) : List ℕ

The product-variable section, together with the chain for x·w = 1.

Equations

• QECCertificates.LRAT.prodVars Rker Rpair n = List.map (fun (j : ℕ) => QECCertificates.LRAT.c2Of Rker Rpair n + j) (List.range n)

def QECCertificates.LRAT.xwClauses (Rker Rpair : List (List ℕ)) (n : ℕ) : List Clause

Clauses asserting that the componentwise product has odd parity.

Equations

• QECCertificates.LRAT.xwClauses Rker Rpair n = (QECCertificates.LRAT.xorChain (QECCertificates.LRAT.prodVars Rker Rpair n) true (QECCertificates.LRAT.c2Of Rker Rpair n + n)).fst

def QECCertificates.LRAT.c3Of (Rker Rpair : List (List ℕ)) (n : ℕ) : ℕ

First unused auxiliary variable after the odd-pairing chain.

Equations

• QECCertificates.LRAT.c3Of Rker Rpair n = (QECCertificates.LRAT.xorChain (QECCertificates.LRAT.prodVars Rker Rpair n) true (QECCertificates.LRAT.c2Of Rker Rpair n + n)).snd

def QECCertificates.LRAT.buildPair (Rker Rpair : List (List ℕ)) (n k : ℕ) : CNF

The encoding used by this package's pipeline, transcribed verbatim from build_pair of the external encoder.

Rows are given as lists of column indices (the form before to_masks): x_j ↔ variable j+1 and w_j ↔ variable n+j+1. The order of assembly must match verbatim as well, otherwise the instance identity checked by by decide does not go through.

Equations

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

theorem QECCertificates.LRAT.buildPair_sat {Rker Rpair : List (List ℕ)} {n k : ℕ} {σ : Assign} (hn : 0 < n) (hne₁ : ∀ (r : List ℕ), r ∈ Rker → r ≠ []) (hne₂ : ∀ (r : List ℕ), r ∈ Rpair → r ≠ []) (h : SatFormula σ (buildPair Rker Rpair n k)) : cntS σ (List.range n) ≤ k ∧ (∀ (r : List ℕ), r ∈ Rker → dotS σ r = false) ∧ (∀ (r : List ℕ), r ∈ Rpair → dotS (fun (t : ℕ) => σ (n + t)) r = false) ∧ dotS (fun (t : ℕ) => σ t && σ (n + t)) (List.range n) = true

Encoding fidelity (the soundness direction): every satisfying assignment yields

• an x of weight at most k (cntS counts the true positions)
• x in the kernel of Rker and w in the kernel of Rpair
• x.w = 1 (a pointwise conjunction followed by an XOR).

Together with x.w = 1, the third and fourth items make it impossible for x to lie in the row space of Rpair (row space ⊆ (ker)⊥), that is, x is a light logical operator.