12.3 · Book p. 288 · PDF p. 300
Discretization Analysis
Decomposes generation error into initialization, score approximation, and numerical discretization terms.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward Time reversal identifies the exact reverse drift under regular marginal densities. 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
- A score is defined only with respect to a chosen density and representative.
- Reverse-time formulas require time-marginal regularity and a precise filtration statement.
- An L2 score approximation under one law cannot silently be used under another law.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.