From 11c73d9ddf8fcc3e28fc10d57b17b7d735124c7a Mon Sep 17 00:00:00 2001 From: texra-ai Date: Fri, 17 Jul 2026 01:49:50 +0200 Subject: [PATCH 1/2] feat: add low individual degree soundness problem --- .../LowIndividualDegreeTest.lean | 1134 +++++++++++++++++ .../mipstarre_low_individual_degree.toml | 9 + 2 files changed, 1143 insertions(+) create mode 100644 LeanEval/QuantumInformation/LowIndividualDegreeTest.lean create mode 100644 manifests/problems/mipstarre_low_individual_degree.toml diff --git a/LeanEval/QuantumInformation/LowIndividualDegreeTest.lean b/LeanEval/QuantumInformation/LowIndividualDegreeTest.lean new file mode 100644 index 00000000..22f325ab --- /dev/null +++ b/LeanEval/QuantumInformation/LowIndividualDegreeTest.lean @@ -0,0 +1,1134 @@ +import Mathlib +import EvalTools.Markers + +/-! +# Challenge: the low individual degree test main theorem + +Self-contained comparator challenge for `MIPStarRE.LDT.Test.mainFormal`, the +corrected source statement of `thm:main-formal` — the soundness theorem of the +quantum low individual degree test (Ji, Natarajan, Vidick, Wright, Yuen, +"Quantum soundness of the classical low individual degree test", +arXiv:2009.12982), the central technical ingredient of MIP* = RE. + +This file imports **only Mathlib** and re-declares, verbatim and in dependency +order, every definition in the transitive closure of the statement of +`mainFormal`; the theorem itself is stated with `sorry`. It is the entire +human audit surface: a reader who agrees that this file states the intended +theorem does not need to read anything else. The +[comparator](https://github.com/leanprover/comparator) tool verifies +mechanically that the [MIPStarRE](https://github.com/LionSR/MIPStarRE) +library declares statements identical to these and proves the theorem using +no axioms beyond `propext`, `Quot.sound`, and `Classical.choice`. + +Each declaration carries a provenance comment (`-- source: :`) +pointing at its origin in the MIPStarRE library, where docstrings cite the +paper passages being encoded. This file is generated by +`scripts/comparator/` in that repository; see the README alongside this file +for how to run the verification. +-/ + +open scoped BigOperators MatrixOrder Matrix ComplexOrder +-- Compiler-generated declarations in the closure (no source +-- range); they regenerate identically during elaboration: +-- MIPStarRE.LDT.DiagonalLinePolynomial.mk.congr_simp (from MIPStarRE/LDT/Basic/LinePolynomials.lean) +-- MIPStarRE.LDT.AxisLinePolynomial.mk.congr_simp (from MIPStarRE/LDT/Basic/LinePolynomials.lean) +namespace MIPStarRE.LDT + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:18-18 (MIPStarRE.LDT.Error) +abbrev Error := ℝ + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:32-46 (MIPStarRE.LDT.Parameters) +/-- Parameters for the `(m,q,d)` low individual degree test. + +Besides the usual positivity assumptions, we bundle the paper-faithful witness +that `q = p^n` is a prime power. -/ +structure Parameters where + m : ℕ + q : ℕ + d : ℕ + hm : 0 < m + /-- Kept as a compatibility field so existing positivity proofs can continue + to use `params.hq`; it is derivable from `hqPrimePower`. -/ + hq : 0 < q + /-- Paper-faithful witness that `q` is a prime power. -/ + hqPrimePower : ∃ p n, Nat.Prime p ∧ 0 < n ∧ q = p ^ n + deriving DecidableEq +end MIPStarRE.LDT +namespace MIPStarRE.Quantum + +-- source: MIPStarRE/Quantum/FiniteMatrix/Basic.lean:78-79 (MIPStarRE.Quantum.Op) +/-- Square complex matrices as the finite-dimensional operator algebra. -/ +abbrev Op (d : Type*) := Matrix d d ℂ +end MIPStarRE.Quantum +namespace MIPStarRE.LDT + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:169-169 (MIPStarRE.LDT.Fq) +abbrev Fq (params : Parameters) := Fin params.q + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:170-170 (MIPStarRE.LDT.Point) +abbrev Point (params : Parameters) := Fin params.m → Fq params + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:173-174 (MIPStarRE.LDT.instInhabitedFinM) +instance {params : Parameters} : Inhabited (Fin params.m) := + ⟨⟨0, params.hm⟩⟩ + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:176-177 (MIPStarRE.LDT.instInhabitedFq) +instance {params : Parameters} : Inhabited (Fq params) := + ⟨⟨0, params.hq⟩⟩ + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:209-216 (MIPStarRE.LDT.FieldModel) +/-- A bundled field model for the paper's `F_q`, together with a coding equivalence +to the repository's finite carrier `Fin q`. -/ +class FieldModel (q : ℕ) where + K : Type* + instField : Field K + instFintype : Fintype K + instDecidableEq : DecidableEq K + equiv : K ≃ Fin q + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean (attribute command) +attribute [instance_reducible, instance] FieldModel.instField FieldModel.instFintype + FieldModel.instDecidableEq + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:276-276 (MIPStarRE.LDT.Scalar) +abbrev Scalar (params : Parameters) [FieldModel params.q] := FieldModel.K params.q + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:277-278 (MIPStarRE.LDT.PolynomialModel) +abbrev PolynomialModel (params : Parameters) [FieldModel params.q] := + MvPolynomial (Fin params.m) (Scalar params) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:279-280 (MIPStarRE.LDT.LinePolynomialModel) +abbrev LinePolynomialModel (params : Parameters) [FieldModel params.q] := + _root_.Polynomial (Scalar params) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:288-290 (MIPStarRE.LDT.decodeScalar) +/-- Interpret a coded coordinate in `Fin q` as a scalar in the chosen field model. -/ +def decodeScalar {params : Parameters} [FieldModel params.q] (x : Fq params) : Scalar params := + (FieldModel.equiv (q := params.q)).symm x + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:292-294 (MIPStarRE.LDT.encodeScalar) +/-- Re-encode a field-model scalar as its canonical representative in `Fin q`. -/ +def encodeScalar {params : Parameters} [FieldModel params.q] (x : Scalar params) : Fq params := + FieldModel.equiv (q := params.q) x + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:296-298 (MIPStarRE.LDT.encode_decodeScalar) +@[simp] theorem encode_decodeScalar {params : Parameters} [FieldModel params.q] (x : Fq params) : + encodeScalar (decodeScalar x) = x := by + simp [encodeScalar, decodeScalar] + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:300-303 (MIPStarRE.LDT.decode_encodeScalar) +@[simp] theorem decode_encodeScalar {params : Parameters} [FieldModel params.q] + (x : Scalar params) : + decodeScalar (encodeScalar x) = x := by + simp [encodeScalar, decodeScalar] + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:305-307 (MIPStarRE.LDT.zeroCoord) +/-- The zero coordinate. -/ +def zeroCoord {params : Parameters} [FieldModel params.q] : Fq params := + encodeScalar 0 + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:309-311 (MIPStarRE.LDT.addCoord) +/-- Coordinate addition transported through the `Fin q` coding. -/ +def addCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params := + encodeScalar (decodeScalar x + decodeScalar y) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:313-315 (MIPStarRE.LDT.subCoord) +/-- Coordinate subtraction transported through the `Fin q` coding. -/ +def subCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params := + encodeScalar (decodeScalar x - decodeScalar y) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:317-322 (MIPStarRE.LDT.addCoord_subCoord_right) +@[simp] theorem addCoord_subCoord_right {params : Parameters} [FieldModel params.q] + (x y : Fq params) : + addCoord y (subCoord x y) = x := by + unfold addCoord subCoord + rw [decode_encodeScalar] + simp [sub_eq_add_neg] + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:324-329 (MIPStarRE.LDT.addCoord_subCoord_left) +@[simp] theorem addCoord_subCoord_left {params : Parameters} [FieldModel params.q] + (x y : Fq params) : + addCoord (subCoord x y) y = x := by + unfold addCoord subCoord + rw [decode_encodeScalar] + simp [sub_eq_add_neg] + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:338-340 (MIPStarRE.LDT.mulCoord) +/-- Coordinate multiplication transported through the `Fin q` coding. -/ +def mulCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params := + encodeScalar (decodeScalar x * decodeScalar y) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:346-348 (MIPStarRE.LDT.addPoint) +/-- Pointwise addition in the coded ambient space. -/ +def addPoint {params : Parameters} [FieldModel params.q] (u v : Point params) : Point params := + fun i => addCoord (u i) (v i) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:350-353 (MIPStarRE.LDT.smulPoint) +/-- Scalar multiplication in the coded ambient space. -/ +def smulPoint {params : Parameters} [FieldModel params.q] (t : Fq params) (u : Point params) : + Point params := + fun i => mulCoord t (u i) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:405-408 (MIPStarRE.LDT.decodePoint) +/-- Decode a coded point as a tuple of scalars in the chosen field model. -/ +def decodePoint {params : Parameters} [FieldModel params.q] (u : Point params) : + Fin params.m → Scalar params := + fun i => decodeScalar (u i) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:410-413 (MIPStarRE.LDT.evalPolynomialModel) +/-- Evaluate a multivariate polynomial over the chosen field model on a coded point. -/ +noncomputable def evalPolynomialModel (params : Parameters) [FieldModel params.q] + (p : PolynomialModel params) (u : Point params) : Fq params := + encodeScalar (MvPolynomial.eval (decodePoint u) p) + +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:415-418 (MIPStarRE.LDT.evalLinePolynomialModel) +/-- Evaluate a univariate polynomial over the chosen field model on a coded point. -/ +noncomputable def evalLinePolynomialModel (params : Parameters) [FieldModel params.q] + (p : LinePolynomialModel params) (t : Fq params) : Fq params := + encodeScalar (_root_.Polynomial.eval (decodeScalar t) p) + +-- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:18-22 (MIPStarRE.LDT.AxisParallelLine) +/-- A genuinely axis-parallel affine line in `F_q^m`. -/ +structure AxisParallelLine (params : Parameters) where + base : Point params + direction : Fin params.m + deriving DecidableEq, Inhabited +end MIPStarRE.LDT +namespace MIPStarRE.Quantum + +-- elaboration context of MIPStarRE/Quantum/FiniteMatrix/NormalizedTrace.lean +section +open scoped Matrix.Norms.Elementwise +open WithLp +variable {d : Type*} [Fintype d] + +-- source: MIPStarRE/Quantum/FiniteMatrix/NormalizedTrace.lean:20-22 (MIPStarRE.Quantum.normalizedTrace) +/-- The normalized trace `τ(A) = tr(A) / |d|`. -/ +noncomputable def normalizedTrace (A : Op d) : ℂ := + A.trace / (Fintype.card d : ℂ) +end -- module scope +end MIPStarRE.Quantum +namespace MIPStarRE.LDT +namespace AxisParallelLine + +-- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:26-33 (MIPStarRE.LDT.AxisParallelLine.pointAt) +/-- The canonical affine parameterization `t ↦ base + t e_i`. -/ +def pointAt {params : Parameters} [FieldModel params.q] + (ℓ : AxisParallelLine params) : Fq params → Point params := + fun t i => + if i = ℓ.direction then + addCoord (ℓ.base i) t + else + ℓ.base i + +-- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:50-55 (MIPStarRE.LDT.AxisParallelLine.rebaseAt) +/-- Rebase an axis-parallel line so that the old point `ℓ.pointAt t` +becomes the new base point. -/ +def rebaseAt {params : Parameters} [FieldModel params.q] + (ℓ : AxisParallelLine params) (t : Fq params) : AxisParallelLine params where + base := ℓ.pointAt t + direction := ℓ.direction +end AxisParallelLine + +-- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:16-20 (MIPStarRE.LDT.DiagonalLine) +/-- A genuinely affine diagonal line in `F_q^m`. -/ +structure DiagonalLine (params : Parameters) where + base : Point params + direction : Point params + deriving DecidableEq, Inhabited +namespace DiagonalLine + +-- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:24-27 (MIPStarRE.LDT.DiagonalLine.pointAt) +/-- The canonical affine parameterization `t ↦ base + t · direction`. -/ +def pointAt {params : Parameters} [FieldModel params.q] + (ℓ : DiagonalLine params) : Fq params → Point params := + fun t => addPoint ℓ.base (smulPoint t ℓ.direction) +end DiagonalLine +namespace Test + +-- source: MIPStarRE/LDT/Test/MainTheorem/ScalarBounds/Definitions.lean:28-36 (MIPStarRE.LDT.Test.mainFormalError) +/-- The formal final error envelope for `thm:main-formal`. + +The sharper pre-completion line-169 repair keeps the point-transport scale at +the original `1/40000` exponent used by the surrounding Step 8 cascade. -/ +noncomputable def mainFormalError (params : Parameters) (k : ℕ) (eps : Error) : Error := + 100000 * ((k : Error) ^ (2 : ℕ)) * ((params.m : Error) ^ (4 : ℕ)) * + (Real.rpow eps (1 / (40000 : Error)) + + Real.rpow (((params.d : Error) / (params.q : Error))) (1 / (40000 : Error)) + + Real.exp (-((k : Error) / (2560000 * ((params.m : Error) ^ (2 : ℕ)))))) +end Test +namespace DiagonalLine + +-- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:99-103 (MIPStarRE.LDT.DiagonalLine.rebaseAt) +/-- Rebase a diagonal line so that the old point `ℓ.pointAt t` becomes the new base point. -/ +def rebaseAt {params : Parameters} [FieldModel params.q] + (ℓ : DiagonalLine params) (t : Fq params) : DiagonalLine params where + base := ℓ.pointAt t + direction := ℓ.direction +end DiagonalLine + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:33-41 (MIPStarRE.LDT.natDegree_comp_C_add_X_le) +/-- Composing with the degree-one translation `C a + X` preserves `natDegree` +bounds. Shared degree bookkeeping for the `reparamAt` reparametrizations +below. -/ +theorem natDegree_comp_C_add_X_le {params : Parameters} [FieldModel params.q] + (p : LinePolynomialModel params) (a : Scalar params) {n : ℕ} + (hp : p.natDegree ≤ n) : + (p.comp (_root_.Polynomial.C a + _root_.Polynomial.X)).natDegree ≤ n := + le_trans (_root_.Polynomial.natDegree_comp_le) + (by rw [add_comm, _root_.Polynomial.natDegree_X_add_C, Nat.mul_one]; exact hp) + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:43-46 (MIPStarRE.LDT.AxisLinePolynomial) +/-- Axis-parallel line answers are genuine univariate degree-`d` polynomials. -/ +structure AxisLinePolynomial (params : Parameters) [FieldModel params.q] where + poly : LinePolynomialModel params + degreeBounded : poly.natDegree ≤ params.d +namespace AxisLinePolynomial + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:55-58 (MIPStarRE.LDT.AxisLinePolynomial.toFun) +/-- Evaluation of an axis-line answer on the line parameter. -/ +noncomputable def toFun {params : Parameters} [FieldModel params.q] + (f : AxisLinePolynomial params) : Fq params → Fq params := + evalLinePolynomialModel params f.poly + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean (elaboration context) +noncomputable instance {params : Parameters} [FieldModel params.q] : + CoeFun (AxisLinePolynomial params) (fun _ => Fq params → Fq params) := + ⟨AxisLinePolynomial.toFun⟩ + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:86-93 (MIPStarRE.LDT.AxisLinePolynomial.ext) +@[ext] theorem ext {params : Parameters} [FieldModel params.q] + {f g : AxisLinePolynomial params} (hpoly : f.poly = g.poly) : f = g := by + cases f with + | mk polyf hpolyf => + cases g with + | mk polyg hpolyg => + cases hpoly + congr + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:95-99 (MIPStarRE.LDT.AxisLinePolynomial.reparamAt) +/-- Reparametrize an axis-line answer by translating the line parameter. -/ +noncomputable def reparamAt {params : Parameters} [FieldModel params.q] + (f : AxisLinePolynomial params) (t : Fq params) : AxisLinePolynomial params where + poly := f.poly.comp (_root_.Polynomial.C (decodeScalar t) + _root_.Polynomial.X) + degreeBounded := natDegree_comp_C_add_X_le f.poly (decodeScalar t) f.degreeBounded + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:111-115 (MIPStarRE.LDT.AxisLinePolynomial.reparamAt_zero) +@[simp] theorem reparamAt_zero {params : Parameters} [FieldModel params.q] + (f : AxisLinePolynomial params) : + reparamAt f zeroCoord = f := by + refine AxisLinePolynomial.ext ?_ + simp [reparamAt, zeroCoord] + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:127-136 (MIPStarRE.LDT.AxisLinePolynomial.reparamAt_reparamAt) +theorem reparamAt_reparamAt {params : Parameters} [FieldModel params.q] + (f : AxisLinePolynomial params) (t s : Fq params) : + reparamAt (reparamAt f t) s = reparamAt f (addCoord t s) := by + refine AxisLinePolynomial.ext ?_ + change + (f.poly.comp (_root_.Polynomial.C (decodeScalar t) + _root_.Polynomial.X)).comp + (_root_.Polynomial.C (decodeScalar s) + _root_.Polynomial.X) = + f.poly.comp (_root_.Polynomial.C (decodeScalar (addCoord t s)) + _root_.Polynomial.X) + rw [_root_.Polynomial.comp_assoc] + simp [addCoord, add_left_comm, add_comm] + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:138-146 (MIPStarRE.LDT.AxisLinePolynomial.reparamAtEquiv) +/-- Reparametrization by translation is an equivalence on axis-line answers. -/ +noncomputable def reparamAtEquiv {params : Parameters} [FieldModel params.q] + (t : Fq params) : AxisLinePolynomial params ≃ AxisLinePolynomial params where + toFun := fun f => reparamAt f t + invFun := fun f => reparamAt f (subCoord zeroCoord t) + left_inv := fun f => (reparamAt_reparamAt f t (subCoord zeroCoord t)).trans + ((congrArg (reparamAt f) (addCoord_subCoord_right zeroCoord t)).trans (reparamAt_zero f)) + right_inv := fun f => (reparamAt_reparamAt f (subCoord zeroCoord t) t).trans + ((congrArg (reparamAt f) (addCoord_subCoord_left zeroCoord t)).trans (reparamAt_zero f)) +end AxisLinePolynomial + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:194-197 (MIPStarRE.LDT.DiagonalLinePolynomial) +/-- Diagonal-line answers are genuine univariate degree-`md` polynomials. -/ +structure DiagonalLinePolynomial (params : Parameters) [FieldModel params.q] where + poly : LinePolynomialModel params + degreeBounded : poly.natDegree ≤ params.m * params.d +namespace DiagonalLinePolynomial + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:206-209 (MIPStarRE.LDT.DiagonalLinePolynomial.toFun) +/-- Evaluation of a diagonal-line answer on the line parameter. -/ +noncomputable def toFun {params : Parameters} [FieldModel params.q] + (f : DiagonalLinePolynomial params) : Fq params → Fq params := + evalLinePolynomialModel params f.poly + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean (elaboration context) +noncomputable instance {params : Parameters} [FieldModel params.q] : + CoeFun (DiagonalLinePolynomial params) (fun _ => Fq params → Fq params) := + ⟨DiagonalLinePolynomial.toFun⟩ + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:215-222 (MIPStarRE.LDT.DiagonalLinePolynomial.ext) +@[ext] theorem ext {params : Parameters} [FieldModel params.q] + {f g : DiagonalLinePolynomial params} (hpoly : f.poly = g.poly) : f = g := by + cases f with + | mk polyf hpolyf => + cases g with + | mk polyg hpolyg => + cases hpoly + congr + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:224-240 (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt) +/-- Reparametrize a diagonal-line answer by translating the line parameter. + +Concretely, the underlying univariate polynomial `f.poly` (over `Scalar params` in +the chosen field model) is precomposed with `X + C (decodeScalar t)`, i.e. the +coefficients are shifted using genuine *field* addition on `Scalar params` — not +the `Fin q` arithmetic on `Fq params`. Transporting back through `encodeScalar` +gives the answer-level identity `reparamAt f t s = f (addCoord t s)` (see +`reparamAt_apply`), where `addCoord` is field addition lifted through the coding +`FieldModel.equiv`. Composition with a degree-one polynomial preserves the +`natDegree ≤ params.m * params.d` bound. + +This is the answer-level geometric fact behind rebasing a diagonal line at +parameter `t`: the old parameter `addCoord t s` becomes the new parameter `s`. -/ +noncomputable def reparamAt {params : Parameters} [FieldModel params.q] + (f : DiagonalLinePolynomial params) (t : Fq params) : DiagonalLinePolynomial params where + poly := f.poly.comp (_root_.Polynomial.C (decodeScalar t) + _root_.Polynomial.X) + degreeBounded := natDegree_comp_C_add_X_le f.poly (decodeScalar t) f.degreeBounded + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:252-256 (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_zero) +@[simp] theorem reparamAt_zero {params : Parameters} [FieldModel params.q] + (f : DiagonalLinePolynomial params) : + reparamAt f zeroCoord = f := by + refine DiagonalLinePolynomial.ext ?_ + simp [reparamAt, zeroCoord] + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:268-277 (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_reparamAt) +theorem reparamAt_reparamAt {params : Parameters} [FieldModel params.q] + (f : DiagonalLinePolynomial params) (t s : Fq params) : + reparamAt (reparamAt f t) s = reparamAt f (addCoord t s) := by + refine DiagonalLinePolynomial.ext ?_ + change + (f.poly.comp (_root_.Polynomial.C (decodeScalar t) + _root_.Polynomial.X)).comp + (_root_.Polynomial.C (decodeScalar s) + _root_.Polynomial.X) = + f.poly.comp (_root_.Polynomial.C (decodeScalar (addCoord t s)) + _root_.Polynomial.X) + rw [_root_.Polynomial.comp_assoc] + simp [addCoord, add_left_comm, add_comm] + +-- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:279-287 (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAtEquiv) +/-- Reparametrization by translation is an equivalence on diagonal-line answers. -/ +noncomputable def reparamAtEquiv {params : Parameters} [FieldModel params.q] + (t : Fq params) : DiagonalLinePolynomial params ≃ DiagonalLinePolynomial params where + toFun := fun f => reparamAt f t + invFun := fun f => reparamAt f (subCoord zeroCoord t) + left_inv := fun f => (reparamAt_reparamAt f t (subCoord zeroCoord t)).trans + ((congrArg (reparamAt f) (addCoord_subCoord_right zeroCoord t)).trans (reparamAt_zero f)) + right_inv := fun f => (reparamAt_reparamAt f (subCoord zeroCoord t) t).trans + ((congrArg (reparamAt f) (addCoord_subCoord_left zeroCoord t)).trans (reparamAt_zero f)) +end DiagonalLinePolynomial + +-- source: MIPStarRE/LDT/Basic/QuantumState.lean:14-27 (MIPStarRE.LDT.QuantumState) +/-- A PSD density matrix indexed by `ι`. + +There is intentionally no global `Inhabited` instance: the zero matrix is PSD but +not a physical state of unit trace, so an ambient default would silently +trivialize later statements. Use `IsNormalized` to additionally require +`τ(ρ) = 1`. + +This remains the ambient state space for the current LDT development: strategy +packages in `LDT/Test/StrategyCore.lean`, the SWAP-symmetry API `PermInvState`, +and the expectation-value lemmas in `LDT/Basic/OperatorExpectations.lean` are all +stated for arbitrary density matrices, not only pure states. -/ +structure QuantumState (ι : Type*) [Fintype ι] [DecidableEq ι] where + density : MIPStarRE.Quantum.Op ι := 0 + density_psd : 0 ≤ density := by positivity + +-- source: MIPStarRE/LDT/Basic/LowDegreePolynomial.lean:17-20 (MIPStarRE.LDT.Polynomial) +/-- Global low-individual-degree polynomial outcomes. -/ +structure Polynomial (params : Parameters) [FieldModel params.q] where + poly : PolynomialModel params + lowIndividualDegree : ∀ i, MvPolynomial.degreeOf i poly ≤ params.d + +-- source: MIPStarRE/LDT/Basic/Distribution.lean:22-27 (MIPStarRE.LDT.Distribution) +/-- A finite-support weighted distribution with nonnegative real-valued weights. -/ +structure Distribution (α : Type*) where + support : Finset α := ∅ + weight : α → Error := fun _ => 0 + nonnegative : ∀ a, 0 ≤ weight a := by intro _; positivity + outsideSupport : ∀ a, a ∉ support → weight a = 0 := by intro _ _; rfl + +-- source: MIPStarRE/LDT/Basic/QuantumState.lean:29-32 (MIPStarRE.LDT.QuantumState.IsNormalized) +/-- Unit normalized trace for the concrete matrix carried by a state. -/ +def QuantumState.IsNormalized {ι : Type*} [Fintype ι] [DecidableEq ι] + (ψ : QuantumState ι) : Prop := + MIPStarRE.Quantum.normalizedTrace ψ.density = 1 +namespace Polynomial + +-- source: MIPStarRE/LDT/Basic/LowDegreePolynomial.lean:36-39 (MIPStarRE.LDT.Polynomial.toFun) +/-- Evaluation of the stored multivariate polynomial on a coded point. -/ +noncomputable def toFun {params : Parameters} [FieldModel params.q] (g : Polynomial params) : + Point params → Fq params := + evalPolynomialModel params g.poly + +-- source: MIPStarRE/LDT/Basic/LowDegreePolynomial.lean (elaboration context) +noncomputable instance {params : Parameters} [FieldModel params.q] : + CoeFun (Polynomial params) (fun _ => Point params → Fq params) := + ⟨Polynomial.toFun⟩ +end Polynomial + +-- source: MIPStarRE/LDT/Basic/QuantumState.lean:168-171 (MIPStarRE.LDT.ev) +/-- The expectation `Re τ(ψ X)`. Dimensions match by construction. -/ +noncomputable def ev {ι : Type*} [Fintype ι] [DecidableEq ι] + (ψ : QuantumState ι) (X : MIPStarRE.Quantum.Op ι) : Error := + Complex.re <| MIPStarRE.Quantum.normalizedTrace (ψ.density * X) + +-- source: MIPStarRE/LDT/Basic/QuantumState.lean:180-184 (MIPStarRE.LDT.opTensor) +/-- Tensor product of two operators via Kronecker product. -/ +abbrev opTensor {ι₁ ι₂ : Type*} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] + (A : MIPStarRE.Quantum.Op ι₁) (B : MIPStarRE.Quantum.Op ι₂) : + MIPStarRE.Quantum.Op (ι₁ × ι₂) := + Matrix.kronecker A B + +-- source: MIPStarRE/LDT/Basic/Distribution.lean:224-226 (MIPStarRE.LDT.avgOver) +/-- Average a scalar function against the stored finite support of a distribution. -/ +def avgOver {α : Type*} (𝒟 : Distribution α) (f : α → Error) : Error := + ∑ a ∈ 𝒟.support, 𝒟.weight a * f a +namespace Distribution + +-- source: MIPStarRE/LDT/Basic/Distribution.lean:412-430 (MIPStarRE.LDT.Distribution.uniformOnFinset) +/-- The uniform distribution on a specified finite support. + +The stored support is `s`, and the weight of a point is the elementary finite +uniform weight `1 / s.card` on `s` and `0` off `s`. When the support is empty +this gives the zero sub-probability distribution, matching the convention used +for degenerate filtered supports in the LDT development. -/ +noncomputable def uniformOnFinset {α : Type*} (s : Finset α) : Distribution α := by + classical + exact + { support := s + weight := fun a => if a ∈ s then 1 / (s.card : Error) else 0 + nonnegative := by + intro a + by_cases ha : a ∈ s + · simp [ha] + · simp [ha] + outsideSupport := by + intro a ha + simp [ha] } +end Distribution + +-- source: MIPStarRE/LDT/Basic/Distribution.lean:492-495 (MIPStarRE.LDT.uniformDistribution) +/-- The uniform distribution on a nonempty finite type. -/ +noncomputable def uniformDistribution (α : Type*) + [Fintype α] [DecidableEq α] [Nonempty α] : Distribution α := + Distribution.uniformOnFinset Finset.univ + +-- source: MIPStarRE/LDT/Basic/SubMeasurementCore.lean:13-23 (MIPStarRE.LDT.SubMeas) +/-- A paper-local submeasurement with outcomes in `α` and Hilbert space index `ι`. + +There is intentionally no global `Inhabited` instance: the zero family satisfies +these raw axioms, but using it as an ambient default would silently turn later +arguments into vacuous submeasurement statements. -/ +structure SubMeas (α : Type*) [Fintype α] (ι : Type*) [Fintype ι] [DecidableEq ι] where + outcome : α → MIPStarRE.Quantum.Op ι := fun _ => 0 + total : MIPStarRE.Quantum.Op ι := 0 + outcome_pos : ∀ a, 0 ≤ outcome a + sum_eq_total : ∑ a, outcome a = total + total_le_one : total ≤ 1 + +-- source: MIPStarRE/LDT/Basic/SubMeasurementCore.lean:25-28 (MIPStarRE.LDT.Measurement) +/-- A paper-local measurement: a POVM whose PSD effects sum to the identity. -/ +structure Measurement (α : Type*) (ι : Type*) [Fintype α] [Fintype ι] [DecidableEq ι] + extends SubMeas α ι where + total_eq_one : total = 1 + +-- source: MIPStarRE/LDT/Basic/ParametersFiniteAnswers.lean:28-39 (MIPStarRE.LDT.linePolynomial_coeff_fin_injective) +/-- A univariate polynomial of `natDegree ≤ n` is determined by its first +`n + 1` coefficients. Shared injectivity fact behind the finite-answer-space +instances below. -/ +theorem linePolynomial_coeff_fin_injective (params : Parameters) [FieldModel params.q] + {n : ℕ} {p q : LinePolynomialModel params} + (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) + (h : ∀ i : Fin (n + 1), p.coeff i = q.coeff i) : p = q := by + ext k + by_cases hk : k < n + 1 + · exact h ⟨k, hk⟩ + · rw [p.coeff_eq_zero_of_natDegree_lt (hp.trans_lt (by omega)), + q.coeff_eq_zero_of_natDegree_lt (hq.trans_lt (by omega))] + +-- source: MIPStarRE/LDT/Basic/ParametersFiniteAnswers.lean:41-49 (MIPStarRE.LDT.instFintypeAxisLinePolynomial) +/-- Axis-line polynomial answers form a finite type via their bounded coefficient vectors. -/ +noncomputable instance (params : Parameters) [FieldModel params.q] : + Fintype (AxisLinePolynomial params) := by + classical + exact Fintype.ofInjective + (fun f : AxisLinePolynomial params => fun i : Fin (params.d + 1) => f.poly.coeff i) + fun f g h => AxisLinePolynomial.ext + (linePolynomial_coeff_fin_injective params f.degreeBounded g.degreeBounded + fun i => congrFun h i) + +-- source: MIPStarRE/LDT/Basic/ParametersFiniteAnswers.lean:51-60 (MIPStarRE.LDT.instFintypeDiagonalLinePolynomial) +/-- Diagonal-line polynomial answers form a finite type via their bounded coefficient vectors. -/ +noncomputable instance (params : Parameters) [FieldModel params.q] : + Fintype (DiagonalLinePolynomial params) := by + classical + exact Fintype.ofInjective + (fun f : DiagonalLinePolynomial params => + fun i : Fin (params.m * params.d + 1) => f.poly.coeff i) + fun f g h => DiagonalLinePolynomial.ext + (linePolynomial_coeff_fin_injective params f.degreeBounded g.degreeBounded + fun i => congrFun h i) + +-- source: MIPStarRE/LDT/Basic/ParametersFiniteAnswers.lean:62-79 (MIPStarRE.LDT.instFintypePolynomial) +/-- Global low-individual-degree polynomial answers form a finite type, by +injecting into the finite space of degree-restricted multivariate polynomials. -/ +noncomputable instance (params : Parameters) [FieldModel params.q] : + Fintype (Polynomial params) := by + classical + letI : Finite (MvPolynomial.restrictDegree (Fin params.m) (Scalar params) params.d) := + Module.finite_of_finite (Scalar params) + letI : Fintype (MvPolynomial.restrictDegree (Fin params.m) (Scalar params) params.d) := + Fintype.ofFinite _ + exact Fintype.ofInjective + (fun g : Polynomial params => + (⟨g.poly, by + rw [MvPolynomial.mem_restrictDegree_iff_sup] + simpa [MvPolynomial.degreeOf_def] using g.lowIndividualDegree⟩ : + MvPolynomial.restrictDegree (Fin params.m) (Scalar params) params.d)) + fun g g' h => by + cases g; cases g' + simpa using congrArg Subtype.val h + +-- source: MIPStarRE/LDT/Basic/SubMeasurementCore.lean:73-76 (MIPStarRE.LDT.ProjMeas) +/-- A paper-local projective measurement (complete POVM + projective). -/ +structure ProjMeas (α : Type*) (ι : Type*) [Fintype α] [Fintype ι] [DecidableEq ι] + extends Measurement α ι where + proj : ∀ a, outcome a * outcome a = outcome a + +-- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:16-19 (MIPStarRE.LDT.IdxSubMeas) +/-- Question-indexed family of submeasurements. -/ +abbrev IdxSubMeas (Question Outcome : Type*) (ι : Type*) + [Fintype Outcome] [Fintype ι] [DecidableEq ι] := + Question → SubMeas Outcome ι + +-- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:31-34 (MIPStarRE.LDT.IdxProjMeas) +/-- Question-indexed family of projective measurements. -/ +abbrev IdxProjMeas (Question Outcome : Type*) (ι : Type*) + [Fintype Outcome] [Fintype ι] [DecidableEq ι] := + Question → ProjMeas Outcome ι +namespace IdxProjMeas + +-- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:67-72 (MIPStarRE.LDT.IdxProjMeas.toIdxSubMeas) +/-- Forget both projectivity and completeness from an indexed projective measurement family. -/ +def toIdxSubMeas {Question Outcome : Type*} {ι : Type*} + [Fintype Outcome] [Fintype ι] [DecidableEq ι] + (A : IdxProjMeas Question Outcome ι) : + IdxSubMeas Question Outcome ι := + fun q => (A q).toSubMeas +end IdxProjMeas + +-- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:76-88 (MIPStarRE.LDT.postprocess) +open scoped Classical in +/-- Post-process the outcomes of a submeasurement. The processed operator at `b` is the +sum of the operators of all `a` with `f a = b`. -/ +noncomputable def postprocess {α β : Type*} {ι : Type*} [Fintype ι] [DecidableEq ι] + [Fintype α] [Fintype β] + (A : SubMeas α ι) (f : α → β) : + SubMeas β ι where + outcome := fun b => + ∑ a ∈ Finset.univ.filter (fun a => f a = b), A.outcome a + total := A.total + outcome_pos := fun _ => Finset.sum_nonneg fun a _ => A.outcome_pos a + sum_eq_total := (Finset.sum_fiberwise Finset.univ f A.outcome).trans A.sum_eq_total + total_le_one := A.total_le_one +namespace SubMeas + +-- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:123-132 (MIPStarRE.LDT.SubMeas.transport) +/-- Transport a submeasurement along an equivalence of outcome types. -/ +noncomputable def transport {α β : Type*} {ι : Type*} + [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] + (e : α ≃ β) (A : SubMeas α ι) : + SubMeas β ι where + outcome := fun b => A.outcome (e.symm b) + total := A.total + outcome_pos := fun b => A.outcome_pos (e.symm b) + sum_eq_total := (Equiv.sum_comp e.symm A.outcome).trans A.sum_eq_total + total_le_one := A.total_le_one +end SubMeas +namespace Measurement + +-- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:272-278 (MIPStarRE.LDT.Measurement.transport) +/-- Transport a measurement along an equivalence of outcome types. -/ +noncomputable def transport {α β : Type*} {ι : Type*} + [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] + (e : α ≃ β) (A : Measurement α ι) : + Measurement β ι where + toSubMeas := SubMeas.transport e A.toSubMeas + total_eq_one := A.total_eq_one +end Measurement +namespace ProjMeas + +-- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:328-334 (MIPStarRE.LDT.ProjMeas.transport) +/-- Transport a projective measurement along an equivalence of outcome types. -/ +noncomputable def transport {α β : Type*} {ι : Type*} + [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] + (e : α ≃ β) (A : ProjMeas α ι) : + ProjMeas β ι where + toMeasurement := Measurement.transport e A.toMeasurement + proj := fun b => A.proj (e.symm b) +end ProjMeas + +-- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:420-424 (MIPStarRE.LDT.constSubMeasFamily) +/-- Constant indexed family taking the same submeasurement on every question. -/ +def constSubMeasFamily {α : Type*} {ι : Type*} [Fintype α] [Fintype ι] [DecidableEq ι] + (A : SubMeas α ι) : + IdxSubMeas Unit α ι := + fun _ => A + +-- source: MIPStarRE/LDT/Test/Defs.lean:18-22 (MIPStarRE.LDT.evaluateAt) +/-- Evaluate a polynomial-valued submeasurement at a point. -/ +noncomputable def evaluateAt {ι : Type*} [Fintype ι] [DecidableEq ι] + (params : Parameters) [FieldModel params.q] (u : Point params) + (G : SubMeas (Polynomial params) ι) : SubMeas (Fq params) ι := + postprocess G (fun g => g u) + +-- source: MIPStarRE/LDT/Test/Defs.lean:40-45 (MIPStarRE.LDT.polynomialEvaluationFamily) +/-- View a global polynomial submeasurement as a point-indexed answer family. -/ +noncomputable def polynomialEvaluationFamily {ι : Type*} [Fintype ι] [DecidableEq ι] + (params : Parameters) [FieldModel params.q] + (G : SubMeas (Polynomial params) ι) : + IdxSubMeas (Point params) (Fq params) ι := + fun u => evaluateAt params u G + +-- source: MIPStarRE/LDT/Test/Defs.lean:176-183 (MIPStarRE.LDT.qBipartiteMatchMass) +/-- Bipartite matching mass `∑_a ⟨ψ, (A_a ⊗ B_a) ψ⟩`, with `A` on the left +register and `B` on the right register of a tensor-product state. -/ +noncomputable def qBipartiteMatchMass {Outcome : Type*} + {ιA ιB : Type*} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] + [Fintype Outcome] + (ψ : QuantumState (ιA × ιB)) + (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : Error := + ∑ a, ev ψ (opTensor (A.outcome a) (B.outcome a)) + +-- source: MIPStarRE/LDT/Test/Defs.lean:185-198 (MIPStarRE.LDT.qBipartiteConsDefect) +/-- Bipartite questionwise consistency defect. + +In the paper (Definition 4.8), the consistency of `A` on `H_A` and `B` on +`H_B` for a shared state `|ψ⟩ ∈ H_A ⊗ H_B` is: + `E_x ∑_{a≠b} ⟨ψ| A^x_a ⊗ B^x_b |ψ⟩ ≤ δ` +which equals + `max 0 (⟨ψ| A_total ⊗ B_total |ψ⟩ − ∑_a ⟨ψ| A_a ⊗ B_a |ψ⟩)`. -/ +noncomputable def qBipartiteConsDefect {Outcome : Type*} + {ιA ιB : Type*} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] + [Fintype Outcome] + (ψ : QuantumState (ιA × ιB)) + (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : Error := + let totalOverlap := ev ψ (opTensor A.total B.total) + max 0 (totalOverlap - qBipartiteMatchMass ψ A B) + +-- source: MIPStarRE/LDT/Test/Defs.lean:200-207 (MIPStarRE.LDT.bipartiteConsError) +/-- Averaged bipartite off-diagonal mass for consistency statements. -/ +noncomputable def bipartiteConsError {Question Outcome : Type*} + {ιA ιB : Type*} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] + [Fintype Outcome] + (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) + (A : IdxSubMeas Question Outcome ιA) + (B : IdxSubMeas Question Outcome ιB) : Error := + avgOver 𝒟 (fun q => qBipartiteConsDefect ψ (A q) (B q)) + +-- source: MIPStarRE/LDT/Test/Defs.lean:239-251 (MIPStarRE.LDT.ConsRel) +/-- Consistency relation (bipartite, paper Definition 4.8). + +The state `ψ` lives on `H_A ⊗ H_B`, Alice's submeasurement `A` acts on +`H_A`, and Bob's submeasurement `B` acts on `H_B`. The relation encodes + `E_{x ∼ D} ∑_{a≠b} ⟨ψ| A^x_a ⊗ B^x_b |ψ⟩ ≤ δ`. -/ +structure ConsRel {Question Outcome : Type*} + {ιA ιB : Type*} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] + [Fintype Outcome] + (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) + (A : IdxSubMeas Question Outcome ιA) + (B : IdxSubMeas Question Outcome ιB) + (δ : Error) : Prop where + offDiagonalBound : bipartiteConsError ψ 𝒟 A B ≤ δ +namespace AxisParallelLine + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:189-195 (MIPStarRE.LDT.AxisParallelLine.transportMeasurement) +/-- Transport an axis-parallel-line measurement along rebasing of the line +question by translating its polynomial outcomes. -/ +noncomputable def transportMeasurement {params : Parameters} [FieldModel params.q] + {ι : Type*} [Fintype ι] [DecidableEq ι] + (M : ProjMeas (AxisLinePolynomial params) ι) (t : Fq params) : + ProjMeas (AxisLinePolynomial params) ι := + ProjMeas.transport (AxisLinePolynomial.reparamAtEquiv (params := params) t) M +end AxisParallelLine +namespace DiagonalLine + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:219-225 (MIPStarRE.LDT.DiagonalLine.transportMeasurement) +/-- Transport a diagonal-line measurement along rebasing of the line question by +translating its polynomial outcomes. -/ +noncomputable def transportMeasurement {params : Parameters} [FieldModel params.q] + {ι : Type*} [Fintype ι] [DecidableEq ι] + (M : ProjMeas (DiagonalLinePolynomial params) ι) (t : Fq params) : + ProjMeas (DiagonalLinePolynomial params) ι := + ProjMeas.transport (DiagonalLinePolynomial.reparamAtEquiv (params := params) t) M +end DiagonalLine + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:247-255 (MIPStarRE.LDT.AxisParallelMeasurementTransportInvariant) +/-- 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. -/ +def AxisParallelMeasurementTransportInvariant (params : Parameters) + [FieldModel params.q] {ι : Type*} [Fintype ι] [DecidableEq ι] + (M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι) : Prop := + ∀ (ℓ : AxisParallelLine params) (t : Fq params), + M (AxisParallelLine.rebaseAt ℓ t) = + AxisParallelLine.transportMeasurement (params := params) (M ℓ) t + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:257-265 (MIPStarRE.LDT.DiagonalMeasurementTransportInvariant) +/-- 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. -/ +def DiagonalMeasurementTransportInvariant (params : Parameters) + [FieldModel params.q] {ι : Type*} [Fintype ι] [DecidableEq ι] + (M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι) : Prop := + ∀ (ℓ : DiagonalLine params) (t : Fq params), + M (DiagonalLine.rebaseAt ℓ t) = + DiagonalLine.transportMeasurement (params := params) (M ℓ) t + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:291-298 (MIPStarRE.LDT.AxisParallelCovariantMeasurement) +/-- Axis-parallel line measurements bundled with the stronger transport-level +rebasing covariance. -/ +structure AxisParallelCovariantMeasurement (params : Parameters) + [FieldModel params.q] (ι : Type*) [Fintype ι] [DecidableEq ι] where + toIdxProjMeas : + IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι + transportInvariant : + AxisParallelMeasurementTransportInvariant params toIdxProjMeas + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean (elaboration context) +instance {params : Parameters} [FieldModel params.q] {ι : Type*} + [Fintype ι] [DecidableEq ι] : + CoeFun (AxisParallelCovariantMeasurement params ι) + (fun _ => AxisParallelLine params → ProjMeas (AxisLinePolynomial params) ι) where + coe M := M.toIdxProjMeas + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:318-325 (MIPStarRE.LDT.DiagonalCovariantMeasurement) +/-- Diagonal line measurements bundled with the stronger transport-level +rebasing covariance. -/ +structure DiagonalCovariantMeasurement (params : Parameters) + [FieldModel params.q] (ι : Type*) [Fintype ι] [DecidableEq ι] where + toIdxProjMeas : + IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι + transportInvariant : + DiagonalMeasurementTransportInvariant params toIdxProjMeas + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean (elaboration context) +instance {params : Parameters} [FieldModel params.q] {ι : Type*} + [Fintype ι] [DecidableEq ι] : + CoeFun (DiagonalCovariantMeasurement params ι) + (fun _ => DiagonalLine params → ProjMeas (DiagonalLinePolynomial params) ι) where + coe M := M.toIdxProjMeas + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:418-425 (MIPStarRE.LDT.AxisParallelTestSample) +/-- 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. -/ +abbrev AxisParallelTestSample (params : Parameters) := + Point params × Fin params.m + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:427-439 (MIPStarRE.LDT.extendRestrictedDirection) +/-- 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`. -/ +def extendRestrictedDirection {params : Parameters} + [FieldModel params.q] (j : Fin params.m) + (freeCoords : Fin (j.val + 1) → Fq params) : + Point params := + fun k => + if h : k.val ≤ j.val then + freeCoords ⟨k.val, Nat.lt_succ_of_le h⟩ + else zeroCoord + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:441-447 (MIPStarRE.LDT.RestrictedDiagonalSample) +/-- 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}`. -/ +abbrev RestrictedDiagonalSample (params : Parameters) + (j : Fin params.m) := + Point params × (Fin (j.val + 1) → Fq params) + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:449-452 (MIPStarRE.LDT.restrictedDiagonalSampleNonempty) +/-- The restricted diagonal sample space is nonempty. -/ +instance restrictedDiagonalSampleNonempty (params : Parameters) (j : Fin params.m) : + Nonempty (RestrictedDiagonalSample params j) := + inferInstance + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:661-688 (MIPStarRE.LDT.ProjStrat) +/-- 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`. -/ +structure ProjStrat (params : Parameters) [FieldModel params.q] + (ιA : Type*) [Fintype ιA] [DecidableEq ιA] + (ιB : Type*) [Fintype ιB] [DecidableEq ιB] where + /-- Bipartite state on the tensor product of Alice's and Bob's local carriers. -/ + state : QuantumState (ιA × ιB) + /-- The bipartite state's density operator is trace-normalized. -/ + isNormalized : state.IsNormalized + /-- Alice's point-measurement family, acting on `ιA`. -/ + pointMeasurementA : IdxProjMeas (Point params) (Fq params) ιA + /-- Alice's axis-parallel-line measurement family, acting on `ιA`. -/ + axisParallelMeasurementA : AxisParallelCovariantMeasurement params ιA + /-- Alice's diagonal-line measurement family, acting on `ιA`. -/ + diagonalMeasurementA : DiagonalCovariantMeasurement params ιA + /-- Bob's point-measurement family, acting on `ιB`. -/ + pointMeasurementB : IdxProjMeas (Point params) (Fq params) ιB + /-- Bob's axis-parallel-line measurement family, acting on `ιB`. -/ + axisParallelMeasurementB : AxisParallelCovariantMeasurement params ιB + /-- Bob's diagonal-line measurement family, acting on `ιB`. -/ + diagonalMeasurementB : DiagonalCovariantMeasurement params ιB +namespace ProjStrat + +-- elaboration context of MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean +section +open MIPStarRE.Quantum +variable {params : Parameters} [FieldModel params.q] +variable {ιA : Type*} [Fintype ιA] [DecidableEq ιA] +variable {ιB : Type*} [Fintype ιB] [DecidableEq ιB] + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:330-335 (MIPStarRE.LDT.ProjStrat.axisParallelPointAnswerFamilyA) +/-- 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}`. -/ +noncomputable def axisParallelPointAnswerFamilyA + (strategy : ProjStrat params ιA ιB) : + IdxSubMeas (AxisParallelTestSample params) (Fq params) ιA := + fun s => (strategy.pointMeasurementA s.1).toSubMeas + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:337-342 (MIPStarRE.LDT.ProjStrat.axisParallelPointAnswerFamilyB) +/-- 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}`. -/ +noncomputable def axisParallelPointAnswerFamilyB + (strategy : ProjStrat params ιA ιB) : + IdxSubMeas (AxisParallelTestSample params) (Fq params) ιB := + fun s => (strategy.pointMeasurementB s.1).toSubMeas + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:344-355 (MIPStarRE.LDT.ProjStrat.axisParallelLineAnswerFamilyA) +/-- Alice's axis-parallel-line answers: Alice receives `ℓ`, answers with +`B^{A,ℓ}`, and the verifier postprocesses to the value at the sampled base +point. -/ +noncomputable def axisParallelLineAnswerFamilyA + (strategy : ProjStrat params ιA ιB) : + IdxSubMeas (AxisParallelTestSample params) (Fq params) ιA := + fun s => + let ℓ : AxisParallelLine params := + { base := s.1, direction := s.2 } + postprocess + ((strategy.axisParallelMeasurementA ℓ).toSubMeas) + (· zeroCoord) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:357-368 (MIPStarRE.LDT.ProjStrat.axisParallelLineAnswerFamilyB) +/-- Bob's axis-parallel-line answers: Bob receives `ℓ`, answers with +`B^{B,ℓ}`, and the verifier postprocesses to the value at the sampled base +point. -/ +noncomputable def axisParallelLineAnswerFamilyB + (strategy : ProjStrat params ιA ιB) : + IdxSubMeas (AxisParallelTestSample params) (Fq params) ιB := + fun s => + let ℓ : AxisParallelLine params := + { base := s.1, direction := s.2 } + postprocess + ((strategy.axisParallelMeasurementB ℓ).toSubMeas) + (· zeroCoord) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:370-375 (MIPStarRE.LDT.ProjStrat.diagonalPointAnswerFamilyA) +/-- Alice's point answers in the restricted diagonal branch: Alice receives the +sampled base point `u` and answers with `A^{A,u}`. -/ +noncomputable def diagonalPointAnswerFamilyA + (strategy : ProjStrat params ιA ιB) (j : Fin params.m) : + IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιA := + fun s => (strategy.pointMeasurementA s.1).toSubMeas + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:377-382 (MIPStarRE.LDT.ProjStrat.diagonalPointAnswerFamilyB) +/-- Bob's point answers in the restricted diagonal branch: Bob receives the +sampled base point `u` and answers with `A^{B,u}`. -/ +noncomputable def diagonalPointAnswerFamilyB + (strategy : ProjStrat params ιA ιB) (j : Fin params.m) : + IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιB := + fun s => (strategy.pointMeasurementB s.1).toSubMeas + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:384-396 (MIPStarRE.LDT.ProjStrat.diagonalLineAnswerFamilyA) +/-- Alice's restricted diagonal-line answers: Alice receives `ℓ`, answers with +`L^{A,ℓ}`, and the verifier postprocesses to the value at the sampled base +point. -/ +noncomputable def diagonalLineAnswerFamilyA + (strategy : ProjStrat params ιA ιB) (j : Fin params.m) : + IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιA := + fun s => + let v := extendRestrictedDirection j s.2 + let ℓ : DiagonalLine params := + { base := s.1, direction := v } + postprocess + ((strategy.diagonalMeasurementA ℓ).toSubMeas) + (· zeroCoord) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:398-410 (MIPStarRE.LDT.ProjStrat.diagonalLineAnswerFamilyB) +/-- Bob's restricted diagonal-line answers: Bob receives `ℓ`, answers with +`L^{B,ℓ}`, and the verifier postprocesses to the value at the sampled base +point. -/ +noncomputable def diagonalLineAnswerFamilyB + (strategy : ProjStrat params ιA ιB) (j : Fin params.m) : + IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιB := + fun s => + let v := extendRestrictedDirection j s.2 + let ℓ : DiagonalLine params := + { base := s.1, direction := v } + postprocess + ((strategy.diagonalMeasurementB ℓ).toSubMeas) + (· zeroCoord) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:412-419 (MIPStarRE.LDT.ProjStrat.axisParallelLineLeftPointRightFailureProbability) +/-- Axis-parallel branch component where Alice receives the sampled line and Bob +receives its base point. -/ +noncomputable def axisParallelLineLeftPointRightFailureProbability + (strategy : ProjStrat params ιA ιB) : Error := + bipartiteConsError strategy.state + (uniformDistribution (AxisParallelTestSample params)) + (axisParallelLineAnswerFamilyA strategy) + (axisParallelPointAnswerFamilyB strategy) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:421-428 (MIPStarRE.LDT.ProjStrat.axisParallelPointLeftLineRightFailureProbability) +/-- Axis-parallel branch component where Alice receives the sampled base point +and Bob receives the sampled line. -/ +noncomputable def axisParallelPointLeftLineRightFailureProbability + (strategy : ProjStrat params ιA ιB) : Error := + bipartiteConsError strategy.state + (uniformDistribution (AxisParallelTestSample params)) + (axisParallelPointAnswerFamilyA strategy) + (axisParallelLineAnswerFamilyB strategy) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:430-435 (MIPStarRE.LDT.ProjStrat.axisParallelRoleAverage) +/-- The paper's axis-parallel branch for a two-space general strategy, averaged +over the two role choices. -/ +noncomputable def axisParallelRoleAverage + (strategy : ProjStrat params ιA ιB) : Error := + (axisParallelLineLeftPointRightFailureProbability strategy + + axisParallelPointLeftLineRightFailureProbability strategy) / 2 + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:437-444 (MIPStarRE.LDT.ProjStrat.pointAgreementFailureProbability) +/-- Point-agreement branch: both provers receive the same point and the verifier +checks equality of their field answers. -/ +noncomputable def pointAgreementFailureProbability + (strategy : ProjStrat params ιA ιB) : Error := + bipartiteConsError strategy.state + (uniformDistribution (Point params)) + (IdxProjMeas.toIdxSubMeas strategy.pointMeasurementA) + (IdxProjMeas.toIdxSubMeas strategy.pointMeasurementB) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:446-455 (MIPStarRE.LDT.ProjStrat.diagonalLineLeftPointRightFailureProbability) +/-- Diagonal branch component where Alice receives the sampled diagonal line and +Bob receives its base point. -/ +noncomputable def diagonalLineLeftPointRightFailureProbability + (strategy : ProjStrat params ιA ιB) : Error := + (1 / (params.m : Error)) * + ∑ j : Fin params.m, + bipartiteConsError strategy.state + (uniformDistribution (RestrictedDiagonalSample params j)) + (diagonalLineAnswerFamilyA strategy j) + (diagonalPointAnswerFamilyB strategy j) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:457-466 (MIPStarRE.LDT.ProjStrat.diagonalPointLeftLineRightFailureProbability) +/-- Diagonal branch component where Alice receives the sampled base point and +Bob receives the sampled diagonal line. -/ +noncomputable def diagonalPointLeftLineRightFailureProbability + (strategy : ProjStrat params ιA ιB) : Error := + (1 / (params.m : Error)) * + ∑ j : Fin params.m, + bipartiteConsError strategy.state + (uniformDistribution (RestrictedDiagonalSample params j)) + (diagonalPointAnswerFamilyA strategy j) + (diagonalLineAnswerFamilyB strategy j) + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:468-473 (MIPStarRE.LDT.ProjStrat.diagonalRoleAverage) +/-- The paper's diagonal branch for a two-space general strategy, averaged over +the two role choices and the restricted diagonal samples. -/ +noncomputable def diagonalRoleAverage + (strategy : ProjStrat params ιA ιB) : Error := + (diagonalLineLeftPointRightFailureProbability strategy + + diagonalPointLeftLineRightFailureProbability strategy) / 2 + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:475-485 (MIPStarRE.LDT.ProjStrat.lowIndividualDegreeFailureProbability) +/-- Trace-based failure surrogate for the full low-individual-degree test for a +paper-faithful two-space projective strategy. + +This is the paper-faithful two-space failure surrogate: axis-parallel +consistency, point agreement, and diagonal consistency are averaged with weights +`1 / 3`, while the line branches are themselves averaged over the two role +choices. -/ +noncomputable def lowIndividualDegreeFailureProbability + (strategy : ProjStrat params ιA ιB) : Error := + (strategy.axisParallelRoleAverage + strategy.pointAgreementFailureProbability + + strategy.diagonalRoleAverage) / 3 + +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:487-491 (MIPStarRE.LDT.ProjStrat.PassesLowIndividualDegreeTest) +/-- Passing the full low-individual-degree test with error `ε`, for the +paper-faithful two-space strategy container. -/ +structure PassesLowIndividualDegreeTest + (strategy : ProjStrat params ιA ιB) (eps : Error) : Prop where + soundnessHypothesis : strategy.lowIndividualDegreeFailureProbability ≤ eps +end -- module scope +end ProjStrat +end MIPStarRE.LDT + +namespace MIPStarRE.LDT +namespace Test + +-- source: MIPStarRE/LDT/Test/MainTheorem/MainFormal.lean:288-326 (MIPStarRE.LDT.Test.mainFormal) +/-- +Corrected source statement of `thm:main-formal`. + +Paper origin: `references/ldt-paper/test_definition.tex:180-202`. + +This theorem records the two-space source theorem with the confirmed large-`k` +correction `k ≥ 400 m d`. The paper prints the weaker hypothesis `k ≥ m d`; +the missing factor `400` is documented in +`docs/paper-gaps/issue-906-main-formal-k-bound.tex`. The additional condition +`0 < k` corrects the zero-sampling boundary where the printed error collapses +to zero; this boundary is documented in +`docs/paper-gaps/issue-422-main-formal-zero-k-boundary.tex`. -/ +@[eval_problem] +theorem mainFormal + (params : Parameters) + [FieldModel params.q] + {ιA ιB : Type*} + [Fintype ιA] [DecidableEq ιA] + [Fintype ιB] [DecidableEq ιB] + (strategy : ProjStrat params ιA ιB) + (eps : Error) + (hpass : strategy.PassesLowIndividualDegreeTest eps) + (k : ℕ) + (hk : 400 * params.m * params.d ≤ k) + (hk0 : 0 < k) : + ∃ G_A : ProjMeas (Polynomial params) ιA, + ∃ G_B : ProjMeas (Polynomial params) ιB, + ConsRel strategy.state (uniformDistribution (Point params)) + (IdxProjMeas.toIdxSubMeas strategy.pointMeasurementA) + (polynomialEvaluationFamily params G_B.toSubMeas) + (mainFormalError params k eps) ∧ + ConsRel strategy.state (uniformDistribution (Point params)) + (polynomialEvaluationFamily params G_A.toSubMeas) + (IdxProjMeas.toIdxSubMeas strategy.pointMeasurementB) + (mainFormalError params k eps) ∧ + ConsRel strategy.state (uniformDistribution Unit) + (constSubMeasFamily G_A.toSubMeas) + (constSubMeasFamily G_B.toSubMeas) + (mainFormalError params k eps) := by + sorry + +end Test +end MIPStarRE.LDT diff --git a/manifests/problems/mipstarre_low_individual_degree.toml b/manifests/problems/mipstarre_low_individual_degree.toml new file mode 100644 index 00000000..686c9519 --- /dev/null +++ b/manifests/problems/mipstarre_low_individual_degree.toml @@ -0,0 +1,9 @@ +id = "mipstarre_low_individual_degree" +title = "Quantum soundness of the low individual degree test" +test = false +module = "LeanEval.QuantumInformation.LowIndividualDegreeTest" +holes = ["MIPStarRE.LDT.Test.mainFormal"] +submitter = "Sirui Lu" +notes = "Formal statement of the main low individual degree test soundness theorem, including the corrected k ≥ 400md and k > 0 boundary hypotheses documented by the MIPStarRE formalization. The trusted prelude is the statement closure audited with leanprover/comparator." +source = "Ji, Natarajan, Vidick, Wright, and Yuen, Quantum soundness of the classical low individual degree test, arXiv:2009.12982, Theorem thm:main-formal." +informal_solution = "A complete Lean proof is available in https://github.com/LionSR/MIPStarRE at MIPStarRE.LDT.Test.mainFormal; the companion comparator audit is https://github.com/LionSR/LDT-comparator." From b7bfe188e5dffd7cfce7433dc6e5b5447b8c4824 Mon Sep 17 00:00:00 2001 From: texra-ai Date: Fri, 17 Jul 2026 06:31:46 +0200 Subject: [PATCH 2/2] chore: refresh low individual degree challenge --- .../LowIndividualDegreeTest.lean | 588 ++++-------------- 1 file changed, 133 insertions(+), 455 deletions(-) diff --git a/LeanEval/QuantumInformation/LowIndividualDegreeTest.lean b/LeanEval/QuantumInformation/LowIndividualDegreeTest.lean index 22f325ab..1e8800b8 100644 --- a/LeanEval/QuantumInformation/LowIndividualDegreeTest.lean +++ b/LeanEval/QuantumInformation/LowIndividualDegreeTest.lean @@ -28,16 +28,12 @@ for how to run the verification. -/ open scoped BigOperators MatrixOrder Matrix ComplexOrder --- Compiler-generated declarations in the closure (no source --- range); they regenerate identically during elaboration: --- MIPStarRE.LDT.DiagonalLinePolynomial.mk.congr_simp (from MIPStarRE/LDT/Basic/LinePolynomials.lean) --- MIPStarRE.LDT.AxisLinePolynomial.mk.congr_simp (from MIPStarRE/LDT/Basic/LinePolynomials.lean) namespace MIPStarRE.LDT -- source: MIPStarRE/LDT/Basic/ParametersBase.lean:18-18 (MIPStarRE.LDT.Error) abbrev Error := ℝ --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:32-46 (MIPStarRE.LDT.Parameters) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:32-45 (MIPStarRE.LDT.Parameters) /-- Parameters for the `(m,q,d)` low individual degree test. Besides the usual positivity assumptions, we bundle the paper-faithful witness @@ -52,7 +48,6 @@ structure Parameters where hq : 0 < q /-- Paper-faithful witness that `q` is a prime power. -/ hqPrimePower : ∃ p n, Nat.Prime p ∧ 0 < n ∧ q = p ^ n - deriving DecidableEq end MIPStarRE.LDT namespace MIPStarRE.Quantum @@ -62,21 +57,21 @@ abbrev Op (d : Type*) := Matrix d d ℂ end MIPStarRE.Quantum namespace MIPStarRE.LDT --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:169-169 (MIPStarRE.LDT.Fq) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:170-170 (MIPStarRE.LDT.Fq) abbrev Fq (params : Parameters) := Fin params.q --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:170-170 (MIPStarRE.LDT.Point) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:171-171 (MIPStarRE.LDT.Point) abbrev Point (params : Parameters) := Fin params.m → Fq params --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:173-174 (MIPStarRE.LDT.instInhabitedFinM) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:174-175 (MIPStarRE.LDT.instInhabitedFinM) instance {params : Parameters} : Inhabited (Fin params.m) := ⟨⟨0, params.hm⟩⟩ --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:176-177 (MIPStarRE.LDT.instInhabitedFq) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:177-178 (MIPStarRE.LDT.instInhabitedFq) instance {params : Parameters} : Inhabited (Fq params) := ⟨⟨0, params.hq⟩⟩ --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:209-216 (MIPStarRE.LDT.FieldModel) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:210-217 (MIPStarRE.LDT.FieldModel) /-- A bundled field model for the paper's `F_q`, together with a coding equivalence to the repository's finite carrier `Fin q`. -/ class FieldModel (q : ℕ) where @@ -90,109 +85,76 @@ class FieldModel (q : ℕ) where attribute [instance_reducible, instance] FieldModel.instField FieldModel.instFintype FieldModel.instDecidableEq --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:276-276 (MIPStarRE.LDT.Scalar) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:277-277 (MIPStarRE.LDT.Scalar) abbrev Scalar (params : Parameters) [FieldModel params.q] := FieldModel.K params.q --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:277-278 (MIPStarRE.LDT.PolynomialModel) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:278-279 (MIPStarRE.LDT.PolynomialModel) abbrev PolynomialModel (params : Parameters) [FieldModel params.q] := MvPolynomial (Fin params.m) (Scalar params) --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:279-280 (MIPStarRE.LDT.LinePolynomialModel) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:280-281 (MIPStarRE.LDT.LinePolynomialModel) abbrev LinePolynomialModel (params : Parameters) [FieldModel params.q] := _root_.Polynomial (Scalar params) --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:288-290 (MIPStarRE.LDT.decodeScalar) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:289-291 (MIPStarRE.LDT.decodeScalar) /-- Interpret a coded coordinate in `Fin q` as a scalar in the chosen field model. -/ def decodeScalar {params : Parameters} [FieldModel params.q] (x : Fq params) : Scalar params := (FieldModel.equiv (q := params.q)).symm x --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:292-294 (MIPStarRE.LDT.encodeScalar) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:293-295 (MIPStarRE.LDT.encodeScalar) /-- Re-encode a field-model scalar as its canonical representative in `Fin q`. -/ def encodeScalar {params : Parameters} [FieldModel params.q] (x : Scalar params) : Fq params := FieldModel.equiv (q := params.q) x --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:296-298 (MIPStarRE.LDT.encode_decodeScalar) -@[simp] theorem encode_decodeScalar {params : Parameters} [FieldModel params.q] (x : Fq params) : - encodeScalar (decodeScalar x) = x := by - simp [encodeScalar, decodeScalar] - --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:300-303 (MIPStarRE.LDT.decode_encodeScalar) -@[simp] theorem decode_encodeScalar {params : Parameters} [FieldModel params.q] - (x : Scalar params) : - decodeScalar (encodeScalar x) = x := by - simp [encodeScalar, decodeScalar] - --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:305-307 (MIPStarRE.LDT.zeroCoord) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:306-308 (MIPStarRE.LDT.zeroCoord) /-- The zero coordinate. -/ def zeroCoord {params : Parameters} [FieldModel params.q] : Fq params := encodeScalar 0 --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:309-311 (MIPStarRE.LDT.addCoord) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:310-312 (MIPStarRE.LDT.addCoord) /-- Coordinate addition transported through the `Fin q` coding. -/ def addCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params := encodeScalar (decodeScalar x + decodeScalar y) --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:313-315 (MIPStarRE.LDT.subCoord) -/-- Coordinate subtraction transported through the `Fin q` coding. -/ -def subCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params := - encodeScalar (decodeScalar x - decodeScalar y) - --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:317-322 (MIPStarRE.LDT.addCoord_subCoord_right) -@[simp] theorem addCoord_subCoord_right {params : Parameters} [FieldModel params.q] - (x y : Fq params) : - addCoord y (subCoord x y) = x := by - unfold addCoord subCoord - rw [decode_encodeScalar] - simp [sub_eq_add_neg] - --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:324-329 (MIPStarRE.LDT.addCoord_subCoord_left) -@[simp] theorem addCoord_subCoord_left {params : Parameters} [FieldModel params.q] - (x y : Fq params) : - addCoord (subCoord x y) y = x := by - unfold addCoord subCoord - rw [decode_encodeScalar] - simp [sub_eq_add_neg] - --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:338-340 (MIPStarRE.LDT.mulCoord) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:339-341 (MIPStarRE.LDT.mulCoord) /-- Coordinate multiplication transported through the `Fin q` coding. -/ def mulCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params := encodeScalar (decodeScalar x * decodeScalar y) --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:346-348 (MIPStarRE.LDT.addPoint) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:347-349 (MIPStarRE.LDT.addPoint) /-- Pointwise addition in the coded ambient space. -/ def addPoint {params : Parameters} [FieldModel params.q] (u v : Point params) : Point params := fun i => addCoord (u i) (v i) --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:350-353 (MIPStarRE.LDT.smulPoint) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:351-354 (MIPStarRE.LDT.smulPoint) /-- Scalar multiplication in the coded ambient space. -/ def smulPoint {params : Parameters} [FieldModel params.q] (t : Fq params) (u : Point params) : Point params := fun i => mulCoord t (u i) --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:405-408 (MIPStarRE.LDT.decodePoint) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:406-409 (MIPStarRE.LDT.decodePoint) /-- Decode a coded point as a tuple of scalars in the chosen field model. -/ def decodePoint {params : Parameters} [FieldModel params.q] (u : Point params) : Fin params.m → Scalar params := fun i => decodeScalar (u i) --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:410-413 (MIPStarRE.LDT.evalPolynomialModel) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:411-414 (MIPStarRE.LDT.evalPolynomialModel) /-- Evaluate a multivariate polynomial over the chosen field model on a coded point. -/ noncomputable def evalPolynomialModel (params : Parameters) [FieldModel params.q] (p : PolynomialModel params) (u : Point params) : Fq params := encodeScalar (MvPolynomial.eval (decodePoint u) p) --- source: MIPStarRE/LDT/Basic/ParametersBase.lean:415-418 (MIPStarRE.LDT.evalLinePolynomialModel) +-- source: MIPStarRE/LDT/Basic/ParametersBase.lean:416-419 (MIPStarRE.LDT.evalLinePolynomialModel) /-- Evaluate a univariate polynomial over the chosen field model on a coded point. -/ noncomputable def evalLinePolynomialModel (params : Parameters) [FieldModel params.q] (p : LinePolynomialModel params) (t : Fq params) : Fq params := encodeScalar (_root_.Polynomial.eval (decodeScalar t) p) --- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:18-22 (MIPStarRE.LDT.AxisParallelLine) +-- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:18-21 (MIPStarRE.LDT.AxisParallelLine) /-- A genuinely axis-parallel affine line in `F_q^m`. -/ structure AxisParallelLine (params : Parameters) where base : Point params direction : Fin params.m - deriving DecidableEq, Inhabited end MIPStarRE.LDT namespace MIPStarRE.Quantum @@ -211,7 +173,7 @@ end MIPStarRE.Quantum namespace MIPStarRE.LDT namespace AxisParallelLine --- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:26-33 (MIPStarRE.LDT.AxisParallelLine.pointAt) +-- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:27-34 (MIPStarRE.LDT.AxisParallelLine.pointAt) /-- The canonical affine parameterization `t ↦ base + t e_i`. -/ def pointAt {params : Parameters} [FieldModel params.q] (ℓ : AxisParallelLine params) : Fq params → Point params := @@ -221,7 +183,7 @@ def pointAt {params : Parameters} [FieldModel params.q] else ℓ.base i --- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:50-55 (MIPStarRE.LDT.AxisParallelLine.rebaseAt) +-- source: MIPStarRE/LDT/Basic/AxisParallelLine.lean:51-56 (MIPStarRE.LDT.AxisParallelLine.rebaseAt) /-- Rebase an axis-parallel line so that the old point `ℓ.pointAt t` becomes the new base point. -/ def rebaseAt {params : Parameters} [FieldModel params.q] @@ -230,15 +192,14 @@ def rebaseAt {params : Parameters} [FieldModel params.q] direction := ℓ.direction end AxisParallelLine --- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:16-20 (MIPStarRE.LDT.DiagonalLine) +-- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:16-19 (MIPStarRE.LDT.DiagonalLine) /-- A genuinely affine diagonal line in `F_q^m`. -/ structure DiagonalLine (params : Parameters) where base : Point params direction : Point params - deriving DecidableEq, Inhabited namespace DiagonalLine --- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:24-27 (MIPStarRE.LDT.DiagonalLine.pointAt) +-- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:25-28 (MIPStarRE.LDT.DiagonalLine.pointAt) /-- The canonical affine parameterization `t ↦ base + t · direction`. -/ def pointAt {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) : Fq params → Point params := @@ -259,7 +220,7 @@ noncomputable def mainFormalError (params : Parameters) (k : ℕ) (eps : Error) end Test namespace DiagonalLine --- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:99-103 (MIPStarRE.LDT.DiagonalLine.rebaseAt) +-- source: MIPStarRE/LDT/Basic/DiagonalLine.lean:100-104 (MIPStarRE.LDT.DiagonalLine.rebaseAt) /-- Rebase a diagonal line so that the old point `ℓ.pointAt t` becomes the new base point. -/ def rebaseAt {params : Parameters} [FieldModel params.q] (ℓ : DiagonalLine params) (t : Fq params) : DiagonalLine params where @@ -312,36 +273,6 @@ noncomputable def reparamAt {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (t : Fq params) : AxisLinePolynomial params where poly := f.poly.comp (_root_.Polynomial.C (decodeScalar t) + _root_.Polynomial.X) degreeBounded := natDegree_comp_C_add_X_le f.poly (decodeScalar t) f.degreeBounded - --- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:111-115 (MIPStarRE.LDT.AxisLinePolynomial.reparamAt_zero) -@[simp] theorem reparamAt_zero {params : Parameters} [FieldModel params.q] - (f : AxisLinePolynomial params) : - reparamAt f zeroCoord = f := by - refine AxisLinePolynomial.ext ?_ - simp [reparamAt, zeroCoord] - --- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:127-136 (MIPStarRE.LDT.AxisLinePolynomial.reparamAt_reparamAt) -theorem reparamAt_reparamAt {params : Parameters} [FieldModel params.q] - (f : AxisLinePolynomial params) (t s : Fq params) : - reparamAt (reparamAt f t) s = reparamAt f (addCoord t s) := by - refine AxisLinePolynomial.ext ?_ - change - (f.poly.comp (_root_.Polynomial.C (decodeScalar t) + _root_.Polynomial.X)).comp - (_root_.Polynomial.C (decodeScalar s) + _root_.Polynomial.X) = - f.poly.comp (_root_.Polynomial.C (decodeScalar (addCoord t s)) + _root_.Polynomial.X) - rw [_root_.Polynomial.comp_assoc] - simp [addCoord, add_left_comm, add_comm] - --- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:138-146 (MIPStarRE.LDT.AxisLinePolynomial.reparamAtEquiv) -/-- Reparametrization by translation is an equivalence on axis-line answers. -/ -noncomputable def reparamAtEquiv {params : Parameters} [FieldModel params.q] - (t : Fq params) : AxisLinePolynomial params ≃ AxisLinePolynomial params where - toFun := fun f => reparamAt f t - invFun := fun f => reparamAt f (subCoord zeroCoord t) - left_inv := fun f => (reparamAt_reparamAt f t (subCoord zeroCoord t)).trans - ((congrArg (reparamAt f) (addCoord_subCoord_right zeroCoord t)).trans (reparamAt_zero f)) - right_inv := fun f => (reparamAt_reparamAt f (subCoord zeroCoord t) t).trans - ((congrArg (reparamAt f) (addCoord_subCoord_left zeroCoord t)).trans (reparamAt_zero f)) end AxisLinePolynomial -- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:194-197 (MIPStarRE.LDT.DiagonalLinePolynomial) @@ -390,36 +321,6 @@ noncomputable def reparamAt {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t : Fq params) : DiagonalLinePolynomial params where poly := f.poly.comp (_root_.Polynomial.C (decodeScalar t) + _root_.Polynomial.X) degreeBounded := natDegree_comp_C_add_X_le f.poly (decodeScalar t) f.degreeBounded - --- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:252-256 (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_zero) -@[simp] theorem reparamAt_zero {params : Parameters} [FieldModel params.q] - (f : DiagonalLinePolynomial params) : - reparamAt f zeroCoord = f := by - refine DiagonalLinePolynomial.ext ?_ - simp [reparamAt, zeroCoord] - --- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:268-277 (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_reparamAt) -theorem reparamAt_reparamAt {params : Parameters} [FieldModel params.q] - (f : DiagonalLinePolynomial params) (t s : Fq params) : - reparamAt (reparamAt f t) s = reparamAt f (addCoord t s) := by - refine DiagonalLinePolynomial.ext ?_ - change - (f.poly.comp (_root_.Polynomial.C (decodeScalar t) + _root_.Polynomial.X)).comp - (_root_.Polynomial.C (decodeScalar s) + _root_.Polynomial.X) = - f.poly.comp (_root_.Polynomial.C (decodeScalar (addCoord t s)) + _root_.Polynomial.X) - rw [_root_.Polynomial.comp_assoc] - simp [addCoord, add_left_comm, add_comm] - --- source: MIPStarRE/LDT/Basic/LinePolynomials.lean:279-287 (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAtEquiv) -/-- Reparametrization by translation is an equivalence on diagonal-line answers. -/ -noncomputable def reparamAtEquiv {params : Parameters} [FieldModel params.q] - (t : Fq params) : DiagonalLinePolynomial params ≃ DiagonalLinePolynomial params where - toFun := fun f => reparamAt f t - invFun := fun f => reparamAt f (subCoord zeroCoord t) - left_inv := fun f => (reparamAt_reparamAt f t (subCoord zeroCoord t)).trans - ((congrArg (reparamAt f) (addCoord_subCoord_right zeroCoord t)).trans (reparamAt_zero f)) - right_inv := fun f => (reparamAt_reparamAt f (subCoord zeroCoord t) t).trans - ((congrArg (reparamAt f) (addCoord_subCoord_left zeroCoord t)).trans (reparamAt_zero f)) end DiagonalLinePolynomial -- source: MIPStarRE/LDT/Basic/QuantumState.lean:14-27 (MIPStarRE.LDT.QuantumState) @@ -636,42 +537,6 @@ noncomputable def postprocess {α β : Type*} {ι : Type*} [Fintype ι] [Decidab outcome_pos := fun _ => Finset.sum_nonneg fun a _ => A.outcome_pos a sum_eq_total := (Finset.sum_fiberwise Finset.univ f A.outcome).trans A.sum_eq_total total_le_one := A.total_le_one -namespace SubMeas - --- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:123-132 (MIPStarRE.LDT.SubMeas.transport) -/-- Transport a submeasurement along an equivalence of outcome types. -/ -noncomputable def transport {α β : Type*} {ι : Type*} - [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] - (e : α ≃ β) (A : SubMeas α ι) : - SubMeas β ι where - outcome := fun b => A.outcome (e.symm b) - total := A.total - outcome_pos := fun b => A.outcome_pos (e.symm b) - sum_eq_total := (Equiv.sum_comp e.symm A.outcome).trans A.sum_eq_total - total_le_one := A.total_le_one -end SubMeas -namespace Measurement - --- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:272-278 (MIPStarRE.LDT.Measurement.transport) -/-- Transport a measurement along an equivalence of outcome types. -/ -noncomputable def transport {α β : Type*} {ι : Type*} - [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] - (e : α ≃ β) (A : Measurement α ι) : - Measurement β ι where - toSubMeas := SubMeas.transport e A.toSubMeas - total_eq_one := A.total_eq_one -end Measurement -namespace ProjMeas - --- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:328-334 (MIPStarRE.LDT.ProjMeas.transport) -/-- Transport a projective measurement along an equivalence of outcome types. -/ -noncomputable def transport {α β : Type*} {ι : Type*} - [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] - (e : α ≃ β) (A : ProjMeas α ι) : - ProjMeas β ι where - toMeasurement := Measurement.transport e A.toMeasurement - proj := fun b => A.proj (e.symm b) -end ProjMeas -- source: MIPStarRE/LDT/Basic/SubMeasurementFamilies.lean:420-424 (MIPStarRE.LDT.constSubMeasFamily) /-- Constant indexed family taking the same submeasurement on every question. -/ @@ -745,126 +610,32 @@ structure ConsRel {Question Outcome : Type*} (B : IdxSubMeas Question Outcome ιB) (δ : Error) : Prop where offDiagonalBound : bipartiteConsError ψ 𝒟 A B ≤ δ -namespace AxisParallelLine --- source: MIPStarRE/LDT/Test/StrategyCore.lean:189-195 (MIPStarRE.LDT.AxisParallelLine.transportMeasurement) -/-- Transport an axis-parallel-line measurement along rebasing of the line -question by translating its polynomial outcomes. -/ -noncomputable def transportMeasurement {params : Parameters} [FieldModel params.q] - {ι : Type*} [Fintype ι] [DecidableEq ι] - (M : ProjMeas (AxisLinePolynomial params) ι) (t : Fq params) : - ProjMeas (AxisLinePolynomial params) ι := - ProjMeas.transport (AxisLinePolynomial.reparamAtEquiv (params := params) t) M -end AxisParallelLine -namespace DiagonalLine +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:162-171 (MIPStarRE.LDT.AxisParallelMeasurementReparamInvariant) +/-- Direct outcome-level covariance for axis-parallel-line measurements. --- source: MIPStarRE/LDT/Test/StrategyCore.lean:219-225 (MIPStarRE.LDT.DiagonalLine.transportMeasurement) -/-- Transport a diagonal-line measurement along rebasing of the line question by -translating its polynomial outcomes. -/ -noncomputable def transportMeasurement {params : Parameters} [FieldModel params.q] - {ι : Type*} [Fintype ι] [DecidableEq ι] - (M : ProjMeas (DiagonalLinePolynomial params) ι) (t : Fq params) : - ProjMeas (DiagonalLinePolynomial params) ι := - ProjMeas.transport (DiagonalLinePolynomial.reparamAtEquiv (params := params) t) M -end DiagonalLine - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:247-255 (MIPStarRE.LDT.AxisParallelMeasurementTransportInvariant) -/-- 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. -/ -def AxisParallelMeasurementTransportInvariant (params : Parameters) +Rebasing a line question by `t` and reparametrizing an outcome polynomial by +the same translation leaves the corresponding projector unchanged. -/ +def AxisParallelMeasurementReparamInvariant (params : Parameters) [FieldModel params.q] {ι : Type*} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι) : Prop := - ∀ (ℓ : AxisParallelLine params) (t : Fq params), - M (AxisParallelLine.rebaseAt ℓ t) = - AxisParallelLine.transportMeasurement (params := params) (M ℓ) t - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:257-265 (MIPStarRE.LDT.DiagonalMeasurementTransportInvariant) -/-- 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. -/ -def DiagonalMeasurementTransportInvariant (params : Parameters) + ∀ (ℓ : AxisParallelLine params) (t : Fq params) (f : AxisLinePolynomial params), + (M (ℓ.rebaseAt t)).outcome (AxisLinePolynomial.reparamAt f t) = + (M ℓ).outcome f + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:173-182 (MIPStarRE.LDT.DiagonalMeasurementReparamInvariant) +/-- 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. -/ +def DiagonalMeasurementReparamInvariant (params : Parameters) [FieldModel params.q] {ι : Type*} [Fintype ι] [DecidableEq ι] (M : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι) : Prop := - ∀ (ℓ : DiagonalLine params) (t : Fq params), - M (DiagonalLine.rebaseAt ℓ t) = - DiagonalLine.transportMeasurement (params := params) (M ℓ) t - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:291-298 (MIPStarRE.LDT.AxisParallelCovariantMeasurement) -/-- Axis-parallel line measurements bundled with the stronger transport-level -rebasing covariance. -/ -structure AxisParallelCovariantMeasurement (params : Parameters) - [FieldModel params.q] (ι : Type*) [Fintype ι] [DecidableEq ι] where - toIdxProjMeas : - IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ι - transportInvariant : - AxisParallelMeasurementTransportInvariant params toIdxProjMeas - --- source: MIPStarRE/LDT/Test/StrategyCore.lean (elaboration context) -instance {params : Parameters} [FieldModel params.q] {ι : Type*} - [Fintype ι] [DecidableEq ι] : - CoeFun (AxisParallelCovariantMeasurement params ι) - (fun _ => AxisParallelLine params → ProjMeas (AxisLinePolynomial params) ι) where - coe M := M.toIdxProjMeas - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:318-325 (MIPStarRE.LDT.DiagonalCovariantMeasurement) -/-- Diagonal line measurements bundled with the stronger transport-level -rebasing covariance. -/ -structure DiagonalCovariantMeasurement (params : Parameters) - [FieldModel params.q] (ι : Type*) [Fintype ι] [DecidableEq ι] where - toIdxProjMeas : - IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ι - transportInvariant : - DiagonalMeasurementTransportInvariant params toIdxProjMeas - --- source: MIPStarRE/LDT/Test/StrategyCore.lean (elaboration context) -instance {params : Parameters} [FieldModel params.q] {ι : Type*} - [Fintype ι] [DecidableEq ι] : - CoeFun (DiagonalCovariantMeasurement params ι) - (fun _ => DiagonalLine params → ProjMeas (DiagonalLinePolynomial params) ι) where - coe M := M.toIdxProjMeas - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:418-425 (MIPStarRE.LDT.AxisParallelTestSample) -/-- 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. -/ -abbrev AxisParallelTestSample (params : Parameters) := - Point params × Fin params.m - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:427-439 (MIPStarRE.LDT.extendRestrictedDirection) -/-- 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`. -/ -def extendRestrictedDirection {params : Parameters} - [FieldModel params.q] (j : Fin params.m) - (freeCoords : Fin (j.val + 1) → Fq params) : - Point params := - fun k => - if h : k.val ≤ j.val then - freeCoords ⟨k.val, Nat.lt_succ_of_le h⟩ - else zeroCoord - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:441-447 (MIPStarRE.LDT.RestrictedDiagonalSample) -/-- 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}`. -/ -abbrev RestrictedDiagonalSample (params : Parameters) - (j : Fin params.m) := - Point params × (Fin (j.val + 1) → Fq params) - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:449-452 (MIPStarRE.LDT.restrictedDiagonalSampleNonempty) -/-- The restricted diagonal sample space is nonempty. -/ -instance restrictedDiagonalSampleNonempty (params : Parameters) (j : Fin params.m) : - Nonempty (RestrictedDiagonalSample params j) := - inferInstance - --- source: MIPStarRE/LDT/Test/StrategyCore.lean:661-688 (MIPStarRE.LDT.ProjStrat) + ∀ (ℓ : DiagonalLine params) (t : Fq params) (f : DiagonalLinePolynomial params), + (M (ℓ.rebaseAt t)).outcome (DiagonalLinePolynomial.reparamAt f t) = + (M ℓ).outcome f + +-- source: MIPStarRE/LDT/Test/StrategyCore.lean:761-808 (MIPStarRE.LDT.ProjStrat) /-- Paper-faithful two-space projective strategy data. This matches the paper's `def:general-projective-strategy` @@ -873,7 +644,11 @@ 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`. -/ +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. -/ structure ProjStrat (params : Parameters) [FieldModel params.q] (ιA : Type*) [Fintype ιA] [DecidableEq ιA] (ιB : Type*) [Fintype ιB] [DecidableEq ιB] where @@ -884,15 +659,31 @@ structure ProjStrat (params : Parameters) [FieldModel params.q] /-- Alice's point-measurement family, acting on `ιA`. -/ pointMeasurementA : IdxProjMeas (Point params) (Fq params) ιA /-- Alice's axis-parallel-line measurement family, acting on `ιA`. -/ - axisParallelMeasurementA : AxisParallelCovariantMeasurement params ιA + axisParallelMeasurementA : + IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ιA + /-- Alice's axis-parallel measurement is covariant under line rebasing. -/ + axisParallelReparamInvariantA : + AxisParallelMeasurementReparamInvariant params axisParallelMeasurementA /-- Alice's diagonal-line measurement family, acting on `ιA`. -/ - diagonalMeasurementA : DiagonalCovariantMeasurement params ιA + diagonalMeasurementA : + IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ιA + /-- Alice's diagonal measurement is covariant under line rebasing. -/ + diagonalReparamInvariantA : + DiagonalMeasurementReparamInvariant params diagonalMeasurementA /-- Bob's point-measurement family, acting on `ιB`. -/ pointMeasurementB : IdxProjMeas (Point params) (Fq params) ιB /-- Bob's axis-parallel-line measurement family, acting on `ιB`. -/ - axisParallelMeasurementB : AxisParallelCovariantMeasurement params ιB + axisParallelMeasurementB : + IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) ιB + /-- Bob's axis-parallel measurement is covariant under line rebasing. -/ + axisParallelReparamInvariantB : + AxisParallelMeasurementReparamInvariant params axisParallelMeasurementB /-- Bob's diagonal-line measurement family, acting on `ιB`. -/ - diagonalMeasurementB : DiagonalCovariantMeasurement params ιB + diagonalMeasurementB : + IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) ιB + /-- Bob's diagonal measurement is covariant under line rebasing. -/ + diagonalReparamInvariantB : + DiagonalMeasurementReparamInvariant params diagonalMeasurementB namespace ProjStrat -- elaboration context of MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean @@ -902,185 +693,72 @@ variable {params : Parameters} [FieldModel params.q] variable {ιA : Type*} [Fintype ιA] [DecidableEq ιA] variable {ιB : Type*} [Fintype ιB] [DecidableEq ιB] --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:330-335 (MIPStarRE.LDT.ProjStrat.axisParallelPointAnswerFamilyA) -/-- 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}`. -/ -noncomputable def axisParallelPointAnswerFamilyA - (strategy : ProjStrat params ιA ιB) : - IdxSubMeas (AxisParallelTestSample params) (Fq params) ιA := - fun s => (strategy.pointMeasurementA s.1).toSubMeas - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:337-342 (MIPStarRE.LDT.ProjStrat.axisParallelPointAnswerFamilyB) -/-- 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}`. -/ -noncomputable def axisParallelPointAnswerFamilyB - (strategy : ProjStrat params ιA ιB) : - IdxSubMeas (AxisParallelTestSample params) (Fq params) ιB := - fun s => (strategy.pointMeasurementB s.1).toSubMeas - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:344-355 (MIPStarRE.LDT.ProjStrat.axisParallelLineAnswerFamilyA) -/-- Alice's axis-parallel-line answers: Alice receives `ℓ`, answers with -`B^{A,ℓ}`, and the verifier postprocesses to the value at the sampled base -point. -/ -noncomputable def axisParallelLineAnswerFamilyA - (strategy : ProjStrat params ιA ιB) : - IdxSubMeas (AxisParallelTestSample params) (Fq params) ιA := - fun s => - let ℓ : AxisParallelLine params := - { base := s.1, direction := s.2 } - postprocess - ((strategy.axisParallelMeasurementA ℓ).toSubMeas) - (· zeroCoord) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:357-368 (MIPStarRE.LDT.ProjStrat.axisParallelLineAnswerFamilyB) -/-- Bob's axis-parallel-line answers: Bob receives `ℓ`, answers with -`B^{B,ℓ}`, and the verifier postprocesses to the value at the sampled base -point. -/ -noncomputable def axisParallelLineAnswerFamilyB - (strategy : ProjStrat params ιA ιB) : - IdxSubMeas (AxisParallelTestSample params) (Fq params) ιB := - fun s => - let ℓ : AxisParallelLine params := - { base := s.1, direction := s.2 } - postprocess - ((strategy.axisParallelMeasurementB ℓ).toSubMeas) - (· zeroCoord) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:370-375 (MIPStarRE.LDT.ProjStrat.diagonalPointAnswerFamilyA) -/-- Alice's point answers in the restricted diagonal branch: Alice receives the -sampled base point `u` and answers with `A^{A,u}`. -/ -noncomputable def diagonalPointAnswerFamilyA - (strategy : ProjStrat params ιA ιB) (j : Fin params.m) : - IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιA := - fun s => (strategy.pointMeasurementA s.1).toSubMeas - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:377-382 (MIPStarRE.LDT.ProjStrat.diagonalPointAnswerFamilyB) -/-- Bob's point answers in the restricted diagonal branch: Bob receives the -sampled base point `u` and answers with `A^{B,u}`. -/ -noncomputable def diagonalPointAnswerFamilyB - (strategy : ProjStrat params ιA ιB) (j : Fin params.m) : - IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιB := - fun s => (strategy.pointMeasurementB s.1).toSubMeas - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:384-396 (MIPStarRE.LDT.ProjStrat.diagonalLineAnswerFamilyA) -/-- Alice's restricted diagonal-line answers: Alice receives `ℓ`, answers with -`L^{A,ℓ}`, and the verifier postprocesses to the value at the sampled base -point. -/ -noncomputable def diagonalLineAnswerFamilyA - (strategy : ProjStrat params ιA ιB) (j : Fin params.m) : - IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιA := - fun s => - let v := extendRestrictedDirection j s.2 - let ℓ : DiagonalLine params := - { base := s.1, direction := v } - postprocess - ((strategy.diagonalMeasurementA ℓ).toSubMeas) - (· zeroCoord) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:398-410 (MIPStarRE.LDT.ProjStrat.diagonalLineAnswerFamilyB) -/-- Bob's restricted diagonal-line answers: Bob receives `ℓ`, answers with -`L^{B,ℓ}`, and the verifier postprocesses to the value at the sampled base -point. -/ -noncomputable def diagonalLineAnswerFamilyB - (strategy : ProjStrat params ιA ιB) (j : Fin params.m) : - IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιB := - fun s => - let v := extendRestrictedDirection j s.2 - let ℓ : DiagonalLine params := - { base := s.1, direction := v } - postprocess - ((strategy.diagonalMeasurementB ℓ).toSubMeas) - (· zeroCoord) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:412-419 (MIPStarRE.LDT.ProjStrat.axisParallelLineLeftPointRightFailureProbability) -/-- Axis-parallel branch component where Alice receives the sampled line and Bob -receives its base point. -/ -noncomputable def axisParallelLineLeftPointRightFailureProbability - (strategy : ProjStrat params ιA ιB) : Error := - bipartiteConsError strategy.state - (uniformDistribution (AxisParallelTestSample params)) - (axisParallelLineAnswerFamilyA strategy) - (axisParallelPointAnswerFamilyB strategy) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:421-428 (MIPStarRE.LDT.ProjStrat.axisParallelPointLeftLineRightFailureProbability) -/-- Axis-parallel branch component where Alice receives the sampled base point -and Bob receives the sampled line. -/ -noncomputable def axisParallelPointLeftLineRightFailureProbability - (strategy : ProjStrat params ιA ιB) : Error := - bipartiteConsError strategy.state - (uniformDistribution (AxisParallelTestSample params)) - (axisParallelPointAnswerFamilyA strategy) - (axisParallelLineAnswerFamilyB strategy) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:430-435 (MIPStarRE.LDT.ProjStrat.axisParallelRoleAverage) -/-- The paper's axis-parallel branch for a two-space general strategy, averaged -over the two role choices. -/ -noncomputable def axisParallelRoleAverage - (strategy : ProjStrat params ιA ιB) : Error := - (axisParallelLineLeftPointRightFailureProbability strategy + - axisParallelPointLeftLineRightFailureProbability strategy) / 2 - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:437-444 (MIPStarRE.LDT.ProjStrat.pointAgreementFailureProbability) -/-- Point-agreement branch: both provers receive the same point and the verifier -checks equality of their field answers. -/ -noncomputable def pointAgreementFailureProbability - (strategy : ProjStrat params ιA ιB) : Error := - bipartiteConsError strategy.state - (uniformDistribution (Point params)) - (IdxProjMeas.toIdxSubMeas strategy.pointMeasurementA) - (IdxProjMeas.toIdxSubMeas strategy.pointMeasurementB) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:446-455 (MIPStarRE.LDT.ProjStrat.diagonalLineLeftPointRightFailureProbability) -/-- Diagonal branch component where Alice receives the sampled diagonal line and -Bob receives its base point. -/ -noncomputable def diagonalLineLeftPointRightFailureProbability - (strategy : ProjStrat params ιA ιB) : Error := - (1 / (params.m : Error)) * - ∑ j : Fin params.m, - bipartiteConsError strategy.state - (uniformDistribution (RestrictedDiagonalSample params j)) - (diagonalLineAnswerFamilyA strategy j) - (diagonalPointAnswerFamilyB strategy j) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:457-466 (MIPStarRE.LDT.ProjStrat.diagonalPointLeftLineRightFailureProbability) -/-- Diagonal branch component where Alice receives the sampled base point and -Bob receives the sampled diagonal line. -/ -noncomputable def diagonalPointLeftLineRightFailureProbability - (strategy : ProjStrat params ιA ιB) : Error := - (1 / (params.m : Error)) * - ∑ j : Fin params.m, - bipartiteConsError strategy.state - (uniformDistribution (RestrictedDiagonalSample params j)) - (diagonalPointAnswerFamilyA strategy j) - (diagonalLineAnswerFamilyB strategy j) - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:468-473 (MIPStarRE.LDT.ProjStrat.diagonalRoleAverage) -/-- The paper's diagonal branch for a two-space general strategy, averaged over -the two role choices and the restricted diagonal samples. -/ -noncomputable def diagonalRoleAverage - (strategy : ProjStrat params ιA ιB) : Error := - (diagonalLineLeftPointRightFailureProbability strategy + - diagonalPointLeftLineRightFailureProbability strategy) / 2 - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:475-485 (MIPStarRE.LDT.ProjStrat.lowIndividualDegreeFailureProbability) +-- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:455-519 (MIPStarRE.LDT.ProjStrat.lowIndividualDegreeFailureProbability) /-- Trace-based failure surrogate for the full low-individual-degree test for a paper-faithful two-space projective strategy. -This is the paper-faithful two-space failure surrogate: axis-parallel -consistency, point agreement, and diagonal consistency are averaged with weights -`1 / 3`, while the line branches are themselves averaged over the two role -choices. -/ +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. -/ noncomputable def lowIndividualDegreeFailureProbability (strategy : ProjStrat params ιA ιB) : Error := - (strategy.axisParallelRoleAverage + strategy.pointAgreementFailureProbability + - strategy.diagonalRoleAverage) / 3 - --- source: MIPStarRE/LDT/Test/StrategyBiProj/Measurements.lean:487-491 (MIPStarRE.LDT.ProjStrat.PassesLowIndividualDegreeTest) -/-- Passing the full low-individual-degree test with error `ε`, for the -paper-faithful two-space strategy container. -/ -structure PassesLowIndividualDegreeTest - (strategy : ProjStrat params ιA ιB) (eps : Error) : Prop where - soundnessHypothesis : strategy.lowIndividualDegreeFailureProbability ≤ eps + let axisPointA : IdxSubMeas (Point params × Fin params.m) (Fq params) ιA := + fun s => (strategy.pointMeasurementA s.1).toSubMeas + let axisPointB : IdxSubMeas (Point params × Fin params.m) (Fq params) ιB := + fun s => (strategy.pointMeasurementB s.1).toSubMeas + let axisLineA : IdxSubMeas (Point params × Fin params.m) (Fq params) ιA := + fun s => + let ℓ : AxisParallelLine params := { base := s.1, direction := s.2 } + postprocess ((strategy.axisParallelMeasurementA ℓ).toSubMeas) (· zeroCoord) + let axisLineB : IdxSubMeas (Point params × Fin params.m) (Fq params) ιB := + fun s => + let ℓ : AxisParallelLine params := { base := s.1, direction := s.2 } + postprocess ((strategy.axisParallelMeasurementB ℓ).toSubMeas) (· zeroCoord) + let extendDirection (j : Fin params.m) + (freeCoords : Fin (j.val + 1) → Fq params) : Point params := + fun k => + if h : k.val ≤ j.val then + freeCoords ⟨k.val, Nat.lt_succ_of_le h⟩ + else zeroCoord + let diagonalPointA (j : Fin params.m) : + IdxSubMeas (Point params × (Fin (j.val + 1) → Fq params)) (Fq params) ιA := + fun s => (strategy.pointMeasurementA s.1).toSubMeas + let diagonalPointB (j : Fin params.m) : + IdxSubMeas (Point params × (Fin (j.val + 1) → Fq params)) (Fq params) ιB := + fun s => (strategy.pointMeasurementB s.1).toSubMeas + let diagonalLineA (j : Fin params.m) : + IdxSubMeas (Point params × (Fin (j.val + 1) → Fq params)) (Fq params) ιA := + fun s => + let ℓ : DiagonalLine params := { base := s.1, direction := extendDirection j s.2 } + postprocess ((strategy.diagonalMeasurementA ℓ).toSubMeas) (· zeroCoord) + let diagonalLineB (j : Fin params.m) : + IdxSubMeas (Point params × (Fin (j.val + 1) → Fq params)) (Fq params) ιB := + fun s => + let ℓ : DiagonalLine params := { base := s.1, direction := extendDirection j s.2 } + postprocess ((strategy.diagonalMeasurementB ℓ).toSubMeas) (· zeroCoord) + ((bipartiteConsError strategy.state + (@uniformDistribution (Point params × Fin params.m) _ _ + ⟨(fun _ => zeroCoord, default)⟩) axisLineA axisPointB + + bipartiteConsError strategy.state + (@uniformDistribution (Point params × Fin params.m) _ _ + ⟨(fun _ => zeroCoord, default)⟩) axisPointA axisLineB) / ((2 : ℕ) : Error) + + bipartiteConsError strategy.state + (@uniformDistribution (Point params) _ _ ⟨fun _ => zeroCoord⟩) + (IdxProjMeas.toIdxSubMeas strategy.pointMeasurementA) + (IdxProjMeas.toIdxSubMeas strategy.pointMeasurementB) + + ((1 / (params.m : Error)) * ∑ j : Fin params.m, + bipartiteConsError strategy.state + (@uniformDistribution (Point params × (Fin (j.val + 1) → Fq params)) _ _ + ⟨(fun _ => zeroCoord, fun _ => zeroCoord)⟩) + (diagonalLineA j) (diagonalPointB j) + + (1 / (params.m : Error)) * ∑ j : Fin params.m, + bipartiteConsError strategy.state + (@uniformDistribution (Point params × (Fin (j.val + 1) → Fq params)) _ _ + ⟨(fun _ => zeroCoord, fun _ => zeroCoord)⟩) + (diagonalPointA j) (diagonalLineB j)) / ((2 : ℕ) : Error)) / 3 end -- module scope end ProjStrat end MIPStarRE.LDT @@ -1088,7 +766,7 @@ end MIPStarRE.LDT namespace MIPStarRE.LDT namespace Test --- source: MIPStarRE/LDT/Test/MainTheorem/MainFormal.lean:288-326 (MIPStarRE.LDT.Test.mainFormal) +-- source: MIPStarRE/LDT/Test/MainTheorem/MainFormal.lean:288-327 (MIPStarRE.LDT.Test.mainFormal) /-- Corrected source statement of `thm:main-formal`. @@ -1110,7 +788,7 @@ theorem mainFormal [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) (eps : Error) - (hpass : strategy.PassesLowIndividualDegreeTest eps) + (hpass : strategy.lowIndividualDegreeFailureProbability ≤ eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) (hk0 : 0 < k) :