Section 12 pasting: G-hat facts

Quadrant decompositions and \widehat G bookkeeping facts, cor:G-hat-facts: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/GHatFacts.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, and a strategy is a SymStrat params.next 𝔓 K; the slice family is an IdxPolyFamily params 𝔓. The placed families take S as their first explicit argument.

The vendored gHatFacts and gHatFacts_ofComMainAndSelfConsistency read strategy.permInvState only to pass it to gCompleteSelfConsistency and gBotSelfConsistency, whose ported forms take no such hypothesis (section "Swap symmetry is a theorem"), so the statements here are the vendored ones, translated, and the proofs no longer read that field.

Every outcome of the \widehat G pair product is, by definition, the outcome of one of the four quadrant families, so the quadrant decomposition is a regrouping of the sum over Option _ × Option _ with each summand matched by rfl, where the vendored proof rebuilds the outcome functions by simp. The swapped incomplete quadrant is the incomplete point quadrant with the questions and the two families exchanged, so its bound is sddOpRel_swap_questions followed by Preliminaries.sddOpRel_symm.

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.gHatPairProduct_qSDDOp_decompose {𝔓 : 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 𝔓) (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) : S.qSDDOp (gHatPairProductLeft S params family q) (gHatPairProductRight S params family q) = S.qSDDOp (OpFamily.leftPlacedOpFamily S (CommutativityPoints.orderedProductOpFamily (family.meas q.1).toSubMeas (family.meas q.2).toSubMeas)) (OpFamily.leftPlacedOpFamily S (CommutativityPoints.reversedProductOpFamily (family.meas q.1).toSubMeas (family.meas q.2).toSubMeas)) + S.qSDDOp (incompletePartPointProductLeft S params family q) (incompletePartPointProductRight S params family q) + S.qSDDOp (OpFamily.leftPlacedOpFamily S (multiplyByTotalOnLeft (incompletePartSubMeas params family q.1) (family.meas q.2).toSubMeas)) (OpFamily.leftPlacedOpFamily S (multiplyByTotalOnRight (family.meas q.2).toSubMeas (incompletePartSubMeas params family q.1))) + S.qSDDOp (incompletePartTotalProductLeft S params family q) (incompletePartTotalProductRight S params family q)

The pointwise \widehat G pair product splits into the complete-complete, complete-incomplete, incomplete-complete, and incomplete-incomplete quadrants.

theorem MIPRE.LIDT.Co.Pasting.gHatFacts_ofSelfConsistencyAndCommutation {𝔓 : 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 zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hgamma : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : params.d ≤ params.q) (hselfComplete : GCompleteSelfConsistencyStatement params S family zeta) (hselfIncomplete : GBotSelfConsistencyStatement params S family zeta) (hcommComplete : CommutingWithGCompleteStatement params S family gamma zeta) (hcommIncomplete : CommutingWithGIncompleteStatement params S family gamma zeta) : GHatFactsStatement params S family gamma zeta

Internal form of cor:G-hat-facts after applying lem:g-complete-self-consistency, cor:g-bot-self-consistency, cor:commuting-with-G-complete, and cor:commuting-with-G-incomplete.

Source: The proof in references/ldt-paper/ld-pasting.tex:817-862 uses these four preceding Section 12 results internally. The paper-facing theorem gHatFacts below derives them from the source hypotheses rather than exposing them as public hypotheses.

theorem MIPRE.LIDT.Co.Pasting.gHatFacts {𝔓 : 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 𝔓) (eps delta gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hgamma : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : params.d ≤ params.q) (hgood : strategy.IsGood eps delta gamma) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) : GHatFactsStatement params strategy.state family gamma zeta

cor:G-hat-facts, source-facing form.

theorem MIPRE.LIDT.Co.Pasting.gHatFacts_ofComMainAndSelfConsistency {𝔓 : 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 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hgamma : gamma ≤ 1) (hzeta_nonneg : 0 ≤ zeta) (hzeta : zeta ≤ 1) (hd_le_q : params.d ≤ params.q) (hcom : Commutativity.ComMainConclusion params strategy family gamma zeta) (hself : family.StronglySelfConsistent strategy.state zeta) : GHatFactsStatement params strategy.state family gamma zeta

Internal form of cor:G-hat-facts after applying thm:com-main.

The construction of the \widehat G estimates needs the commutativity conclusion of Section 11 and the strong self-consistency of the slice family. The full good-strategy hypothesis is therefore not part of this passage; it is used only upstream when proving thm:com-main.