Pauli sampling with the explicit binary seed enumeration

The sampler retains its canonical binary seed and uses the efficient high-bit selector. Only the mathematical decoder permutes that seed to the enumeration used in qldGame. A permutation of the common random content proves equality with the existing QLD question law, including the line seeds in the questions.

noncomputable def MIPRE.QLD.PauliCL.ExplicitSeed.secondMap {F : Type u_1} [Field F] {m : ℕ} (χ : F → Fin m) (t : Ty) (s : F) : CL.RegLinear F (directionSet m)

Equations

• MIPRE.QLD.PauliCL.ExplicitSeed.secondMap χ (MIPRE.QLD.Ty.dline W) s = MIPRE.QLD.PauliCL.directionMap (χ s)
• MIPRE.QLD.PauliCL.ExplicitSeed.secondMap χ t s = 0

noncomputable def MIPRE.QLD.PauliCL.ExplicitSeed.finalMap {F : Type u_1} [Field F] {m : ℕ} (χ : F → Fin m) (t : Ty) (s : F) (v : Fin m → F) : CL.RegLinear F (finalSet m)

Equations

• MIPRE.QLD.PauliCL.ExplicitSeed.finalMap χ (MIPRE.QLD.Ty.point W) s v = MIPRE.QLD.PauliCL.pointMap W LinearMap.id
• MIPRE.QLD.PauliCL.ExplicitSeed.finalMap χ (MIPRE.QLD.Ty.aline W) s v = MIPRE.QLD.PauliCL.pointMap W (MIPRE.CL.canonLin (F ∙ Pi.single (χ s) 1))
• MIPRE.QLD.PauliCL.ExplicitSeed.finalMap χ (MIPRE.QLD.Ty.dline W) s v = MIPRE.QLD.PauliCL.pointMap W (MIPRE.CL.canonLin (F ∙ v))
• MIPRE.QLD.PauliCL.ExplicitSeed.finalMap χ (MIPRE.QLD.Ty.pauli W) s v = 0
• MIPRE.QLD.PauliCL.ExplicitSeed.finalMap χ t s v = MIPRE.CL.RegLinear.id (MIPRE.QLD.PauliCL.finalSet m)

noncomputable def MIPRE.QLD.PauliCL.ExplicitSeed.presentation {F : Type u_1} [Field F] {m : ℕ} (χ : F → Fin m) (t : Ty) : CL.CLFun F (Coord m) 3

The concrete three-stage presentation with a specified seed selector.

Equations

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

theorem MIPRE.QLD.PauliCL.ExplicitSeed.presentation_exactlyOn {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (χ : F → Fin m) (t : Ty) : (presentation χ t).ExactlyOn Finset.univ

def MIPRE.QLD.PauliCL.ExplicitSeed.contentPermutation {F : Type u_1} {m : ℕ} (π : F ≃ F) : Content F m ≃ Content F m

Permute just the shared seed; all other random content stays fixed.

Equations

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

def MIPRE.QLD.PauliCL.ExplicitSeed.decode {F : Type u_1} {m : ℕ} (π : F ≃ F) (t : Ty) (x : Coord m → F) : Question F m

Decode the explicit seed into the fixed enumeration used by the legacy QLD question type. No program needs to evaluate this mathematical relabelling.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.QLD.PauliCL.ExplicitSeed.decode π (MIPRE.QLD.Ty.point W) x = MIPRE.QLD.Question.point W (((MIPRE.QLD.PauliCL.ExplicitSeed.contentPermutation π) (MIPRE.QLD.PauliCL.vectorContent x)).pt W)
• MIPRE.QLD.PauliCL.ExplicitSeed.decode π (MIPRE.QLD.Ty.pauli W) x = MIPRE.QLD.Question.pauli W
• MIPRE.QLD.PauliCL.ExplicitSeed.decode π (MIPRE.QLD.Ty.pairB W) x = MIPRE.QLD.Question.pairB W ((MIPRE.QLD.PauliCL.ExplicitSeed.contentPermutation π) (MIPRE.QLD.PauliCL.vectorContent x)).omega
• MIPRE.QLD.PauliCL.ExplicitSeed.decode π MIPRE.QLD.Ty.pair x = MIPRE.QLD.Question.pair ((MIPRE.QLD.PauliCL.ExplicitSeed.contentPermutation π) (MIPRE.QLD.PauliCL.vectorContent x)).omega
• MIPRE.QLD.PauliCL.ExplicitSeed.decode π (MIPRE.QLD.Ty.con i) x = MIPRE.QLD.Question.con i ((MIPRE.QLD.PauliCL.ExplicitSeed.contentPermutation π) (MIPRE.QLD.PauliCL.vectorContent x)).omega
• MIPRE.QLD.PauliCL.ExplicitSeed.decode π (MIPRE.QLD.Ty.var j) x = MIPRE.QLD.Question.var j ((MIPRE.QLD.PauliCL.ExplicitSeed.contentPermutation π) (MIPRE.QLD.PauliCL.vectorContent x)).omega

theorem MIPRE.QLD.PauliCL.ExplicitSeed.decode_presentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (t : Ty) (c : Content F m) : decode π t ((presentation χ t).eval (contentVector c)) = Content.question hm ((contentPermutation π) c) t

Literal equality of the full decoded questions, not merely equality of the chosen direction index.

def MIPRE.QLD.PauliCL.ExplicitSeed.samplePermutation {F : Type u_1} {m : ℕ} (π : F ≃ F) : Sample F m ≃ TyEdge × (Coord m → F)

Equations

• MIPRE.QLD.PauliCL.ExplicitSeed.samplePermutation π = (Equiv.refl MIPRE.QLD.TyEdge).prodCongr ((MIPRE.QLD.PauliCL.ExplicitSeed.contentPermutation π).symm.trans MIPRE.QLD.PauliCL.contentEquiv)

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

Equations

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

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

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

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

Equations

• MIPRE.QLD.PauliCL.ExplicitSeed.binaryDecode π b T x = MIPRE.QLD.PauliCL.ExplicitSeed.decode π T ((MIPRE.QLD.PauliCL.binaryVectorEquiv b).symm x)

theorem MIPRE.QLD.PauliCL.ExplicitSeed.binaryDecode_presentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] [Algebra (ZMod 2) F] {t : ℕ} (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) (c : Content F m) : binaryDecode π b T ((binaryPresentation χ b T).eval ((binaryVectorEquiv b) (contentVector c))) = Content.question hm ((contentPermutation π) c) T

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

Equations

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

theorem MIPRE.QLD.PauliCL.ExplicitSeed.qldGame_mu_binaryPresentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] [Algebra (ZMod 2) F] {t d : ℕ} (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (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)) => binaryDecode π b (↑p.1).1 ((binaryPresentation χ b (↑p.1).1).eval p.2)) (fun (p : TyEdge × (Fin ((3 * m + 3) * t) → ZMod 2)) => binaryDecode π b (↑p.1).2 ((binaryPresentation χ b (↑p.1).2).eval p.2)) x y

noncomputable def MIPRE.QLD.PauliCL.ExplicitSeed.seedPermutation {k : ℕ} (E : SAT.BinField k) : E.carrier ≃ E.carrier

The concrete permutation from canonical bit rank to the legacy numbering.

Equations

• MIPRE.QLD.PauliCL.ExplicitSeed.seedPermutation E = ((MIPRE.Introspection.SeedProgram.fieldEnumeration E).trans (finCongr ⋯)).trans (Fintype.equivFin E.carrier).symm

theorem MIPRE.QLD.PauliCL.ExplicitSeed.seedPermutation_rank {k : ℕ} (E : SAT.BinField k) (s : E.carrier) : ↑((Fintype.equivFin E.carrier) ((seedPermutation E) s)) = ↑(Introspection.SeedProgram.fieldIndex E s)

theorem MIPRE.QLD.PauliCL.ExplicitSeed.chi_seedPermutation {k : ℕ} (E : SAT.BinField k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card E.carrier) (s : E.carrier) : LIDT.CL.chi hm ((seedPermutation E) s) = Introspection.SeedProgram.selector E j hj s

The arbitrary legacy enumeration appears only in the seed relabelling. The branch chosen by the actual presentation is computed by selectorProg.

theorem MIPRE.QLD.PauliCL.ExplicitSeed.dyadic_divides {k : ℕ} (E : SAT.BinField k) (j : ℕ) (hj : j ≤ k) : 2 ^ j ∣ Fintype.card E.carrier

theorem MIPRE.QLD.PauliCL.ExplicitSeed.qldGame_mu_selector_binary {k j : ℕ} (E : SAT.BinField k) (hj : j ≤ k) [Algebra (ZMod 2) E.carrier] {t d : ℕ} (b : Module.Basis (Fin t) (ZMod 2) E.carrier) (x y : Question E.carrier (2 ^ j)) : (qldGame ⋯).μ x y = SampledGame.dist (fun (p : TyEdge × (Fin ((3 * 2 ^ j + 3) * t) → ZMod 2)) => binaryDecode (seedPermutation E) b (↑p.1).1 ((binaryPresentation (Introspection.SeedProgram.selector E j hj) b (↑p.1).1).eval p.2)) (fun (p : TyEdge × (Fin ((3 * 2 ^ j + 3) * t) → ZMod 2)) => binaryDecode (seedPermutation E) b (↑p.1).2 ((binaryPresentation (Introspection.SeedProgram.selector E j hj) b (↑p.1).2).eval p.2)) x y

The instantiated explicit sampler has the actual legacy QLD law. The selector correspondence has been proved, rather than supplied as a premise.