# Quantitative trace-reconstruction bounds with a uniform decoder The following describes the scope of the Lean formalization related to the following accompanying paper(s): - [Quantitative lower bounds for trace reconstruction](../../preprints/quantitative-lower-bounds-for-trace-reconstruction-September-24-2026/paper.pdf) ## Scope The formalization proves superpolynomial sample lower bounds for exact worst-case reconstruction of binary words from independent deletion traces, with unrestricted computation and any fixed positive success probability. For every fixed deletion probability $q\in(0,1)$, sample complexity grows faster than every fixed power of the word length; the minimum total-variation distance between two one-trace laws decays faster than every inverse power. More quantitatively, along sequences with $q^3\log n\to\infty$, the required number of samples is at least $n^{c\log(q^3\log n)}$ eventually for every fixed $0