The three stages of tailored compression, as hypotheses

Paper II of the Aldous–Lyons track (Bowen–Chapman–Vidick, arXiv:2501.00173): question reduction (thm:h_level_question_reduciton, II:5712), answer reduction (thm:main_ans_red, II:6883) and parallel repetition (thm:repetition, II:11103), each in value form; the plan is planning/aldous-lyons-track.md, §4 and §5. Each structure is the data its theorem provides, in the vocabulary of MIPRE.Introspection, MIPRE.AnswerReduction and MIPRE.Repetition — the same parameters, budgets and soundness losses — with tailored verifiers in and out:

• the output's answer-length calculator is part of the data, as a function of the parameters (the paper's A^λ_qr and A_ar depend on λ only, II:5712 and II:6883) or, for repetition, of the input's sampler and answer-length calculator;
• the answer-length calculators halt on the sampler's questions (len_total), and the budgets bound the lengths (TailoredVerifier.Within);
• completeness is read in perfect Z-aligned permutation strategies commuting along edges;
• the answer bounds of the existing contracts disappear: a tailored game reads every answer at its own length. Repetition keeps one, the bound B on the input's lengths, which its soundness loss depends on; its parse parameter β disappears with it, as the repeated linear-constraints processor reads the coordinates' lengths from the input's calculator (II:11464–11516).

These are the Phase 0 contracts, written before any construction; the stages that inhabit them (Phases 2–4) may revise them, as the existing contracts were revised when theirs were built. TailoredGapCompression.ofTailoredPipeline, their composition, is Phase 5.

structure MIPRE.Tailored.TailoredIntrospection (ℓ : ℕ) : Type

Question reduction (II:5712) for ℓ-level tailored inputs, in value form. On the plan's Route A its inhabitant is a tailored presentation of the repository's introspection verifier (MIPRE.Introspection.seven), applied to the input padded to constant lengths (II:6219): the same sampler, an answer-length calculator reading the question's type, and a linear-constraints processor whose constraints accept exactly what the introspective decider accepts.

• a : ℝ

  The constant a of the soundness loss, normalized to a ≥ 1.

• b : ℝ

  The exponent b of the soundness loss, 0 < b ≤ 1.

• one_le_a : 1 ≤ self.a
• b_pos : 0 < self.b
• b_le_one : self.b ≤ 1
• C : ℕ

  The complexity constant.

• sampler : ℕ → CL.Sampler 5

  The introspective sampler, depending only on λ.

• samplerProg : Cost.PolyTimeFun ℕ Cost.Prog
• samplerProg_eq (lam : ℕ) : self.samplerProg.toFun lam = (self.sampler lam).prog
• len : ℕ → Decider

  The introspective answer-length calculator, depending only on λ.

• lenProg : Cost.PolyTimeFun ℕ Cost.Prog
• lenProg_eq (lam : ℕ) : self.lenProg.toFun lam = (self.len lam).prog
• compute : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog × Cost.Prog) × ℕ) Cost.Prog

  The introspective linear-constraints processor, from the input programs and λ, in polynomial time.

• output : Cost.Prog × Cost.Prog × Cost.Prog → ℕ → TailoredVerifier 5
• output_sampler (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (self.output V lam).sampler = self.sampler lam
• output_len (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (self.output V lam).len = self.len lam
• output_lp (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (self.output V lam).lp.prog = self.compute.toFun (V, lam)
• within (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam n : ℕ) : (self.output V lam).Within n (Introspection.budget self.C lam n)

  The complexity clauses, for every input and index.

• lp_size (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (self.output V lam).lp.size ≤ self.C * (lam + 1) ^ self.C

  |LP^intro| ≤ C λ^C, for every input.

• len_total (lam n : ℕ) : LenTotal (self.len lam) n ((self.sampler lam).dim n)
• completeness (V : TailoredVerifier ℓ) (lam n : ℕ) : V.IsBounded lam → V.HasPerfectZPC (2 ^ n) → (self.output V.progs lam).HasPerfectZPC n

  Completeness. For a λ-bounded input.

• soundness (V : TailoredVerifier ℓ) (lam n : ℕ) (ε : ℝ) : V.IsBounded lam → 1 ≤ n → 0 < ε → 1 - ε < (self.output V.progs lam).valStar n → 1 - Introspection.delta self.a self.b lam n ε ≤ V.valStar (2 ^ n)

  Soundness. For a λ-bounded input and n ≥ 1: val*(𝒱^intro_n) > 1 - ε gives val*(𝒱_{2^n}) ≥ 1 - δ(ε, n).

structure MIPRE.Tailored.TailoredAnswerReduction (ℓ : ℕ) : Type

Answer reduction (II:6883) for ℓ-level tailored inputs, in value form: the paper's tailored PCP (purification, oracularization, triangulation, decoupling, the output indicator and its decoupled Cook–Levin description, the low-degree test), with the parameters (λ, μ, σ) and the budgets of MIPRE.AnswerReduction.

• a : ℝ

  The constant a of the soundness loss, normalized to a ≥ 1.

• b : ℝ

  The exponent b of the soundness loss, 0 < b ≤ 1.

• one_le_a : 1 ≤ self.a
• b_pos : 0 < self.b
• b_le_one : self.b ≤ 1
• C : ℕ

  The threshold above which the completeness and soundness clauses hold.

• bound : Polynomial ℕ

  The base polynomial of the output bound AnswerReduction.outBound.

• deg : ℕ

  The base degree; the output's degree is AnswerReduction.outDegree deg μ.

• sampler : CL.Sampler ℓ → ℕ → ℕ → ℕ → CL.Sampler (max (ℓ + 2) 5)

  The answer-reduced sampler, a function of the input sampler and (λ, μ, σ).

• samplerProg : Cost.PolyTimeFun (Cost.Prog × ℕ × ℕ × ℕ) Cost.Prog
• samplerProg_eq (S : CL.Sampler ℓ) (lam mu sigma : ℕ) : self.samplerProg.toFun (S.prog, lam, mu, sigma) = (self.sampler S lam mu sigma).prog
• len : ℕ → ℕ → ℕ → Decider

  The answer-reduced answer-length calculator, depending only on (λ, μ, σ).

• lenProg : Cost.PolyTimeFun (ℕ × ℕ × ℕ) Cost.Prog
• lenProg_eq (lam mu sigma : ℕ) : self.lenProg.toFun (lam, mu, sigma) = (self.len lam mu sigma).prog
• compute : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog × Cost.Prog) × ℕ × ℕ × ℕ) Cost.Prog

  The answer-reduced linear-constraints processor, from the input programs and (λ, μ, σ), in polynomial time.

• output : TailoredVerifier ℓ → ℕ → ℕ → ℕ → TailoredVerifier (max (ℓ + 2) 5)
• output_sampler (V : TailoredVerifier ℓ) (lam mu sigma : ℕ) : (self.output V lam mu sigma).sampler = self.sampler V.sampler lam mu sigma
• output_len (V : TailoredVerifier ℓ) (lam mu sigma : ℕ) : (self.output V lam mu sigma).len = self.len lam mu sigma
• output_lp (V : TailoredVerifier ℓ) (lam mu sigma : ℕ) : (self.output V lam mu sigma).lp.prog = self.compute.toFun (V.progs, lam, mu, sigma)
• within (V : TailoredVerifier ℓ) (lam mu sigma n : ℕ) : V.Within n (AnswerReduction.inBudget lam mu n) → V.size ≤ sigma → (self.output V lam mu sigma).Within n (Budget.uniform (AnswerReduction.outBound self.bound lam mu sigma n) (AnswerReduction.outDegree self.deg mu))

  The complexity clause, as MIPRE.AnswerReduction.within.

• len_total (V : TailoredVerifier ℓ) (lam mu sigma n : ℕ) : LenTotal (self.len lam mu sigma) n ((self.sampler V.sampler lam mu sigma).dim n)
• completeness (V : TailoredVerifier ℓ) (lam mu sigma n : ℕ) : self.C ≤ n → 1 ≤ lam → 1 ≤ mu → V.Within n (AnswerReduction.inBudget lam mu n) → V.size ≤ sigma → V.HasPerfectZPC n → (self.output V lam mu sigma).HasPerfectZPC n

  Completeness, for n ≥ C and λ, μ ≥ 1.

• soundness (V : TailoredVerifier ℓ) (lam mu sigma n : ℕ) (ε : ℝ) : self.C ≤ n → 2 ≤ n → 1 ≤ lam → V.Within n (AnswerReduction.inBudget lam mu n) → V.size ≤ sigma → 0 < ε → 1 - ε < (self.output V lam mu sigma).valStar n → 1 - AnswerReduction.delta self.a self.b lam mu sigma n ε ≤ V.valStar n

  Soundness, for n ≥ max C 2 and λ ≥ 1: val*(𝒱^ans_n) > 1 - ε gives val*(𝒱_n) ≥ 1 - δ(ε, n).

@[reducible, inline]

abbrev MIPRE.Tailored.TailoredRepetition.arg (lam tau n : ℕ) (R : Budget) (s : ℕ) : ℕ

The argument of the polynomial bounding the repeated verifier at index n: the repetition count, the input's budget and description length, the parameters, and 10^{R.k}, the input's cost on the dimension query (as in MIPRE.Repetition.arg, without the parse length, which a tailored verifier does not need).

Equations

• MIPRE.Tailored.TailoredRepetition.arg lam tau n R s = MIPRE.Repetition.reps lam tau n + R.S + R.d + R.D + R.B + s + lam + tau + n + 10 ^ R.k

structure MIPRE.Tailored.TailoredRepetition (ℓ : ℕ) : Type

Parallel repetition (II:11103) of ℓ-level tailored verifiers, in value form and direct rather than anchored: k(n) = Repetition.reps λ τ n independent copies, the lengths added coordinate by coordinate, the constraints of each coordinate padded with zeros to the whole answer (II:11464–11516), and the soundness of the vendored direct repetition theorem (MIPRE.Repetition.quantumValue_repeat_le). The paper's anchored, entanglement-preserving form is not needed on the plan's route (§4.1).

• c : ℝ

  The constant of the soundness exponent.

• c_pos : 0 < self.c
• bound : Polynomial ℕ

  The polynomial bounding the running times and dimension of the output.

• deg : ℕ

  The degree multiplier of the output's running times.

• sampler : CL.Sampler ℓ → ℕ → ℕ → CL.Sampler ℓ

  The repeated sampler, a function of the input sampler and (λ, τ).

• samplerProg : Cost.PolyTimeFun (Cost.Prog × ℕ × ℕ) Cost.Prog
• samplerProg_eq (S : CL.Sampler ℓ) (lam tau : ℕ) : self.samplerProg.toFun (S.prog, lam, tau) = (self.sampler S lam tau).prog
• len : CL.Sampler ℓ → Decider → ℕ → ℕ → Decider

  The repeated answer-length calculator, a function of the input sampler, the input answer-length calculator and (λ, τ).

• lenProg : Cost.PolyTimeFun (Cost.Prog × Cost.Prog × ℕ × ℕ) Cost.Prog
• lenProg_eq (S : CL.Sampler ℓ) (L : Decider) (lam tau : ℕ) : self.lenProg.toFun (S.prog, L.prog, lam, tau) = (self.len S L lam tau).prog
• compute : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog × Cost.Prog) × ℕ × ℕ) Cost.Prog

  The repeated linear-constraints processor, from the input programs and (λ, τ), in polynomial time.

• output : TailoredVerifier ℓ → ℕ → ℕ → TailoredVerifier ℓ
• output_sampler (V : TailoredVerifier ℓ) (lam tau : ℕ) : (self.output V lam tau).sampler = self.sampler V.sampler lam tau
• output_len (V : TailoredVerifier ℓ) (lam tau : ℕ) : (self.output V lam tau).len = self.len V.sampler V.len lam tau
• output_lp (V : TailoredVerifier ℓ) (lam tau : ℕ) : (self.output V lam tau).lp.prog = self.compute.toFun (V.progs, lam, tau)
• within (V : TailoredVerifier ℓ) (lam tau n : ℕ) (R : Budget) : V.Within n R → (self.output V lam tau).Within n { S := Polynomial.eval (arg lam tau n R V.size) self.bound, d := Polynomial.eval (arg lam tau n R V.size) self.bound, D := Polynomial.eval (arg lam tau n R V.size) self.bound, k := self.deg * (R.k + 1), B := Repetition.reps lam tau n * R.B }

  The complexity clause: within a polynomial of k(n), the input's budget and the input's description length, at degree deg (k + 1), with lengths at most k(n) times the input's.

• len_total (V : TailoredVerifier ℓ) (lam tau n : ℕ) : LenTotal V.len n (V.sampler.dim n) → LenTotal (self.output V lam tau).len n ((self.output V lam tau).sampler.dim n)

  The repeated calculator halts where the input's does.

• completeness (V : TailoredVerifier ℓ) (lam tau n : ℕ) : V.HasPerfectZPC n → (self.output V lam tau).HasPerfectZPC n

  Completeness.

• soundness (V : TailoredVerifier ℓ) (lam tau n B : ℕ) (ε : ℝ) : 0 < ε → ε ≤ 1 → LenBound V.len n B → V.valStar n ≤ 1 - ε → (self.output V lam tau).valStar n ≤ Repetition.soundBound self.c ε (Repetition.reps lam tau n) B

  Soundness. For an input whose lengths are at most B, val*(𝒱_n) ≤ 1 - ε gives val*(𝒱^rep_n) ≤ exp(-c ε^13 k(n) / (B + 1)); the constant absorbs the factor between the bound on each kind of variable and the bound on the answers.