Section 12 pasting: switcheroo completion utilities #
Post-theorem convenience lemmas: question-swapping, complete-part reinterpretations, and self-consistency inheritance.
theorem
MIPStarRE.LDT.Pasting.sddOpRel_swap_questions
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(A B : IdxOpFamily (SlicePairQuestion params) Outcome (ι × ι))
(δ : Error)
:
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) A B δ →
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (fun (q : SlicePairQuestion params) => A (q.2, q.1))
(fun (q : SlicePairQuestion params) => B (q.2, q.1)) δ
Reindexing a uniform slice-pair average along Prod.swap preserves SDDOpRel.
theorem
MIPStarRE.LDT.Pasting.pointWithCompletePart_as_switcheroo_input
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(family : IdxPolyFamily params ι)
(gamma : Error)
(hcomm :
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (completePartPointProductLeft params family)
(completePartPointProductRight params family) gamma)
:
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params))
(switcherooPointProductLeft params family (completePartProjFamily params family))
(switcherooPointProductRight 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
MIPStarRE.LDT.Pasting.completePartProjFamily_selfConsistency
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(zeta : Error)
(hself : GCompleteSelfConsistencyStatement params strategy.state family zeta)
:
SDDRel strategy.state (uniformDistribution (SliceQuestion params))
(switcherooSelfConsistencyLeft params (completePartProjFamily params family))
(switcherooSelfConsistencyRight params (completePartProjFamily params family)) zeta
The complete-part family inherits self-consistency from the slice family by
pointwise comparison of the qSDD defect.