Two-space projective strategies: the failure surrogate #
The failure surrogate of a two-space projective strategy (ProjStrat, Co/Test/StrategyCore.lean)
for the low-individual-degree test: the counterpart of the surrogate half of
MIPRE/Background/LIDT/MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean in the port of
planning/c6b-plan.md (milestone M2; reports/c6b-paper-proofs.md, §4, Theorem D, the
surrogate fail_M). The doubling (Co/Doubling/Strategy.lean) consumes it: a strategy whose
surrogate is at most ε doubles to a (3ε, 3ε, 3ε)-good symmetric strategy.
The two-space defect. The vendored surrogate is built from bipartiteConsError ψ, for a state
ψ on ιA × ιB: the bipartite defect of a submeasurement A of the first factor and B of the
second is inherently a two-space quantity. The port's SymModel.bipartiteConsError
(Co/Test/Defs.lean) is its symmetric-model form, with both families in one local algebra. This
file adds the two-space form over a bipartite model M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ of the
repository, with ev (A ⊗ B) read as the Born probability M.bornProb A B: qBipartiteMatchMass,
qBipartiteConsDefect and bipartiteConsError, in the root namespace MIPRE.LIDT.Co and with the
state an explicit argument, as in the vendored file, so that the vendored text
bipartiteConsError strategy.state 𝒟 A B ports unchanged. On the bipartite model of a symmetric
model they are the symmetric-model quantities (SymModel.bipartiteConsError_toBipartite, by
rfl). This departs from the port convention that bipartite defects are SymModel declarations
(planning/c6b-plan.md, "Port conventions"): the departure is needed because the two-space
ProjStrat keeps its two algebras, and only its failure surrogate is stated with it; its
consistency conclusions remain MIPRE.BipartiteModel.inconsistency.
The surrogate (lowIndividualDegreeFailureProbability) is the vendored expression verbatim,
with the vendored answer families and branch probabilities, and the decomposition into its three
branch averages (lowIndividualDegreeFailureProbability_eq_role_averages, by rfl). The
nonnegativity lemmas of the branches, which the vendored development keeps in
Test/StrategyBiProjRoleAverage/Final.lean, are here, beside the definitions; the goodness bound
of that file is Doubling.symmStrat_isGood_three_mul (Co/Doubling/Strategy.lean).
Not ported #
localDirectSumMeasurement: the role-register direct sumιA ⊕ ιBof the vendored symmetrization; replaced by the doublingCo/Doubling/.localDirectSumMeasurement_outcome: aslocalDirectSumMeasurement.localDirectSumMeasurement_total: aslocalDirectSumMeasurement.localDirectSumProjMeas: aslocalDirectSumMeasurement.localDirectSumProjMeas_outcome: aslocalDirectSumMeasurement.roleBlockMeasurement: the role-register block; replaced by the doubling.roleBlockMeasurement_outcome: asroleBlockMeasurement.roleBlockMeasurement_total: asroleBlockMeasurement.roleBlockProjMeas: asroleBlockMeasurement.roleBlockProjMeas_outcome: asroleBlockMeasurement.roleRegisterProjMeas: the role-register measurement; replaced by the componentwise pairingDoubling.pairProjMeas(Co/Doubling/Strategy.lean).roleRegisterProjMeas_A_inl_inl: asroleRegisterProjMeas.roleRegisterProjMeas_B_inr_inr: asroleRegisterProjMeas.roleRegisterProjMeas_A_B: asroleRegisterProjMeas.roleRegisterProjMeas_B_A: asroleRegisterProjMeas.roleRegisterPointMeasurement: replaced byDoubling.symmStrat's point measurement.roleRegisterAxisParallelMeasurement: replaced byDoubling.symmStrat's axis-parallel measurement.roleRegisterDiagonalMeasurement: replaced byDoubling.symmStrat's diagonal measurement.roleRegisterAxisParallelTransportInvariant: replaced byDoubling.pairAxisParallel_reparamInvariant.roleRegisterDiagonalTransportInvariant: replaced byDoubling.pairDiagonal_reparamInvariant.roleRegisterSymmStrategy: replaced by the doubled strategyDoubling.symmStrat.
The two-space bipartite defect #
Two-space bipartite matching mass ∑_a ⟨ψ, (A_a ⊗ B_a) ψ⟩ = ∑_a bornProb (A_a, B_a), with
A in the first player's algebra and B in the second's (the vendored qBipartiteMatchMass on
ιA × ιB).
Equations
- MIPRE.LIDT.Co.qBipartiteMatchMass M A B = ∑ a : Outcome, M.bornProb (A.outcome a) (B.outcome a)
Instances For
Two-space bipartite questionwise consistency defect
max 0 (⟨ψ, (A_total ⊗ B_total) ψ⟩ − ∑_a ⟨ψ, (A_a ⊗ B_a) ψ⟩) (the vendored
qBipartiteConsDefect on ιA × ιB).
Equations
- MIPRE.LIDT.Co.qBipartiteConsDefect M A B = max 0 (M.bornProb A.total B.total - MIPRE.LIDT.Co.qBipartiteMatchMass M A B)
Instances For
Two-space averaged bipartite consistency defect (the vendored bipartiteConsError on
ιA × ιB).
Equations
- MIPRE.LIDT.Co.bipartiteConsError M 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => MIPRE.LIDT.Co.qBipartiteConsDefect M (A q) (B q)
Instances For
The two-space bipartite consistency defect is nonnegative.
The two-space averaged bipartite consistency defect is nonnegative.
The two-space defect generalizes the symmetric one: on the bipartite model of a symmetric
model, the two-space averaged defect is SymModel.bipartiteConsError.
Answer families #
Alice's point answers in the axis-parallel branch: Alice receives u,
the base point of the sampled line, and answers with A^{A,u}.
Equations
- strategy.axisParallelPointAnswerFamilyA s = (strategy.pointMeasurementA s.1).toSubMeas
Instances For
Bob's point answers in the axis-parallel branch: Bob receives u,
the base point of the sampled line, and answers with A^{B,u}.
Equations
- strategy.axisParallelPointAnswerFamilyB s = (strategy.pointMeasurementB s.1).toSubMeas
Instances For
Alice's axis-parallel-line answers: Alice receives ℓ, answers with
B^{A,ℓ}, and the verifier postprocesses to the value at the sampled base
point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bob's axis-parallel-line answers: Bob receives ℓ, answers with
B^{B,ℓ}, and the verifier postprocesses to the value at the sampled base
point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alice's point answers in the restricted diagonal branch: Alice receives the
sampled base point u and answers with A^{A,u}.
Equations
- strategy.diagonalPointAnswerFamilyA j s = (strategy.pointMeasurementA s.1).toSubMeas
Instances For
Bob's point answers in the restricted diagonal branch: Bob receives the
sampled base point u and answers with A^{B,u}.
Equations
- strategy.diagonalPointAnswerFamilyB j s = (strategy.pointMeasurementB s.1).toSubMeas
Instances For
Alice's restricted diagonal-line answers: Alice receives ℓ, answers with
L^{A,ℓ}, and the verifier postprocesses to the value at the sampled base
point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bob's restricted diagonal-line answers: Bob receives ℓ, answers with
L^{B,ℓ}, and the verifier postprocesses to the value at the sampled base
point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Branch failure probabilities #
Axis-parallel branch component where Alice receives the sampled line and Bob receives its base point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Axis-parallel branch component where Alice receives the sampled base point and Bob receives the sampled line.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paper's axis-parallel branch for a two-space general strategy, averaged over the two role choices.
Equations
- strategy.axisParallelRoleAverage = (strategy.axisParallelLineLeftPointRightFailureProbability + strategy.axisParallelPointLeftLineRightFailureProbability) / 2
Instances For
Point-agreement branch: both provers receive the same point and the verifier checks equality of their field answers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Diagonal branch component where Alice receives the sampled diagonal line and Bob receives its base point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Diagonal branch component where Alice receives the sampled base point and Bob receives the sampled diagonal line.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paper's diagonal branch for a two-space general strategy, averaged over the two role choices and the restricted diagonal samples.
Equations
- strategy.diagonalRoleAverage = (strategy.diagonalLineLeftPointRightFailureProbability + strategy.diagonalPointLeftLineRightFailureProbability) / 2
Instances For
The surrogate #
Failure surrogate for the full low-individual-degree test for a paper-faithful two-space projective strategy (the vendored expression verbatim).
The three outer summands are respectively axis-parallel consistency, point
agreement, and restricted-diagonal consistency, with outer weight 1 / 3.
Each line branch averages the two prover-role orderings with weight 1 / 2, and
the restricted-diagonal branch also averages its restriction index with weight
1 / m. Line answers are evaluated at zeroCoord, the parameter value of the
sampled base point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The direct low-individual-degree score agrees with its decomposition into axis-parallel, point-agreement, and restricted-diagonal role averages.
Passing the full low-individual-degree test with error ε, for the
paper-faithful two-space strategy container.
The failure surrogate is at most
ε.
Instances For
Nonnegativity (the vendored Test/StrategyBiProjRoleAverage/Final.lean) #
The axis-parallel role-average branch of a two-space projective strategy is nonnegative.
The point-agreement branch of a two-space projective strategy is nonnegative.
The diagonal role-average branch of a two-space projective strategy is nonnegative.
The full low-individual-degree failure probability of a two-space projective strategy is nonnegative.
Any passing two-space projective strategy has a nonnegative error parameter.