Documentation

MIPRE.Background.QLD.TypeEncoding

Faithful type labels and the finite Pauli branch decoder #

Only the fixed set of twenty-six question types is tabulated. Field elements, dimensions, seeds and answers are handled by uniform programs.

source
@[instance_reducible]
noncomputable instance MIPRE.QLD.instSizedEncodingTy :
Cost.SizedEncoding Ty
Equations
  • One or more equations did not get rendered due to their size.
source
noncomputable def MIPRE.QLD.PauliCL.typeTable :
Cost.PolyTimeFun Cost.Data Cost.Data
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.QLD.PauliCL.typeTable_encode (t : Ty) :
    typeTable.toFun (Cost.encode t) = Cost.encode (programTag t)
    source
    noncomputable def MIPRE.QLD.PauliCL.typeTag :
    Cost.PolyTimeFun Cost.Data Introspection.PauliStageProgram.Tag
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.QLD.PauliCL.typeTag_encode (t : Ty) :
      typeTag.toFun (Cost.encode t) = programTag t