Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.SourceReduction.Parameters.Defs

Finite parameters for the sumset source reduction #

One global affine breaker handles every parity of at most four outer coordinates and all their candidate calls. Its error pays for the union of those tests. The resulting parity bias and discarded-coordinate allowance are chosen for the checked moment and majority bounds.

These are conservative finite choices for the strategy in Chattopadhyay-- Liao, Extractors for Sum of Two Sources, Lemma 5.4 and equation (5): https://arxiv.org/pdf/2110.12652. The choices alone do not assert the sampler guards, source entropy, asymptotics, or a uniform evaluator.

source
def Algebraic.Cutwidth.Extractor.sourceReductionOuterBits (b : ℕ) :
ℕ

Bit width of the outer sampler index.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.sourceReductionCandidateBits (b : ℕ) :
    ℕ

    Bit width of the candidate index, using the actual padded Gamma seed budget.

    Equations
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.sourceReductionOuterCount (b : ℕ) :
      ℕ

      Number of outer coordinates in the final majority.

      Equations
      Instances For
        source
        def Algebraic.Cutwidth.Extractor.sourceReductionCandidateCount (b : ℕ) :
        ℕ

        Number of affine calls XORed at each outer coordinate.

        Equations
        Instances For
          source
          def Algebraic.Cutwidth.Extractor.sourceReductionTamperingCount (b : ℕ) :
          ℕ

          One honest call and enough tampered slots for every parity of order at most four.

          Equations
          Instances For
            source
            def Algebraic.Cutwidth.Extractor.sourceReductionAdviceLength (b : ℕ) :
            ℕ

            An injective advice word records the outer and candidate indices.

            Equations
            Instances For
              source
              def Algebraic.Cutwidth.Extractor.sourceReductionTarget (b : ℕ) :
              ℕ

              Local dyadic error exponent of the single selected affine breaker.

              Equations
              Instances For
                source
                noncomputable def Algebraic.Cutwidth.Extractor.sourceReductionSamplerError (b : ℕ) :
                ℝ

                Size allowance for the common sampler test.

                Equations
                Instances For
                  source
                  noncomputable def Algebraic.Cutwidth.Extractor.sourceReductionBadThreshold (b : ℕ) :
                  ℝ

                  Discrepancy threshold defining each bad-seed test.

                  Equations
                  Instances For
                    source
                    noncomputable def Algebraic.Cutwidth.Extractor.sourceReductionParityBias (b : ℕ) :
                    ℝ

                    Low-order sign-parity bias furnished outside the bad-seed tests.

                    Equations
                    Instances For