Komorebi Space

Download original file

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

Read the typeset paper

Read this chapter with formatted equations

1 \chap{Coordinates, noise, and a justified stopping rule}\label{sec:stopping-rules}
2 A certificate can be exact and still be interpreted incorrectly. Two common errors are to measure a coordinate covector with the wrong norm, or to keep a solver tolerance fixed while sending the regularization parameter to zero. Both change what a small reported number means.
3 
4 \subsection{The residual of the coordinate equation is a covector}
5 In finite dimensions, use orthonormal coordinates in the ambient candidate and residual spaces. Let the columns of $B$ form an arbitrary basis of $H=\ker p$, not necessarily an orthonormal one. Write $a=Bc$, $S=dB$, and $G=B^{\mathsf T}B$. As before, $G$ is positive definite. For an inexact coefficient vector $c$, the residual of the coordinate normal equation is
6 \[
7  q=(S^{\mathsf T}S+\alpha G)c-S^{\mathsf T}r.
8 \]
9 The vector $q$ stores pairings against basis vectors. It is not the coordinate vector of the Hilbert normal residual unless the basis is orthonormal.
10 
11 \begin{proposition}[The invariant norm of a coordinate certificate]\label{WR15}
12 The actual normal residual is
13 \begin{equation}\label{eq:covector-norm}
14  g=BG^{-1}q,\qquad \norm g^2=q^{\mathsf T}G^{-1}q.
15 \end{equation}
16 For any invertible change of basis $B'=BC$, the same proposed correction has
17 \[
18  c'=C^{-1}c,\quad G'=C^{\mathsf T}GC,\quad q'=C^{\mathsf T}q,
19 \]
20 and
21 \[
22  (q')^{\mathsf T}(G')^{-1}q'=q^{\mathsf T}G^{-1}q.
23 \]
24 \end{proposition}
25 \begin{proof}
26 Because $B$ has independent columns, for every nonzero coefficient vector $c$,
27 \[
28  c^{\mathsf T}Gc=c^{\mathsf T}B^{\mathsf T}Bc=\norm{Bc}^2>0.
29 \]
30 Thus $G$ is positive definite and invertible. The matrix $P=BG^{-1}B^{\mathsf T}$ is symmetric and obeys
31 \[
32  P^2=BG^{-1}(B^{\mathsf T}B)G^{-1}B^{\mathsf T}=P,
33  \qquad PB=B.
34 \]
35 Its range is precisely the column space $H$, so it is the orthogonal projection onto the entire permitted correction space.
36 
37 The restricted Hilbert normal residual is
38 \[
39  g=P d^{\mathsf T}(dBc-r)+\alpha Bc.
40 \]
41 Substitute $S=dB$, $G=B^{\mathsf T}B$ and the expression for $P$:
42 \[
43  g=BG^{-1}\bigl(S^{\mathsf T}(Sc-r)+\alpha Gc\bigr)=BG^{-1}q.
44 \]
45 Equivalently $q=B^{\mathsf T}g$ records the pairings of $g$ with the basis columns. Its squared Hilbert norm is
46 \[
47  g^{\mathsf T}g
48  =q^{\mathsf T}G^{-1}B^{\mathsf T}BG^{-1}q
49  =q^{\mathsf T}G^{-1}q,
50 \]
51 using symmetry of $G^{-1}$. This proves both coordinate formulas.
52 
53 For the basis change $B'=BC$, the same ambient vector is represented by $c'=C^{-1}c$. Also $S'=SC$ and $G'=C^{\mathsf T}GC$. Substitute these formulas into the new coordinate normal equation:
54 \[
55 \begin{aligned}
56  q'&=((S')^{\mathsf T}S'+\alpha G')c'-(S')^{\mathsf T}r\\
57  &=C^{\mathsf T}(S^{\mathsf T}S+\alpha G)CC^{-1}c
58       -C^{\mathsf T}S^{\mathsf T}r=C^{\mathsf T}q.
59 \end{aligned}
60 \]
61 The inverse metric is $(G')^{-1}=C^{-1}G^{-1}(C^{\mathsf T})^{-1}$. Hence
62 \[
63  (q')^{\mathsf T}(G')^{-1}q'
64  =q^{\mathsf T}C C^{-1}G^{-1}(C^{\mathsf T})^{-1}C^{\mathsf T}q
65  =q^{\mathsf T}G^{-1}q.
66 \]
67 For a zero-dimensional kernel these are empty matrices and zero vectors, and the resulting scalar norm is zero. The spanning assumption is indispensable: a basis of a proper subspace would compute a projection to a different correction problem.
68 \end{proof}
69 \written{WR15}
70 
71 In the previous example, $B=(1,1)^{\mathsf T}$, $G=2$, and the proposal $c=1/4$ gives $q=-1/4$. Thus $q^{\mathsf T}G^{-1}q=1/32$, as required. Replacing $B$ by $sB$ changes $q$ to $sq$ and $G$ to $s^2G$. The Euclidean norm of the coordinate covector can be made arbitrarily small or large by changing the nonzero scalar $s$. The actual correction, normal residual, and certified error do not change.
72 
73 \fixedplate{39_covector_metric}{Rescaling the basis of the same protected line rescales the raw coordinate covector. Its Euclidean norm is therefore not a representation-invariant stopping criterion. The Gram-corrected norm stays equal to $1/\sqrt{32}$ for every displayed scale. All systems represent the same proposed correction.}{fig:covector-metric}
74 
75 The finite verifier checks that a supplied basis spans the \emph{whole} protected kernel. A basis of a smaller subspace might give a correct certificate for that smaller optimization problem while missing an allowed direction that decreases the objective. The rank, kernel-membership, and independence checks therefore belong to the certificate contract.
76 
77 \subsection{Separate data error, numerical error, and regularization bias}
78 Let $r$ be the intended datum and $\widetilde r$ the measured datum. Suppose
79 \[
80  \norm{\widetilde r-r}\le\delta,
81  \qquad \norm{T^*(Ta-\widetilde r)+\alpha a}\le\varepsilon.
82 \]
83 The maps $T,p$ and their Hilbert metrics remain fixed. By Theorem~\ref{WR13} and the fixed-parameter part of Theorem~\ref{WR09},
84 \begin{equation}\label{eq:combined-solver-data}
85  \norm{a-a_\alpha(r)}
86  \le \frac{\varepsilon}{\alpha}+\frac{\delta}{2\sqrt\alpha}.
87 \end{equation}
88 The first term is the solver's contribution. The second is the worst-case propagation of data error. They should not be collapsed into one unqualified residual tolerance.
89 
90 \begin{theorem}[A consistent inexact stopping rule]\label{WR16}
91 Assume the projected intended datum belongs to the actual range of $T$, with minimum-norm preimage $a^\dagger$. Along a sequence of positive parameters and measured problems, suppose
92 \[
93  \alpha_n\to0,\qquad
94  \frac{\delta_n}{\sqrt{\alpha_n}}\to0,\qquad
95  \frac{\varepsilon_n}{\alpha_n}\to0.
96 \]
97 If the proposed corrections $a_n\in H$ satisfy the displayed data and normal-residual bounds, then $a_n\to a^\dagger$ in norm. At every index,
98 \[
99  \norm{a_n-a^\dagger}
100  \le\frac{\varepsilon_n}{\alpha_n}
101       +\frac{\delta_n}{2\sqrt{\alpha_n}}
102       +\norm{a_{\alpha_n}(r)-a^\dagger}.
103 \]
104 \end{theorem}
105 \begin{proof}
106 At index $n$, distinguish two exact minimizers: let $\widetilde a_n=a_{\alpha_n}(\widetilde r_n)$ solve the measured problem and let $a_n^0=a_{\alpha_n}(r)$ solve the intended-data problem. All three corrections, including the proposal $a_n$, belong to the same space $H$.
107 
108 The supplied normal-residual bound is for the measured datum. Therefore Theorem~\ref{WR13} applies first to that problem and gives
109 \[
110  \norm{a_n-\widetilde a_n}\le\frac{\varepsilon_n}{\alpha_n}.
111 \]
112 The pointwise data estimate in Theorem~\ref{WR09}, at the same parameter, then gives
113 \[
114  \norm{\widetilde a_n-a_n^0}\le\frac{\delta_n}{2\sqrt{\alpha_n}}.
115 \]
116 Insert these two intermediate vectors between $a_n$ and $a^\dagger$ in the triangle inequality to obtain the displayed three-term estimate.
117 
118 The first term tends to zero by the solver-tolerance hypothesis and the second by the data/parameter hypothesis. Since the projected intended datum is attained and $\alpha_n\to0$, the last term tends to zero by Theorem~\ref{WR08}. For a direct epsilon argument, make each term smaller than one third of a prescribed tolerance beyond its own threshold and take the maximum of the three thresholds. This gives norm convergence of the proposals.
119 
120 Protection is not merely asymptotic: $a_n\in\ker p$ implies $p(f-a_n)=pf$ at every index. The proof compares no changing operators or changing kernels. Both the pointwise certificate and the convergence conclusion have formal counterparts under these hypotheses.
121 \end{proof}
122 \written{WR16}
123 
124 The accompanying Lean formalization includes the pointwise estimate \eqref{eq:combined-solver-data}, the regularization limit, and the resulting convergence theorem. Their statements retain the same fixed operator, Hilbert geometry, and attainment requirements.
125 
126 \subsection{Retaining the explicit diagonal rate with an inexact solver}
127 For the attainable datum of Corollary~\ref{WR12} and $0<\delta\le1$, take $m=\lceil\delta^{-2/3}\rceil$ and $\alpha=m^{-2}$ as before. If an inexact solver satisfies
128 \[
129  \varepsilon\le\kappa\alpha\delta^{1/3}
130  \quad(\kappa\ge0),
131 \]
132 then the same argument gives
133 \[
134  \norm{a-a^\dagger}\le(\sqrt2+1+\kappa)\delta^{1/3}.
135 \]
136 Thus the inner solve can retain the proven outer accuracy if its normal residual decreases on the scale $\alpha\delta^{1/3}$. Since $\alpha$ is on the scale $\delta^{4/3}$, the corresponding normal-residual scale is $\delta^{5/3}$, with the stated ceiling factors retained in the exact rule. This is a sufficient rule for this problem, not a universal optimal stopping law.
137 
138 The declaration \path{DiagonalRegularization.diagonal_inexact_rounded_rate} formalizes this specialization for the actual infinite diagonal operator. Its hypotheses bound both the data error and the normal residual evaluated against the measured datum. It retains the literal ceiling in $m$ and derives the exact-data bias estimate within the model.
139 
140 \fixedplate{40_stopping_schedule}{For the attainable diagonal example, the three displayed terms are the proved bias bound, propagated data-noise bound, and a solver-error budget chosen to preserve the same $\delta^{1/3}$ rate. The ceiling in $m=\lceil\delta^{-2/3}\rceil$ is evaluated explicitly. The plot shows bounds, not measurements from a trained system.}{fig:stopping-schedule}
141 
142 For the escaping datum, the same rule does not create convergence to a nonexistent protected Hilbert answer. It only makes the numerical proposals track the regularized path accurately. Tracking an escaping path and converging to a realization are different conclusions.
143 
144 \subsection{The executable verification contract}
145 The program takes $d,p,f,\alpha$ and a proposed ambient correction, with optional measured residuals, a full kernel basis, and an independent dual witness. It rejects a correction that changes the protected data and checks the basis's dimensions, rank, and kernel membership. It does not silently project a rejected proposal into another problem.
146 
147 The output records $f-a$, protection before and after, measured fit, actual model residual, the Gram-corrected normal certificate, objective values, and squared error bounds. Verification recomputes the record without calling an optimizer. Independent determinant-based tests compare the bounds with actual errors in small ambient constrained systems. A certificate establishes consistency with its included problem, not authentication that this is the externally intended task.
148 
149 \begin{insight}
150 A certificate needs a declared target. Fit measures agreement with data. The normal residual bounds optimizer error at a specified parameter. The duality gap bounds objective error. A realization theorem is still needed to conclude convergence to an intended exact object.
151 \end{insight}

Back to source controls

Back to Komorebi Space