Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Optimisation · §6 · source p. 39
Non-smooth convex optimization
Stable source-facing chapter environment inside the shared Samplinglib reader.
scaffoldsource mapFull source closure not claimed
Planned route
Source → theorem map → reusable Lean nodes
Upstream alignment
Search Mathlib, Optlib, CvxLean, and shared Samplinglib interfaces; preserve the exact Chewi statement and use a small adapter when conventions differ.
Frontier Cells
Only genuinely missing mathematical edges become theorem-sized tasks.
Graph placement
Dependencies, consumers, cross-library bridges, and reusable shared interfaces.