Section 12 pasting: switcheroo completion bounds #
Completion and first-stage switcheroo error bounds.
theorem
MIPStarRE.LDT.Pasting.commutativitySwitcheroo_ofCompleteSelfConsistency
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(ψbi : QuantumState (ι × ι))
(hnorm : ψbi.IsNormalized)
(hfix : swapDensity ψbi.density = ψbi.density)
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
(zeta omega chi : Error)
(hselfG : GCompleteSelfConsistencyStatement params ψbi family zeta)
(hselfM :
SDDRel ψbi (uniformDistribution (SliceQuestion params)) (switcherooSelfConsistencyLeft params M)
(switcherooSelfConsistencyRight params M) omega)
(hcomm :
SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (switcherooPointProductLeft params family M)
(switcherooPointProductRight params family M) chi)
:
CommutativitySwitcherooStatement params ψbi family M zeta omega chi
Internal form of lem:commutativity-switcheroo after applying
lem:g-complete-self-consistency.
Source: The proof in references/ldt-paper/ld-pasting.tex:560-706 uses
the complete-part self-consistency conclusion internally. The paper-facing
theorem commutativitySwitcheroo below derives it from the source strong
self-consistency hypothesis rather than exposing it as a public hypothesis.
theorem
MIPStarRE.LDT.Pasting.commutativitySwitcheroo
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Outcome : Type u_2}
[Fintype Outcome]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(M : IdxProjSubMeas (Fq params) Outcome ι)
(zeta omega chi : Error)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hselfM :
SDDRel strategy.state (uniformDistribution (SliceQuestion params)) (switcherooSelfConsistencyLeft params M)
(switcherooSelfConsistencyRight params M) omega)
(hcomm :
SDDOpRel strategy.state (uniformDistribution (SlicePairQuestion params)) (switcherooPointProductLeft params family M)
(switcherooPointProductRight params family M) chi)
:
CommutativitySwitcherooStatement params strategy.state family M zeta omega chi
lem:commutativity-switcheroo, source-facing form.