Self-consistency: strategy-level extensions

The good-strategy characterization (lem:good-strategy-characterization), self-consistency after evaluation (prop:two-notions-of-self-consistency-after-evaluation) and the completeness transfer from a self-consistent family (prop:completeness-transfer-self-consistent-A). This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SelfConsistency/Extensions.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The strategy of goodStrategyCharacterization is the ported SymStrat params 𝔓 K, and its consistency relations are those of the model strategy.state. The two other statements take a symmetric model S : SymModel 𝔓 K in place of the state ψ : QuantumState (ι × ι), as an explicit first argument, with local families in 𝔓 lifted by IdxSubMeas.liftLeft S and IdxSubMeas.liftRight S. The vendored hypotheses hperm : PermInvState ψ (of both) and hψ : ψ.IsNormalized (of completenessTransferSelfConsistentA) are dropped: swap symmetry enters through twoNotionsOfSelfConsistency and bipartiteSSC_implies_localSSC_liftLeft, and normalization is not used.

The proofs are shorter than the vendored ones. In twoNotionsOfSelfConsistencyAfterEvaluation the monotonicity of the bipartite defect under postprocessing is qBipartiteSSCDefect_postprocess_le (Co ComparisonCore). In completenessTransferSelfConsistentA the per-question mass gap is bounded by the local self-consistency defect plus the two overlap gaps, and the average goes through avgOver_sub, avgOver_add, avgOver_const_mul and avgOver_abs_le_sqrt_of_pointwise, in place of the vendored unfolding of avgOver into finite sums.

Not ported

Every declaration of the vendored file has a counterpart here.

References

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

• references/ldt-paper/preliminaries.tex

theorem MIPRE.LIDT.Co.Preliminaries.goodStrategyCharacterization {𝔓 : 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 𝔓 K) (eps delta gamma : ℝ) : strategy.IsGood eps delta gamma ↔ strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.AxisParallelTestSample params)) (axisParallelPointAnswerFamily strategy) (axisParallelLineAnswerFamily strategy) eps ∧ strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas strategy.pointMeasurement.toIdxSubMeas delta ∧ strategy.diagonalFailureProbability ≤ gamma

lem:good-strategy-characterization.

The axis-parallel branch is already definitionally a consistency bound. The self-consistency branch is the same consistency bound specialized to the point measurement, since that family is complete. The diagonal branch remains bundled as strategy.diagonalFailureProbability because its sampled question type depends on the restriction index j.

theorem MIPRE.LIDT.Co.Preliminaries.twoNotionsOfSelfConsistencyAfterEvaluation {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question α 𝔓) (δ : ℝ) (f : Question → α → β) : S.BipartiteSSCRel 𝒟 A δ → S.SDDRel 𝒟 (IdxSubMeas.liftLeft S fun (q : Question) => postprocess (A q) (f q)) (IdxSubMeas.liftRight S fun (q : Question) => postprocess (A q) (f q)) (2 * δ)

prop:two-notions-of-self-consistency-after-evaluation.

Question-dependent postprocessing preserves the total mass and can only increase the diagonal overlap ∑_b ev(A_[f_q(a)=b] ⊗ A_[f_q(a)=b]) (qBipartiteSSCDefect_postprocess_le), so bipartite SSC transfers from A to the postprocessed family, to which twoNotionsOfSelfConsistency applies. The vendored lemma asks for a permutation-invariant state.

theorem MIPRE.LIDT.Co.Preliminaries.completenessTransferSelfConsistentA {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : IdxSubMeas Question Outcome 𝔓) (δ ε : ℝ) : S.BipartiteSSCRel 𝒟 A δ → S.SDDRel 𝒟 (IdxSubMeas.liftLeft S A) (IdxSubMeas.liftLeft S B) ε → S.idxSubMeasMass 𝒟 (IdxSubMeas.liftLeft S B) ≥ S.idxSubMeasMass 𝒟 (IdxSubMeas.liftLeft S A) - δ - 2 * √ε

prop:completeness-transfer-self-consistent-A.

If A is δ-strongly self-consistent and A ⊗ I ≈_ε B ⊗ I, then the mass of B ⊗ I is at least that of A ⊗ I minus δ + 2√ε. Per question, the mass of A ⊗ I exceeds its diagonal ∑ₐ ev(Aₐ² ⊗ I) by at most the local self-consistency defect (bipartiteSSC_implies_localSSC_liftLeft), the diagonal of A exceeds that of B by at most 2 √(qSDD) (the two overlap gaps), and the diagonal of B is at most its mass. The vendored lemma asks for a permutation-invariant, normalized state.