9.2 · Book p. 234 · PDF p. 246
Query Complexity in One Dimension
Constructs one-dimensional hard instances and turns indistinguishability under queries into sampling lower bounds.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward One-dimensional constructions yield nontrivial smooth log-concave sampling lower bounds. The declaration-level source map is intentionally left inside the formalization layer until exact theorem anchors have been audited.
Why is this valid?
Chapter-level validity conditions
- The oracle transcript and algorithmic randomization must be represented explicitly.
- Pairwise divergence bounds need the exact observation law.
- The hard family must remain inside the stated target class.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.