Documentation

MIPRE.Background.QLD.PauliFactorPrograms

Exact factor masks for the binary Pauli sampler #

The factor program is independent of the field basis and the question type. Its masks are the actual downsized, numbered factors on every binary prefix.

source
def MIPRE.QLD.PauliCL.factorFlag {m : ℕ} (r : ℕ) :
Coord m → Bool
Equations
Instances For
    source
    theorem MIPRE.QLD.PauliCL.bits_getD_append (a b : Cost.BitStr) (i : ℕ) :
    List.getD (a ++ b) i false = if i < List.length a then List.getD a i false else List.getD b (i - List.length a) false
    source
    theorem MIPRE.QLD.PauliCL.bits_getD_replicate (n : ℕ) (b : Bool) (i : ℕ) :
    (List.replicate n b).getD i false = if i < n then b else false
    source
    theorem MIPRE.QLD.PauliCL.factorFlags_getD (m r : ℕ) (c : Coord m) :
    List.getD (Introspection.PauliStageProgram.factorFlags m r) (↑((coordNumbering m) c)) false = factorFlag r c
    source
    theorem MIPRE.QLD.PauliCL.factorFlags_ofFn (m r : ℕ) :
    Introspection.PauliStageProgram.factorFlags m r = List.ofFn fun (i : Fin (3 * m + 3)) => factorFlag r ((coordNumbering m).symm i)
    source
    theorem MIPRE.QLD.PauliCL.indicatorBits_binaryRegister {m k : ℕ} (S : Finset (Coord m)) :
    CL.indicatorBits (Finset.map (binaryCoordEquiv m k).toEmbedding (S ×ˢ Finset.univ)) = (List.ofFn fun (i : Fin (3 * m + 3)) => List.replicate k (decide ((coordNumbering m).symm i ∈ S))).flatten
    source
    theorem MIPRE.QLD.PauliCL.presentation_factor_one {F : Type u_1} [Field F] {m : ℕ} (χ : F → Fin m) (T : Ty) (u : Coord m → F) :
    (ExplicitSeed.presentation χ T).factorOfPrefix 0 u = seedSet m
    source
    theorem MIPRE.QLD.PauliCL.presentation_factor_two {F : Type u_1} [Field F] {m : ℕ} (χ : F → Fin m) (T : Ty) (u : Coord m → F) :
    (ExplicitSeed.presentation χ T).factorOfPrefix 1 u = directionSet m
    source
    theorem MIPRE.QLD.PauliCL.presentation_factor_three {F : Type u_1} [Field F] {m : ℕ} (χ : F → Fin m) (T : Ty) (u : Coord m → F) :
    (ExplicitSeed.presentation χ T).factorOfPrefix 2 u = finalSet m
    source
    theorem MIPRE.QLD.PauliCL.factorFlag_mem {F : Type u_1} [Field F] {m : ℕ} (χ : F → Fin m) (T : Ty) (u : Coord m → F) (r : ℕ) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) (c : Coord m) :
    factorFlag r c = decide (c ∈ (ExplicitSeed.presentation χ T).factorOfPrefix (r - 1) u)
    source
    theorem MIPRE.QLD.PauliCL.binaryPresentation_factor {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m k : ℕ} [NeZero m] (χ : F → Fin m) (b : Module.Basis (Fin k) (ZMod 2) F) (T : Ty) (r : ℕ) (u : Coord m → F) :
    (ExplicitSeed.binaryPresentation χ b T).factorOfPrefix r ((binaryVectorEquiv b) u) = Finset.map (binaryCoordEquiv m k).toEmbedding ((ExplicitSeed.presentation χ T).factorOfPrefix r u ×ˢ Finset.univ)
    source
    theorem MIPRE.QLD.PauliCL.factorBits_correct {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m k : ℕ} [NeZero m] (χ : F → Fin m) (b : Module.Basis (Fin k) (ZMod 2) F) (T : Ty) (j r : ℕ) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) (u : Fin ((3 * m + 3) * k) → ZMod 2) :
    Introspection.PauliStageProgram.factorBits.toFun ((Cost.unary k, Cost.unary j, Cost.unary m), r) = CL.indicatorBits ((ExplicitSeed.binaryPresentation χ b T).factorOfPrefix (r - 1) u)

    Exact correctness for every type, every legal stage, every binary prefix, and any chosen field basis. No prefix validity assumption is needed.