Role-Register Averaging: Goodness Bound

This module packages the branch equalities into the three-times-error goodness bound for the role-register symmetric strategy.

theorem MIPStarRE.LDT.ProjStrat.axisParallelRoleAverage_nonneg {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) : 0 ≤ strategy.axisParallelRoleAverage

The axis-parallel role-average branch of a two-space projective strategy is nonnegative.

theorem MIPStarRE.LDT.ProjStrat.pointAgreementFailureProbability_nonneg {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) : 0 ≤ strategy.pointAgreementFailureProbability

The point-agreement branch of a two-space projective strategy is nonnegative.

theorem MIPStarRE.LDT.ProjStrat.diagonalRoleAverage_nonneg {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) : 0 ≤ strategy.diagonalRoleAverage

The diagonal role-average branch of a two-space projective strategy is nonnegative.

theorem MIPStarRE.LDT.ProjStrat.lowIndividualDegreeFailureProbability_nonneg {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) : 0 ≤ strategy.lowIndividualDegreeFailureProbability

The full low-individual-degree failure probability of a two-space projective strategy is nonnegative.

theorem MIPStarRE.LDT.ProjStrat.eps_nonneg_of_passes {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] {strategy : ProjStrat params ιA ιB} {eps : Error} (hpass : strategy.PassesLowIndividualDegreeTest eps) : 0 ≤ eps

Any passing two-space projective strategy has a nonnegative error parameter.

theorem MIPStarRE.LDT.ProjStrat.roleRegisterSymmStrategy_is_good_three_mul {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] {strategy : ProjStrat params ιA ιB} {eps : Error} (hpass : strategy.PassesLowIndividualDegreeTest eps) : strategy.roleRegisterSymmStrategy.IsGood (3 * eps) (3 * eps) (3 * eps)

The heterogeneous role-register symmetrization of a two-space projective strategy is (3ε, 3ε, 3ε)-good whenever the original strategy passes the full low individual degree test with error ε.