The Pauli constraints at unit vectors

A linear check's constraint vector (LinCheck.toCon) is its value at the unit vectors of the answer bits, then its target (toCon_eq_ofFn); the k coordinate checks of a field equation E(z) = κ are the coordinates of E at the unit vectors (fieldChecks_toCon). A unit vector is the bit vector of a unit bit string (bitVec_unitBits), so its value under a check of PauliCons is the check's expression on the two answers that string decodes to: line_value, pauli_value, prb_value, bitEq_value evaluate the checks of the line, table, probe and bit-equality rules on readings of the answers. This is what the programs of PauliConsProg compute.

Constraint vectors from unit evaluations

theorem MIPRE.Tailored.Intro.PauliConsUnit.toCon_eq_ofFn {N : ℕ} (χ : LinCheck N) : χ.toCon = (List.ofFn fun (p : Fin N) => LowDegree.BinaryLinear.bit (χ.φ (PauliHideProg.unitV p))) ++ [LowDegree.BinaryLinear.bit χ.c]

theorem MIPRE.Tailored.Intro.PauliConsUnit.bit_coord (k : ℕ) (hk : 1 ≤ k) (x : (SAT.shoupBinField k hk).carrier) (s : Fin k) : LowDegree.BinaryLinear.bit ((SAT.shoupCoordinateEquiv k hk) x s) = List.getD ((SAT.shoupBinField k hk).toBits x) (↑s) false

theorem MIPRE.Tailored.Intro.PauliConsUnit.fieldChecks_toCon {N : ℕ} (k : ℕ) (hk : 1 ≤ k) (E : (Fin N → ZMod 2) →ₗ[ZMod 2] (SAT.shoupBinField k hk).carrier) (κ : (SAT.shoupBinField k hk).carrier) : List.map LinCheck.toCon (fieldChecks k hk E κ) = List.ofFn fun (s : Fin k) => (List.ofFn fun (p : Fin N) => List.getD ((SAT.shoupBinField k hk).toBits (E (PauliHideProg.unitV p))) (↑s) false) ++ [List.getD ((SAT.shoupBinField k hk).toBits κ) (↑s) false]

The constraint vectors of a field equation: coordinate s of E at every unit vector.

theorem MIPRE.Tailored.Intro.PauliConsUnit.toBits_zero (k : ℕ) (hk : 1 ≤ k) : (SAT.shoupBinField k hk).toBits 0 = List.replicate k false

theorem MIPRE.Tailored.Intro.PauliConsUnit.bitVec_unitBits {N : ℕ} (p : Fin N) : bitVec N (LowDegree.BinaryLinear.unitBits N ↑p) = PauliHideProg.unitV p

The values of the checks

theorem MIPRE.Tailored.Intro.PauliConsUnit.line_value {N k : ℕ} {hk : 1 ≤ k} (v : Fin N → ZMod 2) {n oP oL : ℕ} (τ : (SAT.shoupBinField k hk).carrier) {f : Fin (n + 1) → (SAT.shoupBinField k hk).carrier} {a : (SAT.shoupBinField k hk).carrier} (hP : (fldAt k hk N oP) v = a) (hL : ∀ (i : Fin (n + 1)), (fldAt k hk N (oL + ↑i * k)) v = f i) : (∑ i : Fin (n + 1), LinearMap.mulRight (ZMod 2) (τ ^ ↑i) ∘ₗ fldAt k hk N (oL + ↑i * k) - fldAt k hk N oP) v = ∑ i : Fin (n + 1), f i * τ ^ ↑i + a

theorem MIPRE.Tailored.Intro.PauliConsUnit.pauli_value {N k : ℕ} {hk : 1 ≤ k} {M : ℕ} (v : Fin N → ZMod 2) {oP oQ : ℕ} (y : Fin M → (SAT.shoupBinField k hk).carrier) {h : (Fin M → Bool) → (SAT.shoupBinField k hk).carrier} {a : (SAT.shoupBinField k hk).carrier} (hP : (fldAt k hk N oP) v = a) (hQ : ∀ (z : Fin M → Bool), (fldAt k hk N (oQ + ↑((Introspection.FieldTableProgram.cubeEnumeration M) z) * k)) v = h z) : (∑ z : Fin M → Bool, LinearMap.mulRight (ZMod 2) ((MvPolynomial.eval y) (LowDegree.ind z)) ∘ₗ fldAt k hk N (oQ + ↑((Introspection.FieldTableProgram.cubeEnumeration M) z) * k) - fldAt k hk N oP) v = (MvPolynomial.eval y) (LowDegree.ldEnc h) + a

theorem MIPRE.Tailored.Intro.PauliConsUnit.prb_value {N k : ℕ} {hk : 1 ≤ k} (v : Fin N → ZMod 2) (r : (SAT.shoupBinField k hk).carrier) {oP oB : ℕ} {a : (SAT.shoupBinField k hk).carrier} {b : ZMod 2} (hP : (fldAt k hk N oP) v = a) (hB : (getv N oB) v = b) : (PauliCons.prbCheck k hk N r oP oB).φ v = QLD.prb a r + b

theorem MIPRE.Tailored.Intro.PauliConsUnit.bitEq_value {N : ℕ} (v : Fin N → ZMod 2) {o o' : ℕ} {b b' : ZMod 2} (h : (getv N o) v = b) (h' : (getv N o') v = b') : (PauliCons.bitEq N o o').φ v = b + b'