Section 3 — Strategy core

Base state-invariance and strategy structures for the low individual degree test.

@[instance_reducible]

instance MIPStarRE.LDT.instFintypeRole_1 : Fintype Role

Equations

• MIPStarRE.LDT.instFintypeRole_1 = { elems := {MIPStarRE.LDT.Role.A, MIPStarRE.LDT.Role.B}, complete := MIPStarRE.LDT.instFintypeRole_1._proof_1 }

def MIPStarRE.LDT.swapDensity {ι : Type u_1} (M : Quantum.Op (ι × ι)) : Quantum.Op (ι × ι)

The SWAP reindexing on ι × ι: permutes the two tensor factors. swapDensity M (i₁,i₂) (j₁,j₂) = M (i₂,i₁) (j₂,j₁).

Equations

• MIPStarRE.LDT.swapDensity M = Matrix.of fun (ij kl : ι × ι) => M (ij.2, ij.1) (kl.2, kl.1)

theorem MIPStarRE.LDT.swapDensity_eq_reindex {ι : Type u_1} (X : Quantum.Op (ι × ι)) : swapDensity X = (Matrix.reindex (Equiv.prodComm ι ι) (Equiv.prodComm ι ι)) X

swapDensity is equal to reindexing by the product-commutation equivalence.

@[simp]

theorem MIPStarRE.LDT.swapDensity_swapDensity {ι : Type u_1} (X : Quantum.Op (ι × ι)) : swapDensity (swapDensity X) = X

@[simp]

theorem MIPStarRE.LDT.swapDensity_add {ι : Type u_1} (X Y : Quantum.Op (ι × ι)) : swapDensity (X + Y) = swapDensity X + swapDensity Y

@[simp]

theorem MIPStarRE.LDT.swapDensity_smul {ι : Type u_1} (c : ℂ) (X : Quantum.Op (ι × ι)) : swapDensity (c • X) = c • swapDensity X

theorem MIPStarRE.LDT.swapDensity_mul {ι : Type u_1} [Fintype ι] (X Y : Quantum.Op (ι × ι)) : swapDensity (X * Y) = swapDensity X * swapDensity Y

swapDensity preserves matrix multiplication.

theorem MIPStarRE.LDT.swapDensity_opTensor {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X Y : Quantum.Op ι) : swapDensity (opTensor X Y) = opTensor Y X

theorem MIPStarRE.LDT.normalizedTrace_swapDensity {ι : Type u_1} [Fintype ι] (X : Quantum.Op (ι × ι)) : Quantum.normalizedTrace (swapDensity X) = Quantum.normalizedTrace X

theorem MIPStarRE.LDT.ev_swapDensity_of_density_fixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (hfix : swapDensity ψ.density = ψ.density) (Z : Quantum.Op (ι × ι)) : ev ψ (swapDensity Z) = ev ψ Z

theorem MIPStarRE.LDT.ev_opTensor_swap_of_density_fixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (hfix : swapDensity ψ.density = ψ.density) (X Y : Quantum.Op ι) : ev ψ (opTensor X Y) = ev ψ (opTensor Y X)

theorem MIPStarRE.LDT.qBipartiteMatchMass_symm_of_density_fixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (hfix : swapDensity ψ.density = ψ.density) {Outcome : Type u_2} [Fintype Outcome] (A B : SubMeas Outcome ι) : qBipartiteMatchMass ψ A B = qBipartiteMatchMass ψ B A

theorem MIPStarRE.LDT.qBipartiteConsDefect_symm_of_density_fixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (hfix : swapDensity ψ.density = ψ.density) {Outcome : Type u_2} [Fintype Outcome] (A B : SubMeas Outcome ι) : qBipartiteConsDefect ψ A B = qBipartiteConsDefect ψ B A

theorem MIPStarRE.LDT.consRel_symm_of_density_fixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (hfix : swapDensity ψ.density = ψ.density) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ι) (δ : Error) : ConsRel ψ 𝒟 A B δ → ConsRel ψ 𝒟 B A δ

structure MIPStarRE.LDT.PermInvState {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) : Prop

Permutation-invariance for a bipartite state on ι × ι.

The primary datum is that the density operator is fixed by the SWAP reindexing, swapDensity ψ.density = ψ.density. We also cache the frequently used one-sided expectation consequence ev ψ (leftTensor M) = ev ψ (rightTensor M). This matches the symmetric-strategy construction used in the paper (Section 3) and exposes enough symmetry to swap fully bipartite consistency expressions.

• density_swap : swapDensity ψ.density = ψ.density

  The density operator is fixed by the SWAP reindexing.

• swap_ev (M : Quantum.Op ι) : ev ψ (leftTensor M) = ev ψ (rightTensor M)

  Swapping tensor factors preserves one-sided expectation values.

def MIPStarRE.LDT.AxisParallelMeasurementReparamInvariant (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι) : Prop

Direct outcome-level covariance for axis-parallel-line measurements.

Rebasing a line question by t and reparametrizing an outcome polynomial by the same translation leaves the corresponding projector unchanged.

Equations

• One or more equations did not get rendered due to their size.

def MIPStarRE.LDT.DiagonalMeasurementReparamInvariant (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι) : Prop

Direct outcome-level covariance for diagonal-line measurements.

Rebasing a line question by t and reparametrizing an outcome polynomial by the same translation leaves the corresponding projector unchanged.

Equations

• One or more equations did not get rendered due to their size.

def MIPStarRE.LDT.DiagonalEvaluationReparamInvariant (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι) : Prop

Reparametrization invariance for diagonal-line measurements: evaluating a rebased line at zeroCoord agrees outcome-wise with evaluating the original line at the rebasing parameter.

At the answer level, the geometric identity is DiagonalLinePolynomial.reparamAt_apply_zero. This predicate is stronger: it asserts that the measurement family itself is covariant under rebasing the question index.

Equations

• One or more equations did not get rendered due to their size.

def MIPStarRE.LDT.AxisParallelEvaluationReparamInvariant (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι) : Prop

Reparametrization invariance for axis-parallel-line measurements: evaluating a rebased line at zeroCoord agrees outcome-wise with evaluating the original line at the rebasing parameter.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.AxisParallelLine.transportMeasurement {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : ProjMeas (AxisLinePolynomial params) ι) (t : Fq params) : ProjMeas (AxisLinePolynomial params) ι

Transport an axis-parallel-line measurement along rebasing of the line question by translating its polynomial outcomes.

Equations

• MIPStarRE.LDT.AxisParallelLine.transportMeasurement M t = MIPStarRE.LDT.ProjMeas.transport (MIPStarRE.LDT.AxisLinePolynomial.reparamAtEquiv t) M

theorem MIPStarRE.LDT.AxisParallelLine.transportMeasurement_postprocess_zero {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : ProjMeas (AxisLinePolynomial params) ι) (t a : Fq params) : (postprocess (transportMeasurement M t).toSubMeas fun (x : AxisLinePolynomial params) => x.toFun zeroCoord).outcome a = (postprocess M.toSubMeas fun (f : AxisLinePolynomial params) => f.toFun t).outcome a

Evaluating a transported axis-line measurement at zeroCoord agrees with reading the original measurement at the rebasing parameter.

noncomputable def MIPStarRE.LDT.DiagonalLine.transportMeasurement {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : ProjMeas (DiagonalLinePolynomial params) ι) (t : Fq params) : ProjMeas (DiagonalLinePolynomial params) ι

Transport a diagonal-line measurement along rebasing of the line question by translating its polynomial outcomes.

Equations

• MIPStarRE.LDT.DiagonalLine.transportMeasurement M t = MIPStarRE.LDT.ProjMeas.transport (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAtEquiv t) M

theorem MIPStarRE.LDT.DiagonalLine.transportMeasurement_postprocess_zero {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : ProjMeas (DiagonalLinePolynomial params) ι) (t a : Fq params) : (postprocess (transportMeasurement M t).toSubMeas fun (x : DiagonalLinePolynomial params) => x.toFun zeroCoord).outcome a = (postprocess M.toSubMeas fun (f : DiagonalLinePolynomial params) => f.toFun t).outcome a

Evaluating a transported diagonal-line measurement at zeroCoord agrees with reading the original measurement at the rebasing parameter.

def MIPStarRE.LDT.AxisParallelMeasurementTransportInvariant (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι) : Prop

Stronger rebasing compatibility for axis-parallel-line measurements: the measurement indexed by the rebased line is equal to the transport of the original measurement along the answer reparametrization equivalence.

Equations

• One or more equations did not get rendered due to their size.

def MIPStarRE.LDT.DiagonalMeasurementTransportInvariant (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι) : Prop

Stronger rebasing compatibility for diagonal-line measurements: the measurement indexed by the rebased line is equal to the transport of the original measurement along the answer reparametrization equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.AxisParallelMeasurementTransportInvariant.toMeasurementReparamInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι} (hM : AxisParallelMeasurementTransportInvariant params M) : AxisParallelMeasurementReparamInvariant params M

Transport-level axis-parallel covariance implies direct outcome covariance.

theorem MIPStarRE.LDT.DiagonalMeasurementTransportInvariant.toMeasurementReparamInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι} (hM : DiagonalMeasurementTransportInvariant params M) : DiagonalMeasurementReparamInvariant params M

Transport-level diagonal covariance implies direct outcome covariance.

theorem MIPStarRE.LDT.AxisParallelMeasurementReparamInvariant.toTransportInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι} (hM : AxisParallelMeasurementReparamInvariant params M) : AxisParallelMeasurementTransportInvariant params M

Direct axis-parallel outcome covariance implies transport-level covariance.

theorem MIPStarRE.LDT.DiagonalMeasurementReparamInvariant.toTransportInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι} (hM : DiagonalMeasurementReparamInvariant params M) : DiagonalMeasurementTransportInvariant params M

Direct diagonal outcome covariance implies transport-level covariance.

theorem MIPStarRE.LDT.axisParallelMeasurementReparamInvariant_iff_transportInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι} : AxisParallelMeasurementReparamInvariant params M ↔ AxisParallelMeasurementTransportInvariant params M

Direct outcome covariance and transport-level covariance are equivalent for axis-parallel-line projective measurements.

theorem MIPStarRE.LDT.diagonalMeasurementReparamInvariant_iff_transportInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι} : DiagonalMeasurementReparamInvariant params M ↔ DiagonalMeasurementTransportInvariant params M

Direct outcome covariance and transport-level covariance are equivalent for diagonal-line projective measurements.

theorem MIPStarRE.LDT.AxisParallelMeasurementTransportInvariant.toEvaluationReparamInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι} (hM : AxisParallelMeasurementTransportInvariant params M) : AxisParallelEvaluationReparamInvariant params M

The stronger transport-level axis-parallel compatibility implies the older outcome-level reparametrization invariant predicate.

theorem MIPStarRE.LDT.DiagonalMeasurementTransportInvariant.toEvaluationReparamInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι} (hM : DiagonalMeasurementTransportInvariant params M) : DiagonalEvaluationReparamInvariant params M

The stronger transport-level diagonal compatibility implies the older outcome-level reparametrization invariant predicate.

structure MIPStarRE.LDT.AxisParallelCovariantMeasurement (params : Parameters) [FieldModel params.q] (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Type (max u_1 u_2)

Axis-parallel line measurements bundled with the stronger transport-level rebasing covariance.

• toIdxProjMeas : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι
• transportInvariant : AxisParallelMeasurementTransportInvariant params self.toIdxProjMeas

@[instance_reducible]

instance MIPStarRE.LDT.instCoeFunAxisParallelCovariantMeasurementForallAxisParallelLineProjMeasAxisLinePolynomial {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] : CoeFun (AxisParallelCovariantMeasurement params ι) fun (x : AxisParallelCovariantMeasurement params ι) => AxisParallelLine params → ProjMeas (AxisLinePolynomial params) ι

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.AxisParallelCovariantMeasurement.reparamInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : AxisParallelCovariantMeasurement params ι) : AxisParallelEvaluationReparamInvariant params M.toIdxProjMeas

A covariant wrapper automatically satisfies the older evaluation-level rebasing invariant.

structure MIPStarRE.LDT.DiagonalCovariantMeasurement (params : Parameters) [FieldModel params.q] (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Type (max u_1 u_2)

Diagonal line measurements bundled with the stronger transport-level rebasing covariance.

• toIdxProjMeas : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι
• transportInvariant : DiagonalMeasurementTransportInvariant params self.toIdxProjMeas

@[instance_reducible]

instance MIPStarRE.LDT.instCoeFunDiagonalCovariantMeasurementForallDiagonalLineProjMeasDiagonalLinePolynomial {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] : CoeFun (DiagonalCovariantMeasurement params ι) fun (x : DiagonalCovariantMeasurement params ι) => DiagonalLine params → ProjMeas (DiagonalLinePolynomial params) ι

Equations

• MIPStarRE.LDT.instCoeFunDiagonalCovariantMeasurementForallDiagonalLineProjMeasDiagonalLinePolynomial = { coe := fun (M : MIPStarRE.LDT.DiagonalCovariantMeasurement params ι) => M.toIdxProjMeas }

theorem MIPStarRE.LDT.DiagonalCovariantMeasurement.reparamInvariant {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : DiagonalCovariantMeasurement params ι) : DiagonalEvaluationReparamInvariant params M.toIdxProjMeas

A covariant wrapper automatically satisfies the older evaluation-level rebasing invariant.

def MIPStarRE.LDT.DiagonalAnswerMeasurementTransportInvariant (params : Parameters) [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (DiagonalLine params) (DiagonalLineAnswer params) ι) : Prop

Transport covariance for diagonal-line measurements whose answers are the paper-level line functions.

Equations

• One or more equations did not get rendered due to their size.

structure MIPStarRE.LDT.DiagonalAnswerCovariantMeasurement (params : Parameters) [FieldModel params.q] (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Type u_1

Diagonal-line measurements with paper-level function answers, bundled with transport-level rebasing covariance.

This parallel API is intended for the paper-faithful restriction redesign: unlike DiagonalLinePolynomial, the function-answer alphabet admits a total slice append/restrict equivalence.

• toIdxProjMeas : IdxProjMeas (DiagonalLine params) (DiagonalLineAnswer params) ι
• transportInvariant : DiagonalAnswerMeasurementTransportInvariant params self.toIdxProjMeas

@[instance_reducible]

instance MIPStarRE.LDT.instCoeFunDiagonalAnswerCovariantMeasurementForallDiagonalLineProjMeasDiagonalLineAnswer {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] : CoeFun (DiagonalAnswerCovariantMeasurement params ι) fun (x : DiagonalAnswerCovariantMeasurement params ι) => DiagonalLine params → ProjMeas (DiagonalLineAnswer params) ι

Equations

• One or more equations did not get rendered due to their size.

structure MIPStarRE.LDT.AnswerSymStrat (params : Parameters) [FieldModel params.q] (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Type (max u_1 u_2)

Paper-level symmetric strategy data whose diagonal-line answers are functions.

This parallel structure is the target shape for the restriction redesign in Section 6: restricting an ambient diagonal line to a slice is total for function answers, unlike the current degree-bounded DiagonalLinePolynomial alphabet.

• state : QuantumState (ι × ι)
• permInvState : PermInvState self.state
• densityFixed : swapDensity self.state.density = self.state.density
• isNormalized : self.state.IsNormalized
• pointMeasurement : IdxProjMeas (Point params) (Fq params) ι
• axisParallelMeasurement : AxisParallelCovariantMeasurement params ι
• diagonalMeasurement : DiagonalAnswerCovariantMeasurement params ι

structure MIPStarRE.LDT.SymStrat (params : Parameters) [FieldModel params.q] (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Type (max u_1 u_2)

Paper-local symmetric strategy data.

The line-measurement fields are bundled as transport-covariant wrappers: rebasing the question index is required to agree with transporting the projective measurement along the corresponding answer reparametrization equivalence. This is stronger than the older evaluation-level formulas at zeroCoord, but those formulas remain available as derived lemmas via AxisParallelCovariantMeasurement.reparamInvariant and DiagonalCovariantMeasurement.reparamInvariant.

The isNormalized field records that the bipartite state's density operator has normalized trace 1. For pure states, this coincides with the usual unit-vector condition (⟨ψ|ψ⟩ = 1) used in the paper. Bundling normalization with the strategy avoids threading a state.IsNormalized hypothesis through every downstream consumer (pasting cascade, triangleSub users, self-improvement helpers).

• state : QuantumState (ι × ι)
• permInvState : PermInvState self.state
• densityFixed : swapDensity self.state.density = self.state.density
• isNormalized : self.state.IsNormalized
• pointMeasurement : IdxProjMeas (Point params) (Fq params) ι
• axisParallelMeasurement : AxisParallelCovariantMeasurement params ι
• diagonalMeasurement : DiagonalCovariantMeasurement params ι

@[reducible, inline]

abbrev MIPStarRE.LDT.AxisParallelTestSample (params : Parameters) : Type

Encoded samples (u, i) for the axis-parallel lines test. The paper samples a random point u ∈ F_q^m and a coordinate i ∈ {1, …, m}. In Lean, Fin params.m represents the 0-indexed coordinates {0, …, m - 1}, corresponding to the paper's 1-indexed choice. The sample forms the axis-parallel line through u in that coordinate direction.

Equations

• MIPStarRE.LDT.AxisParallelTestSample params = (MIPStarRE.LDT.Point params × Fin params.m)

def MIPStarRE.LDT.extendRestrictedDirection {params : Parameters} [FieldModel params.q] (j : Fin params.m) (freeCoords : Fin (↑j + 1) → Fq params) : Point params

Extend restricted direction coordinates to a full direction vector. For restriction index j (0-indexed), the first j + 1 coordinates are the given free coordinates and the remaining are zero. This matches the paper's convention that v has its last m − i coordinates zero, where i = j + 1.

Equations

• MIPStarRE.LDT.extendRestrictedDirection j freeCoords k = if h : ↑k ≤ ↑j then freeCoords ⟨↑k, ⋯⟩ else MIPStarRE.LDT.zeroCoord

@[reducible, inline]

abbrev MIPStarRE.LDT.RestrictedDiagonalSample (params : Parameters) (j : Fin params.m) : Type

Encoded samples (u, freeCoords) for the j-restricted diagonal lines test. The base point u ∈ F_q^m and the free coordinates of the restricted direction (first j + 1 coordinates; rest are zero). The full diagonal test averages over j ∈ {0, …, m − 1}.

Equations

• MIPStarRE.LDT.RestrictedDiagonalSample params j = (MIPStarRE.LDT.Point params × (Fin (↑j + 1) → MIPStarRE.LDT.Fq params))

instance MIPStarRE.LDT.restrictedDiagonalSampleNonempty (params : Parameters) (j : Fin params.m) : Nonempty (RestrictedDiagonalSample params j)

The restricted diagonal sample space is nonempty.

@[reducible, inline]

noncomputable abbrev MIPStarRE.LDT.axisParallelPointAnswerFamilyOf {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (pointMeasurement : IdxProjMeas (Point params) (Fq params) ι) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ι

Sampled point answers in the axis-parallel lines test, obtained from a point measurement.

Equations

• MIPStarRE.LDT.axisParallelPointAnswerFamilyOf pointMeasurement s = (pointMeasurement s.1).toSubMeas

@[reducible, inline]

noncomputable abbrev MIPStarRE.LDT.axisParallelLineAnswerFamilyOf {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (axisParallelMeasurement : AxisParallelLine params → ProjMeas (AxisLinePolynomial params) ι) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ι

Sampled line answers in the axis-parallel lines test, obtained from an axis-parallel measurement and evaluated at the base point.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev MIPStarRE.LDT.diagonalPointAnswerFamilyOf {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (pointMeasurement : IdxProjMeas (Point params) (Fq params) ι) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ι

Sampled point answers in the restricted diagonal test, obtained from a point measurement.

Equations

• MIPStarRE.LDT.diagonalPointAnswerFamilyOf pointMeasurement j s = (pointMeasurement s.1).toSubMeas

@[reducible, inline]

noncomputable abbrev MIPStarRE.LDT.diagonalLineAnswerFamilyOf {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Answer : Type u_2} [Fintype Answer] (diagonalMeasurement : DiagonalLine params → ProjMeas Answer ι) (evalAtBase : Answer → Fq params) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ι

Sampled diagonal-line answers in the restricted diagonal test, obtained from a diagonal-line measurement and evaluated at the base point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.axisParallelPointAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ι

Sampled point answers in the axis-parallel lines test. The point player receives u (the base point) and answers with their measurement at u.

Equations

• MIPStarRE.LDT.axisParallelPointAnswerFamily strategy = MIPStarRE.LDT.axisParallelPointAnswerFamilyOf strategy.pointMeasurement

noncomputable def MIPStarRE.LDT.axisParallelLineAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ι

Sampled line answers in the axis-parallel lines test, evaluated at the base point u. The line player receives ℓ and returns a polynomial f. The verifier checks f(u) = a; since u = ℓ.pointAt zeroCoord, we evaluate f at zeroCoord.

Equations

• MIPStarRE.LDT.axisParallelLineAnswerFamily strategy = MIPStarRE.LDT.axisParallelLineAnswerFamilyOf strategy.axisParallelMeasurement.toIdxProjMeas

def MIPStarRE.LDT.lastDirectionLine (params : Parameters) [FieldModel params.q] (u : Point params) : AxisParallelLine params.next

The axis-parallel line in F_q^(m+1) through (u, 0) in the last coordinate direction. This is the geometric line denoted B^u in the paper's last-direction notation.

Equations

• MIPStarRE.LDT.lastDirectionLine params u = { base := MIPStarRE.LDT.appendPoint params u MIPStarRE.LDT.zeroCoord, direction := MIPStarRE.LDT.lastCoord params }

noncomputable def MIPStarRE.LDT.lastDirectionMeasurementFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params.next ι) : IdxProjMeas (Point params) (AxisLinePolynomial params.next) ι

The axis-parallel line measurement family restricted to the paper's last-direction notation u ↦ B^u.

Equations

• MIPStarRE.LDT.lastDirectionMeasurementFamily strategy u = strategy.axisParallelMeasurement.toIdxProjMeas (MIPStarRE.LDT.lastDirectionLine params u)

noncomputable def MIPStarRE.LDT.diagonalPointAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ι

Sampled point answers in the j-restricted diagonal test. The point player receives u and answers at u.

Equations

• MIPStarRE.LDT.diagonalPointAnswerFamily strategy j = MIPStarRE.LDT.diagonalPointAnswerFamilyOf strategy.pointMeasurement j

noncomputable def MIPStarRE.LDT.diagonalLineAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ι

Sampled diagonal-line answers in the j-restricted diagonal test, evaluated at the base point u. Since u = ℓ.pointAt zeroCoord, we evaluate f at zeroCoord.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.AnswerSymStrat.axisParallelPointAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ι

Sampled point answers in the axis-parallel lines test for an answer-valued symmetric strategy.

Equations

• strategy.axisParallelPointAnswerFamily = MIPStarRE.LDT.axisParallelPointAnswerFamilyOf strategy.pointMeasurement

noncomputable def MIPStarRE.LDT.AnswerSymStrat.axisParallelLineAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ι

Sampled line answers in the axis-parallel lines test for an answer-valued symmetric strategy, evaluated at the base point.

Equations

• strategy.axisParallelLineAnswerFamily = MIPStarRE.LDT.axisParallelLineAnswerFamilyOf strategy.axisParallelMeasurement.toIdxProjMeas

noncomputable def MIPStarRE.LDT.AnswerSymStrat.diagonalPointAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ι

Sampled point answers in the restricted diagonal test for an answer-valued symmetric strategy.

Equations

• strategy.diagonalPointAnswerFamily j = MIPStarRE.LDT.diagonalPointAnswerFamilyOf strategy.pointMeasurement j

noncomputable def MIPStarRE.LDT.AnswerSymStrat.diagonalLineAnswerFamily {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ι

Sampled diagonal-line answers in the restricted diagonal test for an answer-valued symmetric strategy, evaluated at the base point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.AnswerSymStrat.axisParallelFailureProbability {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) : Error

Axis-parallel failure surrogate for an answer-valued symmetric strategy.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.AnswerSymStrat.selfConsistencyFailureProbability {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) : Error

Self-consistency failure surrogate for an answer-valued symmetric strategy.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.AnswerSymStrat.diagonalFailureProbability {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : AnswerSymStrat params ι) : Error

Diagonal-line failure surrogate for an answer-valued symmetric strategy.

Equations

• One or more equations did not get rendered due to their size.

structure MIPStarRE.LDT.AnswerSymStrat.IsGood {params : Parameters} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [FieldModel params.q] (strategy : AnswerSymStrat params ι) (eps delta gamma : Error) : Prop

Goodness data for an answer-valued symmetric strategy.

• axisParallelTest : strategy.axisParallelFailureProbability ≤ eps

  The axis-parallel test fails with probability at most eps.

• selfConsistencyTest : strategy.selfConsistencyFailureProbability ≤ delta

  The self-consistency test fails with probability at most delta.

• diagonalLineTest : strategy.diagonalFailureProbability ≤ gamma

  The diagonal-line test fails with probability at most gamma.

structure MIPStarRE.LDT.ProjStrat (params : Parameters) [FieldModel params.q] (ιA : Type u_1) [Fintype ιA] [DecidableEq ιA] (ιB : Type u_2) [Fintype ιB] [DecidableEq ιB] : Type (max (max u_1 u_2) u_3)

Paper-faithful two-space projective strategy data.

This matches the paper's def:general-projective-strategy (test_definition.tex, lines 98--115): Alice's and Bob's measurements act on separate local carriers ιA and ιB, and the bipartite state lives on ιA × ιB without a built-in swap symmetry.

The isNormalized field records that the bipartite state's density operator has normalized trace 1.

The four covariance conditions express that the line-indexed projectors descend from chosen affine parametrizations to geometric lines; transport and zero-coordinate evaluation are equivalent consequences.

• state : QuantumState (ιA × ιB)

  Bipartite state on the tensor product of Alice's and Bob's local carriers.

• isNormalized : self.state.IsNormalized

  The bipartite state's density operator is trace-normalized.

• pointMeasurementA : IdxProjMeas (Point params) (Fq params) ιA

  Alice's point-measurement family, acting on ιA.

• axisParallelMeasurementA : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ιA

  Alice's axis-parallel-line measurement family, acting on ιA.

• axisParallelReparamInvariantA : AxisParallelMeasurementReparamInvariant params self.axisParallelMeasurementA

  Alice's axis-parallel measurement is covariant under line rebasing.

• diagonalMeasurementA : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ιA

  Alice's diagonal-line measurement family, acting on ιA.

• diagonalReparamInvariantA : DiagonalMeasurementReparamInvariant params self.diagonalMeasurementA

  Alice's diagonal measurement is covariant under line rebasing.

• pointMeasurementB : IdxProjMeas (Point params) (Fq params) ιB

  Bob's point-measurement family, acting on ιB.

• axisParallelMeasurementB : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ιB

  Bob's axis-parallel-line measurement family, acting on ιB.

• axisParallelReparamInvariantB : AxisParallelMeasurementReparamInvariant params self.axisParallelMeasurementB

  Bob's axis-parallel measurement is covariant under line rebasing.

• diagonalMeasurementB : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ιB

  Bob's diagonal-line measurement family, acting on ιB.

• diagonalReparamInvariantB : DiagonalMeasurementReparamInvariant params self.diagonalMeasurementB

  Bob's diagonal measurement is covariant under line rebasing.