Documentation

Complexitylib.Metacomplexity.MCSP.Magnification.AntiChecker.Rounds.Defs

Anti-Checker Lemma round parameters -- definitions #

The good-string argument supplies a genuine 1/(2n) shrinking extension. Relative approximation at precision 8n preserves a 1/(4n) shrink after estimate minimization.

source
def Complexity.GapMCSP.Magnification.AntiCheckerLemma.roundPrecision (arity : ℕ) :
ℕ

Relative-count precision sufficient for one approximate-selection round.

Equations
Instances For
    source
    def Complexity.GapMCSP.Magnification.AntiCheckerLemma.roundShrinkDenominator (arity : ℕ) :
    ℕ

    Survivor-shrink denominator certified after approximate minimization.

    Equations
    Instances For
      source
      def Complexity.GapMCSP.Magnification.AntiCheckerLemma.roundBlockCount (beta : PositiveRationalScale) (arity : ℕ) :
      ℕ

      Number of halving blocks needed to exceed the canonical initial survivor count by a factor of two.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.GapMCSP.Magnification.AntiCheckerLemma.requiredRoundCount (beta : PositiveRationalScale) (arity : ℕ) :
        ℕ

        Number of shrinking rounds used before padding to the published sample count.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.GapMCSP.Magnification.AntiCheckerLemma.IsAccurateRoundEstimator {arity : ℕ} (beta : PositiveRationalScale) (target : BitString arity → Bool) (estimator : List (BitString arity) → BitString arity → ℕ) :
          Prop

          A semantic extension estimator satisfies the required relative-count contract at every sample prefix for the selected small-circuit threshold.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.GapMCSP.Magnification.AntiCheckerLemma.IsAccurateRequiredRoundEstimator {arity : ℕ} (beta : PositiveRationalScale) (target : BitString arity → Bool) (estimator : List (BitString arity) → BitString arity → ℕ) :
            Prop

            A semantic extension estimator satisfies the relative-count contract for exactly the prefix lengths used by the anti-checker construction.

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