Symmetrized-strategy failure probabilities and test bounds #
Failure-probability surrogates and basic low-individual-degree test bounds for
the split strategy interface: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/Test/StrategyFailures.lean in the port of
planning/c6b-plan.md (milestone M0, section "Port conventions").
The vendored file imports the role register Test/StrategyRole/Algebra.lean (the two-role
symmetrization of a two-space strategy, which the port replaces by the doubling of milestone M2),
but none of its declarations mentions it: the failure probabilities and IsGood are stated over
SymStrat alone. So this file imports only Co/Test/StrategyCore.lean, and the failure
probabilities are stated over the ported SymStrat params 𝔓 K, whose state is a symmetric model
strategy.state : SymModel 𝔓 K; the defects are the bipartite ones of Co/Test/Defs.lean, with
the point answers placed by S.L and the line answers by S.R.
The arithmetic lemma three_summand_bounds_of_average_le is classical; it is restated here
(with ℝ for the vendored Error := ℝ) rather than imported, since importing the vendored file
would bring in the role register.
Not ported #
Every declaration of the vendored file has a counterpart here. The vendored file declares nothing about the role register, so no role-register-only declaration is dropped.
Symmetrized strategies and tested-branch bounds #
Failure surrogate for the axis-parallel lines test.
Point answers on the left factor (S.L), line answers (evaluated at the
base point) on the right factor (S.R) of the symmetric model.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Failure surrogate for the self-consistency test.
Uses the bipartite SSC defect (cross-factor overlap).
For projective measurements this equals bipartiteConsError
between the same measurement on both factors.
Equations
- strategy.selfConsistencyFailureProbability = strategy.state.bipartiteSSCError (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas
Instances For
Failure surrogate for the diagonal lines test.
Averages over the restriction index j ∈ {0, …, m − 1}, then
over the j-restricted diagonal test. For each j, direction
vectors have the last m − j − 1 coordinates equal to zero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paper's notion of an (ε,δ,γ)-good symmetric strategy.
Matches the paper's Definition 3.1: three test-passing bounds with no
extra hypotheses. The reparametrization covariance that was formerly
listed here is now a structural property of SymStrat, where it
belongs (the paper treats diagonal measurements as geometrically
covariant by construction).
The axis-parallel test fails with probability at most
eps.The self-consistency test fails with probability at most
delta.The diagonal-line test fails with probability at most
gamma.
Instances For
The diagonal-line failure surrogate is nonnegative.
A good symmetric strategy has a nonnegative axis-parallel error parameter
ε.
A good symmetric strategy has a nonnegative self-consistency error
parameter δ.
A good symmetric strategy has a nonnegative diagonal-lines error parameter
γ.
Answer-valued symmetric strategies #
The answer-valued diagonal-line failure surrogate is nonnegative.
A good answer-valued symmetric strategy has a nonnegative axis-parallel
error parameter ε.
A good answer-valued symmetric strategy has a nonnegative self-consistency
error parameter δ.
A good answer-valued symmetric strategy has a nonnegative diagonal-lines
error parameter γ.