Section 12 pasting: switcheroo completion utilities

Post-theorem convenience lemmas: question-swapping, complete-part reinterpretations, and self-consistency inheritance. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooCompletion/Utilities.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

sddOpRel_swap_questions uses only the state, on joint operator families, so its vendored ψbi is a vector state V : VecState K in the vendored argument position (callers pass S or strategy.state); pointWithCompletePart_as_switcheroo_input places families, so its ψbi is the symmetric model S : SymModel 𝔓 K; completePartProjFamily_selfConsistency takes a SymStrat params.next 𝔓 K. The slice family is an IdxPolyFamily params 𝔓.

sddOpRel_swap_questions is avgOver_uniform_equiv along Equiv.prodComm, whose inverse is Prod.swap by definition. pointWithCompletePart_as_switcheroo_input splits the Polynomial params × Unit sum by Fintype.sum_prod_type and Fintype.sum_unique, and matches the outcomes by change (the ordered and reversed product families unfold on a pair) and completePartSubMeas_outcome_unit, in place of the vendored simp over the family definitions.

Not ported

Nothing: every declaration of the vendored file is ported here.

References

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

• references/ldt-paper/ld-pasting.tex

theorem MIPRE.LIDT.Co.Pasting.sddOpRel_swap_questions {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (V : VecState K) (A B : IdxOpFamily (MIPStarRE.LDT.Pasting.SlicePairQuestion params) Outcome (K →L[ℂ] K)) (δ : ℝ) : V.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) A B δ → V.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => A (q.2, q.1)) (fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => B (q.2, q.1)) δ

Reindexing a uniform slice-pair average along Prod.swap preserves SDDOpRel.

theorem MIPRE.LIDT.Co.Pasting.pointWithCompletePart_as_switcheroo_input {𝔓 : 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] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma : ℝ) (hcomm : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (completePartPointProductLeft S params family) (completePartPointProductRight S params family) gamma) : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (switcherooPointProductLeft S params family (completePartProjFamily params family)) (switcherooPointProductRight S params family (completePartProjFamily params family)) gamma

Reinterpret the point-with-complete-part commutation bound as a relation on the Polynomial × Unit outcome type expected by commutativitySwitcheroo.

theorem MIPRE.LIDT.Co.Pasting.completePartProjFamily_selfConsistency {𝔓 : 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 : GCompleteSelfConsistencyStatement params strategy.state family zeta) : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (switcherooSelfConsistencyLeft strategy.state params (completePartProjFamily params family)) (switcherooSelfConsistencyRight strategy.state params (completePartProjFamily params family)) zeta

The complete-part family inherits self-consistency from the slice family by pointwise comparison of the qSDD defect.