Gap-preserving compression of tailored verifiers, as a hypothesis

Paper II of the Aldous–Lyons track (Bowen–Chapman–Vidick, arXiv:2501.00173), Theorem thm:compression (II:1852), proved as thm:h_level_compression (II:5643), in the value form that the paper's Remark II:1876 calls the content of its proofs; the plan is planning/aldous-lyons-track.md, §4.1 and §4.4. The structure TailoredGapCompression ℓ is the data the theorem provides, as MIPRE.GapCompression is for the existing pipeline; its inhabitation is the theorem (Phase 5 of the plan, from the three stage contracts of MIPRE.Tailored.Stages), and the halting reduction is to consume it (Phase 1).

What differs from MIPRE.GapCompression:

• the verifiers are tailored, so the output has two components depending on λ only — the sampler S^λ and the answer-length calculator L^λ — and the compression procedure computes the linear-constraints processor;
• the answer-length calculator never fails on the sampler's questions (len_total, the paper's "never decodes to error", II:1863), which the halting protocol spends once (II:1965, item 3: when the machine has halted, the game accepts every well-formatted answer);
• the lengths it outputs are bounded (len_bound), in place of output_rejects_long: the canonical decider rejects every answer of another length;
• completeness is read in perfect Z-aligned permutation strategies commuting along edges (TailoredVerifier.HasPerfectZPC), not in PCC strategies;
• soundness is the value form, as there: val*(𝒱_{2^n}) ≤ 1/2 gives val*(𝒱'_n) ≤ 1/2. The paper states it in entanglement form, Ent(𝒱'_n, 1/2) ≥ max{Ent(𝒱_{2^n}, 1/2), 2^{2^{λn}-1}}, which needs the anchored parallel repetition theorem and the almost-synchronous rounding; the plan's §4.1 records why the value form is taken, and how the halting argument then gets its base case from Lin's search branch instead.

The level ℓ is a parameter: the fixed point of the halting protocol has input and output at the same level, that of S^λ.

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

Gap-preserving compression of tailored verifiers (II:1852, value form): the data of a compression procedure together with the guarantees of the theorem. An instance of this structure is the theorem.

• C₀ : ℕ

  The universal constant above which the guarantees hold.

• sampler : ℕ → CL.Sampler ℓ

  The compressed sampler S^λ, depending only on λ.

• samplerProg : Cost.PolyTimeFun ℕ Cost.Prog

  Its program, computable from λ in time polynomial in the length of λ.

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

  The compressed answer-length calculator L^λ, depending only on λ.

• lenProg : Cost.PolyTimeFun ℕ Cost.Prog

  Its program, computable from λ in time polynomial in the length of λ.

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

  Compress: from the three programs of a tailored verifier and λ, the program of the compressed linear-constraints processor, in polynomial time.

• output : Cost.Prog × Cost.Prog × Cost.Prog → ℕ → TailoredVerifier ℓ

  The output on any input is a tailored verifier with the compressed sampler, the compressed answer-length calculator and the compressed linear-constraints processor.

• 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.compress.toFun (V, lam)
• bound : Polynomial ℕ

  The polynomial poly(n, λ) bounding the running times of the output at index n, the dimension of the compressed sampler, and the lengths.

• deg : ℕ

  The degree, in the size of the input, of the running times of the output.

• sampler_time (lam n : ℕ) : (self.sampler lam).TimeBoundAt n (Polynomial.eval (n + lam) self.bound) self.deg
• sampler_dim (lam n : ℕ) : (self.sampler lam).dim n ≤ Polynomial.eval (n + lam) self.bound
• len_time (lam n : ℕ) : (self.len lam).TimeBoundAt n (Polynomial.eval (n + lam) self.bound) self.deg
• lp_time (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam n : ℕ) : (self.output V lam).lp.TimeBoundAt n (Polynomial.eval (n + lam) self.bound) self.deg
• len_bound (lam n : ℕ) : LenBound (self.len lam) n (Polynomial.eval (n + lam) self.bound)

  The lengths are at most poly(n, λ).

• len_total (lam n : ℕ) : LenTotal (self.len lam) n ((self.sampler lam).dim n)

  The answer-length calculator halts on every question of the sampler.

• completeness (V : TailoredVerifier ℓ) (lam n : ℕ) : V.IsBounded lam → self.C₀ ≤ n → V.HasPerfectZPC (2 ^ n) → (self.output V.progs lam).HasPerfectZPC n

  Completeness. For a λ-bounded input and n ≥ C₀: a perfect Z-aligned permutation strategy commuting along edges for 𝒱_{2^n} gives one for 𝒱'_n.

• soundness (V : TailoredVerifier ℓ) (lam n : ℕ) : V.IsBounded lam → self.C₀ ≤ n → V.valStar (2 ^ n) ≤ 1 / 2 → (self.output V.progs lam).valStar n ≤ 1 / 2

  Soundness, value form. For a λ-bounded input and n ≥ C₀: val*(𝒱_{2^n}) ≤ 1/2 implies val*(𝒱'_n) ≤ 1/2.