Executable multilinear indicator weights

A full Pauli outcome is evaluated by weighting each field entry by its Boolean cube indicator. This module supplies the uniform weight program, including its exact connection to LowDegree.indVec. No field values or cube points are tabulated by the program: it scans the supplied coordinate/bit pairs.

theorem MIPRE.Introspection.FieldIndicatorProgram.shoupArithmeticFold_mul_correct (k : ℕ) (hk : 1 ≤ k) (values : List (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) : LowDegree.BinaryPolynomial.arithmeticFold true (LowDegree.BinaryPolynomial.shoupLowerCoeffs.toFun (Cost.unary k)) ((SAT.shoupBinField k hk).toBits a) (List.map (SAT.shoupBinField k hk).toBits values) = (SAT.shoupBinField k hk).toBits (a * values.prod)

Modular multiplication of canonical field rows computes their product.

noncomputable def MIPRE.Introspection.FieldIndicatorProgram.factorProg : Cost.PolyTimeFun (Cost.BitStr × Bool) Cost.BitStr

x for a true cube coordinate, and 1-x for a false coordinate.

Equations

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

theorem MIPRE.Introspection.FieldIndicatorProgram.factorProg_correct (k : ℕ) (hk : 1 ≤ k) (x : (SAT.shoupBinField k hk).carrier) (b : Bool) : factorProg.toFun ((SAT.shoupBinField k hk).toBits x, b) = (SAT.shoupBinField k hk).toBits (if b = true then x else 1 - x)

noncomputable def MIPRE.Introspection.FieldIndicatorProgram.indicatorProg : Cost.PolyTimeFun (Cost.Unary × List (Cost.BitStr × Bool)) Cost.BitStr

The field modulus is computed once for the entire coordinate product.

Equations

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

theorem MIPRE.Introspection.FieldIndicatorProgram.indicatorProg_correct (k : ℕ) (hk : 1 ≤ k) (coords : List ((SAT.shoupBinField k hk).carrier × Bool)) : indicatorProg.toFun (Cost.unary k, List.map (fun (p : (SAT.shoupBinField k hk).carrier × Bool) => ((SAT.shoupBinField k hk).toBits p.1, p.2)) coords) = (SAT.shoupBinField k hk).toBits (List.map (fun (p : (SAT.shoupBinField k hk).carrier × Bool) => if p.2 = true then p.1 else 1 - p.1) coords).prod

theorem MIPRE.Introspection.FieldIndicatorProgram.indicatorProg_indVec (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (x : Fin m → (SAT.shoupBinField k hk).carrier) (y : Fin m → Bool) : indicatorProg.toFun (Cost.unary k, List.ofFn fun (i : Fin m) => ((SAT.shoupBinField k hk).toBits (x i), y i)) = (SAT.shoupBinField k hk).toBits (LowDegree.indVec x y)

Exact indicator semantics at an arbitrary field point, not only on the cube.