Section 11 commutativity: evaluated-slice commutation consequences

Downstream consequences of the evaluated-slice commutation estimate: pulling single-point evaluated-family self-consistency bounds up to evaluated-slice questions. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/EvaluatedSliceCommutation/Consequences.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The relations are strategy.state.SDDRel, a vector-state relation on joint operators, and the placed families evaluatedPointFamilyLeft strategy.state and evaluatedPointFamilyRight strategy.state take the model explicitly in the port (Co/Commutativity/Defs/Core.lean). Each proof is the marginalization of the uniform product distribution, as a term.

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/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPRE.LIDT.Co.Commutativity.evaluatedPointSelfConsistency_fst {𝔓 : 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 𝔓) (zeta : ℝ) (hssc : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (evaluatedPointFamilyLeft strategy.state params family) (evaluatedPointFamilyRight strategy.state params family) zeta) : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft strategy.state params family q.1) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => evaluatedPointFamilyRight strategy.state params family q.1) zeta

Pull a single-point evaluated-family self-consistency bound up to the first coordinate of an evaluated-slice question.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedPointSelfConsistency_snd {𝔓 : 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 𝔓) (zeta : ℝ) (hssc : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (evaluatedPointFamilyLeft strategy.state params family) (evaluatedPointFamilyRight strategy.state params family) zeta) : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft strategy.state params family q.2) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => evaluatedPointFamilyRight strategy.state params family q.2) zeta

Pull a single-point evaluated-family self-consistency bound up to the second coordinate of an evaluated-slice question.