Section 12 pasting: complete and incomplete part self-consistency

State-dependent-distance consequences for the complete and incomplete parts of the pasted slice family: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Core/CompletePart.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The vendored second bipartite state ψbi : QuantumState (ι × ι) is the symmetric model S : SymModel 𝔓 K, in the vendored argument position, as in Co/Pasting/Statements.lean; the slice family is an IdxPolyFamily params 𝔓. The vendored hypotheses PermInvState ψbi of gCompleteSelfConsistency, gBotSelfConsistency_ofCompleteSelfConsistency and gBotSelfConsistency were unused there and are dropped (section "Swap symmetry is a theorem").

Each placed projector X contributes ev((L X - R X)^* (L X - R X)) = 2 (ev L X - ev(L X R X)) (Preliminaries.ev_adjoint_self_leftTensor_sub_rightTensor), so the complete-part bound is the matching-mass monotonicity under the readout g ↦ () (Preliminaries.qMatchMass_leftRight_postprocess_ge), in place of the vendored entrywise Kronecker expansions; and the incomplete part has the same distance as the complete part because L (1 - T) - R (1 - T) = R T - L T.

Not ported

• first_construction_scalar_inequality: classical, imported.

References

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

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

theorem MIPRE.LIDT.Co.Pasting.qSDD_completePart_le_slice {𝔓 : 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 𝔓) (x : MIPStarRE.LDT.Fq params) : S.qSDD (SubMeas.liftLeft S (completePartSubMeas params family x)) (SubMeas.liftRight S (completePartSubMeas params family x)) ≤ S.qSDD (SubMeas.liftLeft S (family.meas x).toSubMeas) (SubMeas.liftRight S (family.meas x).toSubMeas)

lem:q-sdd-complete-part-slice-bound: the complete part G^x of a slice is no farther from its right placement than the slice measurement itself.

theorem MIPRE.LIDT.Co.Pasting.gCompleteSelfConsistency {𝔓 : 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 𝔓) (zeta : ℝ) (hself : family.StronglySelfConsistent S zeta) : GCompleteSelfConsistencyStatement params S family zeta

lem:g-complete-self-consistency. This is exactly the slice strong self-consistency hypothesis, stated under the Section 12 statement name.

theorem MIPRE.LIDT.Co.Pasting.gBotSelfConsistency_ofCompleteSelfConsistency {𝔓 : 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 𝔓) (zeta : ℝ) (hcomplete : GCompleteSelfConsistencyStatement params S family zeta) : GBotSelfConsistencyStatement params S family zeta

Internal form of cor:g-bot-self-consistency after applying lem:g-complete-self-consistency.

Source: The proof in references/ldt-paper/ld-pasting.tex:537-558 uses lem:g-complete-self-consistency internally. The paper-facing theorem gBotSelfConsistency below derives that input from strong self-consistency rather than exposing it as a public hypothesis.

theorem MIPRE.LIDT.Co.Pasting.gBotSelfConsistency {𝔓 : 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 𝔓) (zeta : ℝ) (hself : family.StronglySelfConsistent S zeta) : GBotSelfConsistencyStatement params S family zeta

cor:g-bot-self-consistency, source-facing form.