Evaluating a faithfully ordered full Pauli answer

The answer table is ordered by the little-endian binary rank of its Boolean cube argument. The evaluator scans only the supplied rows, so even a malformed short answer is processed in polynomial time. On a full canonical table it computes the low-degree encoding at an arbitrary field point.

def MIPRE.Introspection.FieldTableProgram.cubeIndex {m : ℕ} (y : Fin m → Bool) : Fin (2 ^ m)

The standard little-endian rank of a Boolean cube point.

Equations

• MIPRE.Introspection.FieldTableProgram.cubeIndex y = ⟨MIPRE.Cost.bitsVal (List.ofFn y), ⋯⟩

theorem MIPRE.Introspection.FieldTableProgram.cubeIndex_injective (m : ℕ) : Function.Injective cubeIndex

noncomputable def MIPRE.Introspection.FieldTableProgram.cubeEnumeration (m : ℕ) : (Fin m → Bool) ≃ Fin (2 ^ m)

A faithful cube enumeration; finite choice is used only for its inverse.

Equations

• MIPRE.Introspection.FieldTableProgram.cubeEnumeration m = Equiv.ofBijective MIPRE.Introspection.FieldTableProgram.cubeIndex ⋯

theorem MIPRE.Introspection.FieldTableProgram.cubeEnumeration_bits {m : ℕ} (y : Fin m → Bool) : SAT.padBits m (↑((cubeEnumeration m) y)).bits = List.ofFn y

theorem MIPRE.Introspection.FieldTableProgram.cubeEnumeration_symm_bits {m : ℕ} (i : Fin (2 ^ m)) : SAT.padBits m (↑i).bits = List.ofFn ((cubeEnumeration m).symm i)

noncomputable def MIPRE.Introspection.FieldTableProgram.termProg : Cost.PolyTimeFun ((Cost.BitStr × ℕ) × Cost.Unary × List Cost.BitStr) Cost.BitStr

One supplied answer row, weighted by the indicator at its binary index.

Equations

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

theorem MIPRE.Introspection.FieldTableProgram.termProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (x : Fin m → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) (i : Fin (2 ^ m)) : termProg.toFun (((SAT.shoupBinField k hk).toBits a, ↑i), Cost.unary k, List.ofFn fun (j : Fin m) => (SAT.shoupBinField k hk).toBits (x j)) = (SAT.shoupBinField k hk).toBits (a * LowDegree.indVec x ((cubeEnumeration m).symm i))

noncomputable def MIPRE.Introspection.FieldTableProgram.tableProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × List Cost.BitStr) Cost.BitStr

Width, evaluation point, and supplied answer rows. The range is bounded by the actual answer length, not by a binary size claimed in the answer.

Equations

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

theorem MIPRE.Introspection.FieldTableProgram.tableProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (x : Fin m → (SAT.shoupBinField k hk).carrier) (h : (Fin m → Bool) → (SAT.shoupBinField k hk).carrier) : tableProg.toFun (Cost.unary k, List.ofFn fun (j : Fin m) => (SAT.shoupBinField k hk).toBits (x j), List.ofFn fun (i : Fin (2 ^ m)) => (SAT.shoupBinField k hk).toBits (h ((cubeEnumeration m).symm i))) = (SAT.shoupBinField k hk).toBits ((MvPolynomial.eval x) (LowDegree.ldEnc h))