Bridge, part 8, over models: the soundness theorem in our vocabulary #
The model counterpart of the repository's matrix bridge MIPRE/Background/LIDT/Bridge/Main.lean
(not a vendored file; it serves the tensor instance and stays), in the port of
planning/c6b-plan.md (milestone M14, unit M14-2).
The port's main theorem MIPRE.LIDT.Co.Test.mainFormal_isPVMIn (Co/Test/MainTheorem/MainFormal),
applied to the induced strategy toCoProjStrat S of a projective strategy
S : M.ProjStrat (lidtGame F m d) in a bipartite model M that is a dyadic pair, produces two
projective measurements of the port with outcomes the polynomials of individual degree at most
d, one in each player's algebra, which are projective measurements of the repository
(MIPRE.IsPVMIn). ofProjMeas reads them as POVMs with outcomes in LowIndDegPoly along
lowIndDegEquiv, projective by ofProjMeas_isPVMIn, and the three consistency conclusions are
transferred with inconsistency_eq_bipartiteConsError (Co/Bridge/Consistency.lean), the
hypothesis on the value through failure_le (Co/Bridge/Value.lean). The result is soundness,
and its packaging as the canonical-line theorem of M, soundLidtIn_of_isDyadicPair : SoundLidtIn M (Co/Chain/Defs.lean).
Departures from the matrix statements. soundness takes hM : M.IsDyadicPair and
hd : 1 ≤ d, which the port's main theorem needs (Co/Test/MainTheorem/MainFormal); its
measurements are single POVMs of the players' algebras with IsPVMIn of their operators, as in
SoundLidtIn, where the matrix one returns matrix projective measurements over the one-point
question set Unit; its error is M.inconsistency. ofProjMeas is accordingly a POVMIn, and
its projectivity is the separate ofProjMeas_isPVMIn. The point and evaluation readings are
pointPOVMAIn, pointPOVMBIn and evalPOVMIn of Co/Chain/Defs.lean.
Reused by import. The classical declarations of the matrix bridge (lidtParams, enc,
encP, decP_encP, pointEquiv, scalarEquiv, lowIndDegEquiv, lowIndDegEquiv_apply_encP,
enc_injective) are named through an explicit open MIPRE.LIDT.Bridge (…) list, which names none
of the declarations redeclared here. mainFormalError_eq is classical too, but is restated here
under its name rather than imported from the matrix Bridge/Main.lean.
Not ported #
Every declaration of the matrix bridge is redeclared here under its name, for a bipartite model:
ofProjMeas (a POVMIn, with the departure above), ofProjMeas_M (as ofProjMeas_op, the
operators of a POVMIn being op), mainFormalError_eq, pointPOVMA_val, pointPOVMB_val,
evalPOVM_val and soundness.
New here #
ofProjMeas_isPVMIn: the projectivity ofofProjMeas G, from that ofG.soundLidtIn_of_isDyadicPair:soundnessasSoundLidtIn M.
Polynomial measurements as POVMs #
A projective measurement of the port with polynomial outcomes, as a POVM with outcomes in
LowIndDegPoly (the outcomes relabelled along lowIndDegEquiv). Its projectivity is
ofProjMeas_isPVMIn.
Equations
- MIPRE.LIDT.Co.Bridge.ofProjMeas G = { mats := fun (c : MIPRE.LIDT.LowIndDegPoly) => ⟨G.outcome (MIPRE.LIDT.Bridge.lowIndDegEquiv c), ⋯⟩, nonneg := ⋯, normalized := ⋯ }
Instances For
The operators of ofProjMeas G are the outcome operators of G.
ofProjMeas G is projective when the outcome operators of G form a projective
measurement of the repository.
The error bounds of the two developments agree.
The readings of the conclusions #
The point POVMs of player A, as outcomes of the induced strategy's point measurements.
The point POVMs of player B, as outcomes of the induced strategy's point measurements.
Evaluation of a converted global measurement, as the port's evaluation family.
The soundness theorem #
The soundness theorem in a dyadic pair, assembled from the port's main theorem: a
projective strategy for the (m, q, d)-low individual degree test with value at least 1 - ε
has projective measurements GA in 𝒜 and GB in ℬ, with outcomes the polynomials of
individual degree d, consistent with the other player's point measurements and with each other,
up to lidtError m d q k ε.
Departure from the matrix statement: hM and hd are new (the port's main theorem needs them),
and the measurements are POVMs of the players' algebras with IsPVMIn operators.
The canonical-line theorem holds in every dyadic pair: soundness, read as
SoundLidtIn M (Co/Chain/Defs.lean).