General sampling lower bound
A paper-first mathematical case study: read the theorem, the derivation route, and the hidden prerequisites before opening formal infrastructure.
Open problem
Matching lower bound not currently known in the pinned literature trail
No finite matching rate is asserted by the pinned literature record.
Reading. The useful mathematical content is the missing matching rate under exactly this setting and accuracy notion.
Open problem: SampleWiki records the matching result as unknown. ASTIS shows the target regime but does not manufacture a theorem or rate.
No theorem, hence no synthetic proof
There is no matching source theorem here, so there is no source proof to reproduce. The absence itself is part of the frontier.
What must be true before the rate can be read
Model and geometry
- The target is supported on a convex body and access is through the membership-oracle model fixed by the source setting.
- Geometric quantities such as radius, warmness, and any Gaussian-annealing parameter keep the normalization used by the cited paper.
- The displayed divergence/accuracy target is part of the theorem contract, not an interchangeable metric.
Analytic / proof prerequisites
- No additional hypothesis is introduced merely to turn the open lower-bound question into a theorem.
ASTIS rigorous LaTeX
No audited theorem-level LaTeX is asserted beyond the open-problem description.
Lean formalization
This fold is intentionally quiet while the source statement, proof route, and assumptions are being completed case by case. A source-facing Lean theorem will appear here only after it compiles and its statement has been matched to the audited source.
References and provenance
ASTIS-SW-SETTING-CONVEX-BODY-MEMBERSHIP-LOWER-UNKNOWN-GENERAL-SAMPLING-LOWER-BOUND · source snapshot c6e6860a0fdc6297