Computing the Pauli commutation bit

The dot product of the two exponentially long indicator vectors factors as a product over the supplied coordinates. The program uses this product, followed by the field trace, and never constructs either indicator vector.

theorem MIPRE.Introspection.FieldGammaProgram.indPair_eq_prod {K : Type u_1} [CommRing K] {m : ℕ} (x z : Fin m → K) : LowDegree.indPair x z = ∏ i : Fin m, ((1 - x i) * (1 - z i) + x i * z i)

theorem MIPRE.Introspection.FieldGammaProgram.indPair_eq_prod_charTwo {K : Type u_1} [CommRing K] [CharP K 2] {m : ℕ} (x z : Fin m → K) : LowDegree.indPair x z = ∏ i : Fin m, (1 + x i + z i)

noncomputable def MIPRE.Introspection.FieldGammaProgram.pairFactorProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

Equations

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

theorem MIPRE.Introspection.FieldGammaProgram.pairFactorProg_correct (k : ℕ) (hk : 1 ≤ k) (x z : (SAT.shoupBinField k hk).carrier) : pairFactorProg.toFun ((SAT.shoupBinField k hk).toBits x, (SAT.shoupBinField k hk).toBits z) = (SAT.shoupBinField k hk).toBits (1 + x + z)

noncomputable def MIPRE.Introspection.FieldGammaProgram.pairingProg : Cost.PolyTimeFun (Cost.Unary × List (Cost.BitStr × Cost.BitStr)) Cost.BitStr

Equations

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

theorem MIPRE.Introspection.FieldGammaProgram.pairingProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (x z : Fin m → (SAT.shoupBinField k hk).carrier) : pairingProg.toFun (Cost.unary k, List.ofFn fun (i : Fin m) => ((SAT.shoupBinField k hk).toBits (x i), (SAT.shoupBinField k hk).toBits (z i))) = (SAT.shoupBinField k hk).toBits (LowDegree.indPair x z)

noncomputable def MIPRE.Introspection.FieldGammaProgram.gammaProg : Cost.PolyTimeFun (Cost.Unary × List (Cost.BitStr × Cost.BitStr) × Cost.BitStr × Cost.BitStr) Bool

Width, coordinate pairs, and the two scalar probe multipliers.

Equations

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

theorem MIPRE.Introspection.FieldGammaProgram.gammaProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (x z : Fin m → (SAT.shoupBinField k hk).carrier) (rX rZ : (SAT.shoupBinField k hk).carrier) : gammaProg.toFun (Cost.unary k, List.ofFn fun (i : Fin m) => ((SAT.shoupBinField k hk).toBits (x i), (SAT.shoupBinField k hk).toBits (z i)), (SAT.shoupBinField k hk).toBits rX, (SAT.shoupBinField k hk).toBits rZ) = LowDegree.BinaryLinear.bit (LowDegree.acGamma (ZMod 2) x z rX rZ)

noncomputable def MIPRE.Introspection.FieldGammaProgram.probeProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr × Cost.BitStr) Bool

The two-outcome scalar probe used by the point consistency rules.

Equations

• MIPRE.Introspection.FieldGammaProgram.probeProg = MIPRE.SAT.shoupTraceBitProg.comp (MIPRE.Cost.PolyTimeFun.fst.pair MIPRE.SAT.shoupMulProg)

theorem MIPRE.Introspection.FieldGammaProgram.probeProg_correct (k : ℕ) (hk : 1 ≤ k) (a r : (SAT.shoupBinField k hk).carrier) : probeProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).toBits a, (SAT.shoupBinField k hk).toBits r) = LowDegree.BinaryLinear.bit ((Algebra.trace (ZMod 2) (SAT.shoupBinField k hk).carrier) (a * r))