Full-slice normalization and self-consistency machinery

Normalization-condition bounds, evaluated projective submeasurements, and full-slice and evaluated-slice self-consistency estimates used by the scalar-to-tensor comparison: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/FullSlice/Machinery/Normalization.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

normalizationCondition_sandwich_bound and evaluateAtProjSubMeas are stated over any C*-algebra with its order, so they serve the local algebra 𝔓 and the joint operators K →L[ℂ] K alike. The two placed normalization bounds take the model (S : SymModel 𝔓 K) as their first explicit argument, the placement lemma rule of M3: the vendored leftTensor (ι₂ := ι) is S.L, and ᴴ is star. The self-consistency bounds are stated with strategy.state.qSDDCore on strategy.state.L and strategy.state.R; they read the average of a function of one coordinate as the average over that coordinate (avgOver_uniform_fst, avgOver_uniform_snd, the classical avgOver_xEvaluatedQuestion_to_pointNext), where the vendored proofs restate it in a calc.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPRE.LIDT.Co.Commutativity.normalizationCondition_sandwich_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (P : SubMeas α 𝔓) (Q : ProjSubMeas β 𝔓) : ∑ a : α, (∑ b : β, Q.outcome b * P.outcome a * Q.outcome b) * star (∑ b : β, Q.outcome b * P.outcome a * Q.outcome b) ≤ 1

Paper lem:normalization-condition (commutativity-G.tex line 309).

For a sub-measurement P and projective sub-measurement Q, the sandwiched family C_{a,b} = Q_b · P_a · Q_b satisfies the closenessOfIP normalization condition ∑_a (∑_b C_{a,b}) (∑_b C_{a,b})^* ≤ I.

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluateAtProjSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (u : MIPStarRE.LDT.Point params) (P : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : ProjSubMeas (MIPStarRE.LDT.Fq params) 𝔓

Evaluate a polynomial-indexed projective submeasurement at a point, retaining projectivity of the postprocessed outcomes.

This reuses the shared postprocessing projectivity lemma rather than reproving the orthogonality/postprocessing infrastructure locally.

Equations

• MIPRE.LIDT.Co.Commutativity.evaluateAtProjSubMeas params u P = { toSubMeas := MIPRE.LIDT.Co.evaluateAt params u P.toSubMeas, proj := ⋯ }

theorem MIPRE.LIDT.Co.Commutativity.leftTensor_normalizationCondition_sandwich_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (P : SubMeas α 𝔓) (Q : ProjSubMeas β 𝔓) : ∑ a : α, (∑ b : β, S.L (Q.outcome b * P.outcome a * Q.outcome b)) * star (∑ b : β, S.L (Q.outcome b * P.outcome a * Q.outcome b)) ≤ 1

Placed form of normalizationCondition_sandwich_bound, used as the C-normalization hypothesis in closenessOfIP.

For C_{a,b} = Q_b P_a Q_b ⊗ I, the square-sum condition on the joint operators follows by applying the placement S.L to paper lem:normalization-condition.

theorem MIPRE.LIDT.Co.Commutativity.leftTensor_normalizationCondition_sandwich_adjoint_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (P : SubMeas α 𝔓) (Q : ProjSubMeas β 𝔓) : ∑ a : α, star (∑ b : β, S.L (Q.outcome b * P.outcome a * Q.outcome b)) * ∑ b : β, S.L (Q.outcome b * P.outcome a * Q.outcome b) ≤ 1

Adjoint-side placed normalization condition used with closenessOfIPAdjoint.

theorem MIPRE.LIDT.Co.Commutativity.fullSlice_selfConsistency_fst_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (hself : family.StronglySelfConsistent strategy.state zeta) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.FullSliceQuestion params)) fun (xy : MIPStarRE.LDT.Commutativity.FullSliceQuestion params) => strategy.state.qSDDCore (fun (g : MIPStarRE.LDT.Polynomial params) => strategy.state.L ((family.meas xy.1).outcome g)) fun (g : MIPStarRE.LDT.Polynomial params) => strategy.state.R ((family.meas xy.1).outcome g)) ≤ zeta

Full-slice strong self-consistency pulled to the first coordinate of a full-slice question.

This is the A^x_g = G^x_g ⊗ I, B^x_g = I ⊗ G^x_g input for the closenessOfIP applications in paper commutativity-G.tex line 334.

theorem MIPRE.LIDT.Co.Commutativity.fullSlice_selfConsistency_snd_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (hself : family.StronglySelfConsistent strategy.state zeta) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.FullSliceQuestion params)) fun (xy : MIPStarRE.LDT.Commutativity.FullSliceQuestion params) => strategy.state.qSDDCore (fun (h : MIPStarRE.LDT.Polynomial params) => strategy.state.L ((family.meas xy.2).outcome h)) fun (h : MIPStarRE.LDT.Polynomial params) => strategy.state.R ((family.meas xy.2).outcome h)) ≤ zeta

Full-slice strong self-consistency pulled to the second coordinate of a full-slice question.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSlice_selfConsistency_snd_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (hself : family.StronglySelfConsistent strategy.state zeta) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => strategy.state.qSDDCore (fun (b : MIPStarRE.LDT.Fq params) => strategy.state.L ((evaluatedSliceSecondFactor params family q).outcome b)) fun (b : MIPStarRE.LDT.Fq params) => strategy.state.R ((evaluatedSliceSecondFactor params family q).outcome b)) ≤ zeta

Evaluated-slice point self-consistency pulled to the second coordinate of an evaluated-slice question.

theorem MIPRE.LIDT.Co.Commutativity.xEvaluated_selfConsistency_fst_bound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (hself : family.StronglySelfConsistent strategy.state zeta) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params × MIPStarRE.LDT.Commutativity.FullSliceQuestion params)) fun (ux : MIPStarRE.LDT.Point params × MIPStarRE.LDT.Commutativity.FullSliceQuestion params) => strategy.state.qSDDCore (fun (a : MIPStarRE.LDT.Fq params) => strategy.state.L ((evaluateAt params ux.1 (family.meas ux.2.1).toSubMeas).outcome a)) fun (a : MIPStarRE.LDT.Fq params) => strategy.state.R ((evaluateAt params ux.1 (family.meas ux.2.1).toSubMeas).outcome a)) ≤ zeta

Point-level self-consistency pulled to mixed (u, x, y) data for the already x-evaluated first coordinate.