Documentation

Complexity.Computability.PCP.Amplification.Arithmetic

Fixed amplification parameters for the arithmetic expanders #

The arithmetic family has degree 2 * 257 ^ 12 and a uniform spectral bound strictly below one. The fixed killing rate 2 ^ 324 + 1 suffices to double the value after preprocessing, powering, and selected composition over the 128-symbol answer alphabet, up to the gap 2 ^ (-61). Its walk length is 2 ^ 333. The threshold uses the full denominator of the second-moment bound, rather than the smaller cutoff 1 / walkLength².

Both parameters are concrete natural numbers, with no search or choice in their definitions. They are irreducible to keep elaboration from evaluating the astronomical finite types built from them. The construction is asymptotic: these parameters are not intended for practical use.

Main definitions #

Main results #

References #

source
theorem Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.killRate_def :
killRate = 4 ^ 162 + 1
source
@[irreducible]
def Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.killRate :
ℕ

A fixed killing rate large enough for the concrete arithmetic spectral bound.

Instances For
    source
    theorem Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.walkLength_def :
    walkLength = 2 * 4 ^ 166
    source
    @[irreducible]
    def Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.walkLength :
    ℕ

    The walk length required by the powering bound over the fixed answer alphabet.

    Instances For
      source
      noncomputable def Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.gap :
      ℝ

      A soundness threshold supported by the exact second-moment bound.

      Instances For
        source
        theorem Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.gap_pos :
        0 < gap

        The concrete soundness gap is positive.

        source
        theorem Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.gap_le_one :
        gap ≤ 1

        The concrete soundness gap is at most one.

        source
        instance Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.instNeZeroNatKillRate :
        NeZero killRate
        source
        theorem Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.two_le_killRate :
        2 ≤ killRate

        The chosen killing rate is at least two.

        source
        theorem Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.one_le_walkLength :
        1 ≤ walkLength

        The chosen walk length is positive.

        source
        theorem Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.walkLength_eq :
        walkLength = 4 * Fintype.card (Bool × (Fin 6 → Bool)) * (killRate - 1)

        The chosen walk length matches the alphabet size and killing rate.

        source
        theorem Cslib.PCP.ConstraintGraph.Amplification.Arithmetic.gain :
        2 ≤ Amplification.gain 840 (Fintype.card (Bool × (Fin 6 → Bool))) (Fintype.card (RotationMap.AffinePlaneFamilyLabel (ZMod 257) 257)) walkLength killRate (1 - 9 / (400 * 257 ^ 16)) gap

        The concrete killing rate pays for preprocessing and composition with a factor of two left.