Binary coordinates for the concrete Pauli CL family

A supplied basis of the actual finite field converts the twenty-six concrete presentations into three-level binary presentations on (3m+3)t numbered coordinates. The theorems identify both the exact question map and the existing Pauli game's joint question law. No executable or uniform runtime claim is part of this coordinate conversion.

def MIPRE.QLD.PauliCL.basisFin : Bas ≃ Fin 2

Equations

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

def MIPRE.QLD.PauliCL.unitIndex : Unit ≃ Fin 1

Equations

• MIPRE.QLD.PauliCL.unitIndex = { toFun := fun (x : Unit) => 0, invFun := fun (x : Fin 1) => (), left_inv := ⋯, right_inv := ⋯ }

def MIPRE.QLD.PauliCL.coordNumbering (m : ℕ) : Coord m ≃ Fin (3 * m + 3)

Field coordinates in the fixed order: uX, uZ, seed, direction, rX, rZ. The numbering contains no arbitrary finite-type enumeration.

Equations

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

@[simp]

theorem MIPRE.QLD.PauliCL.coordNumbering_point_X (m : ℕ) (i : Fin m) : ↑((coordNumbering m) (Coord.point Bas.X i)) = ↑i

@[simp]

theorem MIPRE.QLD.PauliCL.coordNumbering_point_Z (m : ℕ) (i : Fin m) : ↑((coordNumbering m) (Coord.point Bas.Z i)) = m + ↑i

@[simp]

theorem MIPRE.QLD.PauliCL.coordNumbering_seed (m : ℕ) : ↑((coordNumbering m) Coord.seed) = 2 * m

@[simp]

theorem MIPRE.QLD.PauliCL.coordNumbering_direction (m : ℕ) (i : Fin m) : ↑((coordNumbering m) (Coord.direction i)) = 2 * m + 1 + ↑i

@[simp]

theorem MIPRE.QLD.PauliCL.coordNumbering_scalar_X (m : ℕ) : ↑((coordNumbering m) (Coord.scalar Bas.X)) = 3 * m + 1

@[simp]

theorem MIPRE.QLD.PauliCL.coordNumbering_scalar_Z (m : ℕ) : ↑((coordNumbering m) (Coord.scalar Bas.Z)) = 3 * m + 2

def MIPRE.QLD.PauliCL.binaryCoordEquiv (m t : ℕ) : Coord m × Fin t ≃ Fin ((3 * m + 3) * t)

Each field coordinate is followed by its t bits in basis order.

Equations

• MIPRE.QLD.PauliCL.binaryCoordEquiv m t = ((MIPRE.QLD.PauliCL.coordNumbering m).prodCongr (Equiv.refl (Fin t))).trans finProdFinEquiv

theorem MIPRE.QLD.PauliCL.binaryCoordEquiv_val (m t : ℕ) (c : Coord m) (j : Fin t) : ↑((binaryCoordEquiv m t) (c, j)) = ↑((coordNumbering m) c) * t + ↑j

noncomputable def MIPRE.QLD.PauliCL.binaryVectorEquiv {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m t : ℕ} (b : Module.Basis (Fin t) (ZMod 2) F) : (Coord m → F) ≃ₗ[ZMod 2] Fin ((3 * m + 3) * t) → ZMod 2

Equations

• MIPRE.QLD.PauliCL.binaryVectorEquiv b = (MIPRE.CL.downsizeEquiv b).trans (MIPRE.CL.reindexEquiv (MIPRE.QLD.PauliCL.binaryCoordEquiv m t))

theorem MIPRE.QLD.PauliCL.binaryVectorEquiv_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] (b : Module.Basis (Fin t) (ZMod 2) F) (x : Coord m → F) (c : Coord m) (j : Fin t) : (binaryVectorEquiv b) x ((binaryCoordEquiv m t) (c, j)) = (b.repr (x c)) j

noncomputable def MIPRE.QLD.PauliCL.binaryPresentation {F : Type u_1} [Field F] [Fintype F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) : CL.CLFun (ZMod 2) (Fin ((3 * m + 3) * t)) 3

Equations

• MIPRE.QLD.PauliCL.binaryPresentation hm b T = MIPRE.CL.CLFun.reindex (MIPRE.QLD.PauliCL.binaryCoordEquiv m t) (MIPRE.CL.CLFun.downsize b (MIPRE.QLD.PauliCL.presentation hm T))

theorem MIPRE.QLD.PauliCL.binaryPresentation_exactlyOn {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) : (binaryPresentation hm b T).ExactlyOn Finset.univ

theorem MIPRE.QLD.PauliCL.binaryPresentation_eval {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) (x : Coord m → F) : (binaryPresentation hm b T).eval ((binaryVectorEquiv b) x) = (binaryVectorEquiv b) ((presentation hm T).eval x)

Evaluation agrees with the actual field presentation under the binary coordinate equivalence.

theorem MIPRE.QLD.PauliCL.binaryPresentation_pauli_eval {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (W : Bas) (x : Fin ((3 * m + 3) * t) → ZMod 2) : (binaryPresentation hm b (Ty.pauli W)).eval x = 0

noncomputable def MIPRE.QLD.PauliCL.binaryQuestion {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m t : ℕ} (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) (x : Fin ((3 * m + 3) * t) → ZMod 2) : Question F m

Decode the binary content of a question of the given type.

Equations

• MIPRE.QLD.PauliCL.binaryQuestion b T x = MIPRE.QLD.PauliCL.questionOfVector T ((MIPRE.QLD.PauliCL.binaryVectorEquiv b).symm x)

theorem MIPRE.QLD.PauliCL.binaryQuestion_presentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) (c : Content F m) : binaryQuestion b T ((binaryPresentation hm b T).eval ((binaryVectorEquiv b) (contentVector c))) = Content.question hm c T

noncomputable def MIPRE.QLD.PauliCL.binarySampleEquiv {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m t : ℕ} (b : Module.Basis (Fin t) (ZMod 2) F) : Sample F m ≃ TyEdge × (Fin ((3 * m + 3) * t) → ZMod 2)

Equations

• MIPRE.QLD.PauliCL.binarySampleEquiv b = (Equiv.refl MIPRE.QLD.TyEdge).prodCongr (MIPRE.QLD.PauliCL.contentEquiv.trans (MIPRE.QLD.PauliCL.binaryVectorEquiv b).toEquiv)

theorem MIPRE.QLD.PauliCL.qldGame_mu_binaryPresentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] {d : ℕ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (x y : Question F m) : (qldGame hm).μ x y = SampledGame.dist (fun (p : TyEdge × (Fin ((3 * m + 3) * t) → ZMod 2)) => binaryQuestion b (↑p.1).1 ((binaryPresentation hm b (↑p.1).1).eval p.2)) (fun (p : TyEdge × (Fin ((3 * m + 3) * t) → ZMod 2)) => binaryQuestion b (↑p.1).2 ((binaryPresentation hm b (↑p.1).2).eval p.2)) x y

The existing Pauli game is exactly the decoded binary CL sampler law, including its uniform ordered-edge choice.