Bridge, part 6, over models: the value of a strategy bounds the failure surrogate #
The model counterpart of the repository's matrix bridge MIPRE/Background/LIDT/Bridge/Value.lean
(not a vendored file; it serves the tensor instance and stays), in the port of
planning/c6b-plan.md (milestone M14, unit M14-1).
The port's soundness hypothesis is a bound on lowIndividualDegreeFailureProbability
(Co/Test/StrategyBiProj/Measurements.lean), the vendored failure surrogate verbatim: an average,
over the verifier's samples, of two-space consistency defects between coarse-grained
measurements. Our hypothesis is a bound on the value S.value = M.povmValue (lidtGame F m d) S.PA S.PB of a projective strategy S : M.ProjStrat (lidtGame F m d) in a bipartite model M. This
file shows
(toCoProjStrat S).lowIndividualDegreeFailureProbability ≤ 1 - S.value (failure_le).
The value is the sum over samples s of s.weight · acc S s where acc S x y is the acceptance
probability given the questions (x, y), a sum of Born probabilities M.bornProb of the
strategy's projections (value_eq_sum, through the model's condWin). For each sample the defect
of the corresponding branch is at most the rejection probability 1 - acc S s
(qBipartiteConsDefect_postprocess_le, Co/Bridge/Defect.lean), because acceptance forces the two
coarse-grained outcomes to agree (the coarse-graining of the line answer is its evaluation at the
sampled point, that of the point answer its value). The branch weights of the two developments
agree, which gives the bound after reindexing the sample spaces through the field coding
(failure_eq_sum); the surrogate being the vendored expression verbatim, the reindexing is the
matrix bridge's.
Reused by import. The classical declarations of the matrix bridge, which mention no
measurement or state, are imported from MIPRE.Background.LIDT.Bridge.Value and named through an
explicit open MIPRE.LIDT.Bridge (…) list, which names none of the declarations redeclared here:
lidtGame_μ, the five acceptance characterizations accepts_axisLine_point,
accepts_point_axisLine, accepts_point_point, accepts_diagLine_point,
accepts_point_diagLine, decP_extendLam and sum_fin_fun; Sample.sum_weight and
Sample.equivSum are those of MIPRE/Background/LIDT/Game.lean.
Not ported #
Of the matrix bridge, born and born_eq_ev are not carried over: born S x y a b is the Born
probability star ψ ⬝ᵥ ((P ⊗ₖ Q) *ᵥ ψ) of a tensor-product strategy, which is the model's
M.bornProb ((S.PA x).op a) ((S.PB y).op b) here, written out in acc. The equations
pointMeasA_eq, pointMeasB_eq, axisMeasA_zero_eq, axisMeasB_zero_eq and diagMeas_zero_eq
are stated in Co/Bridge/Strategy.lean, for toCoProjStrat. Every other declaration that
mentions a strategy is redeclared here under its name: acc, value_eq_sum, one_sub_value,
defect_le_rej, axisA_defect_le, axisB_defect_le, point_defect_le, diagA_defect_le,
diagB_defect_le, mdef, mdef_le, failure_eq_sum and failure_le.
The value as a sum over samples #
The acceptance probability of the strategy S given the questions (x, y): the Born
probabilities of the answer pairs the verifier accepts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value of a strategy is the weighted sum, over the verifier's samples, of the acceptance probabilities given their questions.
The rejection probability of a strategy is the weighted sum, over the verifier's samples, of the rejection probabilities given their questions.
Pointwise bounds #
The defect of two coarse-grained measurements of a strategy is at most the rejection probability whenever acceptance forces the coarse-grained outcomes to agree.
Axis-parallel lines test, line to A.
Axis-parallel lines test, line to B.
Self-consistency test.
Diagonal lines test, line to A.
Diagonal lines test, line to B.
The bound #
The two-space consistency defect of the branch of a sample of our game.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Each branch defect is at most the rejection probability of the sample.
The failure surrogate of the induced strategy is the weighted sum of the branch defects over our samples.
The failure surrogate of the induced strategy is at most the rejection probability of the strategy in the game.