Main-formal soundness theorem

The two-space final theorem thm:main-formal of the low individual degree test: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Test/MainTheorem/MainFormal.lean in the port of planning/c6b-plan.md (milestone M13, section "Port conventions"). It is the last theorem of the port. A projective strategy strategy : ProjStrat params 𝒞 𝒜 ℬ whose bipartite model is a dyadic pair and which passes the test with error ε has projective polynomial measurements G_A in 𝒜 and G_B in ℬ consistent with the point measurements and with each other up to mainFormalError params k ε. The statement is two-space, as the vendored one is: the symmetric model appears only inside, as the doubled model D(M) in which the main induction runs (Co SourceRoleRegister/Core).

Translation. That of Co Test/MainTheorem/TwoSpace.lean: the vendored ConsRel strategy.state 𝒟 A B δ is bipartiteConsError strategy.state 𝒟 A B ≤ δ, the measurements are ProjMeas (MIPStarRE.LDT.Polynomial params) in 𝒜 (Alice) and ℬ (Bob), and the saturated branch bounds a defect by 1 through TwoSpace.bipartiteConsError_uniform_le_one. The small-error branch is the vendored scalar absorption, verbatim, applied to ProjStrat.sourceRoleRegisterFinalPointConsistency.

Departure: new hypotheses. mainFormalConclusion_ofRoleRegisterScalarBoundary, mainFormal_smallErrorConclusion, mainFormalConclusion and mainFormal take (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) right after strategy, as Co SourceRoleRegister/Final does: the main induction runs in the doubled model of a dyadic pair and needs 1 ≤ params.d, and the two-space orthonormalizations need hM and ζ₁ > 0. mainFormal_trivial_witness uses neither and does not take them. No statement carries a swap, density or normalization hypothesis (the strategy's state is a unit vector by strategy.isNormalized).

Departure: transparency. The vendored file sets backward.isDefEq.respectTransparency false for the whole file; this one does not set it.

Classical, imported. The scalar files of the vendored directory are wholly classical (the error mainFormalError, the cascade scalars and their absorption bounds). They get no Co file: this module imports the vendored Test/MainTheorem/SourceScalars.lean, which imports the others, and names their declarations through explicit open lists. They are

• Test/MainTheorem/ScalarBounds/Definitions.lean,
• Test/MainTheorem/ScalarBounds/EnvelopeBounds.lean,
• Test/MainTheorem/ScalarBounds/CascadeBounds/SigmaZeta1.lean,
• Test/MainTheorem/ScalarBounds/CascadeBounds/Zeta2Zeta3.lean,
• Test/MainTheorem/ScalarBounds/CascadeBounds/Zeta4.lean,
• Test/MainTheorem/ScalarBounds/CascadeBounds/Final.lean,
• Test/MainTheorem/SourceScalars.lean, all classical, imported.

New here

• mainFormal_isPVMIn: the conclusion of mainFormal, with the two measurements projective measurements of the repository (MIPRE.IsPVMIn), through MIPRE.LIDT.Co.ProjMeas.isPVMIn_of_isFinitePair and its B form.
• mainFormal_inconsistency: the same, with the three consistency bounds stated as the inconsistency of the bipartite model (MIPRE.BipartiteModel.inconsistency), the form of MIPRE.LIDT.Simul.SoundIn, through bipartiteConsError_eq_inconsistency.

Not ported

Every declaration of the vendored file has a counterpart here; all but mainFormal_trivial_witness carry the new hypotheses hM and hd.

References

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

• references/ldt-paper/test_definition.tex, thm:main-formal at line 180;
• references/ldt-paper/inductive_step.tex, lines 26–236;
• docs/paper-gaps/issue-906-main-formal-k-bound.tex (k ≥ 400 m d) and docs/paper-gaps/issue-422-main-formal-zero-k-boundary.tex (0 < k).

theorem MIPRE.LIDT.Co.Test.mainFormal_trivial_witness {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (eps : ℝ) (k : ℕ) (herr : 1 ≤ MIPStarRE.LDT.Test.mainFormalError params k eps) : ∃ (G_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps

Saturated-error branch of thm:main-formal. Whenever mainFormalError params k ε ≥ 1, the three consistency conclusions hold for arbitrary projective polynomial measurements (here the trivial ones), since each two-space consistency defect is at most 1 for a unit vector and a uniform question distribution. Neither the test hypothesis nor hM, hd is used.

theorem MIPRE.LIDT.Co.Test.mainFormalConclusion_ofRoleRegisterScalarBoundary {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.PassesLowIndividualDegreeTest eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) (hk0 : 0 < k) (hsmall : ¬1 ≤ MIPStarRE.LDT.Test.mainFormalError params k eps) : ∃ (G_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps

The role-register conclusion with the scalar absorption, once the scalar branch has supplied 0 < k and mainFormalError params k ε < 1: sourceRoleRegisterFinalPointConsistency with its explicit errors weakened to mainFormalError by the vendored Step 8 cascade (MainFormalScalarBounds).

Departure: the hypotheses hM : strategy.state.IsDyadicPair and hd : 1 ≤ params.d are new.

theorem MIPRE.LIDT.Co.Test.mainFormal_smallErrorConclusion {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.PassesLowIndividualDegreeTest eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) (hk0 : 0 < k) (hsmall : ¬1 ≤ MIPStarRE.LDT.Test.mainFormalError params k eps) : ∃ (G_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps

Small-error branch of thm:main-formal: the role-register route with the scalar absorption, once 0 < k is supplied and mainFormalError params k ε < 1. It is not an additional hypothesis of thm:main-formal: mainFormalConclusion calls it only after the saturated branch has been discharged by mainFormal_trivial_witness.

Departure: the hypotheses hM : strategy.state.IsDyadicPair and hd : 1 ≤ params.d are new.

theorem MIPRE.LIDT.Co.Test.mainFormalConclusion {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.PassesLowIndividualDegreeTest eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) (hk0 : 0 < k) : ∃ (G_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps

Source-boundary reduction of thm:main-formal: the saturated branch (mainFormal_trivial_witness) when mainFormalError params k ε ≥ 1, the small-error branch (mainFormal_smallErrorConclusion) otherwise.

Departure: the hypotheses hM : strategy.state.IsDyadicPair and hd : 1 ≤ params.d are new.

theorem MIPRE.LIDT.Co.Test.mainFormal {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.lowIndividualDegreeFailureProbability ≤ eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) (hk0 : 0 < k) : ∃ (G_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps

thm:main-formal, for a dyadic pair. A projective strategy whose bipartite model is a dyadic pair and whose failure probability in the low individual degree test is at most ε has projective polynomial measurements G_A in 𝒜 and G_B in ℬ such that Alice's points are consistent with Bob's evaluations of G_B, Alice's evaluations of G_A with Bob's points, and G_A with G_B, each up to mainFormalError params k ε. As in the vendored theorem, the paper's k ≥ m d is corrected to k ≥ 400 m d, and 0 < k is assumed.

Departure: the hypotheses hM : strategy.state.IsDyadicPair and hd : 1 ≤ params.d are new.

Readouts for the soundness adapters

theorem MIPRE.LIDT.Co.Test.mainFormal_isPVMIn {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.lowIndividualDegreeFailureProbability ≤ eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) (hk0 : 0 < k) : ∃ (G_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), IsPVMIn G_A.outcome ∧ IsPVMIn G_B.outcome ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps

thm:main-formal with projective measurements of the repository: the measurements of mainFormal are MIPRE.IsPVMIn in 𝒜 and ℬ, as every projective measurement of a player's algebra of a finite pair is (MIPRE.LIDT.Co.ProjMeas.isPVMIn_of_isFinitePair).

theorem MIPRE.LIDT.Co.Test.mainFormal_inconsistency {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.lowIndividualDegreeFailureProbability ≤ eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) (hk0 : 0 < k) : ∃ (G_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), IsPVMIn G_A.outcome ∧ IsPVMIn G_B.outcome ∧ (strategy.state.inconsistency (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)).weight (fun (u : MIPStarRE.LDT.Point params) => (strategy.pointMeasurementA u).toPOVMIn) fun (u : MIPStarRE.LDT.Point params) => (polynomialEvaluationMeasurementFamily params G_B.toMeasurement u).toPOVMIn) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ (strategy.state.inconsistency (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)).weight (fun (u : MIPStarRE.LDT.Point params) => (polynomialEvaluationMeasurementFamily params G_A.toMeasurement u).toPOVMIn) fun (u : MIPStarRE.LDT.Point params) => (strategy.pointMeasurementB u).toPOVMIn) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps ∧ (strategy.state.inconsistency (MIPStarRE.LDT.uniformDistribution Unit).weight (fun (x : Unit) => G_A.toPOVMIn) fun (x : Unit) => G_B.toPOVMIn) ≤ MIPStarRE.LDT.Test.mainFormalError params k eps

thm:main-formal as inconsistencies of the bipartite model: the three consistency bounds of mainFormal_isPVMIn, stated as MIPRE.BipartiteModel.inconsistency of measurement families weighted by the uniform question distribution, the form of the consistency conclusions of MIPRE.LIDT.Simul.SoundIn (through bipartiteConsError_eq_inconsistency).