Documentation

Complexitylib.Metacomplexity.MCSP.Magnification.AntiChecker.Counter.Encoding.Defs

Anti-checker counter encodings -- definitions #

Approximate counter circuits receive a fixed number of labeled samples. Each sample occupies one row of arity + 1 bits: its input coordinates in the library's usual order, followed by the required output bit. Counter outputs are interpreted as little-endian natural numbers, matching MCSP truth-table indices.

source
def Complexity.GapMCSP.Magnification.AntiCheckerLemma.packLabeledSamples {count arity : ℕ} (samples : Fin count → SuccinctMCSP.Sample arity) :
BitString (count * (arity + 1))

Pack fixed-width labeled samples in row-major order.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackLabeledSample {count arity : ℕ} (input : BitString (count * (arity + 1))) (sample : Fin count) :
    SuccinctMCSP.Sample arity

    Read one labeled sample from a row-major packed bit string.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.GapMCSP.Magnification.AntiCheckerLemma.unpackLabeledSamples {count arity : ℕ} (input : BitString (count * (arity + 1))) :
      Fin count → SuccinctMCSP.Sample arity

      Split a packed bit string into its fixed-width labeled samples.

      Equations
      Instances For
        source
        def Complexity.GapMCSP.Magnification.AntiCheckerLemma.packTargetSamples {count arity : ℕ} (target : BitString arity → Bool) (inputs : Fin count → BitString arity) :
        BitString (count * (arity + 1))

        Pack inputs labeled by a target Boolean function.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterValue {width : ℕ} (output : BitString width) :
          ℕ

          Interpret a counter circuit's output as a little-endian natural number.

          Equations
          Instances For