D Proof and formal verification
On this page · Permalink · Source line 2
The printed arguments and the accompanying Lean development have complementary roles. The text explains constructions and their mathematical context. A Lean declaration fixes a precise statement whose proof is checked by the kernel. A correspondence between them records the actual hypotheses and conclusion, while allowing the formal proof to use a different route.
All 16 principal theorem groups on bounded realization, budgets, regularization, and certificates have complete formal counterparts. The table identifies these statements by their numbers in the main text. This coverage concerns the stated results, rather than every proof route or illustrative calculation.
| Result | Topic | Formal counterpart |
|---|---|---|
| 27.2 | Bounded approximate feasibility | Verified |
| 27.3 | Nested affine minimum corrections | Verified |
| 28.1 | Attainment and shape of the budget profile | Verified |
| 28.2 | Sharp budget certificate | Verified |
| 28.3 | Robust budget comparison | Verified |
| 29.1 | Unique regularized correction | Verified |
| 29.2 | Parameter and budget comparison | Verified |
| 29.3 | Regularization limit alternative | Verified |
| 29.4 | Data sensitivity and convergent parameter choice | Verified |
| 30.1 | Infinite diagonal family and certified tails | Verified |
| 30.2 | Sharp diagonal budget asymptotic | Verified |
| 30.3 | Rounded noisy diagonal rate | Verified |
| 31.1 | Normal-residual solver certificate | Verified |
| 31.2 | Regularized primal and dual gap | Verified |
| 32.1 | Coordinate certificate and arbitrary basis change | Verified |
| 32.2 | Consistent inexact stopping rule | Verified |
D.1 Bounded realization and budget geometry
On this page · Permalink · Source line 27
The formal bounded-realization theorem concerns bounded linear maps between real Hilbert spaces. It gives an exact preimage within the same norm bound as the approximating corrections. Its proof uses compactness of a dual ball and the Riesz isometric equivalence. The printed proof uses the weak-subsequence lemma, Lemma 27.1, whose particular proof route is not separately formalized here. Neither route requires separability or closed range. Neither asserts strong convergence of the original approximating sequence.
The nested-constraint theorem constructs the minimum-norm points of nonempty closed affine sets. It proves the exact energy identity, norm monotonicity, and the equivalence between a nonempty intersection and bounded minimum norms. Under that bound, the corrections converge strongly to the unique minimum-norm point of the intersection. If the intersection is empty, their norms tend to infinity. The affine assumption is retained: for general convex sets the corresponding energy statement is an inequality.
| Namespace | Representative declarations |
|---|---|
BoundedApproximateRealization | exists_solution_of_bounded_residual_tendsto_zero mem_range_iff_bounded_approximation norm_tendsto_atTop_of_not_mem_range |
NestedMinimumCorrections | nested_affine_energy nested_affine_intersection_iff_bounded nested_affine_strong_realization nested_affine_escape |
ProtectedBoundedRealization | exists_exact_repair_of_bounded_approximation |
All namespaces in this appendix have the prefix KomorebiSpace. The protected application uses the actual subtype \(\ker p\) with its inherited Hilbert norm. It constructs a repaired candidate preserving the declared observable and the original correction budget.
The budget-profile theorems concern bounded operators between real complete Hilbert spaces. The budget is nonnegative and may be zero. Attainment of a residual minimum over a bounded correction ball does not require the entire operator range to be closed. The sharp support formula supplies an actual maximizing witness, expressed formally by IsGreatest. It does not infer attainment from the mere existence of a supremum.
| Namespace | Representative declarations |
|---|---|
BudgetProfile | exists_budget_minimizer beta_eq_iInf beta_tendsto_floor beta_eq_floor_iff beta_eq_zero_iff |
BudgetProfileGeometry | beta_antitone beta_zero beta_convex_combination beta_profile_bounds |
BudgetDuality | dualValue_le_beta exists_attaining_dual_witness sharp_budget_duality strict_exclusion_certificate |
BudgetRobustness | candidate_residual_le beta_abs_sub_le nominal_dual_lower_certificate excludes_budget_of_nominal_dual_certificate |
The robustness comparison uses the same correction space for both problems. Its bound \(\delta+\eta M\) controls data and operator uncertainty at budget \(M\). A changing protected kernel is a different problem and is not covered by that estimate.
D.2 Regularization, noise, and stopping
On this page · Permalink · Source line 52
For positive parameter \(\alpha\), the regularized normal operator is constructed as a continuous linear equivalence. Its inverse defines the correction. The formal development proves uniqueness, the energy identity, parameter monotonicity, budget optimality, and the two data-sensitivity estimates. The fixed-space protected application uses the restricted operator and its actual adjoint.
The limit theory distinguishes projection onto the closure of the range from membership in the range itself. Fitted values converge to the projected datum and residual norms converge to the irreducible floor. If that projected datum is attained, the corrections converge in norm to its unique minimum-norm preimage. Otherwise their norms tend to infinity. The data and stopping theorems use this limit theorem together with their explicit parameter, noise, and solver-tolerance assumptions.
| Namespace | Representative declarations |
|---|---|
RegularizedHilbertRepair | exists_unique_minimizer energy_identity residual_best_at_budget parameter_norm_antitone parameter_residual_monotone data_noise_bound data_fitted_bound |
RegularizationLimits | fitted_tendsto_projectedDatum residual_norm_tendsto_floor weighted_penalty_tendsto_zero norm_tendsto_atTop_of_not_mem_range |
RegularizationStrongLimit | exists_unique_minimum_and_limit |
RegularizationNoiseLimits | data_noise_coefficient_attained noisy_parameter_choice inexact_parameter_choice stopping_rule_sequence |
The stopping theorem compares proposals, exact regularized corrections, and the intended minimum correction in one fixed Hilbert model. It includes the pointwise three-term bound and the convergence conclusion. Protection is exact at every index. The explicit diagonal schedule at the end of Section 32 combines this solver bound with the formalized noisy rate in Corollary 30.3. The declaration DiagonalRegularization.diagonal_inexact_rounded_rate proves this specialization with the literal ceiling, the data-noise hypothesis, and the actual measured-data normal-residual bound. The exact-data bias estimate is derived rather than assumed.
D.3 Certificates and their coordinate metric
On this page · Permalink · Source line 67
The solver certificate controls correction error, fitted error, and objective excess through the actual Hilbert normal residual. The primal and dual identity supplies objective bracketing and a correction-distance bound for an arbitrary dual witness. These are universal statements over the declared Hilbert spaces, with \(\alpha>0\) wherever coercivity is used.
| Namespace | Representative declarations |
|---|---|
RegularizedHilbertRepair | correction_error_bound fitted_error_bound objective_gap_bound |
RegularizationCertificates | primal_dual_gap dual_maximizer gap_controls_correction residual_witness_gap |
CoordinateCovector | gram_isUnit protected_coordinate_certificate computed_normalResidual_changedBasis computed_certificate_changedBasis changedBasis_coordinates |
The coordinate certificate uses a basis of the entire permitted correction space, with its inherited Hilbert metric. The proof derives invertibility of the Gram matrix from that basis, identifies the coordinate residual with the pairings of the Hilbert normal residual, and proves
Every invertible basis change is allowed. The changed coordinates describe the same correction, the residual transforms as a covector, and the displayed squared norm is invariant. The proof includes the zero-dimensional correction space. It does not replace the Hilbert norm by a coordinate supremum norm or assume that the basis is orthonormal. These metric identities hold for every real \(\alpha\). The optimizer estimates still require positive \(\alpha\).
D.4 The infinite diagonal example
On this page · Permalink · Source line 83
Proposition 30.1, Theorem 30.2, and Corollary 30.3 have formal counterparts in the namespace KomorebiSpace.DiagonalRegularization. The formal space is the real Hilbert space lp at exponent two. Its natural index starts at zero, so formal coordinate \(j\) denotes printed coordinate \(n=j+1\). The operator, data, corrections, residuals, and hard prefixes are elements or maps of that actual infinite space.
The first pair identifies the universal regularized correction, proves it is the unique global minimizer, equates the infinite squared norms with \(A_m\) and \(B_m\), and proves all four global bounds and both nonnegative omitted-tail bounds. The asymptotic theorem proves both scalar limits, the budget-profile limit \(\pi/4\) over all real \(M\) tending to infinity, and the hard-prefix comparison with constant one. Its budget conclusion is not restricted to the regularization mesh.
The noisy theorem uses the actual attainable datum and its minimum-norm preimage. It retains the literal ceiling in \(m=\lceil\delta^{-2/3}\rceil\) and proves both displayed inequalities for every Hilbert perturbation within the stated noise bound. The bias estimate is derived within the model. The inexact rate adds the stated solver tolerance to this same model and parameter choice.
The range obstruction uses actual unit coordinate vectors with residual norm \(1/(j+1)\) and applies the general unit-witness theorem. The hard-prefix images converge in Hilbert norm to \(w\), placing it in the closure of the range. An exact preimage would have every coordinate equal to one, contradicting square summability. These declarations formalize the concrete example following Theorem 18.2. Exact finite enclosures remain separate illustrations of the infinite results.
D.5 Verification record and trust boundary
On this page · Permalink · Source line 101
The source contains 166 compilation targets (162 production modules and 4 entry points), 1,859 explicit theorem or lemma declarations, and 5,339 exported declarations. The latter includes definitions and generated helpers; neither count measures independent mathematical discoveries.
Fresh compilation treated warnings as errors and disabled automatic implicit parameters. The complete declaration audit checked defining modules and recursive axioms, rejecting unsafe declarations and project-specific axioms. Source, compiler, cache, and generated-object identities bind this replay.
All 56 diagnostic controls had their specified outcomes: 18 successes, 35 intended elaboration rejections, and three axiom-policy rejections. The 52 inherited controls were rerun alongside four new controls. Earlier records remain historical.
The environment is Lean 4.34.0-rc2 with mathlib commit aeb72f1e9981b6d35b426b16dca7759be3e7ba06. Permitted axioms are propext, Classical.choice, and Quot.sound. Lean's compiler and kernel and the pinned external dependency cache remain trusted; the cache was recorded but not rebuilt. Finite executable examples provide separate computational evidence; they are not verified extractions of the Lean proofs.