Exact High-Rate Distortion for Random-Access Coding of Permutations

This preprint proves the exact finite high-rate rate-distortion curve for a uniform permutation encoded before a later random coordinate query. For n!/n <= M <= n!, the optimum average query error is 2(n!-M)/(n n!). The proof allows arbitrary function-valued decoders, gives a matching star construction for every integer message count, and shows that finite randomization does not improve the result. Lean 4 checks the theorem for every parameter in the stated range. The accompanying archive reproduces the formal proof, exact finite controls, machine-readable records, and paper build. The separate 256-byte calculation is specific to one frozen packet format. It does not claim a converse for arbitrary protocols, learned or heterogeneous-model key/value-cache transfer, or efficiency relative to text.