B A hypothesis atlas
On this page · Permalink · Source line 2
A longer monograph is useful only if the reader can locate the theorem that answers the actual question. This atlas groups the main obligations by the desired conclusion. The references lead to the statements and proofs, not just to examples that resemble the intended application.
B.1 Existence and identification
On this page · Permalink · Source line 5
| Desired conclusion | Data and hypotheses to establish | Main entry |
|---|---|---|
| A coherent family | A view system with its actual restrictions and all compatibility equations. Nonemptiness is separate. | 1.3–1.5 |
| A prescribed extension | The declared partial section and an actual vanishing relative obstruction, or matching data on a transition cover. | 2.1, 3.2, 4.1 |
| A unique extension | Existence and vanishing of the invisible coherent ambiguity, not existence alone. | 3.3, 11.4 |
| An infinite point from finite views | A sequential inverse system with nonempty finite fibers, or another proved lifting/compactness hypothesis. A prescribed value must lie in the persistent image. | 35.1, 35.2 |
| Descent of objects and witnesses | The actual groupoid data, coherent overlap isomorphisms, and a composition-covering family on the specified site. | 12.1–13.2 |
| Invariance of a boundary problem | An identified boundary and the specified comparison equivalences. Literal freezing of every representative is a different construction. | 14.3–14.4, 15.1 |
| The same limit from two paths | Convergence of both paths in a metric space and a pairwise distance budget tending to zero. | 24.4 |
B.2 Approximation and numerical meaning
On this page · Permalink · Source line 18
| Desired conclusion | Data and hypotheses to establish | Main entry |
|---|---|---|
| An exact limit of approximations | Completeness, a nonnegative lower semicontinuous residual, vanishing residuals, and summable candidate movement. | 24.1–24.2 |
| A protected exact limit | In addition, continuity of the protected map and preservation along the candidate path. | 24.3 |
| Exact cancellation from zero floor | Closedness of the actual admissible residual image. Without it only closure membership follows. | 25.1–25.2 |
| A stable residual-to-distance bound | The required closed range or bounded inverse in the declared normed model. In a protected problem, use the restriction to \(\ker p\). | 18.2, 18.3 |
| A controlled moving exact space | Two residual certificates, or a proved split-surjective regime with the strict smallness condition. Norm closeness alone does not preserve rank. | Section 21 |
| An independent object distance | An arrow category and an extended nonnegative cost with zero identity cost and composition subadditivity. Separation is another question. | 23.1–23.2 |
B.3 Bounded budgets, regularization, and solver certificates
On this page · Permalink · Source line 30
Every entry has a printed proof. Formal coverage includes the bounded-budget, regularization-limit, noise, solver-certificate, coordinate-invariance, and stopping results under their stated hypotheses. The explicit infinite diagonal estimates, asymptotic budget constant over all real budgets, and rounded noisy rate also have formal counterparts. The formal-source appendix gives the precise correspondence.
| Desired conclusion | Data and hypotheses to establish | Main entry |
|---|---|---|
| An exact answer from bounded approximations | A fixed bounded linear equation between real Hilbert spaces, residual convergence, and a uniform correction bound. | 27.2 |
| Strong convergence of finite repairs | Nested nonempty closed affine constraints, minimum norm answers, and a uniform energy budget. | 27.3 |
| A sharp finite-budget exclusion | The correction ball, the restricted adjoint, and a dual witness in the unit ball. | 28.1–28.2 |
| Robustness to model uncertainty | A fixed correction space and certified operator and data error bounds. | 28.3 |
| A unique protected regularized answer | Positive regularization parameter and the actual Hilbert metric on the protected kernel. | 29.1–29.2 |
| A convergent regularization limit | Actual attainment of the projected datum, not merely its membership in the closure. | 29.3 |
| A noisy convergent answer | The same attained datum, vanishing parameter, and noise divided by the square root of the parameter tending to zero. | 29.4, 30.3 |
| A leading approximation-cost constant | The explicit diagonal model and a proof controlling its infinite Riemann-sum tails. | 30.1–30.2 |
| A certified inexact optimizer | Positive parameter, the actual normal residual in the protected Hilbert norm, or an exact primal and dual gap. | 31.1–31.2 |
| A basis-independent solver residual | A full independent kernel basis and its Gram inverse. The normal-equation coordinate residual is a covector. | 32.1 |
| A convergent stopping schedule | Attained projected datum and separate vanishing bias, rescaled data noise, and rescaled normal residual. | 32.2 |
B.4 Three questions before using a finite check
On this page · Permalink · Source line 47
First determine whether the tested object is the actual object in the theorem. A scalar simulation can illustrate an operator-valued statement without checking every dependent fiber. Next determine whether the test checks a universal finite domain or a selected finite range. Finally identify any limit that remains outside the computation.
The phase extension is exhaustively checked on its eight elements. The diagonal example is different: rational finite sums verify its displayed enclosures, while the proof of nonexistence uses the infinite square-summability condition. Calling both results simply “tested” would conceal the most important distinction.
The companion Lean guide records these scopes and identifies the checked examples. General source declarations are checked in the accompanying formal project. Printed examples and conceptual connections have only the formal coverage explicitly documented for them.