Phase 2 stability defect infrastructure

Internal helper definitions and lemmas for the Phase 2 scalar bridge in ProcessedG. These definitions extract and bound the one-dimensional stability defect controlled by gCommStability_scalar (the paper's clm:g-comm-stability), reindex the question-level defect into the stability defect via finite marginalization, and perform the subtraction algebra that rewrites the phase-2 insertion/removal difference as the negative defect.

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseTwoStabilityDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (y : Fq params) : Error

The scalar defect controlled by gCommStability_scalar after averaging out all evaluated-slice variables except the second slice height y.

This is the paper's boundedness witness term for clm:g-comm-stability: for a fixed y, gCommStabilityR params family y averages the left-register sandwich G^{u,x}_a G^y_g G^{u,x}_a, while IdxPolyFamily.averagedSlicePointEvaluationOperator strategy y g averages the right-register point answer A^{v,y}_{g(v)} over the tail point v.

Equations

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

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseTwo_stability_defect_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (zeta : Error) (hnorm : strategy.state.IsNormalized) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) : |avgOver (uniformDistribution (Fq params)) (evaluatedSlicePhaseTwoStabilityDefect params strategy family G)| ≤ √zeta

Direct √ζ control of the phase-2 stability defect.

The remaining bridge from the explicit evaluated-slice difference to this one-dimensional defect is pure finite reindexing and averaging: expand totalSandwichFamily, decompose the sampled second point as (v,y), collect the postprocessing fiber ∑_b ∑_{g : g(v)=b} into ∑_g, and average the first sampled point into gCommStabilityR.

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseTwoQuestionDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (q : EvaluatedSliceQuestion params) : Error

The still-unmarginalized phase-2 defect at a sampled evaluated-slice question.

This is the exact question-level term obtained after expanding totalSandwichFamily and using S * G^y.total - S = -S * (1 - G^y.total) for the left-register sandwich S. The remaining reindexing residual averages this term to evaluatedSlicePhaseTwoStabilityDefect.

Equations

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

theorem MIPStarRE.LDT.Commutativity.postprocess_sandwichByOuter_prod_snd_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (b : β) : (postprocess (sandwichByOuterSubMeas A B) Prod.snd).outcome b = ∑ a : α, A.outcome a * B.outcome b * A.outcome a

Postprocessing a sandwiched product by its second coordinate sums over the outer outcome.

For the sandwiched submeasurement with outcomes (a, b) and effect A_a B_b A_a, the Prod.snd postprocessing has outcome b equal to ∑ a, A_a B_b A_a. This is the finite-fiber identity used to recognize the gCommStabilityR averaged sandwich.

theorem MIPStarRE.LDT.Commutativity.avgOver_avgOver_phaseTwo_linear {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Q : Type u_2} {V : Type u_3} {Γ : Type u_4} {Aidx : Type u_5} [Fintype Γ] [Fintype Aidx] (𝒟Q : Distribution Q) (𝒟V : Distribution V) (ψ : QuantumState (ι × ι)) (F : Q → Γ → Aidx → Quantum.Op ι) (P : Γ → V → Quantum.Op ι) (R : Quantum.Op ι) : (avgOver 𝒟V fun (v : V) => avgOver 𝒟Q fun (q : Q) => ∑ g : Γ, ∑ a : Aidx, ev ψ (leftTensor (F q g a * R) * rightTensor (P g v))) = ∑ g : Γ, ev ψ (leftTensor ((averageOperatorOverDistribution 𝒟Q fun (q : Q) => ∑ a : Aidx, F q g a) * R) * rightTensor (averageOperatorOverDistribution 𝒟V fun (v : V) => P g v))

Pull two finite averages into a bipartite expectation with averaged operators.

For a fixed polynomial outcome g, the left register is averaged over 𝒟Q while the right register is averaged over 𝒟V. The identity rewrites the nested scalar average of ev ψ (leftTensor (F q g a * R) * rightTensor (P g v)) into the expectation of leftTensor ((E_q ∑_a F q g a) * R) * rightTensor (E_v P g v), preserving the outer sum over g.

theorem MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseTwoQuestionDefect_append_eq_sum_poly {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (q1 : Point params.next) (v : Point params) (y : Fq params) : evaluatedSlicePhaseTwoQuestionDefect params strategy family G (q1, appendPoint params v y) = ∑ g : Polynomial params, ∑ a : Fq params, ev strategy.state (leftTensor ((evaluatedPointFamily params family q1).outcome a * (family.meas y).outcome g * (evaluatedPointFamily params family q1).outcome a * (1 - (G y).total)) * rightTensor ((strategy.pointMeasurement (appendPoint params v y)).outcome (g.toFun v)))

Reindex the pointwise phase-2 question defect by polynomial outcomes.

When the sampled second point is appendPoint v y, the postprocessed slice outcome (evaluatedSliceSecondFactor ...).outcome b is the sum of G^y_g over the fiber g v = b. Expanding this fiber inside the sandwiched left-register expression and summing over b collapses the defect to a polynomial-indexed sum whose right-register outcome is A^{v,y}_{g(v)}.

The proof is heartbeat-heavy because it keeps the finite-fiber and tensor linearity steps explicit rather than hiding the #714 marginalization residual in one large simp.

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseTwo_term_diff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (q : EvaluatedSliceQuestion params) (a b : Fq params) : ev strategy.state (leftTensor ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).outcome a) * (Preliminaries.totalSandwichFamily (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.2).outcome b) - ev strategy.state (leftTensor ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).outcome a) * rightTensor ((evaluatedSlicePointMeas params strategy q.2).outcome b)) = -ev strategy.state (leftTensor ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).outcome a * (1 - (G (pointHeight params q.2)).total)) * rightTensor ((evaluatedSlicePointMeas params strategy q.2).outcome b))

Pointwise algebra for the phase-2 subtraction.

After expanding totalSandwichFamily, the inserted summand has the extra factor G^y.total on the left register. This lemma rewrites the difference with the removed summand as the negative defect, using the noncommutative identity S * T - S = -(S * (1 - T)).

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseTwo_avg_diff_eq_neg_questionDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) : have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params); have inserted := fun (q : EvaluatedSliceQuestion params) => ∑ b : Fq params, ∑ a : Fq params, ev strategy.state (leftTensor ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).outcome a) * (Preliminaries.totalSandwichFamily (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.2).outcome b); have removed := fun (q : EvaluatedSliceQuestion params) => ∑ b : Fq params, ∑ a : Fq params, ev strategy.state (leftTensor ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).outcome a) * rightTensor ((evaluatedSlicePointMeas params strategy q.2).outcome b)); avgOver 𝒟 inserted - avgOver 𝒟 removed = -avgOver 𝒟 (evaluatedSlicePhaseTwoQuestionDefect params strategy family G)

Average the pointwise phase-2 algebra over evaluated-slice questions.

This proves the advertised sign rewrite avgOver 𝒟 phase1Inserted - avgOver 𝒟 phase2Removed = -avgOver 𝒟 questionDefect. It leaves only the finite marginalization from the question-level defect to the one-dimensional evaluatedSlicePhaseTwoStabilityDefect.

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseTwo_questionDefect_avg_eq_stabilityDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) : avgOver (uniformDistribution (EvaluatedSliceQuestion params)) (evaluatedSlicePhaseTwoQuestionDefect params strategy family G) = avgOver (uniformDistribution (Fq params)) (evaluatedSlicePhaseTwoStabilityDefect params strategy family G)

Exact finite reindexing identity for the phase-2 scalar bridge.

Paper origin: references/ldt-paper/commutativity-G.tex:60-83, the finite averaging and reindexing step leading to the scalar eq:add-an-a bridge.

This statement contains no analytic estimate. It says that the question-level phase-2 defect averages to the one-dimensional scalar defect bounded by gCommStability_scalar. The proof is only finite marginalization and fiber bookkeeping: decompose the second sampled point as (v,y), collapse the postprocessing fibers, and average the first sampled point into gCommStabilityR.