Documentation

MIPRE.Foundations.Introspection.PauliFactorProg

The executable Pauli factor query #

The field registers are fixed across all types and prefixes. Stage one reads the seed, stage two the direction, and stage three the points and scalars. Each field flag is repeated for all of its binary basis coordinates. Invalid stages return the all-zero mask of the same ambient length.

source
def MIPRE.Introspection.PauliStageProgram.factorFlags (m r : ℕ) :
Cost.BitStr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.Introspection.PauliStageProgram.factorFlagsProg :
    Cost.PolyTimeFun (Parameters × ℕ) Cost.BitStr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Introspection.PauliStageProgram.factorFlagsProg_apply (p : Parameters) (r : ℕ) :
      factorFlagsProg.toFun (p, r) = factorFlags (List.length p.2.2) r
      source
      noncomputable def MIPRE.Introspection.PauliStageProgram.factorBits :
      Cost.PolyTimeFun (Parameters × ℕ) Cost.BitStr

      A single total program prints the factor mask for arbitrary unary widths and dimensions. The selector width is retained in the common parameter tuple.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.Introspection.PauliStageProgram.factorBits_apply (p : Parameters) (r : ℕ) :
        factorBits.toFun (p, r) = (List.map (fun (b : Bool) => List.replicate (List.length p.1) b) (factorFlags (List.length p.2.2) r)).flatten
        source
        theorem MIPRE.Introspection.PauliStageProgram.factorFlags_length (m r : ℕ) :
        List.length (factorFlags m r) = 3 * m + 3
        source
        theorem MIPRE.Introspection.PauliStageProgram.factorBits_length (p : Parameters) (r : ℕ) :
        List.length (factorBits.toFun (p, r)) = (3 * List.length p.2.2 + 3) * List.length p.1