Reindexing and evaluation utilities for the evaluated-slice paper chain

This file contains finite-reindexing and evaluated-family identities used by the paper-faithful scalar approximation chain.

theorem MIPStarRE.LDT.Commutativity.evaluatedPointFamily_total_eq_G_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (u : Point params.next) : (evaluatedPointFamily params family u).total = (G (pointHeight params u)).total

The evaluated point family has the same total as the underlying slice measurement G at the sampled height.

This unfolds evaluatedPointFamily as postprocessing of family.meas y; the postprocessing total is unchanged, and hG identifies the slice with G y.

theorem MIPStarRE.LDT.Commutativity.ev_leftTensor_mul_middle_finset_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} (s : Finset α) (ψ : QuantumState (ι × ι)) (A C R D : Quantum.Op ι) (B : α → Quantum.Op ι) : ev ψ (leftTensor ((A * ∑ x ∈ s, B x) * C * R) * rightTensor D) = ∑ x ∈ s, ev ψ (leftTensor (A * B x * C * R) * rightTensor D)

Expand a finite sum in the middle factor of a left-register sandwich.

Linearity of matrix multiplication, left tensor placement, multiplication by a fixed right-register operator, and ev turns A (∑ x, B_x) C R ⊗ D into the corresponding sum of expectations ∑ x, A B_x C R ⊗ D.

theorem MIPStarRE.LDT.Commutativity.evaluatedPointFamily_appendPoint_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (x : Fq params) (u : Point params) (a : Fq params) : (evaluatedPointFamily params family (appendPoint params u x)).outcome a = ∑ g : Polynomial params with g.toFun u = a, (G x).outcome g

Evaluating the slice family at an appended point is postprocessing the slice measurement by the fiber {g | g u = a}.