Documentation

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

Hashing circuits for anti-checker counters -- definitions #

This layer specializes the generic relative-counting circuit contract to the fixed-width encoded survivor set used by the Anti-Checker Lemma.

source
@[reducible]
def Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterInputWidth (arity prefixLength : ℕ) :
ℕ

Width of the packed labeled-sample input for the counter extending a prefix of length prefixLength.

Equations
Instances For
    source
    instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatCounterInputWidth (arity prefixLength : ℕ) :
    NeZero (counterInputWidth arity prefixLength)
    source
    def Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashingCounterSeedWidth (beta : PositiveRationalScale) (arity prefixLength : ℕ) :
    ℕ

    Randomness needed by the relative hashing estimator on the encoded survivor domain, with enough failure exponent to fix one seed for every labeled-sample input.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashingCircuitImplements {arity prefixLength internalGates : ℕ} (beta : PositiveRationalScale) (circuit : Circuit Basis.andOr2 (hashingCounterSeedWidth beta arity prefixLength + counterInputWidth arity prefixLength) (counterOutputWidth beta arity) internalGates) :
      Prop

      A seed-prefix circuit exactly implements the amplified hashing estimator for the encoded labeled-survivor set.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For