The proof ledger: theorems, code, tests

The Lean development under proofs/lean/Rgmin/ pins the exact rational facts the solvers’ termination and honesty arguments rest on. It builds on Mathlib, so the statements are the real ones: widths and radii over the reals, `Real.sqrt` in the boundary root rather than a named-root hypothesis, actual limits for the termination envelopes, and the Gram positive-semidefiniteness of the sketch as a matrix theorem. Check it with lake exe cache get && lake build in proofs/lean/; the cache makes Mathlib a download, not a compile.

The division of labor is deliberate. The Lean side proves the exact algebra and the budget envelopes – facts about the formulas, true in every execution. The Rust tests hold the floating-point implementation to those facts at concrete tolerances. A claim without a row in both columns is an opinion.

Theorem (Rgmin.*)	Pins	Code	Rust test
guarded_above, guarded_below	zoom trials land in the interior band	linesearch/zoom.rs	the_cubic_zoom_keeps_the_evaluation_budget
zoom_shrinks	bracket loses >= 10 percent per step	linesearch/zoom.rs	(same)
width_envelope, _tendsto	geometric width envelope, and it reaches zero	linesearch/zoom.rs	(same)
armijo_strict	an accepted point strictly improves	linesearch/conditions.rs	armijo_and_curvature_match_xtsci
boundary_on_sphere	the boundary root lands on the trust sphere	hvp.rs::boundary_tau	negative_curvature_walks_to_the_trust_boundary
boundary_tau_nonneg	a boundary exit never retracts	hvp.rs::boundary_tau	(same)
ray_further_is_lower	negative curvature: boundary is optimal greed	hvp.rs::steihaug_pcg	(same)
step_scale_invariant	CG step ignores preconditioner scale	hvp.rs::steihaug_pcg	nystrom_flattens_a_decaying_spectrum
beta_scale_invariant	conjugacy weight ignores preconditioner scale	hvp.rs::steihaug_pcg	the_preconditioned_boundary_lives_in_the_sketch_metric
metric_update_scales	tracked M-norm recurrence is scale-consistent	hvp.rs::steihaug_pcg	(same)
shrink_ge_floor, shrink_pos	the trust radius stays positive	trust.rs::update_radius	hvp.rs suite
shrink_strict, collapse_envelope, collapse_tendsto	rejections decay the radius to any floor	hvp.rs::minimize_newton_cg	TrustCollapsed paths
grow_le_cap, grow_ge	growth is capped and never loses ground	trust.rs::update_radius	dogleg_stays_on_the_trust_sphere
rejection_propagates	an uphill step cannot be accepted	trust.rs::reduction_ratio	an_uphill_everywhere_oracle_is_refused_not_moved
sketch_posSemidef, sketch_form_nonneg, sumSq_nonneg	the Gram sketch is PSD, as a matrix theorem	hvp.rs::NystromPrecond	nystrom_flattens_a_decaying_spectrum
shifted_weight_pos, equalized_weight_bounds	the solve’s weights are positive, damping only	hvp.rs::NystromPrecond::solve	(same)

The narrative behind each block lives in the explanation pages: the line search, the secant family, trust regions and Steihaug, the Nystrom preconditioner, scaled conjugate gradients.