Compress, Explained

Write V for a verifier — a program that, given an index n, samples a pair of questions and then decides whether a pair of answers is acceptable. The paper's compression machine is a composition:

The analytic document opens with a machine so small it fits in five rows: M₌, which reads one bit off each of two input tapes and writes their equality bit to an output tape. It has two non-halting states and one halting state, four tapes, and a catch-all row that makes the table total. On legal one-bit inputs it halts after exactly three transitions.

The self-referential verifier at the heart of the Halting reduction is a fixed point. In the lambda calculus that is Y = λF.(λx.F(xx))(λx.F(xx)): no recursive name appears anywhere in the syntax, and recursion is produced when two copies meet. The project's evaluator is deterministic call-by-value, so its constructor must behave like the eta-delayed Z, and the implementation closes a single self_code hole rather than materialising the unfolding.

Evaluation is a deterministic call-by-value CEK machine with a fuel counter. One charged transition is one fuel unit, so a bounded trace has exactly one row per unit spent. Running out is not an error — it is the outcome OutOfFuel, alongside Value and SortError. The evaluator never throws.

This is the requirement that shapes the whole prototype. Compress must measure a verifier's length, substitute static parameters into it, and emit new code — so a runtime function value will not do. Every sampler in the package is therefore asked four questions, and a sampler that cannot answer them from its own bytes is returned as NotDescribable rather than silently working.

This is the structural constraint the whole construction is organised around. A conditionally linear map of level ℓ splits the ambient space into ℓ factor registers; it reads the first, applies a linear map to it, and only then chooses the linear map for the second. For (q,m,d) = (8,2,1) the ambient space is V_pt ⊕ V_coord ⊕ V_dir, of dimension 5, and the three maps of the low-degree test sit at levels 1, 2 and 3.

The decider D^ld sees two typed questions and two answers. If the types are equal it demands equal answers. If one is a point and the other a line through that point, it demands that the line polynomial has degree at most d (axis) or md (diagonal) and that evaluating it at the point reproduces the point answer. If nothing applies, it accepts.

Tseitin turns a circuit into a formula by giving every gate a wire variable and asserting each gate's local relation; arithmetization turns that formula into a polynomial by sending ∧ to ×, ¬ to 1−·, and ∨ through De Morgan. The arithmetization of a formula tree is multilinear in its leaf occurrences, so a variable's individual degree is bounded by how many times it appears — which grows with the fan-out of the gate that produced it.

The PCP's central object is a polynomial c₀ built so that it vanishes on {0,1}ⁿ exactly when the underlying circuit is satisfied. Vanishing on the cube is equivalent to lying in the ideal generated by z_i(1 − z_i), so the prototype divides c₀ by that ideal and keeps the quotients as part of the proof. If the division leaves a remainder, no certificate is issued.

The proof string is Π = (g₁,…,g₅, c₀, c₁,…,c_{m′}): five low-degree extensions of the witness blocks, the composite polynomial, and its quotients. The verifier picks a random point, restricts the proof to axis-parallel and diagonal lines through it, checks degrees, and then checks two algebraic identities — the formula test and the zero-on-subcube test. Everything below is measured on the six-gate instance.

Answer reduction replaces long answers with short ones by making the provers answer a PCP about their own long answers. The verifier's question type set becomes a product: each of the three oracularised roles (alice, bob, oracle) carries the eighteen PCP question types {Point_i, ALine_i, DLine_i}_i=1..6. The decider is a dispatch table over the resulting 54 types, and the striking fact is how sparse it is.

This is the rung that makes the pipeline real: the decider is quoted to canonical bytes, evaluated under fuel to produce a bounded trace, the trace is turned into succinct 3SAT by a Cook–Levin encoding, the shared 3SAT data is decoupled into five blocks, the result is padded and compiled to a circuit, and that generated circuit goes through the same PCP builder chapter 8 used — and then through chapter 10's decider.

executed at TB6 — C14 TESTED (scoped); critic round 4 pending

Everything in this chapter is transcribed into docs/DESIGN.md §11 with source line references, and as of TB6 it runs: the Pauli sampler and decider, the introspection sampler (typed, then downsized and detyped to level 5 with dimension 142 on fixture E and 179 on fixture M), and the introspection decider, which reads the input verifier only through the four sampler queries on the paper's schedule and meters every child call in units of one primitive interpreter step. Under the paper's budget R = N^λ every honest child call on fixture M times out at exactly 16 steps — so acceptance under the source gate is withdrawn, printed as toy_child_fuel = FAIL(owner=tb6-child-meter) — and under the explicit toy budget of 65,536 steps every call returns (measured costs 5 to 60 steps per mode). The honest strategy is simulated exactly on a stabilizer tableau of 6 (E) and 26 (M) qubits; every one of the 14,378 enumerated outcomes on E carries an exact dyadic probability (structural to the enumerator, so total mass one is an identity and not evidence). The paper's literal ≥ 3Q guard rejects exactly 10 of 116 and 22 of 128 oriented type pairs, which is why the operative guard reads > 3Q. Two further places where the source as written does not typecheck surfaced as red tests and are carried as SOURCE_REPAIR nodes (the dual-map complement and the hiding suffix register); both are disclosed and repaired in the C14 row. It is here because it is the piece that makes compression exponential: a verifier of index n would need 2ⁿ-bit questions, so instead the provers are made to generate their own questions from shared randomness, and the verifier checks the generation with a Pauli test.

executed at TB5 — C13 TESTED (scoped), C12 TESTED

Each stage of Compress degrades the soundness gap, so the last stage restores it by running k(n) copies in parallel. Anchoring comes first: a second question type whose only legal answer is the canonical bit 0, which gives the repetition theorem the structure it needs. TB5 built both as description-level transformations: the anchored sampler on the V_copy fixture has level 3 and dimension 9, the 81-fold repetition is one compact loop term of 85 bytes whose size does not change with k, the repeated decider computes the component bound before reading any payload and rejects an oversized component with an empty child-call log, and two byte-distinct deciders yield the identical repeated-sampler hash. What stays CITED is exactly what the paper proves analytically: PCC completeness and the entanglement relation of thm:repetition.

checkpoint: executes under a toy policy — critic verdict pending (C15 CONJECTURE)

Each rung of the ladder is written by a proposer and then attacked by a critic that recomputes the numbers independently. The critic files a verdict with numbered objections; the proposer repairs; the next critic adjudicates the repairs and files fresh objections. A claim's status moves up only inside such a verdict — never because the author says so.

Nothing returns a bare number. A construction returns a Checked{T,C} — the term together with a certificate whose nodes are graded. verify_certificate replays every CHECKED node against the constructor's own sub-terms, and refuses a certificate borrowed from another proof with :certificate_binding. These are the two real trees the suite printed.