Three kinds of results, three scopes.
Numerical experiments
Tests measure behavior on specific functions, starting points and budgets. They do not prove convergence for every problem that has a root.
Mathematical proofs
The Lean statements concern exact identities and conditional bounds. They do not verify Python, NumPy or callback evaluation from end to end.
449 versus 448 campaign
Each configuration uses the same callback and starting point, without a supplied analytic Jacobian, and at most 6,000 physical evaluations. Three interleaved repetitions are performed; stable success requires three positive verdicts.
| Set | Configurations | 448 | 449 |
|---|---|---|---|
| Known set | 14,695 | 14,673 successes | 14,675 successes |
| Held-out seeds | 3,300 | 3,295 successes | 3,295 successes |
| Total | 17,995 | 17,968 successes | 17,970 successes |
No configuration solved by 448 is lost by 449 in this campaign. The total includes 25 configurations that still fail. The known configurations include development cases, historical tests, structural examples and targeted diagnostics; this is not a fully independent sample.
Root tests require a Euclidean residual no greater than 10−8. Least-squares modes and some MGH problems retain their historical judges, which can accept a positive objective. Success in those cases therefore does not necessarily mean a root.
Timings are sums of per-configuration medians, excluding preparation and judges: 46.600 s versus 46.602 s on the known set, and 7.950 s versus 7.928 s on the held-out set (449 versus 448). They depend on the machine and the cost of evaluating the functions.
Scope of the Lean 449 bundle
The bundle contains 100 unique statements, including two new results about the probe-budget reserve. It was checked with Lean 4.33.1 and Mathlib v4.33.1 in Docker, without sorry, admit, custom axioms or numerical oracles.
- Monotonicity of the quota policy with candidate accuracy.
- Preservation of reserved capacity under exact-count assumptions.
- Conditional mathematical identities and bounds inherited from earlier releases.
The |J|·ulp diagnostic remains a linearized heuristic. Exact residual certificates concern the returned binary64 values, rather than the complete error of an ideal mathematical function. No theorem of universal convergence within a finite budget is claimed.