Documentation

Complexitylib.Metacomplexity.MCSP.Magnification.AntiChecker.Generator.Padding.Defs

Anti-checker generator output padding -- definitions #

The selection circuit prints the inputs chosen during the shrinking rounds. This module prepends all-zero sample rows until the packed output has the published sample count, matching AntiChecker.padInputsTo exactly.

source
def Complexity.GapMCSP.Magnification.AntiCheckerLemma.padPackedSamples {sourceCount targetCount arity : ℕ} (hbudget : sourceCount ≤ targetCount) (input : BitString (sourceCount * arity)) :
BitString (targetCount * arity)

Prepend all-zero rows to a row-major packed sample vector.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.GapMCSP.Magnification.AntiCheckerLemma.packedSamplePaddingSource {sourceCount targetCount arity : ℕ} (hbudget : sourceCount ≤ targetCount) (output : Fin (targetCount * arity)) :
    Circuit.InputSource (sourceCount * arity)

    One source of a packed-sample padding circuit. Padding rows are constant false; remaining rows copy the corresponding source coordinate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.GapMCSP.Magnification.AntiCheckerLemma.packedSamplePaddingCircuit {sourceCount targetCount arity : ℕ} [NeZero (sourceCount * arity)] [NeZero (targetCount * arity)] (hbudget : sourceCount ≤ targetCount) :
      Circuit Basis.andOr2 (sourceCount * arity) (targetCount * arity) 0

      Zero-internal-gate circuit that prepends all-zero rows to a packed sample vector.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.paddedSelectionCircuit {overhead arity : ℕ} {beta : PositiveRationalScale} [NeZero arity] (family : ApproximateCounterFamily overhead beta arity) (hbudget : requiredRoundCount beta arity ≤ sampleCount beta arity) :
        (internalGates : ℕ) × Circuit Basis.andOr2 (2 ^ arity) (outputBitCount beta arity) internalGates

        Full required-round selection followed by zero padding to the published number of sample rows.

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