Documentation

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

Iterable anti-checker selection rounds -- definitions #

One round preserves the target truth table and prepends the labeled sample chosen by exhaustive counter minimization to the carried prefix. Its output therefore has exactly the state layout expected by the next prefix-length counter.

source
def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundSuccessorInput {arity prefixLength : ℕ} (candidate : Fin (2 ^ arity)) (table : BitString (2 ^ arity)) (packedPrefix : BitString (prefixLength * (arity + 1))) :
BitString (selectionRoundInputWidth arity (prefixLength + 1))

State obtained by prepending one fixed candidate sample to a labeled prefix while preserving the target truth table.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundSuccessorInputMap (beta : PositiveRationalScale) (arity prefixLength : ℕ) :
    Fin (selectionRoundInputWidth arity (prefixLength + 1)) → Fin (selectionRoundInputWidth arity prefixLength + (counterOutputWidth beta arity + (arity + 1)))

    Reorder the preserved state and minimum key-payload record into the next round's truth-table-plus-labeled-prefix layout.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundCombinedCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) :
      (internalGates : ℕ) × Circuit Basis.andOr2 (selectionRoundInputWidth arity prefixLength) (selectionRoundInputWidth arity prefixLength + (counterOutputWidth beta arity + (arity + 1))) internalGates

      Preserve the current state in parallel with exhaustive counter minimization.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Complexity.GapMCSP.Magnification.AntiCheckerLemma.selectionRoundStateCircuit {overhead arity prefixLength : ℕ} {beta : PositiveRationalScale} (counter : ApproximateCounterCircuit overhead beta arity prefixLength) :
        (internalGates : ℕ) × Circuit Basis.andOr2 (selectionRoundInputWidth arity prefixLength) (selectionRoundInputWidth arity (prefixLength + 1)) internalGates

        One iterable selection round, returning the preserved truth table followed by the newly selected labeled sample and the old labeled prefix.

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