Documentation

MIPRE.Background.AnswerReduction.SoundError

Soundness of answer reduction: the error assembly #

Piece AR-5f of planning/answer-reduction.md (lem:ar-error-assembly), its arithmetic half: the combined error of the decoded strategy's analysis, at a typed failure θ ≤ Kε, is at most

39204 K Z^{3A} ε^{clB} + (Q + 1)^{-2} + 22 Z^{3A} 2^{-clB Q}, Z = 8 (Q + 1) m'

(errE_le), where A = ⌈simA⌉ and Q ≤ m is the question length, when the field is large: Z^{fieldExp} ≤ q with fieldExp = 40000 (3A + 4). The two prefactors simA (d m r)^simA of the two extractions are at most Z^{3A} (simA_mul_rpow_le), and the field hypothesis puts q^{clB} above Z^{3A + 4} (rpow_clB_ge), which kills both field terms.

The constants #

source
@[irreducible]
noncomputable def MIPRE.AnswerReduction.simAN :
ℕ

simA, rounded up to a natural number.

Equations
Instances For
    source
    theorem MIPRE.AnswerReduction.simAN_def :
    simAN = ⌈LIDT.Simul.simA⌉₊
    source
    theorem MIPRE.AnswerReduction.simA_le_simAN :
    LIDT.Simul.simA ≤ ↑simAN
    source
    theorem MIPRE.AnswerReduction.fieldExp_def :
    fieldExp = 40000 * (3 * simAN + 4)
    source
    @[irreducible]
    noncomputable def MIPRE.AnswerReduction.fieldExp :
    ℕ

    The exponent of the field-size hypothesis: q ≥ Z^{fieldExp} puts q^{clB} above Z^{3A + 4}.

    Equations
    Instances For

      The prefactor and the field #

      source
      theorem MIPRE.AnswerReduction.simA_mul_rpow_le {M Z : ℕ} (hM : 1 ≤ M) (hZ : 2 ≤ Z) (h : M ≤ Z ^ 2) :
      LIDT.Simul.simA * ↑M ^ LIDT.Simul.simA ≤ ↑Z ^ (3 * simAN)

      The prefactor of δ_sim is at most Z^{3A} when its argument is at most Z².

      source
      theorem MIPRE.AnswerReduction.rpow_clB_ge {q Z : ℕ} (hq : Z ^ fieldExp ≤ q) :
      ↑Z ^ (3 * simAN + 4) ≤ ↑q ^ LIDT.clB

      A large field: Z^{fieldExp} ≤ q puts q^{clB} above Z^{3A + 4}.

      The combined error #

      source
      noncomputable def MIPRE.AnswerReduction.errE (q m m' : ℕ) (θ : ℝ) :
      ℝ

      The combined error, at a typed failure θ, over the field of size q: the two extractions' errors, the typed failure, and the Schwartz--Zippel term.

      Equations
      Instances For
        source
        theorem MIPRE.AnswerReduction.deltaSim_le_of {q m d r : ℕ} {x x' Pw β E : ℝ} (hx0 : 0 ≤ x) (hP : LIDT.Simul.simA * ↑(d * m * r) ^ LIDT.Simul.simA ≤ Pw) (hx : x ^ LIDT.clB ≤ x') (hb : Pw * ↑q ^ (-LIDT.clB) ≤ β) (hc : 2 ^ (-(LIDT.clB * ↑m * ↑d)) ≤ E) :
        LIDT.Simul.deltaSim q m d r x ≤ Pw * x' + β + Pw * E

        One extraction's error, term by term.

        source
        theorem MIPRE.AnswerReduction.errE_le {q m m' Q : ℕ} (hm : 1 ≤ m) (hmm : m ≤ m') (hQm : Q ≤ m) (hq : (8 * ((Q + 1) * m')) ^ fieldExp ≤ q) {θ ε K : ℝ} (hθ0 : 0 ≤ θ) (hθ : θ ≤ K * ε) (hK : 1 ≤ K) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) :
        errE q m m' θ ≤ 39204 * K * ↑(8 * ((Q + 1) * m')) ^ (3 * simAN) * ε ^ LIDT.clB + 1 / (↑Q + 1) ^ 2 + 22 * ↑(8 * ((Q + 1) * m')) ^ (3 * simAN) * 2 ^ (-(LIDT.clB * ↑Q))

        The combined error at a typed failure θ ≤ Kε, over a large field.

        The threshold #

        source
        theorem MIPRE.AnswerReduction.exists_threshold_clB (c p : ℕ) :
        ∃ (Q0 : ℕ), ∀ (Q : ℕ), Q0 ≤ Q → 8064 ≤ Q ∧ 177408 * ↑c * ↑Q ^ (p + 1) ≤ 2 ^ (LIDT.clB * ↑Q)

        Past a threshold, 2^{clB Q} beats every polynomial in Q, and Q ≥ 8064.

        The soundness loss #

        source
        def MIPRE.AnswerReduction.aOf (c p K : ℕ) :
        ℕ

        The exponent a of the soundness loss, from the constants c, p of the polynomial bound Z^{3A} ≤ c Q^p σ^p and the detyping factor K.

        Equations
        Instances For
          source
          theorem MIPRE.AnswerReduction.one_le_aOf (c p K : ℕ) :
          1 ≤ aOf c p K
          source
          theorem MIPRE.AnswerReduction.sqrt_le_delta {N μ σ Q c p K : ℕ} (hN : 2 ≤ N) (hμ : 1 ≤ μ) (hσ : 1 ≤ σ) (hQN : Q ≤ N ^ (2 * μ)) (hNQ : N ^ μ ≤ Q) (hQ8 : 8064 ≤ Q) (hc : 177408 * ↑c * ↑Q ^ (p + 1) ≤ 2 ^ (LIDT.clB * ↑Q)) {G e ε : ℝ} (hG : G ≤ ↑c * ↑Q ^ p * ↑σ ^ p) (hε0 : 0 ≤ ε) (he : e ≤ 39204 * ↑K * G * ε ^ LIDT.clB + 1 / (↑Q + 1) ^ 2 + 22 * G * 2 ^ (-(LIDT.clB * ↑Q))) :
          24 * √(7 * e) ≤ ↑σ ^ ↑(aOf c p K) * (↑N ^ (↑μ * ↑(aOf c p K)) * ε ^ (LIDT.clB / 2) + ↑N ^ (-(↑μ * (LIDT.clB / 2))))

          The error is below the soundness loss: with N = λn, Q between N^μ and N^{2μ} and past the threshold, the bound of errE_le gives 24 √(7 e) ≤ σ^a (N^{μa} ε^{clB/2} + N^{-μ clB/2}).