claimroutine

Quantized acceptance tests with a history predictor

Claim·§4.3 Excluding bounded total variation·inside propTotal variation S cannot stay bounded

Statement (paper)

Let 0<τ<min⁡(1,r4128B5)0<\tau<\min\left(1,\frac{r^4}{128B^5}\right), and encode each point at an embedding by quantizing the real and imaginary parts of Zp,WpZ_p,W_p in [−B−1,B+1][-B-1,B+1] into half-open intervals of length at most τ\tau, with an overflow code outside this box; this is a finite alphabet of size M=M(B,τ)M=M(B,\tau) independent of tt and of the field degree, and the acceptance test at qq (whether the point code is attained by some actual neighbor of qq) is always passed by the actual point on an edge. Then for K→∞K\to\infty with K=o(log⁡t)K=o(\log t) and D/K→0D/K\to0, there is a fixed strict-prefix history map HH with at most MK−1=to(1)M^{K-1}=t^{o(1)} values for which the predicted acceptance failure at a fresh uniform embedding is o(1)o(1), and the geometric error bounds already proved remain valid for this HH.

In plain English

Quantize the real and imaginary parts of Zp,WpZ_p,W_p into cells of length at most τ\tau, with τ<min⁡(1,r4/(128B5))\tau<\min(1,r^4/(128B^5)), to get a finite code alphabet of size M(B,τ)M(B,\tau) with acceptance tests that real edge points always pass. For K→∞K\to\infty with K=o(log⁡t)K=o(\log t) and D/K→0D/K\to 0, there is a strict-prefix history map HH with at most MK−1=to(1)M^{K-1}=t^{o(1)} values whose predicted acceptance failure at a fresh uniform embedding is o(1)o(1), and the earlier geometric error bounds still hold for this HH.

Why it's here

The claim applies the prefix-history corollary to the quantization tests. The true code has acceptance-failure rate s0=0s_0=0, so the predicted code fails only 4M(D/K)1/4=o(1)4\sqrt M(D/K)^{1/4}=o(1) of the time, because MM is fixed and D=o(log⁡t)D=o(\log t) by the wedge-law entropy bound. This gives a small history HH whose predictions nearly always pass the tests, which the next claim uses to find a positive-probability outcome with the tests passed and the points separated.
Classified routine:
A direct application of the paper's prefix-history prediction corollary (pred-acceptance) to a quantized finite alphabet, combined with the wedge-law entropy bound D=o(log t). The quantization and parameter choices are bookkeeping.

Uses

lemWedge law has tiny atoms and small informationcorPrefix history predicts acceptance failures

Used by

claimPositive-probability good outcome exists

Sources

PaperOpen
Section
§4.3 Excluding bounded total variation
Page
—
Label
—
Line
sections/03-heights.tex:286
Leannot aligned

Phase 2 aligns this node to a Lean declaration.