The compressor as a program, and the halting reduction from compression alone #
The last piece of obligation O4: the map (c, n) ↦ comprStr c n (λ(n)) as a polynomial-time
function of the ambient model (comprPoly), which exists_compressorSpec turns into a
CompressorSpec, hence into Obligations, hence — through halting_reduction — into the
halting reduction with no hypothesis but gap-preserving compression: halting_reduction_of
in val*, and halting_reduces_to_gameValue_of in the headline's gameValue.
The program writes λ(n) = 2 ^ (2 · size n) in binary by walking the bits of n twice with
lenBody, prepending a 0 per bit to the numeral 1 (lamProg); assembles (c, n, λ(n));
hardcodes it into haltProg with smnProg; pairs the parameter with the result; and serializes
the pair with serProg. Every stage is linear or quadratic in its input, so the whole is
quadratic in |c| + |n|.
The parameter in binary #
lamProg on encode n computes encode (2 ^ (2 · size n)): two walks over the bits of
n, each prepending a nil per bit to the accumulator, from the numeral 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The compressor's program #
The compressor: on encode (c, n), the parameter in binary, the triple (c, n, λ(n)),
its hardcoding into haltProg (smnProg), the pair (λ(n), decider), and its serialization.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The description of the hardcoded decider, as smnProg builds it.
The compressor computes its output.
The compressor, as a polynomial-time function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Obligation O4, discharged #
The compressor's specification is inhabited.
Obligation O4 is discharged, in every value model in which compression is sound:
Obligations ω G U is inhabited.
The halting reduction from gap-preserving compression alone, in val*.
The halting reduction in a value model, RE shape, from soundness of compression in the
model and a lower semidecider for its value.
The halting reduction in a value model, coRE shape, from soundness of compression in
the model and an upper semidecider for its value. At ValueModel.commuting this is
thm:halting-co, with commutingUpperRE as the semidecider.
The headline in both values, conditionally: from a GapCompression, one computable map
from machines to game descriptions whose game has synchronous value 1 and quantum value
1 when the machine halts on the empty input, and both values at most 1/2 when it does not.
halting_reduces_to_gameValue_of (blueprint thm:main) and halting_reduction_quantum_of
(cor:main-quantum) are its two halves, on the same map: the strings form of the reduction
(halting_reduction_lower_strings), tabulated, read in each value.
The headline, conditionally (blueprint thm:main from thm:compression): from a
GapCompression, a computable map from machines to game descriptions whose synchronous game
value is 1 when the machine halts on the empty input and at most 1/2 when it does not.
This is HaltingGameValue.halting_reduces_to_gameValue with the compression theorem as a
hypothesis; MIPRE/MainTheorem.lean supplies the compression and proves the unconditional
statement.
Halting reduces to the quantum value (blueprint cor:main-quantum), on the same map
as thm:main: the quantum value of the game is 1 when the machine halts and at most
1/2 when it does not.