{"id":"palomar/PALOMAR-2026-10-04-000001","url":"https://github.com/lennrt/palomar-formalizations/tree/636768718796b33b36d344d04b8e5f2f840633dd/zenodo-23125523/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-04-000001-v1.json","repo":"https://github.com/lennrt/palomar-formalizations","tags":["math.CO","cs.IT","msc:05C12","msc:05C69","combinatorics","coding-theory","distance-sets","lean-formalization"],"score":0,"title":"Distance-Shell Tomography: Geometric Certificates for Fault-Tolerant Sensing, Moment Compression, and Hypercube Equalization","trust":"high","domain":"math.CO","source":"palomar","authors":["Lennart Rudolph"],"reviews":0,"subject":"math.CO","summary":"Substantive Lean development for labelled distance-shell observations of anonymous integer populations. The focused 14-statement interface covers six result groups. Square grids have an exact four-corner interval-cut characterization of recovery of all populations of mass at most two after one erased report, an equivalent distance-sum compression contract, and exact corner-constrained optimum ceil(3(n+1)/2) for every n at least 3. For every positive q, the actual-distance equalizer cardinality of Q_(4q) lies between 2^(4q-1)+2q-1 and 2^(4q-1)+2q; explicit prefixes also give the infinite…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-04","reactions":{},"formalized":true,"formalizes":[{"title":"Distance-Shell Tomography: Geometric Certificates for Fault-Tolerant Sensing, Moment Compression, and Hypercube Equalization","identifier":"doi:10.5281/zenodo.23125523","relationship":"formalizes"},{"title":"Distance-Shell Tomography on Graphs: Integer Trades and Optimal Grid Sensing","identifier":"doi:10.5281/zenodo.22404456","relationship":"adapts"}]}