Documentation

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

Hashed anti-checker survivor cells -- definitions #

The existential predicate below is the exact query made by Stockmeyer's occupancy test. A witness is a row-major tuple of encoded survivor codes in the prescribed Cartesian power that the selected affine hash sends to zero.

source
def Complexity.GapMCSP.Magnification.AntiCheckerLemma.survivorPowerWidth (arity threshold precision : ℕ) :
ℕ

Width of one witness tuple used by relative counting on the encoded anti-checker survivor domain.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellWitness {count : ℕ} (arity threshold precision rangeWidth : ℕ) (input : BitString (count * (arity + 1))) (seed : BitString (PairwiseIndependentHash.affineSeedWidth (survivorPowerWidth arity threshold precision) rangeWidth)) (witness : BitString (survivorPowerWidth arity threshold precision)) :
    Prop

    One tuple of encoded survivors belongs to the selected affine zero cell.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableHashCellWitness {count : ℕ} (arity threshold precision rangeWidth : ℕ) (input : BitString (count * (arity + 1))) (seed : BitString (PairwiseIndependentHash.affineSeedWidth (survivorPowerWidth arity threshold precision) rangeWidth)) (witness : BitString (survivorPowerWidth arity threshold precision)) :
      Decidable (HashCellWitness arity threshold precision rangeWidth input seed witness)
      Equations
      source
      def Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellNonempty {count : ℕ} (arity threshold precision rangeWidth : ℕ) (input : BitString (count * (arity + 1))) (seed : BitString (PairwiseIndependentHash.affineSeedWidth (survivorPowerWidth arity threshold precision) rangeWidth)) :
      Prop

      The selected affine zero cell contains at least one powered survivor witness.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instDecidableHashCellNonempty {count : ℕ} (arity threshold precision rangeWidth : ℕ) (input : BitString (count * (arity + 1))) (seed : BitString (PairwiseIndependentHash.affineSeedWidth (survivorPowerWidth arity threshold precision) rangeWidth)) :
        Decidable (HashCellNonempty arity threshold precision rangeWidth input seed)
        Equations