Sufficient Resolution

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

1 \documentclass[11pt]{article}
2 \usepackage[letterpaper,margin=0.88in,headheight=15pt]{geometry}
3 \usepackage[T1]{fontenc}
4 \usepackage[utf8]{inputenc}
5 \usepackage{amsmath,amsthm,amssymb,mathtools}
6 \IfFileExists{newtxtext.sty}{\usepackage{newtxtext,newtxmath}}{\usepackage{lmodern}}
7 \usepackage{microtype,booktabs,longtable,tabularx,array,enumitem,xcolor,fancyhdr,titlesec,xurl}
8 \usepackage{hyperref}
9 \definecolor{Navy}{HTML}{17324D}
10 \definecolor{Teal}{HTML}{2F7A78}
11 \hypersetup{colorlinks=true,linkcolor=Navy,urlcolor=Teal,pdfauthor={Komorebi P.},
12 pdftitle={Sufficient Resolution: Exact Reduction, Hidden Memory, and Certified Reconstruction}}
13 \setlength{\parindent}{0pt}\setlength{\parskip}{4.2pt}
14 \setlist{itemsep=2pt,topsep=3pt,leftmargin=1.7em}
15 \allowdisplaybreaks
16 \pagestyle{fancy}\fancyhf{}
17 \fancyhead[L]{\small\textsc{Sufficient Resolution}}
18 \fancyhead[R]{\small Komorebi P.}\fancyfoot[C]{\thepage}
19 \titleformat{\section}{\Large\bfseries\color{Navy}}{\thesection}{0.7em}{}
20 \titleformat{\subsection}{\large\bfseries\color{Navy}}{\thesubsection}{0.6em}{}
21 \newtheorem{theorem}{Theorem}[section]
22 \theoremstyle{definition}\newtheorem{definition}[theorem]{Definition}
23 \newtheorem{example}[theorem]{Example}
24 \theoremstyle{remark}\newtheorem{remark}[theorem]{Remark}
25 \DeclareMathOperator{\Ran}{Ran}\DeclareMathOperator{\dist}{dist}
26 \DeclareMathOperator{\End}{End}\DeclareMathOperator{\id}{id}
27 \DeclareMathOperator{\spanof}{span}\DeclareMathOperator{\cl}{cl}
28 \newcommand{\RR}{\mathbb R}\newcommand{\QQ}{\mathbb Q}
29 \newcommand{\nn}[1]{\left\lVert #1\right\rVert}
30 \newcommand{\ip}[2]{\left\langle #1,#2\right\rangle}
31 \newcommand{\src}[1]{\par{\small\color{Teal}\textit{Formal source:} \path{#1}.}\par}
32 
33 % Operation Komorebi: shared publication profile.
34 \usepackage{komorebi-publication}
35 \renewcommand{\KomorebiTitle}{Sufficient Resolution}
36 \renewcommand{\KomorebiSubtitle}{Exact reduction, hidden memory, and certified reconstruction}
37 \renewcommand{\KomorebiSeries}{Research library}
38 \renewcommand{\KomorebiKind}{Traditional paper}
39 \renewcommand{\KomorebiEdition}{Standardized publication edition / 8 October 2026}
40 \renewcommand{\KomorebiShortTitle}{Sufficient Resolution}
41 \renewcommand{\KomorebiTitleSize}{38}
42 \renewcommand{\KomorebiTitleLeading}{43}
43 \renewcommand{\KomorebiProfile}{classical}
44 \renewcommand{\KomorebiOrientation}{portrait}
45 \KomorebiSetup
46 \begin{document}
47 \KomorebiCover
48 \KomorebiOpeningNote{\textbf{Reading set.} This traditional paper is accompanied by a visual guide,
49 a Lean guide, and the complete source ZIP. The ZIP includes the \texttt{.md}
50 files, editable manuscript sources, Lean sources, Python implementations,
51 example data, and verification records.\par
52 \medskip
53 \textbf{Scope.} Exact linear representation and behavioral reduction;
54 bounded discrete and continuous dynamics; real Hilbert reconstruction and
55 regularization; certified discrepancy rules; and calibration-based operator
56 allowances. Truth allowances and feasibility assumptions are stated explicitly.}
57 
58 \hypersetup{pageanchor=false}
59 
60 \hypersetup{pageanchor=true}
61 \pagenumbering{arabic}
62 \begin{abstract}
63 A representation is sufficient relative to an observation and a family of
64 permitted continuations. This paper develops that principle through exact
65 analysis and synthesis, hidden-return defects, behavioral quotients, finite
66 certificates, quantitative approximation, and certified inverse problems.
67 Split compression fails to preserve composition by an explicit hidden excursion;
68 for finite-dimensional hidden state, finitely many feedback moments decide
69 all-depth closure. Behavioral reduction retains precisely the distinctions that
70 some permitted future observation can detect. In real Hilbert settings,
71 compatibility, realizability, and source identifiability produce separate
72 obstructions and conditioning requirements. Canonical reconstruction,
73 Tikhonov regularization, discrepancy selection, inexact solves, changing
74 operators, and redundant calibration frames are assembled into a common chain
75 of contracts. Classical linear algebra and analysis provide the foundations.
76 The contribution of the assembled calculus is the explicit relation between
77 these contracts, their reusable certificates, and their sharp boundaries.
78 The paper consolidates sixteen development blocks and maps its principal
79 claims to existing Lean declarations. Finite rational implementations are
80 companion evidence and are not asserted to be formally verified.
81 \end{abstract}
82 \tableofcontents\newpage
83 \section{The problem and its mathematical contracts}
84 
85 Sufficiency depends on what a representation must support. A compression that
86 preserves today's observation can lose a distinction needed after a later
87 operation. A coordinate enlargement can be redundant yet exact. A compatible
88 local datum can still fail to have a global source. A small fitting residual
89 can coexist with large source error. These are distinct phenomena with
90 different mathematical witnesses.
91 
92 The paper follows two connected lines. The first is the reduction of known
93 linear dynamics relative to declared observations. The second is the
94 reconstruction of a source from bounded linear data with explicit error
95 allowances. The first yields an exact semantic state quotient. The second yields
96 metric reconstruction and stability contracts. The present formalization does
97 not yet identify every behaviorally minimal state with a stably recoverable
98 target in an inverse problem. That bridge is an open extension, stated in the
99 final section.
100 
101 \subsection{Conventions and domains}
102 Operator multiplication applies the right factor first: $STx=S(Tx)$.
103 A word $w=[i_1,\ldots,i_n]$ is chronological, so
104 $T_w=T_{i_n}\cdots T_{i_1}$; $T_\varnothing=I$. Concatenating $u$ then $v$
105 gives $T_{u\mathbin{+\!+}v}=T_vT_u$. Empty sums are zero and empty products are one.
106 All equalities of operators are equalities on the entire stated domain.
107 
108 The exact redundant-coordinate theory works for modules over a semiring.
109 Subtraction and compression defects use modules over a commutative ring.
110 Dimension and annihilating-polynomial arguments use a field. Norm estimates
111 use bounded linear maps on normed spaces. Continuous flow results use bounded,
112 time-independent real generators on Banach spaces. Reconstruction and
113 regularization use real Hilbert spaces unless a weaker projection hypothesis
114 is printed explicitly. These changes of domain are part of the contracts.
115 
116 For a subspace $L$ admitting orthogonal projection, $P_L$ denotes that actual
117 projection. On a Hilbert space, closed subspaces admit it. The notation
118 $\dist(v,L)=\inf_{\ell\in L}\nn{v-\ell}$ always refers to the actual subspace,
119 not a replacement chosen to make a theorem true. Closure is written $\cl L$.
120 
121 \subsection{How to read the formal evidence}
122 The stable identifiers SR-01 through SR-64 label consolidated theorem groups.
123 They are editorial units, with hypotheses and proofs printed here. A separate
124 CSV/JSON concordance records their exact source declarations and source hashes.
125 Several formal lemmas can support one printed theorem, and one source lemma
126 can serve more than one explanatory purpose. The source inventory contains
127 998 theorem/lemma declarations in 93 production modules, including helper
128 lemmas and examples. It is not a count of independent new mathematical results.
129 
130 The arguments below reconstruct the mathematics of the supplied Lean sources.
131 Classical inputs such as Cayley--Hamilton, orthogonal projection, the open
132 mapping theorem, Lax--Milgram, and the intermediate value theorem enter through
133 the source's Mathlib dependencies. This paper does not assert a new historical
134 priority assessment for those inputs. The Lean guide records exactly which
135 compilations and kernel replays are archived or freshly performed during this
136 release. Python certificates are tested implementations of mathematical
137 contracts; their parsers and algorithms are not Lean-verified.
138 
139 
140 \section{Exact coordinates, compression, and behavioral state}
141 
142 The first contract supplies two maps rather than identifying a coordinate
143 space with the object by convention. Let $a_X:X\to V_X$ and $s_X:V_X\to X$
144 be linear with $s_Xa_X=I_X$. The ambient space $V_X$ may have redundant
145 coordinates. Define $E_X=a_Xs_X$. For another such resolution of $Y$, put
146 \[
147 \mathcal K(T)=a_YTs_X,\qquad \mathcal D(K)=s_YKa_X.
148 \]
149 We call a proposed coordinate operator compatible when $E_YKE_X=K$.
150 
151 
152 \par{\small\textbf{Hypotheses.} Semiring modules; supplied linear analysis/\allowbreak synthesis pairs with s\_X a\_X=I and s\_Y a\_Y=I.}\par
153 
154 \begin{theorem}[SR-01\quad Exact redundant representation]\label{SR-01}
155 
156 $E_X^2=E_X$, and $E_Xv=v$ exactly when $v\in\Ran a_X$. Moreover
157 \[
158 \mathcal D\mathcal K(T)=T,\qquad
159 \mathcal K\mathcal D(K)=E_YKE_X.
160 \]
161 Consequently a compatible $K$ is the encoding of a unique map $T:X\to Y$.
162 Encoding preserves composition. Its identity on resolved coordinates is $E_X$.
163 
164 \end{theorem}
165 \begin{proof}
166 
167 The splitting gives $E_X^2=a_X(s_Xa_X)s_X=a_Xs_X$. If $E_Xv=v$, then
168 $v=a_X(s_Xv)$; conversely $E_Xa_Xx=a_Xx$. Substituting the definitions yields
169 \[
170 s_Y(a_YTs_X)a_X=T,\qquad
171 a_Y(s_YKa_X)s_X=E_YKE_X.
172 \]
173 For compatible $K$, take $T=\mathcal D(K)$. If another $T'$ encodes to $K$,
174 decoding proves $T'=\mathcal D(K)$. Finally, an intermediate resolution of $Y$
175 has $s_Ya_Y=I_Y$, so
176 $\mathcal K(S)\mathcal K(T)=a_ZS(s_Ya_Y)Ts_X=a_ZSTs_X$.
177 Encoding $I_X$ gives $a_Xs_X=E_X$, which acts as identity on compatible kernels.
178 No inverse on all of $V_X$ has been assumed.
179 
180 \end{proof}
181 
182 \src{Resolution.projector_idempotent; Resolution.fixed_iff_realizable; Resolution.compatible_iff_existsUnique; Resolution.encode_comp; Resolution.encode_id}
183 
184 
185 \begin{example}[Redundant coordinates]
186 For $X=\RR$ and $V_X=\RR^2$, take $a(x)=(x,x)$ and
187 $s(u,v)=(u+v)/2$. Then $E(u,v)=((u+v)/2,(u+v)/2)$.
188 The encoded scalar transformation $x\mapsto cx$ has matrix
189 $\frac c2\bigl(\begin{smallmatrix}1&1\\1&1\end{smallmatrix}\bigr)$.
190 Its redundant coordinate identity is $E$, while the ambient identity matrix
191 also acts on an unrealizable anti-diagonal sector. The distinction is exact.
192 \end{example}
193 
194 
195 \par{\small\textbf{Hypotheses.} Commutative-ring modules; linear $C:X\to Z$, $R:Z\to X$ with $CR=I_Z$; arbitrary endomorphisms $S,T,U$ of $X$.}\par
196 
197 \begin{theorem}[SR-02\quad Hidden-return defect and coherence]\label{SR-02}
198 
199 Set $P=RC$, $Q=I-P$, $\Phi(T)=CTR$, and
200 $\Delta(S,T)=\Phi(ST)-\Phi(S)\Phi(T)$. Then
201 \[
202 \Delta(S,T)=CSQTR,
203 \]
204 and associativity gives
205 \[
206 \Delta(S,T)\Phi(U)+\Delta(ST,U)
207 =\Phi(S)\Delta(T,U)+\Delta(S,TU).
208 \]
209 For two successive split compressions,
210 \[
211 \Delta_{21}(S,T)=\Phi_2(\Delta_1(S,T))
212 +\Delta_2(\Phi_1(S),\Phi_1(T)).
213 \]
214 
215 \end{theorem}
216 \begin{proof}
217 
218 Insert $I=P+Q$ between $S$ and $T$:
219 $CSTR=CS(P+Q)TR=(CSR)(CTR)+CSQTR$. This proves the factorization.
220 Expanding either side of the coherence identity cancels the terms
221 $\Phi(S)\Phi(T)\Phi(U)$ and leaves
222 $\Phi(STU)-\Phi(S)\Phi(TU)$ together with the same compensating term.
223 For the two-stage formula, add and subtract
224 $\Phi_2(\Phi_1(S)\Phi_1(T))$ in the composite defect. Linearity of $\Phi_2$
225 identifies the first difference with $\Phi_2(\Delta_1(S,T))$; the second is
226 the second-stage defect. Thus a later representation transports the earlier
227 error and can introduce another one. It does not remove the first term by definition.
228 
229 \end{proof}
230 
231 \src{SplitCompression.defect_factorization; SplitCompression.defect_coherence; SplitCompression.defect_then}
232 
233 \par{\small\textbf{Hypotheses.} Commutative-ring modules and a linear presentation $G\xrightarrow{A}V\xrightarrow{\delta}W$ with $\delta A=0$; a compatible vector $v\in\ker\delta$.}\par
234 
235 \begin{theorem}[SR-03\quad Actual globalization obstruction]\label{SR-03}
236 
237 For $\delta A=0$, define $K=\ker\delta$, $R=\Ran A\subseteq K$, and
238 $\mathcal H=K/R$. A compatible $v$ has class zero exactly when $v=Ag$
239 for some $g$. All classes vanish exactly when $R=K$. If $A$ is injective,
240 a zero class has a unique source.
241 
242 Commuting presentation maps $LA=A'F$ and $\delta'L=M\delta$ induce a map
243 $\overline L:\mathcal H\to\mathcal H'$ by $[v]\mapsto[Lv]$.
244 These maps compose and preserve zero classes. Reflection of zero follows
245 when $\overline L$ is injective.
246 
247 \end{theorem}
248 \begin{proof}
249 
250 The chain condition puts the actual range of $A$ inside $K$. The zero class
251 criterion for a quotient is membership in the submodule divided out, giving
252 $[v]=0\iff v\in R\iff\exists g,Ag=v$. Every compatible class is zero exactly
253 when $K\subseteq R$; the reverse inclusion is already known. Injectivity of
254 $A$ gives uniqueness of any preimage.
255 
256 For transport, if $v\in K$, then $\delta'Lv=M\delta v=0$.
257 If $v=Ag$, then $Lv=A'Fg$ lies in $R'$. Hence $L$ descends to the actual
258 quotients. Evaluating on representatives proves the composition law.
259 A linear map sends zero to zero. If its induced quotient map is injective,
260 $\overline L[v]=0=\overline L[0]$ implies $[v]=0$.
261 The commuting squares alone provide no such injectivity and do not assert
262 that either obstruction quotient vanishes.
263 
264 \end{proof}
265 
266 \src{Globalization.obstructionClass_zero_iff; Globalization.all_obstructions_zero_iff_exact; Globalization.unique_realization_of_zero; Globalization.PresentationMap.obstructionMap_compose; Globalization.PresentationMap.reflects_zero_obstruction}
267 
268 \par{\small\textbf{Hypotheses.} Commutative-ring modules; a linear observation $O:X\to Y$ and an arbitrary family of allowed endomorphisms $T_i:X\to X$; every finite chronological word is included.}\par
269 
270 \begin{theorem}[SR-04\quad The all-future invisible quotient]\label{SR-04}
271 
272 Let $N=\bigcap_w\ker(OT_w)$. It is the largest submodule contained in
273 $\ker O$ and invariant under every $T_i$. The operations and observation
274 descend to $X/N$, preserving every future observation. In particular,
275 \[
276 [x]=[y]\iff OT_wx=OT_wy\quad\text{for every finite word }w.
277 \]
278 If $q:X\to Z$ satisfies $qT_i=U_iq$ and $Vq=O$, then $\ker q\subseteq N$.
279 
280 \end{theorem}
281 \begin{proof}
282 
283 An intersection of kernels is a submodule. If $x\in N$, then
284 $OT_wT_ix=OT_{i::w}x=0$, so $T_ix\in N$. If an invariant submodule
285 $L\subseteq\ker O$ contains $x$, induction on word length gives $T_wx\in L$;
286 therefore $x\in N$. This establishes maximality.
287 
288 Invariance defines quotient operations $[x]\mapsto[T_ix]$; containment in
289 $\ker O$ defines $[x]\mapsto Ox$. Induction gives their all-word fidelity.
290 Equality $[x]=[y]$ means $x-y\in N$, which is precisely equality of the
291 displayed observations by linearity. In an exact competing model, induction
292 gives $qT_w=U_wq$ and hence $OT_w=VU_wq$. If $qx=0$, every future observation
293 of $x$ is zero. Thus a competing model can retain extra distinctions, but
294 cannot erase any distinction visible to the specified future task.
295 
296 \end{proof}
297 
298 \src{Behavioral.invisible_invariant; Behavioral.invariant_submodule_le_invisible; Behavioral.all_future_observations_preserved; Behavioral.quotient_eq_iff_same_future; Behavioral.exact_model_kernel_le}
299 
300 \section{Discrete hidden memory and finite closure}
301 
302 Let $V$ be visible state and $H$ hidden state. Over a commutative ring, specify
303 four maps and form the actual full dynamics
304 \[
305 T(y,z)=(Ay+Bz,Gy+Dz).
306 \]
307 Put $C(y,z)=y$, $Ry=(y,0)$, $E_n=CT^nR$, and $M_k=BD^kG$.
308 The return $M_k$ contains entry into $H$, $k$ hidden transitions, and return
309 to $V$. Its first effect occurs after $k+2$ full transitions.
310 
311 
312 \par{\small\textbf{Hypotheses.} Commutative-ring modules; actual powers of T(y,z)=(Ay+Bz,Gy+Dz); arbitrary initial y\_0,z\_0.}\par
313 
314 \begin{theorem}[SR-05\quad Exact hidden elimination]\label{SR-05}
315 
316 For the trajectory $(y_n,z_n)=T^n(y_0,z_0)$,
317 \[
318 z_n=D^nz_0+\sum_{j=0}^{n-1}D^{n-1-j}Gy_j,
319 \]
320 and
321 \[
322 y_{n+1}=Ay_n+BD^nz_0+\sum_{j=0}^{n-1}M_{n-1-j}y_j.
323 \]
324 Prepared evolution ($z_0=0$) satisfies
325 $E_0=I$, $E_1=A$, and
326 \[
327 E_{n+1}=AE_n+\sum_{j=0}^{n-1}M_{n-1-j}E_j.
328 \]
329 
330 \end{theorem}
331 \begin{proof}
332 
333 At $n=0$, the first formula is $z_0=z_0$ with an empty sum. If it holds at
334 $n$, the actual recurrence $z_{n+1}=Gy_n+Dz_n$ gives the same formula at
335 $n+1$ after distributing $D$ and appending the newest forcing term.
336 Substituting this expression into $y_{n+1}=Ay_n+Bz_n$ proves the visible
337 memory equation. For a prepared input $y_0$, each $y_j$ equals $E_jy_0$.
338 The pointwise memory equation is therefore an operator identity because it
339 holds for every $y_0$. The equations are derived from powers of $T$; the
340 trajectory recurrence is not an extra certificate assumption.
341 
342 \end{proof}
343 
344 \src{BlockDynamics.hidden_elimination; BlockDynamics.discrete_memory_equation; BlockDynamics.prepared_recurrence}
345 
346 \par{\small\textbf{Hypotheses.} Same block dynamics; no finite-dimensional or orthogonality assumption.}\par
347 
348 \begin{theorem}[SR-06\quad Prepared closure and the first return]\label{SR-06}
349 
350 The following conditions are equivalent:
351 \[
352 E_n=A^n\ (\forall n),\qquad M_k=0\ (\forall k),\qquad
353 E_{m+n}=E_mE_n\ (\forall m,n).
354 \]
355 More precisely,
356 \[
357 E_n=A^n\ (n\le N+1)\iff M_k=0\ (k<N).
358 \]
359 If $M_j=0$ for $j<k$, then $E_{k+2}-A^{k+2}=M_k$.
360 Closure for every initial hidden state is equivalent to $B=0$.
361 
362 \end{theorem}
363 \begin{proof}
364 
365 If all memory maps vanish, the recurrence in SR-05 reduces to
366 $E_{n+1}=AE_n$, proving $E_n=A^n$ by induction. Conversely, suppose exact
367 powers hold. Induct on $k$. In the recurrence for $E_{k+2}$, every term
368 except $M_kE_0$ involves a previously vanishing memory map. Thus
369 $E_{k+2}=AE_{k+1}+M_k$, forcing $M_k=0$.
370 The same induction restricted to $k<N$ proves the finite-prefix equivalence
371 and, before setting the last term to zero, the first-return identity.
372 
373 Exact powers imply the semigroup law. The law conversely gives
374 $E_{n+1}=E_nE_1=E_nA$, so it implies exact powers. For arbitrary hidden
375 initialization, evaluating closure at $n=1$, $y_0=0$ gives $Bz_0=0$ for
376 every $z_0$, hence $B=0$. That condition also suffices directly from the
377 visible recurrence. Vanishing $BD^kG$ imposes a weaker prepared-state requirement.
378 
379 \end{proof}
380 
381 \src{BlockDynamics.prepared_powers_iff_memory_zero; BlockDynamics.prepared_semigroup_iff_memory_zero; BlockDynamics.first_return_discrepancy; BlockDynamics.prepared_prefix_iff_memory_prefix; BlockDynamics.all_state_closure_iff_B_zero}
382 
383 \par{\small\textbf{Hypotheses.} Field modules; supplied monic annihilating polynomial p(D)=0, or finite-dimensional hidden H with d=dim H.}\par
384 
385 \begin{theorem}[SR-07\quad Finite all-depth closure certificate]\label{SR-07}
386 
387 If a monic polynomial $p$ annihilates $D$, vanishing of $M_k$ for
388 $k<\deg p$ implies vanishing for all $k$. If $\dim H=d<\infty$, then
389 \[
390 E_n=A^n\ (\forall n)
391 \iff M_k=0\ (0\le k<d)
392 \iff E_n=A^n\ (0\le n\le d+1).
393 \]
394 The visible space need not be finite-dimensional. The case $d=0$ is included.
395 
396 \end{theorem}
397 \begin{proof}
398 
399 Divide $X^n$ by the monic $p$ to obtain a remainder $q_n$ of degree below
400 $\deg p$. Evaluation at $D$ gives $D^n=q_n(D)$ because $p(D)=0$.
401 Writing $q_n(D)$ as a finite linear combination of the powers $D^k$ below
402 $\deg p$ shows $BD^nG=0$. For finite-dimensional $H$, Cayley--Hamilton
403 provides the monic characteristic polynomial of $D$ with degree $d$.
404 SR-06 then yields both displayed equivalences. In dimension zero,
405 all maps through $H$ vanish and the empty list of memory tests is sufficient.
406 If exact closure fails, the contrapositive gives a nonzero memory map with
407 index below $d$. These tests concern complete linear maps, not sampled state
408 vectors or approximate floating-point agreement.
409 
410 \end{proof}
411 
412 \src{BlockDynamics.memory_zero_of_annihilator; BlockDynamics.prepared_powers_iff_finrank_memory; BlockDynamics.prepared_powers_iff_finite_horizon; BlockDynamics.nonclosure_has_finite_feedback_witness}
413 
414 \par{\small\textbf{Hypotheses.} Commutative-ring split C,R with CR=I; hidden H=ker C; finite-H corollary over a field.}\par
415 
416 \begin{theorem}[SR-08\quad Canonical hidden state of a split compression]\label{SR-08}
417 
418 For $C:X\to Z$, $R:Z\to X$, $CR=I$, let $Q=I-RC$ and $H=\ker C$.
419 The maps
420 \[
421 x\longmapsto(Cx,Qx),\qquad (y,z)\longmapsto Ry+z
422 \]
423 are inverse linear maps between $X$ and $Z\times H$.
424 An endomorphism $T$ is conjugate to block dynamics with
425 \[
426 A=CTR,\quad B=CT\iota_H,\quad G=QTR,\quad D=QT\iota_H.
427 \]
428 Their prepared maps equal $CT^nR$. Hence exact compressed powers are
429 equivalent to zero canonical memory. If $\dim\ker C=d$, complete compressed
430 map tests through $d+1$ decide all depths.
431 
432 \end{theorem}
433 \begin{proof}
434 
435 $CQ=C-CRC=0$, so $Qx$ belongs to $H$. Synthesis after analysis gives
436 $RCx+Qx=x$. Conversely, for $z\in\ker C$, one has $C(Ry+z)=y$ and
437 $Q(Ry+z)=z$, using $QR=0$ and $Qz=z$. Conjugating $T$ by these inverse maps
438 gives the four displayed blocks; in the hidden blocks, $Q$ supplies the
439 required codomain. Induction transports powers under conjugacy.
440 The lift of $y$ is $(y,0)$ in these coordinates, so the prepared visible
441 map is precisely $CT^nR$. Apply SR-06 and SR-07. The construction uses the
442 actual discarded subspace and imposes no orthogonality on the chosen splitting.
443 
444 \end{proof}
445 
446 \src{SplitCompression.block_synthesis_analysis; SplitCompression.block_analysis_synthesis; SplitCompression.block_powers_eq; SplitCompression.exact_powers_iff_canonical_memory_zero; SplitCompression.exact_powers_iff_canonical_finite_horizon}
447 
448 
449 \begin{example}[Delayed return and disconnected return]
450 On $\QQ^3$, set $T(y,z_1,z_2)=(z_1,z_2,y)$ and retain $y$.
451 Then $A=0$, $M_0=0$, $M_1=I$, and $E_1=E_2=0$ while $E_3=I$.
452 Two shallow exact checks cannot certify all depths without the dimension budget.
453 For another system, let $A=D=I$, $B(z_1,z_2)=z_1$, and $G(y)=(0,y)$.
454 Both couplings are nonzero but every $BD^kG$ vanishes. Prepared closure is exact,
455 while an arbitrary hidden initial first coordinate affects the next visible state.
456 \end{example}
457 
458 
459 \section{Finite behavioral models and minimality}
460 
461 Now work over a field and, for dimension statements, assume $\dim X<\infty$.
462 The allowed operations need not commute. Define
463 \[
464 N_r=\bigcap_{|w|\le r}\ker(OT_w),\qquad k=\dim\ker O.
465 \]
466 A finite horizon means bounded word length. It gives a finite enumeration of
467 constraints only when the operation alphabet is finite.
468 
469 
470 \par{\small\textbf{Hypotheses.} Finite-dimensional X over a field; arbitrary alphabet; all bounded-length words including empty word.}\par
471 
472 \begin{theorem}[SR-09\quad Exact horizon and plateau certificate]\label{SR-09}
473 
474 $N_0=\ker O$ and
475 \[
476 N_{r+1}=\ker O\cap\bigcap_i T_i^{-1}N_r\subseteq N_r.
477 \]
478 One plateau $N_{r+1}=N_r$ implies $N_r=N$. In all cases $N_k=N$.
479 Thus equality of future observations through word length $k$ is equivalent
480 to equality for every finite word.
481 
482 \end{theorem}
483 \begin{proof}
484 
485 The empty word enforces $Ox=0$. A nonempty word $i::w$ of length at most
486 $r+1$ enforces $OT_wT_ix=0$, yielding the recursion. At a plateau, that
487 recursion shows $N_r$ is invariant under every $T_i$ and lies in $\ker O$.
488 By SR-04, $N_r\subseteq N$, while $N\subseteq N_r$ always holds.
489 
490 Before reaching $N$, each successive inclusion must be strict, since an
491 equality would already certify the final subspace. Every strict inclusion
492 reduces dimension by at least one. Starting from dimension $k$ allows at
493 most $k$ such reductions; if $N_k$ has dimension zero it is already $N$,
494 and otherwise an earlier plateau has occurred. Applying the kernel identity
495 to $x-y$ proves the all-future comparison. No word-order commutativity is used.
496 
497 \end{proof}
498 
499 \src{FiniteHorizon.visibleKernel_succ; FiniteHorizon.visibleKernel_eq_invisible_of_plateau; FiniteHorizon.visibleKernel_stabilizes; FiniteHorizon.same_future_iff_bounded}
500 
501 \par{\small\textbf{Hypotheses.} Finite-dimensional X over a field; exact linear competitor q with qT\_i=U\_iq and Vq=O; finite Z only for final ambient comparison.}\par
502 
503 \begin{theorem}[SR-10\quad Minimum exact state dimension]\label{SR-10}
504 
505 The model $X/N$ is observable. Every exact competitor induces a unique
506 surjection $\Ran q\to X/N$, taking $qx$ to $[x]$. Therefore
507 \[
508 \dim(X/N)\le\dim\Ran q,
509 \]
510 with equality exactly when $\ker q=N$. In that case
511 $\Ran q\cong X/N$. If $Z$ is finite-dimensional, also
512 $\dim\Ran q\le\dim Z$. Surjectivity of $q$ onto $Z$ is not required.
513 
514 \end{theorem}
515 \begin{proof}
516 
517 If $qx=qy$, SR-04 gives $x-y\in N$, so $qx\mapsto[x]$ is well-defined.
518 It is linear and surjective because every class has a representative $x$.
519 Its values on the actual range force uniqueness.
520 Rank-nullity gives $\dim\Ran q=\dim X-\dim\ker q$ and
521 $\dim(X/N)=\dim X-\dim N$. Since $\ker q\subseteq N$, this proves the
522 inequality. Equality of dimensions forces equality of the nested finite-dimensional
523 subspaces; conversely their equality makes the comparison injective and hence
524 an equivalence. In the quotient model, an invisible class $[x]$ has every
525 $OT_wx=0$, so $x\in N$ and $[x]=0$. This establishes observability.
526 Unused coordinates in $Z$ do not change the reachable-image comparison.
527 
528 \end{proof}
529 
530 \src{BehavioralMinimality.quotient_is_observable; BehavioralMinimality.imageComparison; BehavioralMinimality.finrank_state_le_image; BehavioralMinimality.image_dimension_minimal_iff; BehavioralMinimality.minimalImageEquiv}
531 
532 \par{\small\textbf{Hypotheses.} Finite-dimensional X over a field; finite operation alphabet; k=dim ker O; target Y can be infinite-dimensional.}\par
533 
534 \begin{theorem}[SR-11\quad Realizable finite observation tables]\label{SR-11}
535 
536 Let $H_kx=(OT_wx)_{|w|\le k}$ and $Z_k=\Ran H_k$. Then
537 $\ker H_k=N$ and $X/N\cong Z_k$. The formulas
538 \[
539 U_i(H_kx)=H_kT_ix,\qquad V(H_kx)=Ox
540 \]
541 define actual linear maps on $Z_k$ and preserve every finite future word.
542 This model has minimum exact dimension.
543 
544 \end{theorem}
545 \begin{proof}
546 
547 The recursively enumerated words are exactly those of length at most $k$.
548 SR-09 identifies the kernel of their combined observation map with $N$.
549 The first isomorphism theorem gives $X/N\cong\Ran H_k$. If $H_kx=H_ky$,
550 then $x-y\in N$; its invariance gives $H_kT_ix=H_kT_iy$, and
551 $N\subseteq\ker O$ gives $Ox=Oy$. Hence the displayed operations and readout
552 are well-defined on realizable tables. Induction proves
553 $U_wH_kx=H_kT_wx$ and $VU_wH_kx=OT_wx$ for words of any length.
554 Apply SR-10 to get minimality. An arbitrary table in the ambient coordinate
555 product need not be realizable and is not part of this constructed state space.
556 
557 \end{proof}
558 
559 \src{FiniteObservableModel.mem_wordsUpTo; FiniteObservableModel.ker_complete_observation; FiniteObservableModel.observableEquiv; FiniteObservableModel.coordinate_all_future_fidelity; FiniteObservableModel.coordinate_dimension_le_exact_model}
560 
561 \par{\small\textbf{Hypotheses.} Field modules, not necessarily finite-dimensional; finite operation alphabet and finite horizon observation map H\_r; actual maps q=F H\_r, qT\_i=U\_iq, Vq=O.}\par
562 
563 \begin{theorem}[SR-12\quad Finite minimality certificate]\label{SR-12}
564 
565 For a finite operation alphabet, suppose a proposed representation satisfies
566 \[
567 q=F H_r,\qquad qT_i=U_iq,\qquad Vq=O.
568 \]
569 Then $\ker q=N$, regardless of whether $r$ reaches the a priori horizon.
570 If $q$ is surjective, it gives an equivalence $Z\cong X/N$ preserving
571 the observation and intertwining every operation. Without surjectivity,
572 the equivalence applies to $\Ran q$.
573 
574 \end{theorem}
575 \begin{proof}
576 
577 If $x\in N$, then every coordinate of $H_rx$ is zero, so $qx=FH_rx=0$.
578 This gives $N\subseteq\ker q$. Exact intertwining and output give the reverse
579 inclusion by SR-04. The equality makes $qx\mapsto[x]$ injective on the range
580 and surjective onto the quotient. Its inverse is the corresponding quotient
581 map induced by $q$. Evaluating both sides on $qx$ proves that the equivalence
582 intertwines $U_i$ with the quotient operations and preserves the readout.
583 The certificate has two roles: generation by observations prevents retention
584 of invisible distinctions, while exact dynamics and output prevent loss of
585 future-visible distinctions. Finite dimension is needed to guarantee that
586 such a certificate can be found at a bounded depth, not for its soundness.
587 
588 \end{proof}
589 
590 \src{FiniteCertificate.certificate_kernel_eq; FiniteCertificate.certificate_same_future_iff; FiniteCertificate.certificateEquiv; FiniteCertificate.certificateEquiv_dynamics; FiniteCertificate.certificateEquiv_observation}
591 
592 
593 \begin{example}[A noncommuting minimal model]
594 On $\QQ^3$, let $O(x,y,h)=x$,
595 $T_A(x,y,h)=(y,0,h)$, and $T_B(x,y,h)=(0,x,h)$.
596 The two operations do not commute: on $(1,0,0)$ their two compositions
597 give $(1,0,0)$ and $(0,0,0)$. The map $q(x,y,h)=(x,y)$ is generated by
598 $O$ and $OT_A$, intertwines both operations, and factors $O$.
599 It therefore has a depth-one certificate. The hidden coordinate $h$ is
600 invisible to every future word, and the minimum exact state dimension is two.
601 The current observation alone has dimension one and misses the distinction
602 between $(0,1,0)$ and zero, which one application of $T_A$ reveals.
603 \end{example}
604 
605 
606 \section{Quantitative discrete sufficiency}
607 
608 Let $q:X\to Z$ be a proposed representation, with true operations $T_i$,
609 reduced operations $U_i$, and readouts $O:X\to Y$, $V:Z\to Y$.
610 Define the step and word defects
611 \[
612 \delta_i=qT_i-U_iq,\qquad E_w=qT_w-U_wq.
613 \]
614 Algebraic identities require only the stated commutative-ring structure.
615 Quantitative estimates below use continuous linear maps over a nontrivially
616 normed field and their whole-map operator norms.
617 
618 
619 \par{\small\textbf{Hypotheses.} Commutative-ring modules; arbitrary chronological words and linear operations/\allowbreak representation/\allowbreak readouts.}\par
620 
621 \begin{theorem}[SR-13\quad Exact word-defect transport]\label{SR-13}
622 
623 One has $E_\varnothing=0$,
624 \[
625 E_{i::w}=E_wT_i+U_w\delta_i,\qquad
626 E_{u\mathbin{+\!+}v}=E_vT_u+U_vE_u.
627 \]
628 For $w=[i_1,\ldots,i_n]$ this yields
629 \[
630 E_w=\sum_{j=1}^n
631 U_{[i_{j+1},\ldots,i_n]}\delta_{i_j}T_{[i_1,\ldots,i_{j-1}]}.
632 \]
633 The output defect is $(O-Vq)T_w+VE_w$.
634 
635 \end{theorem}
636 \begin{proof}
637 
638 The recursive identity follows by adding and subtracting $U_wqT_i$ in
639 $qT_wT_i-U_wU_iq$. For concatenation, add and subtract $U_vqT_u$;
640 chronological order gives $T_{u\mathbin{+\!+}v}=T_vT_u$ and the analogous
641 identity for $U$. Inducting on the word expands one term per letter:
642 each step defect is transported by its true prefix and reduced suffix.
643 The empty word contributes no terms. Finally
644 $OT_w-VU_wq=(O-Vq)T_w+V(qT_w-U_wq)$.
645 Neither output mismatch nor accumulated dynamics mismatch is discarded.
646 
647 \end{proof}
648 
649 \src{ApproximateAlgebra.wordDefect_cons; ApproximateAlgebra.wordDefect_append; ApproximateAlgebra.wordDefect_eq_sum; ApproximateAlgebra.output_defect_decomposition}
650 
651 \par{\small\textbf{Hypotheses.} Normed spaces over nontrivially normed field; bounded maps; nonnegative letter bounds a\_i,b\_i,epsilon\_i and eta\(\ge\Vert\)O-Vq\(\Vert\).}\par
652 
653 \begin{theorem}[SR-14\quad Heterogeneous operator budgets]\label{SR-14}
654 
655 Suppose $\nn{T_i}\le a_i$, $\nn{U_i}\le b_i$, $\nn{\delta_i}\le\epsilon_i$.
656 Let $A_w,B_w$ be the products of the respective letter bounds and define
657 \[
658 D_\varnothing=0,\qquad D_{i::w}=D_wa_i+B_w\epsilon_i.
659 \]
660 Then $\nn{T_w}\le A_w$, $\nn{U_w}\le B_w$, $\nn{E_w}\le D_w$, and
661 \[
662 D_{u\mathbin{+\!+}v}=D_vA_u+B_vD_u.
663 \]
664 If $\nn{O-Vq}\le\eta$, then
665 \[
666 \nn{OT_w-VU_wq}\le\eta A_w+\nn V D_w.
667 \]
668 For arbitrary initial $x\in X$, $z\in Z$,
669 $\nn{qT_wx-U_wz}\le D_w\nn x+B_w\nn{qx-z}$.
670 
671 \end{theorem}
672 \begin{proof}
673 
674 Induction and submultiplicativity bound the two word operators by the
675 products. Apply the triangle inequality and submultiplicativity to the
676 first identity in SR-13 to obtain exactly the recursion for $D_w$.
677 Induction on $u$ proves the displayed scalar concatenation identity; it
678 tracks the same algebra as the exact defect identity, with nonnegative
679 factors preventing an inequality reversal. The output bound follows from
680 its exact decomposition in SR-13. For initialization, write
681 $qT_wx-U_wz=E_wx+U_w(qx-z)$ and bound both terms. These are operator budgets;
682 agreement on a finite set of sample vectors does not supply them.
683 
684 \end{proof}
685 
686 \src{ApproximateBounds.norm_wordError_le_budget; ApproximateBounds.budget_append; ApproximateBounds.norm_outputError_le; ApproximateBounds.norm_state_error_le}
687 
688 \par{\small\textbf{Hypotheses.} Uniform nonnegative whole-map bounds a,b,epsilon; all finite words with length n; eta bound on output mismatch.}\par
689 
690 \begin{theorem}[SR-15\quad Two-rate response and equal-rate limit]\label{SR-15}
691 
692 For $H_0(a,b)=0$ and
693 $H_{n+1}(a,b)=aH_n(a,b)+b^n$,
694 \[
695 H_n(a,b)=\sum_{j=0}^{n-1}a^jb^{n-1-j},\qquad
696 (a-b)H_n=a^n-b^n.
697 \]
698 If $a\ne b$, $H_n=(a^n-b^n)/(a-b)$; for equal rates,
699 $H_{n+1}(a,a)=(n+1)a^n$. Uniform step bounds give
700 \[
701 \nn{E_w}\le\epsilon H_n(a,b),\qquad
702 \nn{OT_w-VU_wq}\le\eta a^n+\nn V\epsilon H_n(a,b).
703 \]
704 
705 \end{theorem}
706 \begin{proof}
707 
708 Induction proves the finite-sum formula: multiplying the old sum by $a$
709 and adjoining $b^n$ generates every term of the new sum. Multiplication
710 by $a-b$ telescopes, leaving $a^n-b^n$. Division is used only when the
711 rates are distinct. If they coincide, all $n+1$ terms of $H_{n+1}$ equal
712 $a^n$, including the zero-rate boundary with the usual $a^0=1$.
713 For uniform bounds, the heterogeneous budget becomes
714 $D_{i::w}=aD_w+b^{|w|}\epsilon$, so induction gives
715 $D_w=\epsilon H_{|w|}(a,b)$. Apply SR-14. The empty word has zero dynamics
716 defect and is handled by $H_0=0$, with no negative exponent required.
717 
718 \end{proof}
719 
720 \src{ScalarBudgets.response_eq_sum; ScalarBudgets.response_mul_sub; ScalarBudgets.response_of_ne; ScalarBudgets.response_same_succ; StableApproximation.norm_wordError_uniform; StableApproximation.norm_outputError_uniform}
721 
722 \par{\small\textbf{Hypotheses.} Bounded maps on the normed spaces of SR-14; $\nn{T_i}\le1$ for every true operation; $\nn{U_i}\le1$ in the nonexpansive case or a common $0\le b<1$ with $\nn{U_i}\le b$ in the contractive case; $\nn{qT_i-U_iq}\le\epsilon$ and $\nn{O-Vq}\le\eta$ with $\epsilon,\eta\ge0$.}\par
723 
724 \begin{theorem}[SR-16\quad Nonexpansive and contractive continuations]\label{SR-16}
725 
726 If both families are nonexpansive, $\nn{E_w}\le n\epsilon$ and the output
727 defect is at most $\eta+\nn V n\epsilon$.
728 If the reduced family has a common bound $0\le b<1$, then
729 \[
730 \nn{E_w}\le\frac\epsilon{1-b},\qquad
731 \nn{OT_w-VU_wq}\le\eta+\nn V\frac\epsilon{1-b}.
732 \]
733 For arbitrary reduced initialization,
734 \[
735 \nn{OT_wx-VU_wz}
736 \le\left(\eta+\nn V\frac\epsilon{1-b}\right)\nn x
737 +\nn V b^n\nn{qx-z}.
738 \]
739 
740 \end{theorem}
741 \begin{proof}
742 
743 For $a=b=1$, the response sum has $n$ unit terms. For $a=1$ and $b<1$,
744 it is $1+b+\cdots+b^{n-1}\le1/(1-b)$. SR-15 gives the operator estimates.
745 For initialization, add $VU_w(qx-z)$ to the operator output error
746 applied to $x$, and use $\nn{U_w}\le b^n$.
747 The common bound concerns every allowed operation in the chosen norm.
748 Individual spectral radii do not imply a common product bound for a
749 noncommuting family. The nonexpansive estimate is an upper bound and does
750 not state that every such system accumulates error linearly.
751 
752 \end{proof}
753 
754 \src{StableApproximation.norm_wordError_nonexpansive; StableApproximation.norm_outputError_nonexpansive; StableApproximation.norm_wordError_contractive; StableApproximation.norm_output_initial_contractive}
755 
756 \section{Continuous flow and exact hidden memory}
757 
758 Let $L$ be a bounded real operator on a Banach space. Its flow is the actual
759 operator exponential $e^{tL}$. Boundedness allows differentiation of the
760 norm-convergent exponential series and integration of continuous operator
761 curves. Equalities in this section hold for all real $t$, using oriented
762 interval integrals when $t<0$.
763 
764 
765 \par{\small\textbf{Hypotheses.} Real Banach space; bounded autonomous D; continuous forcing f; differentiable actual z with z\({}^{\prime}\)=Dz+f at every real time.}\par
766 
767 \begin{theorem}[SR-17\quad Actual flow and variation of constants]\label{SR-17}
768 
769 $\frac d{dt}e^{tD}=De^{tD}=e^{tD}D$,
770 $e^{(s+t)D}=e^{sD}e^{tD}$, and $e^{-tD}$ is the inverse flow.
771 Every actual curve satisfying $z'=Dz+f$ with continuous $f$ obeys
772 \[
773 z(t)=e^{tD}z(0)+\int_0^t e^{(t-s)D}f(s)\,ds.
774 \]
775 The initial value uniquely determines the homogeneous solution; two forced
776 solutions with the same forcing and initial value also agree.
777 
778 \end{theorem}
779 \begin{proof}
780 
781 Termwise differentiation of the exponential series gives both derivative
782 orders, since all powers of $D$ commute with $D$. The exponential addition
783 identity for commuting multiples of one bounded operator gives the flow law
784 and inverse. For fixed $t$, differentiate $e^{(t-s)D}z(s)$. The product rule
785 produces $-De^{(t-s)D}z(s)+e^{(t-s)D}(Dz(s)+f(s))$; commutation cancels
786 the generator terms. The remaining derivative is the continuous integrand
787 $e^{(t-s)D}f(s)$. The fundamental theorem of calculus on the oriented interval
788 gives the displayed identity. Setting $f=0$ yields the homogeneous formula.
789 Subtracting two forced solutions reduces uniqueness to that case.
790 The theorem starts from the differential equation, not from an assumed
791 integral representation.
792 
793 \end{proof}
794 
795 \src{ContinuousFlow.hasDerivAt_flow; ContinuousFlow.flow_add; ContinuousFlow.variation_of_constants; ContinuousFlow.homogeneous_unique; ContinuousFlow.forced_unique}
796 
797 \par{\small\textbf{Hypotheses.} Bounded real generator algebras and bounded linear observation maps; norm-convergent exponentials; all real times or all natural powers.}\par
798 
799 \begin{theorem}[SR-18\quad Power identities and exponential identities]\label{SR-18}
800 
801 For bounded linear observation maps $K,J$ on bounded generator algebras,
802 \[
803 K(e^{tL})=J(e^{tD})\ (\forall t)
804 \iff K(L^n)=J(D^n)\ (\forall n).
805 \]
806 In particular, $Be^{tD}G=0$ for every $t$ exactly when $BD^nG=0$ for every $n$.
807 For $CR=I$, $A=CLR$, one has
808 \[
809 Ce^{tL}R=e^{tA}\ (\forall t)
810 \iff CL^nR=A^n\ (\forall n),
811 \]
812 and, with $Q=I-RC$,
813 \[
814 Ce^{(s+t)L}R-(Ce^{sL}R)(Ce^{tL}R)=Ce^{sL}Qe^{tL}R.
815 \]
816 
817 \end{theorem}
818 \begin{proof}
819 
820 The $n$th derivative at zero of $e^{tL}$ is $L^n$. Bounded linear maps
821 commute with these derivatives, so equality for all times implies equality
822 of every observed power. Conversely bounded linear maps commute with the
823 sum of the norm-convergent exponential series:
824 $K(e^{tL})=\sum_n(t^n/n!)K(L^n)$. Equality term by term gives equality of
825 the sums. Sandwiching and compression are bounded linear maps on the
826 corresponding operator spaces, so they give the specializations. For the
827 last identity, use the flow law and insert $I=RC+Q$ between the two flows.
828 The defect factorization itself does not need $CR=I$; that condition makes
829 $Q$ the discarded-state projector and ensures $E(0)=I$.
830 
831 \end{proof}
832 
833 \src{ContinuousFlow.mapped_flow_eq_iff_powers_eq; ContinuousFlow.sandwich_flow_zero_iff; ContinuousFlow.compressed_flow_iff_powers; ContinuousFlow.compressed_flow_defect}
834 
835 \par{\small\textbf{Hypotheses.} Real Banach visible/\allowbreak hidden spaces; bounded autonomous blocks A,B,G,D; actual exponential full trajectory; arbitrary hidden initial state.}\par
836 
837 \begin{theorem}[SR-19\quad Continuous hidden elimination]\label{SR-19}
838 
839 For $L(y,z)=(Ay+Bz,Gy+Dz)$ and
840 $(y(t),z(t))=e^{tL}(y_0,z_0)$,
841 \[
842 z(t)=e^{tD}z_0+\int_0^t e^{(t-s)D}Gy(s)\,ds.
843 \]
844 Writing $M(t)=Be^{tD}G$, the visible dynamics satisfy
845 \[
846 y'(t)=Ay(t)+Be^{tD}z_0+\int_0^t M(t-s)y(s)\,ds.
847 \]
848 Prepared initialization removes the term involving $z_0$.
849 
850 \end{theorem}
851 \begin{proof}
852 
853 Projecting the derivative of $e^{tL}$ onto the visible and hidden components
854 gives $y'=Ay+Bz$ and $z'=Gy+Dz$. The visible curve is continuous, so
855 $Gy$ is continuous forcing for the hidden equation. SR-17 yields the hidden
856 elimination formula. Bounded $B$ commutes with the interval integral,
857 giving the memory kernel in the visible equation. Taking $z_0=0$ removes
858 only the initialization term. No converse construction of a full trajectory
859 from an arbitrary Volterra solution is asserted here, and no unbounded
860 generator domain is present.
861 
862 \end{proof}
863 
864 \src{ContinuousBlockDynamics.hasDerivAt_visible; ContinuousBlockDynamics.hidden_elimination; ContinuousBlockDynamics.continuous_memory_equation; ContinuousBlockDynamics.prepared_memory_equation}
865 
866 \par{\small\textbf{Hypotheses.} Bounded real Banach block system; finite-dimensional hidden H only for finite certificates, or supplied monic annihilator.}\par
867 
868 \begin{theorem}[SR-20\quad Continuous closure, finite moments, and jets]\label{SR-20}
869 
870 Let $E(t)=Ce^{tL}R$. The following are equivalent:
871 \[
872 E(t)=e^{tA}\ (\forall t),\quad M(t)=0\ (\forall t),\quad
873 BD^kG=0\ (\forall k),\quad E(s+t)=E(s)E(t)\ (\forall s,t).
874 \]
875 If $\dim H=d$, each is equivalent to $BD^kG=0$ for $k<d$, or to
876 $E^{(n)}(0)=A^n$ for $n\le d+1$. If the first $k$ return moments vanish,
877 \[
878 E^{(k+2)}(0)-A^{k+2}=BD^kG.
879 \]
880 
881 \end{theorem}
882 \begin{proof}
883 
884 SR-18 converts prepared flow equality into prepared power equality and
885 memory flow vanishing into memory moment vanishing. SR-06 equates the
886 corresponding algebraic conditions, and SR-07 supplies the finite moment
887 criterion. Exact prepared flow gives its semigroup law. Conversely, if
888 $E$ is a semigroup, differentiating $E(s+t)=E(s)E(t)$ in $s$ at zero
889 gives $E'(t)=AE(t)$ because $E'(0)=CLR=A$ and $E(0)=I$.
890 The bounded-generator uniqueness theorem yields $E(t)=e^{tA}$.
891 
892 Actual iterated derivatives of the exponential satisfy
893 $E^{(n)}(0)=CL^nR$. Applying the finite algebraic horizon and first-return
894 identity proves the jet statements. The leading Taylor coefficient has
895 the additional denominator $(k+2)!$; the derivative itself does not.
896 The visible Banach space can be infinite-dimensional. The finite tests
897 are whole-operator jet identities, not a finite list of sampled times.
898 
899 \end{proof}
900 
901 \src{ContinuousBlockDynamics.prepared_exact_iff_memory_zero; ContinuousBlockDynamics.prepared_semigroup_iff_memory_zero; ContinuousBlockDynamics.prepared_exact_iff_finite_memory; ContinuousBlockDynamics.prepared_exact_iff_finite_derivatives; ContinuousBlockDynamics.first_return_derivative}
902 
903 
904 \begin{example}[A linear continuous memory kernel]
905 Take $V=\RR$, $H=\RR^2$, $A=0$, $B(z_1,z_2)=z_1$,
906 $G(y)=(0,y)$, and $D(z_1,z_2)=(z_2,0)$. Since $D^2=0$,
907 $e^{tD}(z_1,z_2)=(z_1+tz_2,z_2)$ and $M(t)=tI$.
908 The first two prepared jets agree with the reduced generator, while the
909 third derivative differs by $I$. Changing $D$ to zero leaves both boundary
910 couplings nonzero but makes the memory kernel identically zero.
911 Arbitrary hidden initialization still affects the visible initial derivative.
912 \end{example}
913 
914 
915 \section{Continuous approximate sufficiency}
916 
917 For bounded real generators $L$ on $X$ and $A$ on $Z$, and bounded $q:X\to Z$,
918 write $\delta=qL-Aq$ and $E(t)=qe^{tL}-e^{tA}q$.
919 Algebraic evolution identities hold for all real times. Norm bounds in this
920 section restrict to $t\ge0$, with growth assumptions on the nonnegative-time flows.
921 
922 
923 \par{\small\textbf{Hypotheses.} Real Banach source/\allowbreak reduced spaces; bounded autonomous generators; bounded q and second representation p; all real times.}\par
924 
925 \begin{theorem}[SR-21\quad Duhamel transport and composition]\label{SR-21}
926 
927 One has the operator identity
928 \[
929 E(t)=\int_0^t e^{(t-s)A}\delta e^{sL}\,ds,
930 \]
931 and $\delta=0$ exactly when $E(t)=0$ for every $t$. Also
932 \[
933 E(s+t)=E(s)e^{tL}+e^{sA}E(t).
934 \]
935 For a second representation $p:Z\to W$ with generator $B$,
936 \[
937 \delta_{pq}=p\delta_q+\delta_pq,\qquad
938 E_{pq}(t)=pE_q(t)+E_p(t)q.
939 \]
940 
941 \end{theorem}
942 \begin{proof}
943 
944 Differentiate $F(s)=e^{(t-s)A}qe^{sL}$ using the product rule. Its derivative
945 is $e^{(t-s)A}(qL-Aq)e^{sL}$. Integrating from zero to $t$ gives
946 $F(t)-F(0)=E(t)$ and proves the formula. Zero generator defect therefore
947 forces zero evolution defect; differentiating $E$ at zero gives the
948 converse. The addition identity follows by adding and subtracting
949 $e^{sA}qe^{tL}$ and using the two flow laws.
950 For a composite representation, add and subtract $pAq$ in its generator
951 defect and $pe^{tA}q$ in its evolution defect. Both stages' contributions
952 remain explicit. Boundedness guarantees the continuous operator integrand.
953 
954 \end{proof}
955 
956 \src{ContinuousDefect.duhamel; ContinuousDefect.generatorDefect_zero_iff; ContinuousDefect.evolutionDefect_add; ContinuousDefect.generatorDefect_composite; ContinuousDefect.evolutionDefect_composite}
957 
958 \par{\small\textbf{Hypotheses.} Real Banach spaces $X,Z$; bounded autonomous real generators $L,A$ and bounded representation/readouts $q,O,V$; real rates $a,b$ of either sign; $t\ge0$ and $M_L,M_A,\epsilon,\eta\ge0$. For every $s\ge0$, $\nn{e^{sL}}\le M_Le^{as}$ and $\nn{e^{sA}}\le M_Ae^{bs}$; also $\nn{qL-Aq}\le\epsilon$ and $\nn{O-Vq}\le\eta$.}\par
959 
960 \begin{theorem}[SR-22\quad Growth envelopes and scalar response]\label{SR-22}
961 
962 For $\nn\delta\le\epsilon$, put
963 \[
964 R(a,b,t)=\int_0^t e^{b(t-s)}e^{as}\,ds
965 =\begin{cases}(e^{at}-e^{bt})/(a-b),&a\ne b,\\ te^{at},&a=b.\end{cases}
966 \]
967 Then
968 \[
969 \nn{E(t)}\le M_LM_A\epsilon R(a,b,t).
970 \]
971 If $\nn{O-Vq}\le\eta$, the output defect $F(t)=Oe^{tL}-Ve^{tA}q$ obeys
972 \[
973 \nn{F(t)}\le\eta M_Le^{at}+\nn V M_LM_A\epsilon R(a,b,t).
974 \]
975 
976 \end{theorem}
977 \begin{proof}
978 
979 Apply the integral norm inequality and submultiplicativity to SR-21.
980 For $0\le s\le t$, the integrand norm is at most
981 $M_Ae^{b(t-s)}\epsilon M_Le^{as}$. Integration gives the first estimate.
982 Factoring $e^{bt}$ and integrating $e^{(a-b)s}$ gives the distinct-rate
983 formula; for equal rates the integrand is constant $e^{at}$.
984 The output decomposition is
985 $F(t)=(O-Vq)e^{tL}+VE(t)$, giving the stated bound.
986 The same argument works with continuous nonnegative envelope functions
987 $u,v$ on the interval, replacing the scalar response by
988 $\int_0^tv(t-s)u(s)\,ds$. In particular these assumptions concern actual
989 flow norms, not just eigenvalues of the generators.
990 
991 \end{proof}
992 
993 \src{ExponentialBudgets.response_of_ne; ExponentialBudgets.response_self; ContinuousApproximation.norm_evolution_le_response; ContinuousApproximation.norm_output_le_response}
994 
995 \par{\small\textbf{Hypotheses.} True flow bounded by M\_L; reduced flow bounded by M\_A exp(-rt), r>0, for t\(\ge\)0; generator/\allowbreak readout allowances; arbitrary initial reduced z.}\par
996 
997 \begin{theorem}[SR-23\quad Uniform continuous stability and initialization]\label{SR-23}
998 
999 If $\nn{e^{tL}}\le M_L$ and $\nn{e^{tA}}\le M_Ae^{-rt}$ with $r>0$, then
1000 \[
1001 \nn{E(t)}\le\frac{M_LM_A\epsilon}{r},\qquad
1002 \nn{F(t)}\le\eta M_L+\nn V\frac{M_LM_A\epsilon}{r}.
1003 \]
1004 For arbitrary $x,z$,
1005 \begin{align*}
1006 \nn{Oe^{tL}x-Ve^{tA}z}
1007 &\le\left(\eta M_L+\nn V\frac{M_LM_A\epsilon}{r}\right)\nn x\\
1008 &\quad+\nn V M_Ae^{-rt}\nn{qx-z}.
1009 \end{align*}
1010 Composition through a second representation propagates allowances with
1011 its explicit map norm, as in SR-21.
1012 
1013 \end{theorem}
1014 \begin{proof}
1015 
1016 Use SR-22 with $a=0$, $b=-r$. Its response equals
1017 $(1-e^{-rt})/r\le1/r$ for $t\ge0$. This gives the evolution and output
1018 operator bounds. The initialization error decomposes into $F(t)x$ plus
1019 $Ve^{tA}(qx-z)$, which proves the displayed estimate. The first allowance
1020 must be multiplied by $\nn x$ because it is an operator estimate.
1021 For another representation $p$ with its own evolution defect, SR-21 gives
1022 $\nn{E_{pq}(t)}\le\nn p\nn{E_q(t)}+\nn{E_p(t)}\nn q$.
1023 This retains error introduced at both stages, rather than identifying
1024 their budgets with a single unqualified small quantity.
1025 
1026 \end{proof}
1027 
1028 \src{ContinuousStability.norm_evolution_uniform; ContinuousStability.norm_output_uniform; ContinuousStability.norm_initialization_uniform; ContinuousStability.norm_composite_evolution}
1029 
1030 \par{\small\textbf{Hypotheses.} Actual real scalar bounded generators, q=I; t\(\ge\)0; b\(\le\)a for equality and epsilon>0 for counterexample.}\par
1031 
1032 \begin{theorem}[SR-24\quad Sharp response and small-defect failure]\label{SR-24}
1033 
1034 For scalar generators $a\ge b$,
1035 \[
1036 |e^{at}-e^{bt}|=(a-b)R(a,b,t),
1037 \]
1038 so the response estimate is attained. For every $\epsilon>0$, choosing
1039 $L=\epsilon I$, $A=0$, $q=I$ gives
1040 \[
1041 \nn\delta=\epsilon,\qquad \nn{E(t)}=e^{\epsilon t}-1\ge\epsilon t.
1042 \]
1043 Its evolution defect exceeds every fixed bound at some nonnegative time.
1044 
1045 \end{theorem}
1046 \begin{proof}
1047 
1048 The scalar exponential is the actual flow by the homogeneous ODE uniqueness
1049 theorem. For $a>b$, the response formula immediately gives the equality;
1050 for $a=b$, both sides vanish. In the second example, the generator defect
1051 is multiplication by $\epsilon$, while the evolution defect is multiplication
1052 by $e^{\epsilon t}-1$. The elementary exponential inequality
1053 $e^u\ge1+u$ for $u\ge0$ gives the lower bound. Taking $t$ sufficiently
1054 large makes it exceed any prescribed real bound. Thus a small generator
1055 defect alone does not supply uniform accuracy. The hypothesis of a bounded
1056 true flow in SR-23 fails here.
1057 
1058 \end{proof}
1059 
1060 \src{ContinuousApproxExamples.scalar_response_sharp; ContinuousApproxExamples.unstable_generator_exact; ContinuousApproxExamples.unstable_error_exact; ContinuousApproxExamples.unstable_error_unbounded}
1061 
1062 \section{Orthogonal globalization and conditioning}
1063 
1064 Let $R\subseteq K$ be subspaces of a real inner-product space $V$, both admitting
1065 orthogonal projections. Define the actual maps
1066 \[
1067 r(v)=P_Rv,\quad o(v)=(P_K-P_R)v,\quad i(v)=(I-P_K)v.
1068 \]
1069 They distinguish realized data, compatible obstruction, and incompatibility.
1070 In a globalization presentation use $R=\Ran A$, $K=\ker\delta$ with $\delta A=0$.
1071 
1072 
1073 \par{\small\textbf{Hypotheses.} Real inner-product V; nested subspaces R\(\le\)K both with orthogonal projections; arbitrary v and represented candidate u\(\in\)R.}\par
1074 
1075 \begin{theorem}[SR-25\quad Unique three-component geometry]\label{SR-25}
1076 
1077 The components lie in $R$, $K\cap R^\perp$, and $K^\perp$, respectively,
1078 are pairwise orthogonal, and give the unique decomposition
1079 $v=r(v)+o(v)+i(v)$. Furthermore,
1080 \[
1081 \nn v^2=\nn r^2+\nn o^2+\nn i^2,\qquad
1082 \dist(v,R)^2=\nn o^2+\nn i^2.
1083 \]
1084 For any $u\in R$,
1085 \[
1086 \nn{v-u}^2=\dist(v,R)^2+\nn{r(v)-u}^2.
1087 \]
1088 Thus $r(v)$ is the unique nearest represented vector.
1089 
1090 \end{theorem}
1091 \begin{proof}
1092 
1093 Nested projections satisfy $P_RP_K=P_R$. Hence
1094 $P_Kv-P_Rv$ lies in $K$ and is orthogonal to $R$; the last component is
1095 orthogonal to $K$. Their definitions sum to $v$ and yield pairwise
1096 orthogonality. In any competing decomposition, projection onto $R$
1097 selects its first term and projection onto $K$ selects the first two,
1098 so all components are forced. Pythagoras gives the norm identities.
1099 For $u\in R$, the residual $v-r(v)$ is orthogonal to $r(v)-u$,
1100 so the candidate identity follows. It proves optimality and uniqueness,
1101 and taking the infimum over actual $u\in R$ proves the distance formula.
1102 Each component map is an orthogonal projection onto its displayed sector
1103 and consequently is nonexpansive.
1104 
1105 \end{proof}
1106 
1107 \src{OrthogonalResolution.components_sum; OrthogonalResolution.unique_components; OrthogonalResolution.norm_sq_components; OrthogonalResolution.candidate_error_sq; OrthogonalResolution.infDist_sq_decomposition}
1108 
1109 \par{\small\textbf{Hypotheses.} Real linear presentation \(\delta\)A=0; projections on actual R=range A and K=ker\(\delta\); source G only needs real module structure.}\par
1110 
1111 \begin{theorem}[SR-26\quad Harmonic realization of the obstruction quotient]\label{SR-26}
1112 
1113 The same quotient $\mathcal H=K/R$ from SR-03 is linearly equivalent to
1114 $K\cap R^\perp$ by
1115 \[
1116 [v]\longmapsto v-P_Rv\quad(v\in K).
1117 \]
1118 It is inverse to the quotient map restricted to the harmonic subspace.
1119 For compatible data, the class is zero exactly when $o(v)=0$; equality
1120 of classes is equality of harmonic representatives. The best image $P_Rv$
1121 has an actual source under $A$.
1122 
1123 \end{theorem}
1124 \begin{proof}
1125 
1126 Adding a vector of $R$ leaves $v-P_Rv$ unchanged, so the map descends to
1127 $K/R$. Its values lie in $K\cap R^\perp$ by SR-25. For harmonic $h$,
1128 $P_Rh=0$, so its class maps back to $h$. For compatible $v$, the difference
1129 $v-(v-P_Rv)=P_Rv$ lies in $R$, so the reverse roundtrip returns $[v]$.
1130 The inverse laws prove the equivalence and both class criteria.
1131 Since $P_Rv$ belongs to the actual range, some $g$ satisfies $Ag=P_Rv$.
1132 This is image existence; uniqueness of $g$ requires the separate injectivity
1133 condition in SR-03. No norm isometry is inferred from linear equivalence
1134 alone; the metric statement is proved in SR-33.
1135 
1136 \end{proof}
1137 
1138 \src{HilbertGlobalization.obstructionEquivHarmonic; HilbertGlobalization.class_zero_iff_component_zero; HilbertGlobalization.same_class_iff_same_harmonic; HilbertGlobalization.exists_best_global_image}
1139 
1140 \par{\small\textbf{Hypotheses.} Same projection presentation; bounded \(\delta\); sigma>0 with sigma\(\Vert\)x\(\Vert\le\Vert\delta\)x\(\Vert\) on K\(\perp\); arbitrary data.}\par
1141 
1142 \begin{theorem}[SR-27\quad Residual bounds retain conditioning and obstruction]\label{SR-27}
1143 
1144 If $\sigma\nn x\le\nn{\delta x}$ for $x\in K^\perp$ and $\sigma>0$, then
1145 \[
1146 \delta i(v)=\delta v,\qquad
1147 \nn{i(v)}\le\frac{\nn{\delta v}}\sigma,
1148 \]
1149 and
1150 \[
1151 \nn{o(v)}\le\dist(v,R),\qquad
1152 \dist(v,R)^2\le\nn{o(v)}^2+\left(\frac{\nn{\delta v}}\sigma\right)^2.
1153 \]
1154 For compatible data, $\dist(v,R)=\nn{o(v)}$.
1155 
1156 \end{theorem}
1157 \begin{proof}
1158 
1159 The component $P_Kv$ is in $\ker\delta$, so
1160 $\delta(v-P_Kv)=\delta v$. Apply coercivity to $i(v)\in K^\perp$ and divide
1161 by the positive $\sigma$. SR-25 gives the exact sum of two nonnegative
1162 squares, proving both the lower bound and conditioned upper bound.
1163 If $\delta v=0$, then $v\in K$ and $i(v)=0$, giving equality.
1164 In particular, a compatibility residual bounds only inconsistency. A
1165 residual-only global bound needs a vanished obstruction or exactness
1166 $R=K$. The condition on $\sigma$ is independent of the size of a particular
1167 measured residual and cannot be inferred from that measurement.
1168 
1169 \end{proof}
1170 
1171 \src{HilbertConditioning.inconsistency_residual; HilbertConditioning.inconsistency_le_residual; HilbertConditioning.conditioned_distance_sq; HilbertConditioning.obstruction_lower_bound; HilbertConditioning.compatible_distance}
1172 
1173 \par{\small\textbf{Hypotheses.} Finite-dimensional real V for existence/\allowbreak characterization; fixed metric and K with projected R0\(\le\)R1\(\le\)K for refinement.}\par
1174 
1175 \begin{theorem}[SR-28\quad Finite conditioning and realizable enlargement]\label{SR-28}
1176 
1177 In finite dimension some $\sigma>0$ satisfies SR-27. Under $\delta A=0$,
1178 \[
1179 \exists c>0\ \forall v:\dist(v,\Ran A)\le c\nn{\delta v}
1180 \iff\Ran A=\ker\delta.
1181 \]
1182 For projected $R_0\subseteq R_1\subseteq K$ in a fixed metric, put
1183 $g(v)=(P_{R_1}-P_{R_0})v$. Then
1184 \[
1185 \nn{o_0(v)}^2=\nn{o_1(v)}^2+\nn{g(v)}^2,
1186 \quad
1187 \dist(v,R_0)^2=\dist(v,R_1)^2+\nn{g(v)}^2.
1188 \]
1189 No uniform conditioning constant exists across all nonzero scalar compatibility maps.
1190 
1191 \end{theorem}
1192 \begin{proof}
1193 
1194 Restrict $\delta$ to $K^\perp$. It is injective: a zero image lies in both
1195 $K$ and $K^\perp$. A finite-dimensional injective linear map has a positive
1196 lower norm bound, giving $\sigma$; the zero domain is harmless and permits
1197 any positive choice. If the residual-only inequality holds, every $v\in K$
1198 has zero distance to $\Ran A$. Finite-dimensional ranges are closed, so
1199 $v\in\Ran A$. Conversely exactness removes $o(v)$ in SR-27.
1200 
1201 Nested orthogonal projections split $o_0(v)=o_1(v)+g(v)$ into orthogonal
1202 sectors, and the inconsistency component stays fixed. Pythagoras gives
1203 both refinement identities. For the scalar family $\delta_s(x)=sx$, $s>0$,
1204 take $R=0$ and $v=1$. The reconstruction distance is one and the residual
1205 is $s$. For any proposed common $c$, choosing $s$ sufficiently small
1206 violates $1\le cs$. The theorem guarantees a constant per presentation,
1207 not a common constant across degenerating presentations.
1208 
1209 \end{proof}
1210 
1211 \src{HilbertConditioning.exists_coercivity_finite; FiniteGlobalization.finite_residual_bound_iff_exact; GlobalizationRefinement.obstruction_refinement_sq; GlobalizationRefinement.distance_refinement_sq; GlobalizationExamples.no_uniform_conditioning_over_scalar_family}
1212 
1213 
1214 \begin{example}[A complete error split]
1215 For $A(g)=(g,0,0)$, $\delta(x,y,z)=2z$, and $v=(3,4,5)$,
1216 the components are $(3,0,0)$, $(0,4,0)$, and $(0,0,5)$.
1217 The squared reconstruction distance is $41=16+25$. The compatibility
1218 residual has squared norm $100$, and $\sigma=2$ is sharp on $K^\perp$.
1219 Thus the conditioned upper bound is attained: $16+100/4=41$.
1220 \end{example}
1221 
1222 
1223 \section{Canonical minimum-norm reconstruction}
1224 
1225 Let $A:G\to V$ be bounded between real Hilbert spaces, with actual closed
1226 range $R=\Ran A$. Write $N_A=\ker A$ and $S=N_A^\perp$.
1227 Closedness is a substantive hypothesis for a bounded exact inverse. It will
1228 be removed for regularized recovery in the following sections.
1229 
1230 
1231 \par{\small\textbf{Hypotheses.} Bounded real Hilbert operator A with actual closed range; core needs complete source/\allowbreak range and orthogonal projections.}\par
1232 
1233 \begin{theorem}[SR-29\quad Constructed bounded canonical inverse]\label{SR-29}
1234 
1235 Restriction $A_S:S\to R$ is a bounded linear bijection with bounded inverse.
1236 Define
1237 \[
1238 B=\iota_S A_S^{-1}P_R.
1239 \]
1240 Then $AB=P_R$, $BA=P_S$, $ABA=A$, and $BAB=B$.
1241 Its two projections are symmetric, $\ker B=R^\perp$, and $\Ran B=S$.
1242 The best-image identity $AB=P_R$ and the condition $\Ran B\subseteq S$
1243 uniquely determine $B$.
1244 
1245 \end{theorem}
1246 \begin{proof}
1247 
1248 The restriction is injective because $S\cap\ker A=0$. Every $Ag\in R$
1249 equals $AP_Sg$, so it is surjective. Closed $R$ and closed $S$ are Banach
1250 spaces; the bounded inverse theorem supplies $A_S^{-1}$ as an actual
1251 continuous linear inverse. The definition then gives $AB=P_R$.
1252 For $g$, $BAg$ is the unique element of $S$ with image $Ag$, namely
1253 $P_Sg$. The two inverse identities imply the generalized inverse laws.
1254 Orthogonal projections are symmetric, proving the symmetry conditions.
1255 The definition and injectivity of $A_S^{-1}$ identify the kernel and range.
1256 Finally, if $B'$ has the same best image and values in $S$, then
1257 $B'v-Bv\in S\cap\ker A$ for each $v$, hence it is zero.
1258 This construction is the classical Moore--Penrose inverse with the
1259 actual range and source ambiguity retained.
1260 
1261 \end{proof}
1262 
1263 \src{MinimumNormReconstruction.restrictionEquiv; MinimumNormReconstruction.image_comp_recover; MinimumNormReconstruction.recover_comp_image; MinimumNormReconstruction.recover_unique; ClosedRangeReconstruction.closedRecover}
1264 
1265 \par{\small\textbf{Hypotheses.} Same real Hilbert closed-range constructor; arbitrary data v, candidate g and arbitrary deterministic noise e.}\par
1266 
1267 \begin{theorem}[SR-30\quad All least-squares sources and unique minimum norm]\label{SR-30}
1268 
1269 For every source $g$,
1270 \[
1271 \nn{v-Ag}^2=\dist(v,R)^2+\nn{A(g-Bv)}^2.
1272 \]
1273 All least-squares minimizers are $Bv+k$ with $k\in\ker A$.
1274 Among them $Bv$ is the unique minimum-norm source. Exact source recovery
1275 $BAg=g$ holds exactly for $g\in S$. For data $Ag+e$,
1276 \[
1277 \nn{B(Ag+e)-g}^2=\nn{Be}^2+\nn{P_{N_A}g}^2.
1278 \]
1279 
1280 \end{theorem}
1281 \begin{proof}
1282 
1283 $ABv=P_Rv$, so SR-25's candidate identity with $u=Ag$ proves the first
1284 formula. Equality to the minimum image error is equivalent to
1285 $A(g-Bv)=0$, yielding exactly the affine family of minimizers.
1286 Since $Bv\in S$ and $k\in N_A$, Pythagoras gives
1287 $\nn{Bv+k}^2=\nn{Bv}^2+\nn k^2$. It proves minimum norm and uniqueness.
1288 The identity $BA=P_S$ proves the exact recovery criterion.
1289 For noisy data, linearity gives $B(Ag+e)-g=Be-P_{N_A}g$.
1290 The first term belongs to $S$ and the second to $N_A$, so they are
1291 orthogonal. This last identity does not assume a statistical noise model.
1292 It shows explicitly which source content the operator cannot identify.
1293 
1294 \end{proof}
1295 
1296 \src{MinimumNormOptimality.candidate_error_decomposition; MinimumNormOptimality.all_least_squares_sources; MinimumNormOptimality.unique_minimum_norm_least_squares; MinimumNormOptimality.exact_source_recovery_iff; MinimumNormOptimality.noisy_source_error_sq}
1297 
1298 \par{\small\textbf{Hypotheses.} Closed-range A; alpha>0 with alpha\(\Vert\)g\(\Vert\le\Vert\)Ag\(\Vert\) on S; computed source h may contain a kernel component.}\par
1299 
1300 \begin{theorem}[SR-31\quad Source conditioning and solver ambiguity]\label{SR-31}
1301 
1302 Some $\alpha>0$ satisfies $\alpha\nn g\le\nn{Ag}$ on $S$, and any supplied
1303 such constant gives $\nn B\le1/\alpha$. Therefore
1304 \[
1305 \nn{B(Ag+e)-g}^2\le(\nn e/\alpha)^2+\nn{P_{N_A}g}^2.
1306 \]
1307 For an arbitrary computed source $h$,
1308 \[
1309 \nn{h-Bv}^2
1310 \le\left(\frac{\nn{Ah-P_Rv}}\alpha\right)^2+\nn{P_{N_A}h}^2.
1311 \]
1312 If also $\delta A=0$, a compatibility constant $\sigma$ bounds the local
1313 error as in SR-27. The constants $\alpha$ and $\sigma$ have separate roles.
1314 
1315 \end{theorem}
1316 \begin{proof}
1317 
1318 The bounded inverse on $S$ gives
1319 $\nn g\le\nn B\nn{Ag}$. Taking, for example,
1320 $\alpha=1/(\nn B+1)>0$ handles also the zero complement and proves
1321 existence. For a supplied constant, apply it to $Bv\in S$:
1322 $\alpha\nn{Bv}\le\nn{ABv}=\nn{P_Rv}\le\nn v$.
1323 Take the operator norm and combine with SR-30 for the noisy bound.
1324 For a computed $h$, split
1325 $h-Bv=(P_Sh-Bv)+P_{N_A}h$ orthogonally. Coercivity bounds the first term
1326 by $\nn{Ah-P_Rv}/\alpha$ because $AP_Sh=Ah$.
1327 The compatibility operator bounds distance of local data to realizability;
1328 the forward operator bounds source amplification. Neither condition
1329 establishes the other. A small fit without control of the computed kernel
1330 component does not certify the minimum-norm source.
1331 
1332 \end{proof}
1333 
1334 \src{SourceConditioning.exists_source_coercivity; SourceConditioning.recover_opNorm_bound; SourceConditioning.noisy_source_bound_sq; SourceConditioning.candidate_source_bound_sq; ReconstructionGlobalization.two_condition_reconstruction}
1335 
1336 \par{\small\textbf{Hypotheses.} Bounded A between real Hilbert spaces; actual range closedness; bounded recovery BA=P\_S or off-kernel coercivity.}\par
1337 
1338 \begin{theorem}[SR-32\quad Closed range is equivalent to bounded recovery]\label{SR-32}
1339 
1340 The following conditions are equivalent:
1341 \[
1342 \Ran A\text{ is closed};\qquad
1343 \exists\alpha>0:\alpha\nn g\le\nn{Ag}\ (g\in S);
1344 \qquad \exists B\text{ bounded}:BA=P_S.
1345 \]
1346 Thus a nonclosed range admits no bounded exact identifiable-source recovery.
1347 Finite-dimensional source or target supplies closed range. There is no common
1348 inverse-sensitivity constant across all nonzero real scalar forward maps.
1349 
1350 \end{theorem}
1351 \begin{proof}
1352 
1353 Closed range gives the bounded constructor and coercivity by SR-29--SR-31.
1354 Conversely suppose coercivity holds. If $Ag_n$ converges in $V$, replace
1355 $g_n$ by $P_Sg_n$ without changing its image. Coercivity makes this source
1356 sequence Cauchy. Completeness gives a limit $g\in S$, and continuity gives
1357 the image limit $Ag\in\Ran A$. Hence the range is closed.
1358 If bounded $B$ satisfies $BA=P_S$, then for $g\in S$,
1359 $\nn g=\nn{BAg}\le\nn B\nn{Ag}$. The same positive choice
1360 $1/(\nn B+1)$ gives coercivity. Finite-dimensional image subspaces are
1361 closed in a normed space. Finally $A_cg=cg$, $c>0$, has canonical inverse
1362 $B_cv=v/c$. At $v=c$, data tend to zero with $c$ while the recovered
1363 source remains one, ruling out a common constant as $c\downarrow0$.
1364 
1365 \end{proof}
1366 
1367 \src{ClosedRangeReconstruction.closed_range_iff_coercivity; ClosedRangeReconstruction.bounded_recovery_iff_closed_range; ClosedRangeReconstruction.nonclosed_no_bounded_recovery; ReconstructionExamples.no_uniform_source_conditioning}
1368 
1369 
1370 \begin{example}[Source and image are different optima]
1371 Let $A(g_1,g_2)=(g_1+g_2,0,0)$ and $v=(3,4,5)$.
1372 The best image is $(3,0,0)$, with the same squared local error $41$.
1373 The minimum-norm source is $(3/2,3/2)$ of squared norm $9/2$.
1374 The source $(3,0)$ gives the same best image but has squared norm $9$.
1375 Their difference $(3/2,-3/2)$ is kernel ambiguity, not local obstruction.
1376 \end{example}
1377 
1378 
1379 \section{Intrinsic metric obstruction and transport}
1380 
1381 Retain the globalization presentation $\delta A=0$, the actual projected
1382 subspaces $R=\Ran A\subseteq K=\ker\delta$, and the same algebraic quotient
1383 $\mathcal H=K/R$. Its seminorm is the quotient seminorm induced by the
1384 ambient metric. We prove the harmonic equivalence respects that preexisting
1385 seminorm, rather than defining a new norm to match its answer.
1386 
1387 
1388 \par{\small\textbf{Hypotheses.} Real inner-product V; R=range A,K=ker\(\delta\) both projected; \(\delta\) bounded, \(\delta\)A=0; native quotient seminorm.}\par
1389 
1390 \begin{theorem}[SR-33\quad Native quotient norm and isometry]\label{SR-33}
1391 
1392 The equivalence $K/R\cong K\cap R^\perp$ in SR-26 is a linear isometry.
1393 For compatible $v,w$,
1394 \[
1395 \nn{[v]}=\nn{o(v)}=\dist(v,R),\qquad
1396 \dist([v],[w])=\dist(v-w,R).
1397 \]
1398 The quotient norm detects zero classes. Its standard quotient inner
1399 product is preserved when the induced projection structure in $K$ is used.
1400 
1401 \end{theorem}
1402 \begin{proof}
1403 
1404 Let $h$ be the harmonic representative of a class $z$. For any compatible
1405 representative $v$ of $z$, its harmonic component is $h$, and the
1406 nonexpansive harmonic projection gives $\nn h\le\nn v$.
1407 Taking the infimum over representatives proves $\nn h\le\nn z$.
1408 Conversely $h$ itself represents $z$, so the quotient map's norm bound
1409 gives $\nn z\le\nn h$. This proves isometry against the existing quotient
1410 seminorm. The compatible distance formula follows from SR-25, and
1411 distances of classes follow by applying it to $v-w$.
1412 Zero norm implies zero harmonic vector and hence zero class by the inverse
1413 laws. Orthogonal projection onto $R$ restricts to $K$, constructing the
1414 quotient inner-product structure there. A real linear isometry preserves
1415 its inner product by the polarization identity.
1416 
1417 \end{proof}
1418 
1419 \src{MetricObstruction.quotientToHarmonic_norm; MetricObstruction.obstructionIsometry; MetricObstruction.norm_class_eq_infDist; MetricObstruction.distance_classes; MetricObstruction.quotient_inner_preserved}
1420 
1421 \par{\small\textbf{Hypotheses.} Same projected real presentation; arbitrary v for projected class c(v)=[P\_Kv]; complete/\allowbreak closed source range only when canonical inverse B used.}\par
1422 
1423 \begin{theorem}[SR-34\quad Minimum representatives and intrinsic class of data]\label{SR-34}
1424 
1425 Every class $z$ has a unique compatible minimum-norm representative $s(z)$,
1426 and every compatible representative $v$ satisfies
1427 \[
1428 \nn v^2=\nn z^2+\nn{v-s(z)}^2.
1429 \]
1430 For arbitrary data define $c(v)=[P_Kv]$. This is nonexpansive and
1431 \[
1432 \dist(v,R)^2=\nn{c(v)}^2+\nn{i(v)}^2.
1433 \]
1434 The datum is realizable exactly when both $c(v)=0$ and $\delta v=0$.
1435 When the canonical inverse exists,
1436 \[
1437 \nn{v-Ag}^2=\nn{c(v)}^2+\nn{i(v)}^2+\nn{A(g-Bv)}^2.
1438 \]
1439 
1440 \end{theorem}
1441 \begin{proof}
1442 
1443 Take $s(z)$ to be its harmonic representative from SR-33. The difference
1444 between any other compatible representative and $s(z)$ lies in $R$,
1445 which is orthogonal to the harmonic sector. Pythagoras gives the first
1446 formula, including unique attainment of the minimum.
1447 The composition of $P_K$ and the quotient map is bounded by one; its
1448 harmonic representative is $o(v)$. SR-25 and SR-33 give the intrinsic
1449 distance identity. If both displayed tests vanish, then $v\in K$ and
1450 its obstruction class is zero, so SR-03 supplies a source. Realizability
1451 implies both tests directly. Finally combine the candidate identity
1452 of SR-30 with the intrinsic distance split. The minimum representative
1453 of an obstruction class belongs to local data space; it is a different
1454 construction from the minimum-norm global source $Bv$.
1455 
1456 \end{proof}
1457 
1458 \src{MetricRepresentatives.unique_minimum_representative; MetricRepresentatives.representative_error_energy; IntrinsicGlobalization.projectedClass_opNorm_le; IntrinsicGlobalization.intrinsic_distance_sq; IntrinsicGlobalization.realizable_iff_class_and_residual_zero; IntrinsicGlobalization.intrinsic_candidate_total_error}
1459 
1460 \par{\small\textbf{Hypotheses.} Commuting linear presentation maps; whole local-map norm bound C\(\ge\)0; reverse presentation with bound M>0 and induced left inverse for two-sided estimate.}\par
1461 
1462 \begin{theorem}[SR-35\quad Bounded quotient transport and reflection]\label{SR-35}
1463 
1464 A presentation map with $\nn{Lv}\le C\nn v$ induces the same quotient map
1465 as in SR-03, now satisfying
1466 \[
1467 \nn{\overline Lz}\le C\nn z.
1468 \]
1469 If a reverse presentation has bound $M>0$ and its quotient map is a left
1470 inverse of $\overline L$, then
1471 \[
1472 \frac{\nn z}{M}\le\nn{\overline Lz}\le C\nn z.
1473 \]
1474 The corresponding class distances satisfy the same bounds.
1475 
1476 \end{theorem}
1477 \begin{proof}
1478 
1479 For any representative $v$ of $z$, the quotient norm of $[Lv]$ is at most
1480 $\nn{Lv}\le C\nn v$. Infimizing over representatives gives the upper bound
1481 and supplies a bounded linear map with exactly the algebraic action of
1482 SR-03. Alternatively, the minimum representative from SR-34 realizes the
1483 infimum and yields it immediately. Apply the reverse bound to
1484 $\overline Lz$: the left-inverse identity gives
1485 $\nn z\le M\nn{\overline Lz}$. Division by positive $M$ proves the lower
1486 bound. Apply the bounds to $z-w$ for distances. Forward boundedness alone
1487 does not prove reflection; the reverse identity is genuine additional data.
1488 
1489 \end{proof}
1490 
1491 \src{MetricObstructionTransport.obstructionMap_norm_le; MetricObstructionTransport.boundedObstructionMap_opNorm; MetricObstructionTransport.reverse_bound; MetricObstructionTransport.two_sided_bound}
1492 
1493 \par{\small\textbf{Hypotheses.} Projected nested R0\(\le\)R1\(\le\)K in fixed real metric for energy; arbitrary submodule R in real normed space for nonclosed seminorm boundary.}\par
1494 
1495 \begin{theorem}[SR-36\quad Metric refinement and nonclosed boundary]\label{SR-36}
1496 
1497 Range enlargement induces a surjective contraction $F:K/R_0\to K/R_1$.
1498 For the old minimum representative $s_0(z)$,
1499 \[
1500 \nn z^2=\nn{Fz}^2+\nn{(P_{R_1}-P_{R_0})s_0(z)}^2.
1501 \]
1502 Without a closedness or projection hypothesis, a general quotient instead has
1503 \[
1504 \nn{[v]}=0\iff v\in\cl R,\qquad [v]=0\iff v\in R.
1505 \]
1506 Thus its seminorm detects zero exactly when $R$ is closed. Nonclosed range
1507 can leave a nonzero class of zero seminorm.
1508 
1509 \end{theorem}
1510 \begin{proof}
1511 
1512 The larger realization submodule contains the smaller, so the identity
1513 on $K$ descends to a surjection of quotients. Every old representative is
1514 a new representative, proving contraction by the quotient infimum.
1515 For the energy identity apply the orthogonal refinement identity in
1516 SR-28 to $s_0(z)$, whose old norm is $\nn z$. The new harmonic component
1517 represents $Fz$ and has norm $\nn{Fz}$ by SR-33.
1518 
1519 For any submodule, the native quotient seminorm equals distance to that
1520 submodule. Zero distance is equivalent to membership in its closure by
1521 the metric closure criterion; algebraic quotient zero remains actual
1522 membership. If $R$ is nonclosed, choose $v\in\cl R\setminus R$.
1523 Its class is nonzero with zero seminorm. Conversely closedness makes
1524 zero distance imply membership. This is why the projection hypotheses
1525 in the preceding metric theory cannot be discarded silently.
1526 
1527 \end{proof}
1528 
1529 \src{MetricRefinement.refinementMap_surjective; MetricRefinement.refinementMap_norm_le; MetricRefinement.quotient_refinement_energy; QuotientMetricBoundaries.zero_norm_iff_closure; QuotientMetricBoundaries.nonclosed_nonzero_zero_norm; QuotientMetricBoundaries.norm_detects_zero_iff_closed}
1530 
1531 
1532 \begin{example}[A metric must survive its coordinate change]
1533 For $K=\{(x,y,0)\}$ and $R=\spanof\{(1,0,0)\}$, take the compatible basis
1534 $b_1=(1,0,0)$, $b_2=(1,2,0)$. Its Gram matrix is
1535 $\bigl(\begin{smallmatrix}1&1\\1&5\end{smallmatrix}\bigr)$.
1536 The vector $(3,4,0)$ has coordinates $(1,2)$; its harmonic representative
1537 $(0,4,0)$ has coordinates $(-2,2)$ and squared norm $16$ in that Gram metric.
1538 Computing with an untransported coordinate Euclidean metric would change
1539 the problem. Redundant or nonorthogonal coordinates do not license such a change.
1540 \end{example}
1541 
1542 
1543 \section{Tikhonov construction, bias, and perturbation}
1544 
1545 Fix a bounded operator $A:G\to V$ between real Hilbert spaces, without
1546 assuming closed range. For $\lambda>0$, put
1547 \[
1548 N_\lambda=A^*A+\lambda I,\qquad R_\lambda=N_\lambda^{-1},\qquad
1549 B_\lambda=R_\lambda A^*.
1550 \]
1551 The inverse is constructed from coercivity. It is not supplied as a
1552 certificate premise. Here $A^*$ is the actual Hilbert adjoint.
1553 
1554 
1555 \par{\small\textbf{Hypotheses.} Real Hilbert G,V; actual bounded A and lambda>0; no finite dimension or closed range.}\par
1556 
1557 \begin{theorem}[SR-37\quad Constructed normal inverse and energy]\label{SR-37}
1558 
1559 $N_\lambda$ is a bounded bijection with bounded inverse $R_\lambda$.
1560 For $x_\lambda=B_\lambda v$,
1561 \[
1562 N_\lambda x_\lambda=A^*v,\qquad
1563 A^*(Ax_\lambda-v)+\lambda x_\lambda=0,
1564 \]
1565 and
1566 \[
1567 \nn{Ax_\lambda}^2+\lambda\nn{x_\lambda}^2
1568 =\ip v{Ax_\lambda}.
1569 \]
1570 
1571 \end{theorem}
1572 \begin{proof}
1573 
1574 The bilinear form
1575 $b(x,y)=\ip{Ax}{Ay}+\lambda\ip xy$ is bounded and satisfies
1576 $b(x,x)\ge\lambda\nn x^2$. Lax--Milgram gives a continuous linear
1577 equivalence from the source to itself under the Riesz identification.
1578 The adjoint identity identifies its map with $A^*A+\lambda I$.
1579 The two inverse laws give an actual resolvent. Applying one inverse law
1580 to $A^*v$ yields the normal equation. Taking its inner product with
1581 $x_\lambda$ and using $\ip{A^*v}{x_\lambda}=\ip v{Ax_\lambda}$ gives
1582 the energy identity. Strictly positive $\lambda$ supplies coercivity
1583 even if $A$ has a nontrivial kernel or a nonclosed range.
1584 
1585 \end{proof}
1586 
1587 \src{TikhonovConstruction.normalForm_coercive; TikhonovConstruction.normalEquiv_apply; TikhonovConstruction.normal_resolvent; TikhonovConstruction.resolvent_normal; TikhonovConstruction.normal_equation; TikhonovConstruction.solution_energy}
1588 
1589 \par{\small\textbf{Hypotheses.} Same real Hilbert bounded A with lambda>0; arbitrary source candidate x and data v; actual normal residual.}\par
1590 
1591 \begin{theorem}[SR-38\quad Objective optimality and sharp fixed-parameter bounds]\label{SR-38}
1592 
1593 For $F_\lambda(v,x)=\nn{Ax-v}^2+\lambda\nn x^2$,
1594 \[
1595 F_\lambda(v,x)=F_\lambda(v,x_\lambda)
1596 +\nn{A(x-x_\lambda)}^2+\lambda\nn{x-x_\lambda}^2.
1597 \]
1598 Thus $x_\lambda$ is the unique minimizer and lies in $(\ker A)^\perp$.
1599 The whole-map bounds are
1600 \[
1601 \nn{R_\lambda}\le1/\lambda,\qquad
1602 \nn{B_\lambda}\le\frac1{2\sqrt\lambda},\qquad
1603 \nn{AB_\lambda v}\le\nn v,\quad\nn{AB_\lambda v-v}\le\nn v.
1604 \]
1605 For $r=N_\lambda x-A^*v$, one has
1606 $x-x_\lambda=R_\lambda r$ and $\nn{x-x_\lambda}\le\nn r/\lambda$.
1607 
1608 \end{theorem}
1609 \begin{proof}
1610 
1611 Expand both squared norms around $x_\lambda$. Their cross terms combine to
1612 \[
1613 2\ip{A^*(Ax_\lambda-v)+\lambda x_\lambda}{x-x_\lambda},
1614 \]
1615 which vanishes by SR-37. The remaining positive terms prove the increment
1616 identity and uniqueness. Taking the normal equation against a kernel
1617 vector $k$ yields $\lambda\ip{x_\lambda}k=0$, proving source orthogonality.
1618 
1619 For $y=R_\lambda r$, its energy gives
1620 $\lambda\nn y^2\le\ip ry\le\nn r\nn y$, hence the resolvent bound.
1621 For $x_\lambda$, set $u=\nn{Ax_\lambda}$. The energy gives
1622 $u^2+\lambda\nn{x_\lambda}^2\le\nn v\,u$.
1623 Completing the square in $u$ yields
1624 $4\lambda\nn{x_\lambda}^2\le\nn v^2$ and also $u\le\nn v$.
1625 Comparing the minimum objective with $F_\lambda(v,0)=\nn v^2$ bounds the
1626 fitting residual. Subtract the exact normal equation from the computed
1627 one and apply the resolvent for the correction identity.
1628 
1629 \end{proof}
1630 
1631 \src{TikhonovOptimality.objective_increment; TikhonovOptimality.unique_minimizer; TikhonovBounds.resolvent_opNorm_bound; TikhonovBounds.regularized_opNorm_bound; TikhonovBounds.approximate_solver_bound; TikhonovBounds.source_kernel_orthogonal}
1632 
1633 \par{\small\textbf{Hypotheses.} Same positive Tikhonov construction; arbitrary g,e; source-coercivity alpha>0 only for conditioned bound; g=A*Aw only for source-condition rate.}\par
1634 
1635 \begin{theorem}[SR-39\quad Bias, noise, and kernel content]\label{SR-39}
1636 
1637 Write $p=P_{(\ker A)^\perp}g$, $k=P_{\ker A}g$. Then
1638 \[
1639 B_\lambda Ag+\lambda R_\lambda g=g,
1640 \quad B_\lambda(Ag+e)-g=-\lambda R_\lambda g+B_\lambda e,
1641 \]
1642 and
1643 \[
1644 \nn{B_\lambda(Ag+e)-g}^2
1645 =\nn{-\lambda R_\lambda p+B_\lambda e}^2+\nn k^2.
1646 \]
1647 If $A$ has source coercivity $\alpha>0$, this is at most
1648 \[
1649 \left(\frac\lambda{\alpha^2+\lambda}\nn p
1650 +\frac{\nn e}{2\sqrt\lambda}\right)^2+\nn k^2.
1651 \]
1652 For a supplied source condition $g=A^*Aw$,
1653 $\nn{B_\lambda Ag-g}\le\lambda\nn w$ without requiring closed range.
1654 
1655 \end{theorem}
1656 \begin{proof}
1657 
1658 The inverse identity $R_\lambda(A^*A+\lambda I)=I$ gives the filter
1659 decomposition. Linearity adds the propagated noise. On $\ker A$,
1660 $N_\lambda$ acts as $\lambda I$, so $\lambda R_\lambda k=k$.
1661 The resolvent preserves the orthogonal complement: pairing its normal
1662 equation with every kernel vector proves this directly. Thus the combined
1663 identifiable error is orthogonal to $k$, giving the exact squared formula.
1664 Bias and noise inside that first term need not be orthogonal to each other.
1665 
1666 For $y=R_\lambda p\in(\ker A)^\perp$, source coercivity and its energy
1667 give $(\alpha^2+\lambda)\nn y^2\le\nn p\nn y$.
1668 Multiply by $\lambda$ and combine with the noise bound in SR-38.
1669 For $g=A^*Aw$, the normal-range source filter is a contraction, so
1670 $\nn{R_\lambda A^*Aw}\le\nn w$. Multiplication by $\lambda$ proves
1671 the source-condition bias rate. The representation by $w$ is supplied;
1672 no controlled $w$ is asserted for every identifiable source.
1673 
1674 \end{proof}
1675 
1676 \src{TikhonovBias.filter_decomposition; TikhonovBias.noisy_source_error_squared; TikhonovBias.full_conditioned_error_squared; TikhonovBias.source_condition_bias_bound}
1677 
1678 \par{\small\textbf{Hypotheses.} Real Hilbert bounded A,C; positive lambda,mu; actual closed range only for B=A-dagger and intrinsic globalization formulas.}\par
1679 
1680 \begin{theorem}[SR-40\quad Resolvent sensitivity and irreducible local error]\label{SR-40}
1681 
1682 For two operators and parameters,
1683 \[
1684 R_{A,\lambda}-R_{C,\mu}
1685 =R_{A,\lambda}(N_{C,\mu}-N_{A,\lambda})R_{C,\mu}.
1686 \]
1687 At fixed positive $\lambda$, with $\epsilon=\nn{A-C}$,
1688 \[
1689 \nn{B_{A,\lambda}-B_{C,\lambda}}
1690 \le\frac\epsilon\lambda+
1691 \frac{(\nn A+\nn C)\epsilon\nn C}{\lambda^2}.
1692 \]
1693 If $A$ has closed range and canonical inverse $B$, then
1694 $B_\lambda v-Bv=-\lambda R_\lambda Bv$. For $\delta A=0$,
1695 \[
1696 \nn{v-AB_\lambda v}^2
1697 =\nn{c(v)}^2+\nn{i(v)}^2+\nn{A(B_\lambda v-Bv)}^2.
1698 \]
1699 
1700 \end{theorem}
1701 \begin{proof}
1702 
1703 Multiply the difference of inverses on the left and right by their
1704 normal operators, or insert their inverse laws, to obtain the resolvent
1705 identity. SR-38 bounds its norm by
1706 $\nn{N_{C,\mu}-N_{A,\lambda}}/(\lambda\mu)$.
1707 At equal parameters,
1708 $C^*C-A^*A=(C^*-A^*)C+A^*(C-A)$, whose norm is at most
1709 $(\nn A+\nn C)\epsilon$. Splitting
1710 $R_AA^*-R_CC^*=R_A(A^*-C^*)+(R_A-R_C)C^*$ proves the stated bound.
1711 It permits rank changes and is not uniform as $\lambda$ vanishes.
1712 
1713 Under closed range, $A^*$ ignores the part of data orthogonal to
1714 $\Ran A$, so $B_\lambda v=B_\lambda ABv$. Apply the filter identity
1715 to $Bv$ for its bias. The intrinsic candidate identity SR-34 with
1716 $g=B_\lambda v$ yields the local error split. Regularization introduces
1717 image bias while retaining the same obstruction and inconsistency.
1718 
1719 \end{proof}
1720 
1721 \src{TikhonovPerturbation.resolvent_difference; TikhonovPerturbation.regularized_operator_difference_bound; TikhonovGlobalization.regularized_pseudoinverse_bias; TikhonovGlobalization.regularized_intrinsic_error}
1722 
1723 
1724 \begin{example}[Exact scalar response and a two-coordinate example]
1725 For $A_cx=cx$, $B_\lambda v=cv/(c^2+\lambda)$.
1726 At $c>0$, $\lambda=c^2$, the value is $v/(2c)$, attaining the noise bound.
1727 For $A(g_1,g_2)=(g_1+g_2,0,0)$, $v=(3,4,5)$, and $\lambda=1$,
1728 the source is $(1,1)$. Its squared fit is $42=16+25+1$, separating
1729 obstruction, inconsistency, and regularization image bias. Its objective
1730 is $44$, whereas the unregularized source $(3/2,3/2)$ has penalized
1731 objective $91/2$. Positive regularization solves its own stated objective.
1732 \end{example}
1733 
1734 
1735 \section{Strong limits and the uniform boundary}
1736 
1737 The following limits fix one bounded $A$ between real Hilbert spaces.
1738 Statements can be indexed by an arbitrary filter. When uniqueness of
1739 limits or a converse is used, the filter is required to be nontrivial.
1740 Closed range is unnecessary for strong convergence on each fixed source.
1741 
1742 
1743 \par{\small\textbf{Hypotheses.} Fixed bounded real Hilbert A; positive lambda\_i\(\to\)0 along a filter; arbitrary fixed g; nontrivial filter for exact-limit iff identifiability.}\par
1744 
1745 \begin{theorem}[SR-41\quad Density and strong identifiable-source convergence]\label{SR-41}
1746 
1747 One has $\cl\Ran(A^*A)=(\ker A)^\perp$, and for every $g,w$,
1748 \[
1749 \nn{B_\lambda Ag-g}\le\nn{g-A^*Aw}+\lambda\nn w.
1750 \]
1751 As $\lambda\downarrow0$,
1752 \[
1753 B_\lambda Ag\longrightarrow P_{(\ker A)^\perp}g,
1754 \qquad \nn{B_\lambda Ag-g}\longrightarrow\nn{P_{\ker A}g}.
1755 \]
1756 For a nontrivial parameter filter, convergence to $g$ itself holds exactly
1757 when $g\in(\ker A)^\perp$.
1758 
1759 \end{theorem}
1760 \begin{proof}
1761 
1762 If $x$ is orthogonal to $\Ran(A^*A)$, pairing with $A^*Ax$ gives
1763 $\nn{Ax}^2=0$. Conversely a kernel vector is orthogonal to every
1764 $A^*Aw$ by the adjoint identity. Thus
1765 $(\Ran(A^*A))^\perp=\ker A$, and taking orthogonal complements gives
1766 the closure identity. Decompose the bias into the bias of
1767 $g-A^*Aw$ and of $A^*Aw$. The first is bounded by its input norm because
1768 $\lambda R_\lambda$ is contractive; the second is bounded by
1769 $\lambda\nn w$ from SR-39.
1770 
1771 For identifiable $p$, density lets us choose $w$ making the first term
1772 arbitrarily small, independently of $\lambda$. Then let $\lambda$ tend
1773 to zero to remove the second. For arbitrary $g$, $Ag=Ap$ with
1774 $p=P_{(\ker A)^\perp}g$, yielding the claimed source limit.
1775 Subtracting $g$ and taking norms gives the kernel-error limit.
1776 Uniqueness of limits on a nontrivial filter gives the final equivalence.
1777 
1778 \end{proof}
1779 
1780 \src{TikhonovDensity.gram_range_closure; TikhonovDensity.source_approximation_bound; TikhonovConvergence.tendsto_source; TikhonovConvergence.exact_limit_iff_identifiable; TikhonovConvergence.tendsto_error_norm}
1781 
1782 \par{\small\textbf{Hypotheses.} Fixed real Hilbert bounded A; lambda\_i>0\(\to\)0; deterministic noise with \(\Vert\)e\_i\(\Vert\)/\allowbreak sqrt(lambda\_i)\(\to\)0; actual normal residual scale vanishes for computed sources.}\par
1783 
1784 \begin{theorem}[SR-42\quad Noise schedules and inexact strong limits]\label{SR-42}
1785 
1786 If $\lambda_i>0$ tends to zero and
1787 $\nn{e_i}/\sqrt{\lambda_i}\to0$, then
1788 \[
1789 B_{\lambda_i}(Ag+e_i)\longrightarrow P_{(\ker A)^\perp}g.
1790 \]
1791 The same limit holds for computed $x_i$ when additionally
1792 \[
1793 \frac{\nn{(A^*A+\lambda_iI)x_i-A^*(Ag+e_i)}}{\lambda_i}\to0.
1794 \]
1795 For example, $\lambda_i=s_i^2$, $s_i>0\to0$, and $\nn{e_i}\le s_i^2$
1796 give the exact-solve consistency condition.
1797 
1798 \end{theorem}
1799 \begin{proof}
1800 
1801 The source difference between noisy and exact-data reconstruction is
1802 $B_{\lambda_i}e_i$, whose norm is at most
1803 $\nn{e_i}/(2\sqrt{\lambda_i})$ by SR-38. Combine its vanishing with
1804 the exact-source limit in SR-41. For computed sources, the normal-residual
1805 correction in SR-38 bounds their difference from the actual regularized
1806 source by precisely the second displayed scale. The triangle inequality
1807 then proves the same limit. In the square schedule, the noise ratio is
1808 at most $s_i$, hence vanishes. These schedules are sufficient conditions;
1809 they are not asserted necessary for every favorable operator or noise direction.
1810 
1811 \end{proof}
1812 
1813 \src{NoisyRegularization.noisy_source_tendsto; NoisyRegularization.noisy_inexact_solver_tendsto; NoisyRegularization.square_schedule_consistent}
1814 
1815 \par{\small\textbf{Hypotheses.} Fixed real Hilbert bounded A; positive parameter family\(\to\)0; nontrivial filter for iff; source conditioning alpha only for positive estimate.}\par
1816 
1817 \begin{theorem}[SR-43\quad Operator-norm convergence exactly at closed range]\label{SR-43}
1818 
1819 Let $E_\lambda=B_\lambda A-P_{(\ker A)^\perp}$. Always $\nn{E_\lambda}\le1$.
1820 If $\Ran A$ is nonclosed, then $\nn{E_\lambda}=1$ for every positive parameter.
1821 For a positive family tending to zero along a nontrivial filter,
1822 \[
1823 E_\lambda\to0\text{ in operator norm}\iff\Ran A\text{ is closed}.
1824 \]
1825 Under source coercivity $\alpha>0$,
1826 $\nn{E_\lambda}\le\lambda/(\alpha^2+\lambda)$.
1827 
1828 \end{theorem}
1829 \begin{proof}
1830 
1831 The projected bias bound from SR-39 gives the universal upper bound one.
1832 Suppose any bounded $B'$ satisfies
1833 $c=\nn{B'A-P_S}<1$, where $S=(\ker A)^\perp$.
1834 For $x\in S$,
1835 \[
1836 \nn x\le\nn{x-B'Ax}+\nn{B'Ax}
1837 \le c\nn x+\nn{B'}\nn{Ax}.
1838 \]
1839 Therefore $\alpha=(1-c)/(\nn{B'}+1)>0$ supplies off-kernel coercivity,
1840 forcing closed range by SR-32. A nonclosed range thus cannot have
1841 $\nn{E_\lambda}<1$, proving equality. For closed range, source coercivity
1842 exists and the conditioned bias bound yields the displayed quantity tending
1843 to zero. Conversely convergence to zero contradicts the constant norm one
1844 on any nontrivial filter. Strong convergence in SR-41 remains valid in
1845 the nonclosed case because it fixes a source before taking the limit.
1846 
1847 \end{proof}
1848 
1849 \src{UniformRegularization.closed_range_of_approximate_recovery; UniformRegularization.nonclosed_sourceError_norm; UniformRegularization.conditioned_sourceError_norm; UniformRegularization.uniform_convergence_iff_closed_range}
1850 
1851 \par{\small\textbf{Hypotheses.} Fixed real Hilbert bounded A; positive lambda\_i\(\to\)0; data noise\(\to\)0 for fitted limit; nontrivial filter for impossible source limit.}\par
1852 
1853 \begin{theorem}[SR-44\quad Fitted-data limit and absent source limit]\label{SR-44}
1854 
1855 For arbitrary data $v$,
1856 \[
1857 AB_\lambda^Av=B_\lambda^{A^*}A^*v
1858 \longrightarrow P_{\cl\Ran A}v.
1859 \]
1860 Adding data noise $e_i\to0$ preserves this fitted-data limit.
1861 If $v\in\cl\Ran A\setminus\Ran A$, fitted data converge to $v$ but the
1862 corresponding reconstructed source family has no norm limit in $G$.
1863 
1864 \end{theorem}
1865 \begin{proof}
1866 
1867 The identity
1868 $(AA^*+\lambda I)A=A(A^*A+\lambda I)$ and uniqueness of the positive
1869 normal inverse prove the dual formula. Apply SR-41 to the bounded
1870 operator $A^*$ with source $v$. Its identifiable space is
1871 $(\ker A^*)^\perp=\cl\Ran A$, yielding the fitted limit.
1872 SR-38 shows $AB_\lambda$ is contractive, so changing data by $e_i$
1873 changes the fitted value by at most $\nn{e_i}$.
1874 If reconstructed sources converged in norm to some $g$, continuity of
1875 $A$ would make their images converge to $Ag$. On a nontrivial filter,
1876 the already established image limit $v$ would force $Ag=v$, contrary
1877 to $v\notin\Ran A$. This proves absence of a source norm limit without
1878 adding an unproved assertion that source norms diverge.
1879 
1880 \end{proof}
1881 
1882 \src{RegularizedDataLimit.fitted_adjoint_identity; RegularizedDataLimit.fitted_data_tendsto; RegularizedDataLimit.noisy_fitted_data_tendsto; RegularizedDataLimit.unrealizable_no_source_limit}
1883 
1884 \section{Discrepancy selection and strong consistency}
1885 
1886 Still fix a known bounded $A$ between real Hilbert spaces. Define the actual
1887 residual curve on positive parameters
1888 $r_v(\lambda)=\nn{AB_\lambda v-v}$. Its parameter is mathematical data,
1889 not an assumed noise estimate. Let $\eta$ be a justified true-data allowance
1890 and $\tau>1$ a band multiplier. A total rule must include a small-data branch.
1891 
1892 
1893 \par{\small\textbf{Hypotheses.} Real Hilbert bounded A; lambda>0; strict floor dist(v,range A)<rho<\(\Vert\)v\(\Vert\) for existence; actual positive parameter only.}\par
1894 
1895 \begin{theorem}[SR-45\quad Actual residual curve and unique interior root]\label{SR-45}
1896 
1897 The residual is continuous and nondecreasing on positive parameters;
1898 the source norm is nonincreasing. It is strictly increasing when $A^*v\ne0$,
1899 and constant at $\nn v$ when $A^*v=0$.
1900 For
1901 \[
1902 \dist(v,\Ran A)<\rho<\nn v,
1903 \]
1904 there is exactly one $\lambda>0$ with $r_v(\lambda)=\rho$.
1905 The resulting exact real parameter is a noncomputable choice with a proved
1906 specification.
1907 
1908 \end{theorem}
1909 \begin{proof}
1910 
1911 Compare the minimum objectives at $0<\lambda<\mu$ using each minimizer
1912 as a competitor for the other. Adding the two inequalities gives
1913 $(\mu-\lambda)(\nn{x_\mu}^2-\nn{x_\lambda}^2)\le0$, so source norms
1914 are antitone. Substitution back into the smaller-parameter comparison
1915 shows residual monotonicity. If the two residuals were equal, both
1916 norms and objective values would be equal, and unique minimization would
1917 give $x_\lambda=x_\mu$. Subtracting their normal equations gives
1918 $(\mu-\lambda)x_\lambda=0$, hence $x_\lambda=0$ and $A^*v=0$.
1919 This proves strictness and the constant case.
1920 
1921 The resolvent parameter identity gives, for $s,t\ge a>0$,
1922 \[
1923 |r_v(s)-r_v(t)|\le
1924 \frac{\nn A\nn{A^*v}}{a^2}|s-t|,
1925 \]
1926 proving continuity on positive compact intervals. The strict floor permits
1927 a comparator $g$ with $\nn{Ag-v}<\rho$; objective minimization at sufficiently
1928 small positive $\lambda$ gives a lower residual bracket. For large
1929 $\lambda$, $\nn{B_\lambda v}\le\nn{A^*v}/\lambda$, so the residual
1930 approaches $\nn v>\rho$ and gives an upper bracket. The intermediate
1931 value theorem provides a root; strictness gives uniqueness. The floor
1932 condition itself excludes the constant orthogonal-data case.
1933 
1934 \end{proof}
1935 
1936 \src{DiscrepancyResidual.source_norm_antitone; DiscrepancyResidual.residual_strictMono; DiscrepancyResidual.residual_constant_of_adjoint_zero; DiscrepancyResidual.residual_difference_bound; DiscrepancySelection.exists_unique_parameter_of_distance}
1937 
1938 \par{\small\textbf{Hypotheses.} Fixed bounded real Hilbert A; p\(\in\)(ker A)\(\perp\); family norm bounds \(\Vert\)x\_i\(\Vert\le\Vert\)p\(\Vert\) and true residual \(\Vert\)Ax\_i-Ap\(\Vert\to\)0.}\par
1939 
1940 \begin{theorem}[SR-46\quad Norm domination converts residual convergence to source convergence]\label{SR-46}
1941 
1942 If $\nn{Ag-v}\le r_v(\lambda)$, then $\nn{B_\lambda v}\le\nn g$.
1943 For any $x,p,w$ with $\nn x\le\nn p$,
1944 \[
1945 \nn{x-p}^2\le4\nn p\nn{p-A^*w}+2\nn w\nn{Ax-Ap}.
1946 \]
1947 Consequently, for identifiable fixed $p$, the conditions
1948 $\nn{x_i}\le\nn p$ and $\nn{Ax_i-Ap}\to0$ imply $x_i\to p$ strongly,
1949 without assuming closed range.
1950 
1951 \end{theorem}
1952 \begin{proof}
1953 
1954 Objective minimality gives
1955 $r_v(\lambda)^2+\lambda\nn{B_\lambda v}^2
1956 \le\nn{Ag-v}^2+\lambda\nn g^2$. The residual ordering and positive
1957 $\lambda$ imply norm domination.
1958 For the source estimate, expand $\nn{x-p}^2$ and use $\nn x\le\nn p$
1959 to obtain $\nn{x-p}^2\le2\ip p{p-x}$.
1960 Write $p=(p-A^*w)+A^*w$. The first pairing is at most
1961 $\nn{p-A^*w}\nn{p-x}\le2\nn p\nn{p-A^*w}$; the adjoint identity bounds
1962 the second by $\nn w\nn{Ap-Ax}$. This yields the displayed estimate.
1963 For identifiable $p$, the density in SR-41 permits $w$ with
1964 $p-A^*w$ arbitrarily small (take $w=A u$ from the normal range).
1965 Fixing this $w$, the residual term tends to zero. An epsilon argument
1966 then proves norm convergence. No common inverse bound is invoked.
1967 
1968 \end{proof}
1969 
1970 \src{DiscrepancyConvergence.norm_domination_of_residual; DiscrepancyConvergence.source_distance_estimate; DiscrepancyConvergence.norm_control_residual_tendsto}
1971 
1972 \par{\small\textbf{Hypotheses.} Known bounded $A:G\to V$ between real Hilbert spaces and a fixed true source $g$; a valid pointwise allowance $\nn{Ag-v}\le\eta$. Accepted-source consistency uses a fixed $\tau\ge1$ and genuine bounds $\nn{Ag-v_i}\le\eta_i$ with $\eta_i\to0$. Total selector existence additionally requires $\eta>0$ and $\tau>1$.}\par
1973 
1974 \begin{theorem}[SR-47\quad Accepted bands and the total small-data rule]\label{SR-47}
1975 
1976 Call $x$ accepted when either
1977 \[
1978 \nn v\le\tau\eta,\quad x=0,
1979 \]
1980 or $x=B_\lambda v$ for some $\lambda>0$ with
1981 $\eta\le r_v(\lambda)\le\tau\eta$.
1982 With a valid noise allowance, every accepted source satisfies
1983 \[
1984 \nn x\le\nn{P_{(\ker A)^\perp}g},\qquad
1985 \nn{Ax-Ag}\le(\tau+1)\eta.
1986 \]
1987 For accepted families with $\eta_i\to0$,
1988 \[
1989 x_i\to P_{(\ker A)^\perp}g,
1990 \qquad \nn{x_i-g}\to\nn{P_{\ker A}g}.
1991 \]
1992 With $\eta>0$, $\tau>1$, the total selector chooses zero on small data
1993 and otherwise the root $r_v(\lambda)=\tau\eta$. If $g=A^*w$, accepted
1994 sources obey $\nn{x-g}^2\le2\nn w(\tau+1)\eta$.
1995 
1996 \end{theorem}
1997 \begin{proof}
1998 
1999 Let $p=P_{(\ker A)^\perp}g$, so $Ap=Ag$.
2000 In the positive branch, $\nn{Ap-v}\le\eta\le r_v(\lambda)$ gives norm
2001 domination by SR-46; the triangle inequality gives the true residual.
2002 In the zero branch, norm domination is immediate and
2003 $\nn{Ag}\le\nn{Ag-v}+\nn v\le(\tau+1)\eta$.
2004 SR-46 now gives strong convergence to $p$, and continuity of the error
2005 norm gives the kernel limit. For large data, feasibility supplies
2006 $\dist(v,\Ran A)\le\eta<\tau\eta<\nn v$, so SR-45 provides the exact root.
2007 For $g=A^*w$, the approximation term in SR-46 is zero, and the residual
2008 bound proves the squared source-condition rate. General identifiable
2009 sources have no asserted common rate. The rule controls actual Tikhonov
2010 sources; numerical solve errors require the additional certificates below.
2011 
2012 \end{proof}
2013 
2014 \src{DiscrepancyRule.selectedSource_accepted; DiscrepancyRule.accepted_consistent; DiscrepancyRule.selectedSource_consistent; DiscrepancyRule.accepted_error_norm_limit; DiscrepancyRule.accepted_source_rate}
2015 
2016 \par{\small\textbf{Hypotheses.} Known bounded real Hilbert A and positive lambda; real scalar identity case 0<rho<v.}\par
2017 
2018 \begin{theorem}[SR-48\quad Discrepancy endpoints and scalar formulas]\label{SR-48}
2019 
2020 No positive parameter has residual larger than $\nn v$.
2021 When $A^*v\ne0$, none has residual equal to $\nn v$.
2022 For every positive parameter, $r_v(\lambda)=0$ exactly when $v=0$.
2023 For the real scalar identity model and $0<\rho<v$,
2024 \[
2025 \lambda=\frac\rho{v-\rho},\qquad B_\lambda v=v-\rho
2026 \]
2027 is the unique root at residual $\rho$.
2028 
2029 \end{theorem}
2030 \begin{proof}
2031 
2032 The first assertion is the residual contraction in SR-38.
2033 Equality at $\nn v$ would give
2034 $F_\lambda(v,x_\lambda)\le F_\lambda(v,0)=\nn v^2$ while its fit term
2035 already equals $\nn v^2$. Hence $x_\lambda=0$, forcing $A^*v=0$.
2036 If the residual is zero, then $Ax_\lambda=v$, and the normal equation
2037 reduces to $\lambda x_\lambda=0$. Thus $x_\lambda=0$ and $v=0$.
2038 The converse is direct. For $A=I$, the normal equation gives
2039 $B_\lambda v=v/(1+\lambda)$ and residual
2040 $\lambda v/(1+\lambda)$ for $v>0$. Substitution proves the formula and
2041 SR-45 supplies uniqueness. These endpoints explain the strict root
2042 inequalities and the separate small-data branch.
2043 
2044 \end{proof}
2045 
2046 \src{DiscrepancyBoundaries.no_parameter_above_data; DiscrepancyBoundaries.no_parameter_at_data_norm; DiscrepancyBoundaries.zero_residual_iff_zero_data; DiscrepancyBoundaries.identity_parameter_formula}
2047 
2048 \section{Reliable discrepancy with inexact solves}
2049 
2050 The discrepancy rule of the preceding section selects an actual regularized
2051 source. A computed vector need not equal that source, and a displayed residual
2052 need not equal its exact norm. Those two errors require separate allowances.
2053 The normal equation provides the connection without assuming the computation
2054 has already solved the inverse problem.
2055 
2056 Throughout this section $A:G\to V$ is bounded between real Hilbert spaces,
2057 $N_A=\ker A$, $S_A=N_A^\perp$, and $\lambda>0$. Write
2058 \[
2059 N_\lambda=A^*A+\lambda I,\qquad
2060 x_\lambda=N_\lambda^{-1}A^*v,\qquad
2061 r_\lambda(x)=N_\lambda x-A^*v .
2062 \]
2063 The inverse is the actual positive-parameter constructor already established.
2064 The vector $r_\lambda(x)$ is the normal-equation residual of the computed
2065 source $x$. Its size measures source correction and image correction on
2066 different scales. A fitting residual $\nn{Ax-v}$ alone does not supply
2067 either correction.
2068 
2069 
2070 \par{\small\textbf{Hypotheses.} Real Hilbert spaces; bounded A; lambda>0; actual normal residual.}\par
2071 
2072 \begin{theorem}[SR-49\quad Normal residual, two correction scales]\label{SR-49}
2073 
2074 For every computed source $x$,
2075 \[
2076 x-x_\lambda=N_\lambda^{-1}r_\lambda(x),\qquad
2077 \nn{x-x_\lambda}\le\frac{\nn{r_\lambda(x)}}{\lambda},
2078 \qquad
2079 \nn{Ax-Ax_\lambda}\le
2080 \frac{\nn{r_\lambda(x)}}{2\sqrt\lambda}.
2081 \]
2082 Consequently
2083 \[
2084 \left|\nn{Ax-v}-\nn{Ax_\lambda-v}\right|
2085 \le\frac{\nn{r_\lambda(x)}}{2\sqrt\lambda}.
2086 \]
2087 The bounds use the same actual residual and the existing Hilbert norms.
2088 
2089 \end{theorem}
2090 \begin{proof}
2091 
2092 Subtract $N_\lambda x_\lambda=A^*v$ from the definition of the normal
2093 residual and apply the inverse. For $u=N_\lambda^{-1}r$, the energy identity
2094 gives
2095 \[
2096 \nn{Au}^2+\lambda\nn u^2=\ip ru
2097 \le\nn r\,\nn u .
2098 \]
2099 Dropping the first term shows $\nn u\le\nn r/\lambda$, including $u=0$.
2100 To control the image, complete the scalar square:
2101 \[
2102 \nn{Au}^2\le\nn r\,\nn u-\lambda\nn u^2
2103 \le\frac{\nn r^2}{4\lambda}.
2104 \]
2105 Both sides of the desired norm inequality are nonnegative, so taking square
2106 roots gives the image bound. Set $r=r_\lambda(x)$ and use linearity of
2107 $A$. Finally the reverse triangle inequality bounds the difference of the
2108 two fitting norms by $\nn{A(x-x_\lambda)}$.
2109 
2110 The distinction matters when $\lambda$ is small. A normal residual sufficient
2111 for a prescribed image tolerance may be insufficient for a prescribed
2112 source tolerance. If source correction must be at most $\kappa$ and image
2113 correction at most $\xi$, a sound pair of conditions is
2114 $\nn{r_\lambda(x)}\le\lambda\kappa$ and
2115 $\nn{r_\lambda(x)}\le2\sqrt\lambda\,\xi$.
2116 These are parameter-dependent requirements, not a uniform inverse bound
2117 as $\lambda$ tends to zero.
2118 
2119 \end{proof}
2120 
2121 \src{InexactResidual.correction_identity; InexactResidual.correction_bound; InexactResidual.image_correction_bound; InexactResidual.fitting_residual_difference}
2122 
2123 \par{\small\textbf{Hypotheses.} Same Hilbert setting; nonnegative source/\allowbreak image/\allowbreak evaluation budgets; positive parameter; genuine measurement enclosure.}\par
2124 
2125 \begin{theorem}[SR-50\quad Protected measured discrepancy margins]\label{SR-50}
2126 
2127 Suppose $m$ is a measured fitting norm with
2128 \[
2129 |m-\nn{Ax-v}|\le\omega,\quad
2130 \nn{r_\lambda(x)}\le\lambda\kappa,\quad
2131 \nn{r_\lambda(x)}\le2\sqrt\lambda\,\xi .
2132 \]
2133 If
2134 \[
2135 \eta+\omega+\xi\le m\le\tau\eta-\omega-\xi,
2136 \]
2137 then the actual exact source $x_\lambda$ has discrepancy in
2138 $[\eta,\tau\eta]$, and $\nn{x-x_\lambda}\le\kappa$.
2139 A protected scalar window exists exactly when
2140 \[
2141 2(\omega+\xi)\le(\tau-1)\eta .
2142 \]
2143 Its midpoint $(\tau+1)\eta/2$ is then admissible.
2144 
2145 \end{theorem}
2146 \begin{proof}
2147 
2148 SR-49 and the measurement enclosure imply
2149 \[
2150 |m-\nn{Ax_\lambda-v}|
2151 \le |m-\nn{Ax-v}|+
2152 |\nn{Ax-v}-\nn{Ax_\lambda-v}|
2153 \le\omega+\xi .
2154 \]
2155 Subtracting this total allowance from the lower protected inequality gives
2156 $\eta\le\nn{Ax_\lambda-v}$. Adding it to the upper inequality gives
2157 $\nn{Ax_\lambda-v}\le\tau\eta$. The source-correction bound follows
2158 from the other residual condition in SR-49. Hence the computed source is
2159 within $\kappa$ of an actual accepted discrepancy source.
2160 
2161 The scalar window is nonempty exactly when its lower endpoint is at most
2162 its upper endpoint. Rearrangement gives the displayed condition. The
2163 proposed midpoint is the mean of the endpoints; direct substitution gives
2164 both inequalities. No property of an approximate solver is hidden in this
2165 scalar calculation: its residual, measurement enclosure and correction
2166 allowance have already been supplied.
2167 
2168 For example, let $\eta=1/10$, $\tau=2$, and
2169 $\omega=\xi=1/100$. The total protected margin is $1/50$,
2170 and the interval is $[3/25,9/50]$. Its midpoint is $3/20$.
2171 This allocation proves room for the measurement and image-correction
2172 errors; it does not prove that a particular computed source attains the
2173 interval or that $1/10$ is a true data-noise allowance.
2174 
2175 \end{proof}
2176 
2177 \src{InexactResidual.measured_band_transfer; InexactDiscrepancy.measured_certificate; InexactToleranceCertificates.protected_window_exists_iff; InexactToleranceCertificates.protected_midpoint}
2178 
2179 \par{\small\textbf{Hypotheses.} Fixed bounded real Hilbert A; actual noise bounds; fixed tau; NearAccepted with source budget tending to zero.}\par
2180 
2181 \begin{theorem}[SR-51\quad Near-accepted consistency and kernel leakage]\label{SR-51}
2182 
2183 Call $x$ near accepted with budget $\kappa$ when some exact accepted source
2184 $y$ satisfies $\nn{x-y}\le\kappa$. If
2185 $\nn{Ag-v_i}\le\eta_i$, $\eta_i\to0$, and near-accepted $x_i$ have
2186 $\kappa_i\to0$, then
2187 \[
2188 x_i\longrightarrow P_{S_A}g,\qquad
2189 \nn{x_i-g}\longrightarrow\nn{P_{N_A}g}.
2190 \]
2191 At every index $\nn{P_{N_A}x_i}\le\kappa_i$; therefore the computed true-kernel
2192 component tends to zero. No separate parameter schedule is assumed.
2193 
2194 \end{theorem}
2195 \begin{proof}
2196 
2197 Choose accepted comparison sources $y_i$ from the definition. Exact
2198 accepted consistency gives $y_i\to p=P_{S_A}g$, while
2199 $\nn{x_i-y_i}\le\kappa_i\to0$ gives $x_i-y_i\to0$. Adding the two limits
2200 proves $x_i\to p$. Continuity of the norm gives the source-error limit,
2201 because $p-g=-P_{N_A}g$.
2202 
2203 The exact accepted source belongs to $S_A$, including the small-data zero
2204 branch. Orthogonal projection is nonexpansive, so
2205 \[
2206 \nn{P_{N_A}x_i}
2207 =\nn{P_{N_A}(x_i-y_i)}
2208 \le\nn{x_i-y_i}\le\kappa_i .
2209 \]
2210 This pointwise estimate only needs near acceptance, not a truth-noise
2211 premise. Source consistency additionally needs the stated true-noise
2212 allowance tending to zero.
2213 
2214 The underlying exact consistency theorem has substantive content even
2215 for a nonclosed range. Accepted sources satisfy norm domination
2216 $\nn{y_i}\le\nn p$ and $\nn{Ay_i-Ap}\to0$. Since
2217 $p\in S_A=\cl\Ran A^*$, approximate $p$ by $A^*w$ and use
2218 \[
2219 \nn{y_i-p}^2
2220 \le2\ip{p}{p-y_i}
2221 \le2\nn{p-A^*w}\nn{p-y_i}
2222 +2\nn w\,\nn{A(p-y_i)} .
2223 \]
2224 The first factor $\nn{p-y_i}$ is bounded by $2\nn p$.
2225 First choose the approximation accurately, then let $i$ tend along the
2226 filter. This proves strong convergence without a bounded inverse.
2227 
2228 \end{proof}
2229 
2230 \src{InexactDiscrepancy.NearAccepted; InexactDiscrepancy.near_kernel_leakage; InexactConsistency.near_consistent; InexactConsistency.near_error_norm_limit; InexactConsistency.near_kernel_tendsto_zero}
2231 
2232 \par{\small\textbf{Hypotheses.} Real Hilbert spaces; positive lambda; nonnegative scalar certificate fields; squared inequalities against actual norms.}\par
2233 
2234 \begin{theorem}[SR-52\quad Squared proof-carrying discrepancy certificate]\label{SR-52}
2235 
2236 Suppose a record supplies $\lambda>0$, nonnegative
2237 $\rho,\xi,\kappa,m,\omega$, and
2238 \[
2239 \nn{r_\lambda(x)}^2\le\rho^2,\quad
2240 \rho^2\le(\lambda\kappa)^2,\quad
2241 \rho^2\le4\lambda\xi^2,
2242 \]
2243 \[
2244 \max(0,m-\omega)^2\le\nn{Ax-v}^2\le(m+\omega)^2,
2245 \qquad
2246 \eta+\omega+\xi\le m\le\tau\eta-\omega-\xi .
2247 \]
2248 Then $x$ is near accepted with source budget $\kappa$. Families of such
2249 records give SR-51 when the genuine data allowances and source budgets
2250 tend to zero.
2251 
2252 \end{theorem}
2253 \begin{proof}
2254 
2255 All quantities whose squares are compared are nonnegative. The first
2256 two inequalities therefore give
2257 $\nn{r_\lambda(x)}\le\rho\le\lambda\kappa$.
2258 The third gives $\rho\le2\sqrt\lambda\,\xi$ because
2259 $(2\sqrt\lambda\,\xi)^2=4\lambda\xi^2$.
2260 
2261 Put $d=\nn{Ax-v}\ge0$. The squared fitting enclosure is equivalent to
2262 the unsquared enclosure
2263 $\max(0,m-\omega)\le d\le m+\omega$.
2264 Since $d\ge0$, its lower part is equivalent to $m-\omega\le d$.
2265 Together these say $|m-d|\le\omega$. Thus every premise of SR-50 has
2266 been obtained from the supplied record, and its conclusion proves soundness.
2267 Apply SR-51 pointwise for the family statement.
2268 
2269 The record does not establish the truth of the data-noise allowance.
2270 It establishes a relation between the computed source, actual normal
2271 residual and actual fitting norm. An implementation may check rational
2272 squared inequalities without numerical square roots, but that requires a
2273 faithful enclosure of these actual quantities. The generic Lean structure
2274 is proof-carrying; a serialized Python record and its parser are separate
2275 implementation evidence.
2276 
2277 If the normal residual itself is evaluated approximately as $\widehat r$,
2278 the distinct assumptions
2279 $\nn{r_\lambda(x)-\widehat r}\le\nu$ and
2280 $\nn{\widehat r}\le\widehat\rho$ give the allowance
2281 $\widehat\rho+\nu$. Substituting that sum into both correction tests retains
2282 the evaluation error rather than silently identifying it with zero.
2283 
2284 \end{proof}
2285 
2286 \src{InexactToleranceCertificates.squared_enclosure_iff; InexactToleranceCertificates.squared_image_budget; InexactToleranceCertificates.PositiveCertificate; InexactToleranceCertificates.certificate_sound; InexactToleranceCertificates.certificate_consistent}
2287 
2288 \section{Uncertain operators and changing identifiable models}
2289 
2290 Data noise, solver error and model error are different inputs. Let $A$ be
2291 the true forward operator and $C$ the available operator, acting between the
2292 same real Hilbert spaces. The premise $\nn{C-A}\le\delta$ is a whole-operator
2293 allowance. A small residual for one source does not establish it.
2294 This section first uses a fixed cap $M$ on a true comparison source.
2295 The next section removes that cap from the acceptance rule by making the
2296 allowance depend on the candidate itself.
2297 
2298 
2299 \par{\small\textbf{Hypotheses.} Same normed source/\allowbreak target; bounded A,C; whole operator allowance; genuine data allowance and source cap.}\par
2300 
2301 \begin{theorem}[SR-53\quad Effective model-noise allowance]\label{SR-53}
2302 
2303 If $\nn{C-A}\le\delta$, $\nn p\le M$ and $\nn{Ap-v}\le\eta$, then
2304 \[
2305 \nn{Cp-v}\le\epsilon:=\eta+\delta M.
2306 \]
2307 For every candidate $x$,
2308 \[
2309 |\nn{Ax-v}-\nn{Cx-v}|\le\delta\nn x.
2310 \]
2311 If $|m-\nn{Cx-v}|\le\omega$, then
2312 $|m-\nn{Ax-v}|\le\omega+\delta\nn x$.
2313 The effective-noise allowance is sharp in scalar examples.
2314 
2315 \end{theorem}
2316 \begin{proof}
2317 
2318 The definition of operator norm gives
2319 $\nn{Cp-Ap}\le\delta\nn p$. Because a norm bound implies
2320 $\delta\ge0$, the source cap gives
2321 \[
2322 \nn{Cp-v}\le\nn{Cp-Ap}+\nn{Ap-v}
2323 \le\delta M+\eta .
2324 \]
2325 For the fitting-norm comparison, apply the reverse triangle inequality
2326 to $Ax-v$ and $Cx-v$, whose difference is $(A-C)x$. Combining this
2327 with the measurement enclosure gives the last claim.
2328 
2329 To see the possible equality, take real scalar maps
2330 $A=1$, $C=1+\delta$, $p=M$ and $v=M-\eta$, with
2331 $\eta,\delta,M\ge0$. Then
2332 $Cp-v=\delta M+\eta\ge0$, so its absolute value is exactly $\epsilon$.
2333 The source-size factor cannot generally be omitted: for fixed
2334 $\delta>0$, the action difference $\delta|p|$ grows without bound as
2335 $|p|$ grows. Thus replacing $\delta M$ by an operator-only constant
2336 would strengthen the contract incorrectly.
2337 
2338 \end{proof}
2339 
2340 \src{OperatorUncertainty.action_error; OperatorUncertainty.effective_data_noise; OperatorUncertainty.fitting_norm_difference; OperatorUncertainty.measured_true_fitting_envelope; OperatorUncertaintyExamples.inflated_noise_sharp}
2341 
2342 \par{\small\textbf{Hypotheses.} Same real Hilbert spaces; bounded A,C; positive or arbitrary common normal parameter; whole norm error delta.}\par
2343 
2344 \begin{theorem}[SR-54\quad Transport of actual normal residuals]\label{SR-54}
2345 
2346 For the normal residuals formed with the same parameter,
2347 \[
2348 r^A_\lambda(x)-r^C_\lambda(x)
2349 =(A^*-C^*)(Cx-v)+A^*(A-C)x .
2350 \]
2351 If $\nn{C-A}\le\delta$, then
2352 \[
2353 \nn{r^A_\lambda(x)-r^C_\lambda(x)}
2354 \le\delta\bigl(\nn{Cx-v}+(\nn C+\delta)\nn x\bigr).
2355 \]
2356 Hence a computed-model normal allowance $\nn{r^C_\lambda(x)}\le\rho$
2357 gives the corresponding true normal allowance by adding this expression.
2358 
2359 \end{theorem}
2360 \begin{proof}
2361 
2362 Expand the two residuals. The $\lambda x$ terms cancel. Insert and
2363 subtract $A^*Cx$ to obtain the displayed identity. Adjoint isometry
2364 gives $\nn{A^*-C^*}=\nn{A-C}\le\delta$ and $\nn{A^*}=\nn A$.
2365 Submultiplicativity therefore bounds its two terms by
2366 $\delta\nn{Cx-v}$ and $\nn A\,\delta\nn x$.
2367 The triangle inequality gives $\nn A\le\nn C+\delta$, yielding a
2368 bound written in terms of available-model quantities and the allowance.
2369 Finally apply $\nn{r^A}\le\nn{r^C}+\nn{r^A-r^C}$.
2370 
2371 The identity itself does not require a positive parameter; positivity
2372 is needed when this transported residual is used in SR-49 to control
2373 an inverse correction. The model error remains distinct from the solver's
2374 normal residual. Both contributions are amplified by the corresponding
2375 positive-parameter correction scale. A small fixed model allowance is
2376 therefore not a uniform guarantee when $\lambda$ tends to zero.
2377 
2378 \end{proof}
2379 
2380 \src{OperatorResidualTransport.normal_residual_difference; OperatorResidualTransport.normal_residual_available_bound; OperatorResidualTransport.true_normal_residual_bound}
2381 
2382 \par{\small\textbf{Hypotheses.} Same real Hilbert spaces; fixed true bounded A, fixed real tau and fixed identifiable p; source cap M; true bounds and exact/\allowbreak near accepted uncertain-model sources; vanishing allowances.}\par
2383 
2384 \begin{theorem}[SR-55\quad Strong consistency without matching model kernels]\label{SR-55}
2385 
2386 Suppose $p\in S_A$, $\nn p\le M$, and
2387 \[
2388 \nn{C_i-A}\le\delta_i,\qquad
2389 \nn{Ap-v_i}\le\eta_i .
2390 \]
2391 If $x_i$ lies within $\kappa_i$ of an exact accepted source for
2392 $C_i,v_i$ with allowance $\epsilon_i=\eta_i+\delta_iM$, and
2393 $\eta_i,\delta_i,\kappa_i\to0$, then $x_i\to p$.
2394 The model kernels and ranks may change. For arbitrary $g$, using
2395 $p=P_{S_A}g$ yields
2396 $\nn{x_i-g}\to\nn{P_{N_A}g}$ and $P_{N_A}x_i\to0$.
2397 
2398 \end{theorem}
2399 \begin{proof}
2400 
2401 Let $y_i$ be the exact accepted comparison. SR-53 makes $p$ feasible
2402 for the available model at allowance $\epsilon_i$. In the positive
2403 branch, regularized optimality and the lower discrepancy bound give
2404 $\nn{y_i}\le\nn p$: compare the objective at $y_i$ and $p$, then
2405 cancel the fitting terms using
2406 $\nn{C_ip-v_i}\le\epsilon_i\le\nn{C_iy_i-v_i}$.
2407 The small-data branch is zero and satisfies the same domination.
2408 
2409 The upper discrepancy bound gives
2410 $\nn{C_iy_i-v_i}\le\tau\epsilon_i$. Returning to the true operator,
2411 \[
2412 \nn{Ay_i-Ap}
2413 \le\delta_i\nn{y_i}+\tau\epsilon_i+\eta_i
2414 \le(\tau+1)\epsilon_i .
2415 \]
2416 Thus $y_i$ is norm dominated by the fixed identifiable $p$ and has true
2417 image residual tending to zero. The density argument printed in SR-51
2418 proves $y_i\to p$ without projecting onto the changing model kernels.
2419 The near-source difference then tends to zero, proving $x_i\to p$.
2420 
2421 For arbitrary $g$, $AP_{S_A}g=Ag$, so the same true-data bound applies
2422 to $p=P_{S_A}g$. Continuity of norm and true-kernel projection gives
2423 the remaining limits. The fixed cap concerns this limiting identifiable
2424 source. It is not a claim that the minimum-norm sources for unrelated
2425 models have already converged.
2426 
2427 \end{proof}
2428 
2429 \src{ChangingDiscrepancy.norm_control; ChangingDiscrepancy.near_true_residual; ChangingConsistency.projected_consistent; ChangingConsistency.source_error_limit; ChangingConsistency.true_kernel_leakage_tendsto_zero}
2430 
2431 \par{\small\textbf{Hypotheses.} Real Hilbert setting; operational checks use C; external true allowances and source cap; positive effective allowance and tau>1 for selection.}\par
2432 
2433 \begin{theorem}[SR-56\quad Available-model certificate and selected-source soundness]\label{SR-56}
2434 
2435 A source is certified using $C$ when either
2436 $\nn v\le\tau\epsilon$ and $\nn x\le\kappa$, or it has an SR-52
2437 positive certificate for $C$ with allowance $\epsilon=\eta+\delta M$.
2438 Such a source is near accepted for the available model.
2439 With the external truth premises of SR-55 and vanishing allowances,
2440 certified sources converge to the true identifiable source.
2441 
2442 If $\epsilon>0$ and $\tau>1$, those truth premises also give feasibility
2443 of the total exact discrepancy selector for $C$; the selected exact
2444 sources are consistent under the same vanishing data/operator bounds.
2445 
2446 \end{theorem}
2447 \begin{proof}
2448 
2449 In the small-data branch compare $x$ with the accepted zero source:
2450 $\nn{x-0}\le\kappa$. In the positive branch, SR-52 supplies an actual
2451 accepted comparison source at distance at most $\kappa$. This proves
2452 operational soundness without using $A$.
2453 
2454 For the true conclusion, separately supply $\nn{C-A}\le\delta$,
2455 the true-data bound, and $\nn p\le M$. These hypotheses are not fields
2456 established by an observed fitting certificate. They allow SR-55 to
2457 be applied to every certified source.
2458 
2459 SR-53 gives the feasible witness $p$ for the available model. A positive
2460 effective allowance and $\tau>1$ ensure a strict residual target above
2461 its attainable floor in the non-small-data case; the total discrepancy
2462 construction chooses an actual positive-parameter source there and zero
2463 in the other branch. Each selected source is exact accepted, so SR-55
2464 applies with $\kappa=0$. This selected object is noncomputable in the
2465 generic formalization. Its existence theorem and soundness are distinct
2466 from a finite numerical search implementation.
2467 
2468 \end{proof}
2469 
2470 \src{OperatorCertificates.Certified; OperatorCertificates.certified_near; OperatorCertificates.certified_consistent; OperatorCertificates.inflated_feasibility; OperatorCertificates.selected_from_allowances_consistent}
2471 
2472 \section{Candidate-dependent discrepancy without a supplied source cap}
2473 
2474 The acceptance rule can avoid an externally supplied number $M$ by using
2475 the candidate itself in the uncertainty allowance. Put
2476 \[
2477 c_{\eta,\delta}(x)=\eta+\delta\nn x .
2478 \]
2479 A generalized accepted source is either zero in the small-data branch
2480 $\nn v\le\tau\eta$, or an actual Tikhonov source whose residual lies between
2481 $c_{\eta,\delta}(x)$ and $\tau c_{\eta,\delta}(x)$.
2482 This definition contains $C,v,\eta,\delta,\tau,x$ and the positive parameter;
2483 it does not contain a true-source cap. Feasibility remains a separate
2484 question and retains a quantitative relation between model accuracy and
2485 the true noise scale.
2486 
2487 
2488 \par{\small\textbf{Hypotheses.} Real Hilbert spaces; bounded C; lambda>0; delta\(\ge\)0; feasible comparison p for candidate noise; actual regularized candidate.}\par
2489 
2490 \begin{theorem}[SR-57\quad Candidate-dependent self-bounding]\label{SR-57}
2491 
2492 Let $x$ be the actual regularized source for $C,v,\lambda$. If
2493 \[
2494 \nn{Cp-v}\le c_{\eta,\delta}(p),\qquad
2495 c_{\eta,\delta}(x)\le\nn{Cx-v},
2496 \]
2497 then $\nn x\le\nn p$.
2498 In particular, if $\nn{C-A}\le\delta$ and $\nn{Ap-v}\le\eta$,
2499 every generalized accepted source satisfies $\nn x\le\nn p$.
2500 
2501 \end{theorem}
2502 \begin{proof}
2503 
2504 Suppose instead $\nn x>\nn p$. Since $\delta\ge0$, candidate noise
2505 is monotone in source norm:
2506 $c_{\eta,\delta}(p)\le c_{\eta,\delta}(x)$.
2507 The two displayed hypotheses imply
2508 $\nn{Cp-v}\le\nn{Cx-v}$.
2509 Comparing Tikhonov objectives, the fitting-square term at $p$ is no larger,
2510 whereas its positive weighted source-square term is strictly smaller.
2511 The total objective at $p$ is strictly smaller than the objective at its
2512 actual unique minimizer $x$, a contradiction.
2513 
2514 With true operator bounds, SR-53 applied using $M=\nn p$ gives the
2515 required candidate-noise feasibility. The operator allowance implies
2516 $\delta\ge0$. The positive accepted branch therefore satisfies the lemma;
2517 the small-data branch $x=0$ satisfies the norm conclusion directly.
2518 
2519 The lower discrepancy inequality is decisive. An upper residual bound
2520 alone can allow overly large regularized source norms. Here the lower
2521 bound grows with the candidate norm, and objective minimality prevents
2522 that growth from exceeding a feasible comparison source. The comparison
2523 source enters the proof of soundness, while the acceptance definition
2524 continues to have no externally supplied source cap.
2525 
2526 \end{proof}
2527 
2528 \src{GeneralizedDiscrepancy.regularized_norm_domination; GeneralizedDiscrepancy.accepted_norm_control}
2529 
2530 \par{\small\textbf{Hypotheses.} Real Hilbert spaces; true whole-operator/\allowbreak data bounds; tau\(\ge\)0; generalized accepted or near-accepted sources; vanishing allowances.}\par
2531 
2532 \begin{theorem}[SR-58\quad Generalized true residual and strong consistency]\label{SR-58}
2533 
2534 A generalized accepted $x$ obeys
2535 \[
2536 \nn{Ax-Ap}\le(\tau+1)c_{\eta,\delta}(p).
2537 \]
2538 A source within $\kappa$ of such an $x$ obeys the same bound with
2539 $\nn A\,\kappa$ added. For $p\in S_A$, vanishing data/operator
2540 allowances and near-source budgets imply strong convergence to $p$.
2541 If $p=A^*w$, an inexact accepted candidate also satisfies
2542 \[
2543 \nn{x-p}^2\le
2544 2\kappa^2+4\nn w(\tau+1)c_{\eta,\delta}(p).
2545 \]
2546 
2547 \end{theorem}
2548 \begin{proof}
2549 
2550 SR-57 gives $\nn x\le\nn p$, so
2551 $c_{\eta,\delta}(x)\le c_{\eta,\delta}(p)$.
2552 The upper generalized discrepancy bound and $\tau\ge0$ yield
2553 $\nn{Cx-v}\le\tau c_{\eta,\delta}(p)$. Insert $Cx$ and $v$ into
2554 the true residual:
2555 \[
2556 \nn{Ax-Ap}\le
2557 \delta\nn x+\nn{Cx-v}+\eta
2558 \le(\tau+1)c_{\eta,\delta}(p).
2559 \]
2560 For a near candidate, split its image difference through the exact accepted
2561 comparison and apply the operator norm bound to the correction.
2562 
2563 As $\eta_i,\delta_i\to0$, the comparison-source noise
2564 $\eta_i+\delta_i\nn p$ tends to zero. Exact candidates are norm dominated
2565 by $p$ and have true image error tending to zero; the same density argument
2566 as SR-51 proves their strong convergence. Add a vanishing near-source
2567 difference for inexact candidates. No relative feasibility condition is
2568 needed in this implication once accepted candidates have been supplied.
2569 
2570 For the source-condition rate, norm domination and $p=A^*w$ give
2571 \[
2572 \nn{y-p}^2\le2\ip{p}{p-y}\le2\nn w\,\nn{A(p-y)}
2573 \]
2574 for an exact comparison $y$. Bound its image by the first conclusion.
2575 Then $\nn{x-p}\le\nn{x-y}+\nn{y-p}$ and
2576 $(a+b)^2\le2a^2+2b^2$ prove the stated inexact rate.
2577 
2578 \end{proof}
2579 
2580 \src{GeneralizedDiscrepancy.accepted_true_residual; GeneralizedDiscrepancy.accepted_consistent; GeneralizedInexact.near_true_residual; GeneralizedInexact.near_consistent; GeneralizedInexact.near_source_condition_rate}
2581 
2582 \par{\small\textbf{Hypotheses.} Real Hilbert spaces; eta>0,tau>1; true operator/\allowbreak data bounds; delta\(\Vert\)p\(\Vert\)<(tau-1)eta.}\par
2583 
2584 \begin{theorem}[SR-59\quad Relative feasibility and noncomputable selection]\label{SR-59}
2585 
2586 If $\nn{C-A}\le\delta$, $\nn{Ap-v}\le\eta$ and
2587 \[
2588 \delta\nn p<(\tau-1)\eta,
2589 \]
2590 then an accepted source exists with norm at most $\nn p$. In the large-data
2591 case one can choose a positive parameter whose residual is exactly
2592 $\tau\eta$. A sufficient ratio condition is
2593 $\delta\le\gamma\eta$ and $\gamma\nn p<\tau-1$.
2594 Noncomputably selected families converge to $p\in S_A$ when the data/operator
2595 allowances vanish and the pointwise feasibility conditions hold.
2596 
2597 \end{theorem}
2598 \begin{proof}
2599 
2600 The true bounds imply
2601 $\nn{Cp-v}\le\eta+\delta\nn p<\tau\eta$.
2602 If $\nn v\le\tau\eta$, the zero source is accepted. Otherwise the strict
2603 attainable-floor bound and $\tau\eta<\nn v$ give a positive exact
2604 discrepancy root for $C$ with residual $\tau\eta$.
2605 Let $x$ be its actual Tikhonov source. Objective comparison, or the
2606 fixed-noise domination lemma, gives $\nn x\le\nn p$.
2607 Consequently
2608 \[
2609 c_{\eta,\delta}(x)\le\eta+\delta\nn p<\tau\eta
2610 =\nn{Cx-v}.
2611 \]
2612 Because $\delta\ge0$ and $\tau>1$,
2613 $\tau\eta\le\tau c_{\eta,\delta}(x)$.
2614 Thus both generalized band inequalities hold.
2615 
2616 Multiplying $\delta\le\gamma\eta$ by $\nn p\ge0$ and the strict margin
2617 $\gamma\nn p<\tau-1$ by $\eta>0$ proves the ratio specialization.
2618 The chosen source is defined by classical choice from the existence
2619 theorem. Its raw definition takes $A,p$ and the truth/feasibility proofs
2620 as arguments; it is a theorem-level witness rather than an extracted
2621 algorithm using only available measurements. Each chosen source is
2622 accepted, so SR-58 proves the family convergence. The selection theorem
2623 retains the feasibility premises even though the acceptance predicate has
2624 no supplied scalar source cap.
2625 
2626 \end{proof}
2627 
2628 \src{GeneralizedDiscrepancySelection.positive_parameter_source; GeneralizedDiscrepancySelection.exists_accepted; GeneralizedDiscrepancySelection.selectedSource; GeneralizedFeasibility.relative_accuracy_of_scaled_error; GeneralizedDiscrepancyConsistency.selected_consistent}
2629 
2630 \par{\small\textbf{Hypotheses.} Same Hilbert setting; near exact generalized acceptance with vanishing correction budget; scalar boundary uses valid but nonvanishing model allowance.}\par
2631 
2632 \begin{theorem}[SR-60\quad Inexact generalized sources and the zero-model boundary]\label{SR-60}
2633 
2634 Near-generalized acceptance is preserved by enlarging a source-correction
2635 budget and gives the consistency conclusion of SR-58 when that budget
2636 tends to zero.
2637 Nevertheless valid true-noise and operator allowances alone do not ensure
2638 generalized feasibility. With
2639 $A=1$, $C=0$, $p=v=1$, $\eta=1/10$, $\delta=1$ and $\tau=2$,
2640 no source is generalized accepted.
2641 
2642 \end{theorem}
2643 \begin{proof}
2644 
2645 Near acceptance means there exists an exact generalized accepted comparison
2646 $y$ with $\nn{x-y}\le\kappa$. Increasing $\kappa$ preserves that
2647 inequality. Along a family, choosing the comparisons and adding the
2648 vanishing difference proves consistency by SR-58.
2649 
2650 For the scalar boundary, the true data error is zero and
2651 $\nn{C-A}=1\le\delta$, so both stated truth allowances are valid.
2652 The small-data branch would require $1\le2/10$, which is false.
2653 For every positive parameter, the actual regularized source of $C=0$
2654 is zero and its fitting residual is one. Its candidate noise is
2655 $1/10+1\cdot0=1/10$, so the upper generalized band would again require
2656 $1\le2/10$. Every branch fails. The relative feasibility condition also
2657 fails, since $1<(2-1)/10$ is false. Thus the boundary refutes an
2658 unconditional existence interpretation, not the conditional theorem.
2659 
2660 For comparison, take $A=C=1$, $v=1$, $\eta=1/10$, $\delta=0$,
2661 $\tau=2$ and $\lambda=1/4$. Then
2662 $x_\lambda=4/5$ and the residual is $1/5$.
2663 It lies in $[1/10,2/10]$, so the candidate is accepted, and
2664 $0<(2-1)/10$ verifies the strict feasibility margin.
2665 These examples use the actual scalar normal inverse and exact norms,
2666 not a substituted approximate residual.
2667 
2668 \end{proof}
2669 
2670 \src{GeneralizedInexact.NearAccepted; GeneralizedInexact.near_consistent; GeneralizedDiscrepancyExamples.identity_candidate_accepted; GeneralizedDiscrepancyExamples.zero_model_not_accepted; GeneralizedDiscrepancyExamples.zero_model_valid_true_bounds; GeneralizedDiscrepancyExamples.zero_model_relative_accuracy_fails}
2671 
2672 \section{Calibration generates an operator allowance}
2673 
2674 The final link connects justified calibration measurements with the
2675 whole-operator premise used above. It does not infer the calibration truth
2676 allowance from the model's own fit. Let $K$ be a real normed calibration
2677 coordinate space, $G$ a real normed source space and $V$ a real normed
2678 response space. A split frame has bounded synthesis $U:K\to G$ and
2679 analysis $R:G\to K$ with $UR=I_G$. Its coordinates may be redundant:
2680 $U$ need not be injective or square. The reconstruction identity requires
2681 coverage of every source direction.
2682 
2683 The observed response $Y:K\to V$ is an operator, and the assumptions
2684 $\nn{Y-AU}\le\eta_{\rm cal}$ and $\nn{Y-CU}\le f$ are operator-norm
2685 enclosures. Individual calibration samples do not automatically give these
2686 enclosures. A mathematical or experimental justification of
2687 $\eta_{\rm cal}$ remains a separate input.
2688 
2689 
2690 \par{\small\textbf{Hypotheses.} Real normed spaces; bounded U,R with UR=I; whole calibration truth/\allowbreak model-fit operator bounds.}\par
2691 
2692 \begin{theorem}[SR-61\quad Redundant split calibration identifies the operator]\label{SR-61}
2693 
2694 Every bounded source operator $T$ factors as $T=(TU)R$. Therefore
2695 \[
2696 C-A=((CU)-(AU))R,\qquad
2697 \nn{C-A}\le(\eta_{\rm cal}+f)\nn R .
2698 \]
2699 If a supplied analysis bound is $\nn R\le k$, the allowance is at most
2700 $(\eta_{\rm cal}+f)k$. Exact calibration $Y=AU=CU$ forces $A=C$.
2701 
2702 \end{theorem}
2703 \begin{proof}
2704 
2705 For every source $g$, $URg=g$, so $Tg=TU(Rg)$. This proves the actual
2706 factorization, including its application to $C-A$.
2707 The triangle inequality through the common measured operator gives
2708 \[
2709 \nn{CU-AU}\le\nn{CU-Y}+\nn{Y-AU}
2710 \le f+\eta_{\rm cal}.
2711 \]
2712 Submultiplicativity then yields the displayed allowance.
2713 Both measured bounds imply their scalar allowances are nonnegative;
2714 hence replacing $\nn R$ by a larger $k$ preserves the inequality.
2715 With exact calibration, $CU-AU=0$ and the factorization gives $C-A=0$.
2716 
2717 Redundancy causes no logical problem. For instance, let
2718 $K=\RR^2$, $G=\RR$, $U(k_1,k_2)=k_1$ and $Rg=(g,0)$, with the
2719 standard product norm. Then $UR=I$, $\nn U=\nn R=1$, but
2720 $U$ has a nontrivial kernel. The frame spans the source even though
2721 it has an unused coordinate. A true scalar map $A=a$ and model $C=c$
2722 with measured row $Y(k_1,k_2)=yk_1$ give
2723 $|y-a|\le\eta_{\rm cal}$ and $|y-c|\le f$,
2724 hence $|c-a|\le\eta_{\rm cal}+f$.
2725 The same estimate comes from the general factorization rather than
2726 assuming the coordinates are square and invertible.
2727 
2728 \end{proof}
2729 
2730 \src{CalibrationFrame.Frame.factor_through_frame; CalibrationFrame.Frame.difference_factorization; CalibrationFrame.Frame.measured_operator_bound; CalibrationFrame.Frame.measured_operator_bound_of_analysis_bound; CalibrationFrame.Frame.exact_calibration_identifies}
2731 
2732 \par{\small\textbf{Hypotheses.} Fixed split calibration frame; real Hilbert G,V; fixed bounded true A and tau\(\ge\)0; fixed identifiable p; whole calibration truth/\allowbreak model fit and true data allowances; generalized acceptance; relative feasibility for choice.}\par
2733 
2734 \begin{theorem}[SR-62\quad Calibrated recovery and conditional selected sources]\label{SR-62}
2735 
2736 For recovery assume $G,V$ are real Hilbert spaces, $A$ is a fixed bounded
2737 true operator, $\tau\ge0$ is fixed, and $p\in(\ker A)^\perp$ is fixed.
2738 Retain the whole calibration bounds and the true data bounds
2739 $\nn{Ap-v_i}\le\eta_i$. Put $\delta_i=(\eta_{{\rm cal},i}+f_i)\nn R$.
2740 If the true data,
2741 calibration-truth and model-fit allowances tend to zero, then
2742 $\delta_i\to0$. Generalized accepted sources using this generated
2743 allowance converge to a fixed identifiable true source $p$.
2744 For an arbitrary true source $g$, apply this with $p=P_{S_A}g$ and genuine
2745 data bounds $\nn{Ag-v_i}\le\eta_i$; then the source-error norm tends to
2746 $\nn{P_{N_A}g}$.
2747 
2748 If additionally $\eta_i>0$, $\tau>1$ and
2749 $\delta_i\nn p<(\tau-1)\eta_i$ pointwise, accepted sources exist and the
2750 noncomputable selected sources have the same limit.
2751 
2752 \end{theorem}
2753 \begin{proof}
2754 
2755 Apply SR-61 at every index to obtain the actual operator bound
2756 $\nn{C_i-A}\le\delta_i$. Because the frame is fixed, its finite norm
2757 $\nn R$ is a constant. The sum of the two vanishing calibration
2758 allowances tends to zero, so multiplying by that constant proves
2759 $\delta_i\to0$. With the genuine data-noise bounds, every premise of
2760 the accepted-source consistency theorem SR-58 is now available.
2761 
2762 For arbitrary $g$, use $p=P_{S_A}g$. Its forward image is $Ag$, so the
2763 same data bounds hold. The strong source limit is $p$, and continuity
2764 gives $\nn{x_i-g}\to\nn{p-g}=\nn{P_{N_A}g}$.
2765 No calibration can remove source ambiguity in the true forward kernel
2766 without an additional identifying condition.
2767 
2768 The relative margin feeds the generated allowance into SR-59 and proves
2769 pointwise existence and norm domination. Its chosen sources are accepted,
2770 so the first conclusion applies to them. The raw selection is still
2771 noncomputable and proof-dependent. Calibration has generated the
2772 operator-error premise; it has not eliminated the distinct truth, data,
2773 feasibility or selection obligations.
2774 
2775 In particular, declining observed model-calibration fit alone is
2776 insufficient: the calibration-truth allowance must also vanish.
2777 If the reconstruction frame changes with the index, a growing analysis
2778 norm would require additional control. The printed family theorem uses
2779 the fixed frame it actually assumes.
2780 
2781 \end{proof}
2782 
2783 \src{CalibrationRecovery.generated_operator_bound; CalibrationRecovery.generatedDelta_tendsto_zero; CalibrationRecovery.calibrated_consistent; CalibrationRecovery.calibrated_error_norm_limit; CalibrationSelection.exists_accepted_from_calibration; CalibrationSelection.calibrated_selected_consistent}
2784 
2785 \par{\small\textbf{Hypotheses.} Real normed spaces; bounded split stage frames; or bounded U,R with whole reconstruction defect at most rho<1.}\par
2786 
2787 \begin{theorem}[SR-63\quad Hierarchical and approximate reconstruction frames]\label{SR-63}
2788 
2789 For split frames $(U_E,R_E):J\rightleftarrows K$ and
2790 $(U_F,R_F):K\rightleftarrows G$, the composite is split, with analysis
2791 $R_ER_F$ and
2792 $\nn{R_ER_F}\le\nn{R_E}\nn{R_F}$.
2793 The corresponding calibration allowance is at most
2794 $(\eta_{\rm cal}+f)\nn{R_E}\nn{R_F}$.
2795 
2796 More generally, if $\nn{I-UR}\le\rho<1$, then
2797 \[
2798 \nn T\le\frac{\nn{TU}\nn R}{1-\rho},\qquad
2799 \nn{C-A}\le\frac{(\eta_{\rm cal}+f)\nn R}{1-\rho}.
2800 \]
2801 
2802 \end{theorem}
2803 \begin{proof}
2804 
2805 The composite synthesis is $U_FU_E$ and analysis is $R_ER_F$.
2806 Their product is
2807 $U_F(U_ER_E)R_F=U_FR_F=I_G$.
2808 Submultiplicativity bounds the composite analysis norm; applying
2809 SR-61 and that bound proves the hierarchical allowance. There is no
2810 requirement that either synthesis be square or injective.
2811 
2812 For the approximate frame, use the exact identity
2813 $T=(TU)R+T(I-UR)$.
2814 It gives
2815 \[
2816 \nn T\le\nn{TU}\nn R+\nn T\,\nn{I-UR}
2817 \le\nn{TU}\nn R+\rho\nn T .
2818 \]
2819 Since $1-\rho>0$, absorb the final term and divide.
2820 For $T=C-A$, the measured calibration bounds give
2821 $\nn{TU}\le\eta_{\rm cal}+f$, producing the operator allowance.
2822 This argument only uses norm inequalities; it does not substitute an
2823 assumed exact inverse for the approximate reconstruction.
2824 
2825 The denominator records the loss of control. At $\rho=0$ the exact
2826 frame estimate is recovered. At $\rho=1$ the absorption step gives no
2827 bound, and it is not legitimate to reuse the formula by division.
2828 Likewise the product of hierarchical analysis norms is a valid
2829 conservative bound, not generally an equality or the optimal sensitivity
2830 of the composite. These conditioning factors belong in the certificate.
2831 
2832 \end{proof}
2833 
2834 \src{CalibrationHierarchy.comp; CalibrationHierarchy.comp_analysis_norm_le; CalibrationHierarchy.hierarchical_operator_bound; ApproximateCalibration.approximate_factorization; ApproximateCalibration.approximate_frame_bound; ApproximateCalibration.measured_approximate_operator_bound}
2835 
2836 \par{\small\textbf{Hypotheses.} Actual partial calibration from R to R\({}^2\) with product norm; bounded unseen scalar operators; arbitrary real norm threshold.}\par
2837 
2838 \begin{theorem}[SR-64\quad A missed calibration direction permits unbounded error]\label{SR-64}
2839 
2840 Let $U(t)=(t,0)$ and $C_s(x,y)=sy$. Then $C_sU=0$ and
2841 $\nn{C_s}=|s|$. For every real $M$ there is an operator agreeing
2842 perfectly with zero on the entire calibration subspace yet satisfying
2843 $\nn{C_s}>M$.
2844 The calibration synthesis is not surjective. Thus perfect agreement on a
2845 proper source subspace does not control whole-source operator accuracy.
2846 
2847 \end{theorem}
2848 \begin{proof}
2849 
2850 Direct substitution gives $C_sU(t)=s\cdot0=0$.
2851 The second-coordinate projection has norm one, so scalar multiplication
2852 gives $\nn{C_s}=|s|$; the vector $(0,1)$ also verifies the lower bound.
2853 Choose $s=|M|+1>0$. Then $\nn{C_s}=|M|+1>M$ while its calibrated
2854 response remains zero. Taking the true operator and measured response
2855 both zero shows that both calibration residuals vanish, even though
2856 the whole operator discrepancy exceeds $M$.
2857 
2858 The vector $(0,1)$ is outside the range of $U$, proving nonsurjectivity.
2859 A split reconstruction $UR=I_{\RR^2}$ would make every source a range
2860 vector, so no such reconstruction exists here. Nor can any approximate
2861 reconstruction for this synthesis have whole defect below one:
2862 the range of $UR$ has second coordinate zero, and therefore
2863 $(I-UR)(0,1)$ has second coordinate one and norm at least one.
2864 This last observation explains the direction-coverage role of the
2865 strict absorption threshold in SR-63.
2866 
2867 The positive redundant example and this negative partial example differ
2868 in coverage, not coordinate count. Extra coordinates can coexist with
2869 complete reconstruction of every source. Calibration of fewer source
2870 directions leaves an operator component that all tested calibration
2871 responses fail to see. The theorem makes that obstruction explicit
2872 without claiming that an externally supplied truth allowance can be
2873 inferred from those responses.
2874 
2875 \end{proof}
2876 
2877 \src{CalibrationExamples.partial_not_surjective; CalibrationExamples.unseen_comp_partial; CalibrationExamples.unseen_norm; CalibrationExamples.arbitrarily_large_unseen_error; CalibrationExamples.perfect_partial_calibration_unbounded}
2878 
2879 \section{What the assembled calculus establishes}
2880 
2881 The results support a precise progression. Exact resolutions identify which
2882 coordinate vectors and coordinate kernels describe actual objects and
2883 operations. Split compression identifies the excursion through discarded
2884 state that prevents preservation of composition. Memory maps characterize
2885 prepared closure; finite hidden dimension turns their universal vanishing
2886 into a finite whole-map certificate. Behavioral quotients retain exactly
2887 the distinctions accessible to the declared future task. Normed defect
2888 budgets determine how approximate representations propagate their errors.
2889 
2890 In inverse problems, compatibility, realizability, and source identifiability
2891 remain distinct. The local obstruction quotient measures compatible data
2892 that have no global source. The compatibility residual measures the
2893 inconsistent sector, with its own conditioning constant. A global source
2894 has separate kernel ambiguity and inverse sensitivity. Regularization
2895 controls an actual penalized objective. Its strong limits recover each
2896 fixed identifiable source, while uniform source convergence requires
2897 closed range. Discrepancy rules and calibrated changing models add
2898 operational acceptance contracts whose true error allowances remain visible.
2899 
2900 The common theme is that changing a representation changes the obligations
2901 needed to use it. A certificate can discharge an obligation from concrete
2902 maps and inequalities. A residual can expose the remaining defect.
2903 An obstruction theorem can prove that an obligation is impossible under
2904 the available structure. These outcomes have different mathematical meanings.
2905 
2906 \subsection{Exact representation and information loss}
2907 A redundant exact coordinate space need not lose any information about its
2908 object, because synthesis after analysis is identity. Coarsening a packet
2909 address family can also remain exact if the entire contents of the merged
2910 packets are retained. Information loss is supplied by a separate map and
2911 its kernel. In the behavioral setting, only the largest invariant invisible
2912 subspace can be quotiented without changing any declared future observation.
2913 In source reconstruction, the unavoidable ambiguity is the true forward
2914 operator's kernel. Neither coordinate count nor packet count alone decides
2915 sufficiency.
2916 
2917 \subsection{Relations to established mathematics}
2918 The mathematics deliberately uses established foundations. Split idempotents,
2919 quotients, observability, block elimination, operator exponentials, orthogonal
2920 geometry, Moore--Penrose inversion, Tikhonov regularization, and discrepancy
2921 principles each contribute concrete constructions. The paper's organizing
2922 claim is that their interfaces can be written together, with exact
2923 transport, obstruction, approximation, and certificate obligations.
2924 Historical novelty of each component is a separate question. The formal
2925 inventory and finite test totals do not answer it.
2926 
2927 \subsection{Open bridges and extensions}
2928 The following problems specify further research beyond the printed contracts.
2929 
2930 \begin{enumerate}
2931 \item \textbf{Stable target-only recovery from behavioral minimality.}
2932 The exact quotient $X/N$ preserves all specified future observations.
2933 The Hilbert theory stably recovers an identifiable source under its
2934 reconstruction or regularization assumptions. A general theorem connecting
2935 these two constructions must identify a task target, its quotient metric,
2936 the relevant forward map, and sufficient conditioning. It should recover
2937 that target without requiring reconstruction of the full original source.
2938 No such unrestricted bridge is asserted in this edition.
2939 \item \textbf{Calibration truth allowances from individual samples.}
2940 The calibration theorems start from the whole-operator inequality
2941 $\nn{Y-AU}\le\eta_{\rm cal}$. Deriving it from individual noisy probes
2942 requires a specified sample model, a justified aggregation bound, and
2943 control of untested directions. A measured model fit supplies neither
2944 the true operator nor that truth allowance by itself.
2945 \item \textbf{Verified numerical procedures.}
2946 The formalization proves the certificate contracts. The rational Python
2947 implementations compute and check records under explicit input limits.
2948 Their parsers, arithmetic helpers, row-space saturation, parameter
2949 bracketing, and stopping procedures are not formally verified.
2950 Verified extraction or an independent formal certificate importer would
2951 add a new layer of assurance.
2952 \item \textbf{Additional admissible categories.}
2953 Minimum linear dimension does not establish a minimum positive,
2954 stochastic, integral, geometric, or nonlinear realization. Bounded
2955 autonomous generators do not settle unbounded-domain or time-dependent
2956 flow problems. Such extensions must print the additional admissibility
2957 and domain hypotheses rather than importing them through terminology.
2958 \end{enumerate}
2959 
2960 
2961 \section{Source distribution and verification boundaries}
2962 
2963 This edition contains a traditional paper, a visual guide, a Lean guide,
2964 and a complete source ZIP. The \texttt{.md} files are included in that ZIP,
2965 alongside editable \texttt{.tex}, the 93 production Lean modules, theorem
2966 guides, exact Python companions, example data, source inventories, and
2967 verification records. The original v0.16.0 archive is preserved separately
2968 for provenance. Publication sources and reconciliation records are
2969 additional files, not silent replacements of the mathematical source history.
2970 
2971 The principal concordance uses SR-01 through SR-64 with explicit hypotheses,
2972 dependencies, exact declaration names, and hashes of the source files read
2973 for this assembly. These are consolidated theorem groups. The declaration
2974 inventory comprises 998 theorem/lemma declarations and 1159 enumerated
2975 named declarations in 93 production modules. Supporting identities,
2976 classical specializations, definitions, and checked examples contribute
2977 to these totals.
2978 
2979 The archived v0.16.0 final verification includes two runs of the latest
2980 block's 31-module project dependency closure and audits of its 52 new
2981 named declarations. It does not record a fresh simultaneous compilation
2982 of every one of the 93 modules at that final checkpoint. The complete
2983 release verification record distinguishes archived Lean evidence,
2984 fresh compilation if any, source inspections, finite Python replay,
2985 document builds, and archive integrity. This manuscript makes no fresh
2986 Lean compilation claim merely from the existence of those archives.
2987 
2988 The exact-rational companions cover observation saturation, discrete
2989 memory, quantitative budgets, orthogonal globalization, quotient metrics,
2990 reconstruction, positive-parameter regularization, discrepancy,
2991 inexact solves, changing operators, generalized feasibility, and calibration.
2992 Their finite checks are implementation evidence in the tested dimensions
2993 and inputs. They are not universal proofs and do not infer external truth
2994 allowances. The current release's exact run ranges and counts belong in
2995 its machine-readable verification records so that archived and fresh
2996 results cannot be conflated.
2997 
2998 \subsection{Rebuilding the reading set}
2999 The supplied build scripts invoke pdfLaTeX three times for stable
3000 cross-references and table-of-contents entries. This rebuild creates the
3001 documents. It does not compile Lean, rerun scientific checks, infer a
3002 noise allowance, or authenticate a physical calibration experiment.
3003 Separate scripts and instructions address those activities.
3004 
3005 The standalone Markdown manuscript preserves the same statements and
3006 proofs for readers and tools that work directly with text. The concordance
3007 CSV/JSON provides a structured route from a mathematical claim to its
3008 formal declarations. The visual guide illustrates the same contracts
3009 with exact vector figures and checked rational examples. The Lean guide
3010 explains the production modules, the formal domains, and the evidence
3011 needed to reproduce the recorded builds.
3012 
3013 
3014 \appendix
3015 \section{Coverage of the sixteen development blocks}
3016 The block numbers below preserve the development history; they are not
3017 the section numbers of the reorganized paper. Each row identifies four
3018 consolidated theorem groups and the principal mathematical contract.
3019 
3020 \small
3021 \begin{longtable}{@{}p{0.07\textwidth}p{0.19\textwidth}p{0.66\textwidth}@{}}
3022 \toprule Block & Stable claims & Contract\\\midrule\endhead
3023 1 & SR-01--SR-04 & Exact redundant representation; compression defects; actual globalization obstruction; behavioral quotient.\\
3024 2 & SR-05--SR-08 & Discrete hidden elimination; closure equivalence; finite feedback certificate; canonical hidden-space construction.\\
3025 3 & SR-09--SR-12 & Finite observation horizon; minimal image dimension; realizable observation tables; finite certificate soundness.\\
3026 4 & SR-13--SR-16 & Exact word-defect transport; heterogeneous budgets; two-rate response; stable initialization bounds.\\
3027 5 & SR-17--SR-20 & Actual bounded flows; powers-to-exponentials bridge; continuous memory; finite moment and jet certificates.\\
3028 6 & SR-21--SR-24 & Duhamel defect transport; flow growth envelopes; uniform stability; scalar sharpness and instability boundary.\\
3029 7 & SR-25--SR-28 & Unique orthogonal error split; harmonic obstruction; compatibility conditioning; finite exactness and refinement.\\
3030 8 & SR-29--SR-32 & Constructed canonical inverse; minimum-norm source; source sensitivity; closed-range characterization.\\
3031 9 & SR-33--SR-36 & Native quotient metric; minimum representatives; bounded obstruction transport; refinement and nonclosed seminorm boundary.\\
3032 10 & SR-37--SR-40 & Coercive Tikhonov construction; objective optimality; bias/noise/kernel accounting; perturbation and globalization.\\
3033 11 & SR-41--SR-44 & Normal-range density; strong source limits; noisy and inexact consistency; uniform boundary and fitted-data limits.\\
3034 12 & SR-45--SR-48 & Actual residual curve; noncomputable root existence; norm-controlled strong consistency; accepted rule and endpoints.\\
3035 13 & SR-49--SR-52 & Source/image solver scales; protected measurements; near-accepted consistency; squared certificate soundness.\\
3036 14 & SR-53--SR-56 & Whole-operator uncertainty; model residual transport; changing-model consistency; operational certificates.\\
3037 15 & SR-57--SR-60 & Candidate-dependent self-bounding; source-cap-free acceptance; feasibility-aware selection; inexact and impossible-model boundaries.\\
3038 16 & SR-61--SR-64 & Redundant calibration frames; generated uncertainty and recovery; hierarchical/approximate frames; unseen-direction obstruction.\\
3039 \bottomrule\end{longtable}\normalsize
3040 
3041 \section{Principal dependency paths}
3042 The exact-coordinate path is SR-01 to SR-02. The hidden-memory path is
3043 SR-05 to SR-06 to SR-07, with SR-08 supplying the canonical bridge from an
3044 arbitrary split compression. The behavioral path starts at SR-04 and
3045 passes through SR-09--SR-12. Quantitative discrete transport is
3046 SR-13--SR-16. Bounded analytic flow converts the algebraic memory path
3047 through SR-17--SR-20 and provides approximate transport in SR-21--SR-24.
3048 
3049 The globalization path begins with the actual quotient SR-03 and its
3050 projected geometry SR-25--SR-28. Its intrinsic metric is proved in
3051 SR-33--SR-36. Canonical source reconstruction SR-29--SR-32 needs the
3052 additional source-space and closed-range hypotheses. Regularization
3053 SR-37--SR-40 relaxes closed range at positive parameter. Density and
3054 norm domination in SR-41 and SR-46 provide the common strong-consistency
3055 engine for the discrepancy rules and changing-model extensions.
3056 
3057 Calibration SR-61--SR-63 supplies operator-error allowances from its own
3058 externally justified truth bounds and conditioning. The recovery chain
3059 then uses generalized acceptance and explicit parameter feasibility.
3060 The negative control SR-64 explains why source-direction coverage is
3061 part of that contract.
3062 \end{document}

Back to source controls

Back to Sufficient Resolution