From Boolean certificate replay to matrix-level code distance

The general bridge from upstream Reflect/Certified.lean is preserved without its concrete code instances. Assignments are read as vectors over ZMod 2, Boolean parity becomes the matrix dot product, and the count of true bits becomes Hamming weight. Separation supplies a dual witness for every vector outside the check row space. Encoder completeness then turns any lighter logical operator into a satisfying assignment.

no_light_logical_of_unsat rules out such operators. le_minWeight_of_unsat packages this as a distance bound and composes with unsat_of_checkSteps. Support rows must be nonempty, duplicate-free, within range, and agree with the matrices; these conditions are explicit. No concrete CNFs, solver runs, or generated replay datasets are imported.

The two readings: assignments and code vectors

def QECCertificates.LRAT.vecOf (σ : Assign) (n : ℕ) : Vec n

The first n bits of an assignment read as a code vector: 1 where σ is true and 0 otherwise.

Equations

• QECCertificates.LRAT.vecOf σ n i = if σ ↑i = true then 1 else 0

def QECCertificates.LRAT.rowOf (n : ℕ) (r : List ℕ) : Vec n

A support list read as a code vector: 1 at the positions listed in r and 0 otherwise.

Equations

• QECCertificates.LRAT.rowOf n r i = if ↑i ∈ r then 1 else 0

theorem QECCertificates.LRAT.vecOf_apply_ne_zero {σ : Assign} {n : ℕ} {i : Fin n} : vecOf σ n i ≠ 0 ↔ σ ↑i = true

Nonzeroness for vecOf: entry i is nonzero if and only if σ is true there.

Bridge 1: the support size is exactly the count

theorem QECCertificates.LRAT.support_vecOf_card (σ : Assign) (n : ℕ) : (support (vecOf σ n)).card = cntS σ (List.range n)

The support size of vecOf is exactly the count of the assignment: the two readings give the same weight.

Bridge 2: XOR dot products over a support list and dotProduct

theorem QECCertificates.LRAT.cntS_cons (σ : Assign) (j : ℕ) (s : List ℕ) : cntS σ (j :: s) = (if σ j = true then 1 else 0) + cntS σ s

The recursion for cntS (in this version the predicate of List.filter is Bool).

theorem QECCertificates.LRAT.even_one_add (m : ℕ) : Even (1 + m) ↔ ¬Even m

Adding one flips parity.

theorem QECCertificates.LRAT.dotS_eq_false_iff_even (σ : Assign) (r : List ℕ) : dotS σ r = false ↔ Even (cntS σ r)

dotS is parity: the XOR dot product is false if and only if the number of true entries is even.

This step does not need the support list to have no duplicates, since the XOR and the count each take multiplicities into account.

theorem QECCertificates.LRAT.natCast_zmod2_eq_zero_iff_even (c : ℕ) : ↑c = 0 ↔ Even c

A natural number c : ℕ has image zero in ZMod 2 if and only if c is even.

theorem QECCertificates.LRAT.dotProduct_rowOf_vecOf (σ : Assign) (n : ℕ) (r : List ℕ) : rowOf n r ⬝ᵥ vecOf σ n = ∑ i : Fin n, if ↑i ∈ r then if σ ↑i = true then 1 else 0 else 0

Expansion of the product: the entrywise product of rowOf and vecOf is an indicator function.

theorem QECCertificates.LRAT.sum_indicator_eq_cntS (σ : Assign) {n : ℕ} {r : List ℕ} (hr : ∀ t ∈ r, t < n) (hrn : r.Nodup) : (∑ i : Fin n, if ↑i ∈ r then if σ ↑i = true then 1 else 0 else 0) = ↑(cntS σ r)

The sum of indicators is the count: summing the indicator function over a support list equals the count of the assignment.

This is where hrn (no duplicates) is used: dotS counts multiplicities, while Finset does not.

theorem QECCertificates.LRAT.dotS_eq_false_iff_dotProduct (σ : Assign) {n : ℕ} {r : List ℕ} (hr : ∀ t ∈ r, t < n) (hrn : r.Nodup) : dotS σ r = false ↔ rowOf n r ⬝ᵥ vecOf σ n = 0

Bridge 2: dotS reports false if and only if the vector read out is orthogonal to the support vector.

hr requires the indices of the support list to lie within the code length (the encoder's output satisfies this) and hrn requires no duplicates.

Two facts about arithmetic in ZMod 2

theorem QECCertificates.LRAT.zmod2_eq_one_of_ne_zero {x : ZMod 2} (h : x ≠ 0) : x = 1

In ZMod 2 everything nonzero is one.

theorem QECCertificates.LRAT.zmod2_indicator (x : ZMod 2) : (if decide (x = 1) = true then 1 else 0) = x

An element of ZMod 2 is its own one-bit indicator.

Building a satisfying assignment from a kernel vector and a pairing witness

def QECCertificates.LRAT.certAssign (n : ℕ) (E w : Vec n) : Assign

Concatenate a kernel vector in the first n bits and a pairing witness in the next n bits into one assignment.

From the second block on the bound t < 2n is used, and positions beyond it are false, since Assign is ℕ → Bool and must be a total function.

Equations

• QECCertificates.LRAT.certAssign n E w t = if h : t < n then decide (E ⟨t, h⟩ = 1) else if h2 : t < 2 * n then decide (w ⟨t - n, ⋯⟩ = 1) else false

theorem QECCertificates.LRAT.certAssign_lt {n : ℕ} (E w : Vec n) {t : ℕ} (ht : t < n) : certAssign n E w t = decide (E ⟨t, ht⟩ = 1)

theorem QECCertificates.LRAT.certAssign_mid {n : ℕ} (E w : Vec n) {t : ℕ} (h1 : ¬t < n) (h2 : t < 2 * n) : certAssign n E w t = decide (w ⟨t - n, ⋯⟩ = 1)

theorem QECCertificates.LRAT.vecOf_certAssign {n : ℕ} (E w : Vec n) : vecOf (certAssign n E w) n = E

The first n bits of the assignment read back as the kernel vector itself.

theorem QECCertificates.LRAT.vecOf_certAssign_shift {n : ℕ} (E w : Vec n) : vecOf (fun (t : ℕ) => certAssign n E w (n + t)) n = w

The next n bits of the assignment read back as the pairing witness.

theorem QECCertificates.LRAT.vecOf_and {n : ℕ} (a b : Assign) : vecOf (fun (t : ℕ) => a t && b t) n = fun (i : Fin n) => vecOf a n i * vecOf b n i

The reading of bitwise conjunction: vecOf sends && to multiplication in ZMod 2.

theorem QECCertificates.LRAT.rowOf_range (n : ℕ) : rowOf n (List.range n) = fun (x : Fin n) => 1

The all-ones support list reads out as the all-ones vector.

General form: a replay verdict implies a code-level lower bound

The interface for arbitrary binary parity-check matrices. The encoder-side input (the Rker/Rpair support lists, n, k), the code-level objects (M₁/M₂), the row correspondence between them and three assembly facts are all taken as hypotheses, and the conclusion is a code-level proposition.

theorem QECCertificates.LRAT.all_of_mem_bounds {n : ℕ} {L : List (List ℕ)} (h : (L.all fun (r : List ℕ) => r.all fun (t : ℕ) => decide (t < n)) = true) (r : List ℕ) : r ∈ L → ∀ t ∈ r, t < n

Turn a bound in List.all form into a pointwise form. The quantifier shape ∀ r ∈ L, … is not one the kernel can decide directly, so the three encoder-side facts are first written with all and then converted into theorem hypotheses here.

theorem QECCertificates.LRAT.all_of_mem_nodup {L : List (List ℕ)} (h : (L.all fun (r : List ℕ) => decide r.Nodup) = true) (r : List ℕ) : r ∈ L → r.Nodup

As above, converting to "the support lists have no duplicates".

theorem QECCertificates.LRAT.all_of_mem_ne_nil {L : List (List ℕ)} (h : (L.all fun (r : List ℕ) => decide (r ≠ [])) = true) (r : List ℕ) : r ∈ L → r ≠ []

As above, converting to "the support lists are nonempty".

theorem QECCertificates.LRAT.no_light_logical_of_unsat {n k : ℕ} {Rker Rpair : List (List ℕ)} {m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {F : CNF} (hF : buildPair Rker Rpair n k = F) (hunsat : ¬Satisfiable F) (hn : 0 < n) (hne₁ : ∀ r ∈ Rker, r ≠ []) (hne₂ : ∀ r ∈ Rpair, r ≠ []) (hb₁ : ∀ r ∈ Rker, ∀ t ∈ r, t < n) (hb₂ : ∀ r ∈ Rpair, ∀ t ∈ r, t < n) (hd₁ : ∀ r ∈ Rker, r.Nodup) (hd₂ : ∀ r ∈ Rpair, r.Nodup) (hrow₁ : List.map (rowOf n) Rker = List.ofFn fun (i : Fin m₁) => M₁ i) (hrow₂ : List.map (rowOf n) Rpair = List.ofFn fun (i : Fin m₂) => M₂ i) : ¬∃ (E : Vec n), (support E).card ≤ k ∧ E ∈ (Matrix.toLin' M₁).ker ∧ E ∉ M₂.certificateRowSpace

The certificate is the lower bound (general form): if the formula produced by the encoder at (Rker, Rpair, n, k) is unsatisfiable, then the corresponding code has no logical operator of weight $\le k$.

The row-correspondence, index bounds and duplicate-free hypotheses connect the Boolean encoder inputs to the matrix model. No solver output is assumed sound.

theorem QECCertificates.LRAT.le_minWeight_of_unsat {n k : ℕ} {Rker Rpair : List (List ℕ)} {m₁ m₂ : ℕ} (M₁ : Matrix (Fin m₁) (Fin n) (ZMod 2)) (M₂ : Matrix (Fin m₂) (Fin n) (ZMod 2)) {F : CNF} (hF : buildPair Rker Rpair n k = F) (hunsat : ¬Satisfiable F) (hn : 0 < n) (hne₁ : ∀ r ∈ Rker, r ≠ []) (hne₂ : ∀ r ∈ Rpair, r ≠ []) (hb₁ : ∀ r ∈ Rker, ∀ t ∈ r, t < n) (hb₂ : ∀ r ∈ Rpair, ∀ t ∈ r, t < n) (hd₁ : ∀ r ∈ Rker, r.Nodup) (hd₂ : ∀ r ∈ Rpair, r.Nodup) (hrow₁ : List.map (rowOf n) Rker = List.ofFn fun (i : Fin m₁) => M₁ i) (hrow₂ : List.map (rowOf n) Rpair = List.ofFn fun (i : Fin m₂) => M₂ i) (hk : k + 1 ≤ n) : k + 1 ≤ minWeightKernelOutsideRowSpace M₁ M₂

An unsatisfiable encoding gives a matrix-level distance lower bound. Combine this with unsat_of_checkSteps to consume a kernel-checked RUP certificate.