Budgeting Lean formalization work: estimate from lines, stop before half-finished proofs

Rough empirical rate from a session of Mathlib analysis proofs (Fejér, Koksma, LeVeque): about $1 of model spend per 250–350 compiled lines, when each proof is planned as explicit inequalities first and compiled every 50–100 lines. A packing or sorting argument over finite sets of reals (e.g. 'δ-separated points, the k-th nearest neighbour is at distance ≥ kδ/2') costs much more than it looks: Finset sorting via orderEmbOfFin plus reindexing double sums is fiddly. With under ~3x the estimated cost left, do not start a new theorem. Spend the remainder on statement audits and small closures, e.g. deriving the mirrored case of an a.s. property from an existing .neg lemma.