Extracting arithmetic inputs from Pauli questions

Basis index zero selects X and one selects Z. Axis directions are constructed from the explicit binary seed selector; diagonal directions are already present in the question's direction field.

noncomputable def MIPRE.Introspection.FieldQuestionProgram.selectedPoint : Cost.PolyTimeFun (ℕ × PauliStageProgram.Fields) (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.Introspection.FieldQuestionProgram.selectedScalar : Cost.PolyTimeFun (ℕ × PauliStageProgram.Fields) Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.Introspection.FieldQuestionProgram.selectedPoint_zero (fields : PauliStageProgram.Fields) : selectedPoint.toFun (0, fields) = fields.1

@[simp]

theorem MIPRE.Introspection.FieldQuestionProgram.selectedPoint_one (fields : PauliStageProgram.Fields) : selectedPoint.toFun (1, fields) = fields.2.1

@[simp]

theorem MIPRE.Introspection.FieldQuestionProgram.selectedScalar_zero (fields : PauliStageProgram.Fields) : selectedScalar.toFun (0, fields) = fields.2.2.2.2.1

@[simp]

theorem MIPRE.Introspection.FieldQuestionProgram.selectedScalar_one (fields : PauliStageProgram.Fields) : selectedScalar.toFun (1, fields) = fields.2.2.2.2.2

noncomputable def MIPRE.Introspection.FieldQuestionProgram.unitEntryProg : Cost.PolyTimeFun (ℕ × Cost.Unary × ℕ) Cost.BitStr

Equations

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

theorem MIPRE.Introspection.FieldQuestionProgram.unitEntryProg_correct (k : ℕ) (hk : 1 ≤ k) (i j : ℕ) : unitEntryProg.toFun (i, Cost.unary k, j) = (SAT.shoupBinField k hk).toBits (if i = j then 1 else 0)

noncomputable def MIPRE.Introspection.FieldQuestionProgram.unitDirectionProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × ℕ) (List Cost.BitStr)

Width, dimension, and selected axis index.

Equations

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

theorem MIPRE.Introspection.FieldQuestionProgram.unitDirectionProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (i : Fin m) : unitDirectionProg.toFun (Cost.unary k, Cost.unary m, ↑i) = (SAT.shoupBinField k hk).vecBits (Pi.single i 1)

noncomputable def MIPRE.Introspection.FieldQuestionProgram.axisDirectionProg : Cost.PolyTimeFun ((Cost.Unary × Cost.Unary × Cost.Unary) × Cost.BitStr) (List Cost.BitStr)

Field width, selector width, dimension, followed by the canonical seed.

Equations

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

theorem MIPRE.Introspection.FieldQuestionProgram.axisDirectionProg_correct (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (seed : (SAT.shoupBinField k hk).carrier) : axisDirectionProg.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), (SAT.shoupBinField k hk).toBits seed) = (SAT.shoupBinField k hk).vecBits (Pi.single (SeedProgram.selector (SAT.shoupBinField k hk) j hj seed) 1)