COS Method

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 \chapter{Formalization and theorem correspondence}\label{app:lean}
2 The formal companion covers exact finite Gram algebra, disjoint block
3 refinement, reindexing, streamed actions, nonnegativity, coefficient order,
4 and arithmetic consequences of supplied enclosures. It does not establish
5 the Gaussian reduction, Fourier inversion, analytic remainders, spectral
6 post-verification algorithm, or transcendental interval-library correctness.
7 A theorem that assumes an enclosure does not construct that enclosure.
8 
9 \begin{scopebox}
10 \textbf{Recorded kernel evidence.} The retained compiler record accepts
11 26 theorem declarations and 8 definitions, with a 34-declaration axiom audit.
12 The audited dependencies are confined to \texttt{propext},
13 \texttt{Classical.choice}, and \texttt{Quot.sound}. No \texttt{sorryAx} or
14 custom axiom appears. A valid arithmetic control was accepted, while false
15 arithmetic and an acceptance proof missing its error-budget premise were
16 rejected. This volume preserves that evidence and the pinned sources. It
17 does not claim a new Lean compilation.
18 \end{scopebox}
19 
20 \label{app:lean-contract}
21 \section{How the formal model represents the engine}
22 
23 The factor has a finite sample index type $I$ and an arbitrary variant index
24  type $V$. A variant block is a finite set $s\subseteq V$. The factor entries
25 are exact real numbers, $A:I\times V\to\R$. The Lean type is
26 \decl{Row -> Variant -> Real}. The sample coordinates carry a
27 \decl{Fintype} instance. The variants carry a \decl{DecidableEq} instance to
28 support finite-set unions, singleton blocks, and reindexing.
29 
30 The residualized weighted factor in the main text is
31 \[
32  A=M_X G W^{1/2}.
33 \]
34 For this companion, $A$ is supplied. Proving that a particular floating-point
35 residualization procedure computes that mathematical factor would require
36 additional implementation and numerical-error reasoning. These modules do
37 not assume a covariance model or a distribution for the vector $v$.
38 
39 There are five central finite-algebra definitions:
40 \begin{align*}
41  \operatorname{gramEntry}(s,A,i,j)&=\sum_{k\in s}A_{ik}A_{jk},\\[6pt]
42  \operatorname{matrixAction}(K,v,i)&=\sum_{j\in I}K_{ij}v_j,\\[6pt]
43  \operatorname{streamedAction}(s,A,v,i)&=\sum_{k\in s}A_{ik}\sum_{j\in I}A_{jk}v_j,\\[6pt]
44  \operatorname{quadraticForm}(K,v)&=\sum_{i\in I}v_i\operatorname{matrixAction}(K,v,i),\\[6pt]
45  \operatorname{factorEnergy}(s,A,v)&=\sum_{k\in s}\left(\sum_{i\in I}A_{ik}v_i\right)^2.
46 \end{align*}
47 The source uses ordinary finite sums in $\R$. The factor convention is the
48 sample Gram $AA^\top$, matching \decl{stream_sample_gram}. It is not the dual
49 Gram $A^\top A$. The case-study statistic $Q=\tfrac12 v^\top Kv$ requires the
50 additional scalar factor $\tfrac12$ when applying these identities.
51 
52 \section{Exact block refinement}
53 
54 The principal refinement theorem is \decl{gramEntry_union}. Its hypotheses
55 are finite sets $s,t\subseteq V$ and $\operatorname{Disjoint}(s,t)$. It proves,
56 for all sample coordinates $i,j$,
57 \[
58  \operatorname{gramEntry}(s\cup t,A,i,j)
59  =\operatorname{gramEntry}(s,A,i,j)+\operatorname{gramEntry}(t,A,i,j).
60 \]
61 Disjointness prevents repeated columns from being counted twice. It is a
62 mathematical condition, not a performance assumption. The theorem applies to
63 empty blocks and zero factors. It does not require positive weights, since
64 $A$ is already supplied as a real factor.
65 
66 The proof unfolds \decl{gramEntry} and invokes the finite-sum union identity.
67 No numerical approximation is involved. Repeated application establishes
68 invariance along any explicitly checked sequence of binary disjoint splits.
69 The source does not encode a whole scheduler or its memory allocation policy.
70 A scheduler correctness proof would additionally track complete coverage,
71 disjointness, and termination at every split.
72 
73 The same refinement has formal consequences for the operator action and the
74 quadratic statistic:
75 \begin{align*}
76  (K_{s\cup t}v)_i&=(K_s v)_i+(K_t v)_i,\\
77  v^\top K_{s\cup t}v&=v^\top K_s v+v^\top K_t v.
78 \end{align*}
79 These are \decl{matrixAction_gram_union} and
80 \decl{quadraticForm_gram_union}. The independent
81 \decl{streamedAction_union} proves the corresponding streamed accumulation
82 identity directly.
83 
84 The reindexing theorem \decl{gramEntry_reindex} handles a bijection
85 $e:V\simeq V$. It moves the block to $e(s)$ and transforms the factor to
86 $A'_{ik}=A_{i,e^{-1}(k)}$. The resulting Gram entry is unchanged. Permuting
87 only the coordinates without moving their factor columns falls outside this
88 statement.
89 
90 \section{Streamed actions and the sum-of-squares identity}
91 
92 \decl{matrixAction_gram_eq_streamed} proves
93 \[
94  \sum_{j\in I}\left(\sum_{k\in s}A_{ik}A_{jk}\right)v_j
95  =\sum_{k\in s}A_{ik}\left(\sum_{j\in I}A_{jk}v_j\right).
96 \]
97 This is the exact algebra behind multiplication by a sample Gram matrix
98 without constructing that matrix. Lean checks the finite-sum interchange and
99 associativity of real multiplication. It does not assert that a given
100 sequence of device operations has exact real semantics.
101 
102 The next theorem, \decl{quadraticForm_gram_eq_energy}, proves
103 \[
104  v^\top K_s v=\sum_{k\in s}\left(\sum_{i\in I}A_{ik}v_i\right)^2.
105 \]
106 It expands the action, interchanges the finite sums, factors each coordinate
107 sum, and identifies the product of a projection with itself. The resulting
108 \decl{quadraticForm_gram_nonneg} states $0\le v^\top K_s v$ for every real
109 vector $v$. This is positive semidefiniteness of the supplied Gram form.
110 
111 These identities are useful together. Refinement preserves the represented
112 operator, streaming preserves its action, and the energy identity verifies
113 its positivity. They do not require the eigenvalues or the spectral theorem.
114 The full engine subsequently uses numerical rank compression and spectral
115 information, whose correctness contracts are separate.
116 
117 \section{A complete exact algebra example}
118 
119 Consider one sample coordinate and two variant columns with
120 \[
121  A=(3\quad4),\qquad v=2.
122 \]
123 The two singleton Gram contributions are $9$ and $16$. Their disjoint union
124 has Gram entry $25$. Matrix multiplication gives $Kv=50$ and
125 $v^\top Kv=100$. The streamed action instead computes
126 \[
127  3(3\cdot2)+4(4\cdot2)=18+32=50.
128 \]
129 The energy expression gives
130 \[
131  (3\cdot2)^2+(4\cdot2)^2=36+64=100.
132 \]
133 Thus the engine statistic with the stated half normalization is $Q=50$.
134 All paths are exact real identities. This example explains the type and
135 normalization choices. The universal theorems establish them for arbitrary
136 finite sample coordinates and variant blocks.
137 
138 If the two blocks overlap in one column, their sum repeats that column's
139 outer product. For $s=t=\{1\}$ and $A_{i1}=3$, the union has contribution $9$
140 while the sum of the two blocks is $18$. This is why
141 \decl{gramEntry_union} requires disjointness.
142 
143 \section{Supplied coefficient intervals}
144 
145 The separate definition
146 \[
147  \operatorname{weightedSquares}(s,c,z)=\sum_{k\in s}c_k z_k^2
148 \]
149 models a supplied diagonal quadratic form. Its coefficients need not be
150 eigenvalues obtained by a proved diagonalization. It has three theorems:
151 \begin{itemize}
152  \item \decl{weightedSquares_mono}: if $l_k\le u_k$ for every $k\in s$, then
153  $\sum l_kz_k^2\le\sum u_kz_k^2$.
154  \item \decl{weightedSquares_nonneg}: if $c_k\ge0$ for every $k\in s$, then
155  $\sum c_kz_k^2\ge0$.
156  \item \decl{weightedSquares_tail_imp}: coefficientwise order gives the
157  pointwise implication $q\le\sum l_kz_k^2\Rightarrow q\le\sum u_kz_k^2$.
158 \end{itemize}
159 The first and third allow signed coefficients because squares remain
160 nonnegative. The second has an explicit nonnegativity hypothesis.
161 
162 The pointwise implication is a prerequisite for probabilistic tail
163 sandwiching. It does not itself state a probability inequality or build a
164 coupling. To turn it into such a statement, one must supply measurable random
165 coordinates on a common probability space and use monotonicity of measure.
166 To apply it to matrix spectra, one must also establish that each true
167 coefficient lies inside the supplied interval.
168 
169 \section{Enclosures and error ledgers}
170 
171 The interval module uses two elementary predicates:
172 \begin{align*}
173  \operatorname{Enclosed}(x,L,U)&\;:\Longleftrightarrow\;L\le x\le U,\\
174  \operatorname{ErrorBound}(x,\widehat x,r)&\;:\Longleftrightarrow\;
175  |x-\widehat x|\le r.
176 \end{align*}
177 The equivalence \decl{errorBound_iff_enclosed} proves
178 \[
179  |x-\widehat x|\le r
180  \quad\Longleftrightarrow\quad
181  \widehat x-r\le x\le\widehat x+r.
182 \]
183 There is no extra nonnegativity hypothesis: if this predicate holds, then the
184 radius is necessarily nonnegative. The definition accepts arbitrary real
185 inputs, and the theorem states the exact logical equivalence.
186 
187 For the K-COS error ledger, distinguish the ideal analytic quantity $x$, an
188 exact finite transform $m$, and the computed estimate $\widehat x$. If
189 \[
190  |x-m|\le a,\qquad |m-\widehat x|\le b,
191 \]
192 then \decl{errorBound_compose} proves
193 \[
194  |x-\widehat x|\le a+b.
195 \]
196 The proof is the triangle inequality. The hypotheses must be proved
197 independently. In particular, $a$ can contain a support/alias bound and an
198 omitted-mode bound. This theorem only composes those supplied facts.
199 
200 \decl{errorBound_accept} adds the hypothesis $a+b\le\varepsilon$ and concludes
201 $|x-\widehat x|\le\varepsilon$. This is the arithmetic core of acceptance by a
202 proved budget. A sequence of numerically stable estimates, without valid
203 bounds, does not satisfy its hypotheses.
204 
205 \section{Safe transformations of an enclosure}
206 
207 The remaining interval statements are reusable exact-real rules.
208 \decl{enclosed_add} adds two enclosed quantities.
209 \decl{enclosed_scale} scales the interval by a nonnegative real factor.
210 \decl{enclosed_widen} permits an explicitly wider interval.
211 \decl{enclosed_intersect} combines two independently valid enclosures of the
212 same quantity using $\max$ on the lower endpoints and $\min$ on the upper
213 endpoints.
214 
215 \decl{enclosed_positive} requires a strictly positive lower endpoint. It then
216 proves that the enclosed quantity is positive. This is relevant before
217 applying a logarithm to a corrected tilted finite sum. A lower endpoint equal
218 to zero does not establish positivity.
219 
220 Finally, \decl{enclosed_monotone} transports an interval through a supplied
221 monotone function. Its hypothesis is global monotonicity on $\R$. The source
222 does not directly instantiate this rule with the real logarithm, which needs
223 a positive-domain formulation. A log-tail certificate therefore still needs
224 both positivity and a separate domain-correct monotonicity argument. The
225 interval-library implementation also requires its own correctness contract.
226 
227 \section{Declaration inventory and theorem correspondence}
228 
229 All names below are prefixed by \decl{KomorebiQCOS}. The inventory counts
230 project theorems only. Imported mathlib theorems are not counted.
231 
232 {\small
233 \begin{longtable}{@{}P{0.49\linewidth}P{0.45\linewidth}@{}}
234 \toprule Declaration & Exact formal scope\\\midrule\endhead
235 \decl{gramEntry_empty} & Empty variant block gives zero.\\
236 \decl{gramEntry_singleton} & One column gives its outer product.\\
237 \decl{gramEntry_symm} & Real Gram entry symmetry.\\
238 \decl{gramEntry_union} & Disjoint binary block refinement.\\
239 \decl{gramEntry_reindex} & Factor-column permutation invariance.\\
240 \decl{matrixAction_gram_eq_streamed} & Gram action equals streamed factor action.\\
241 \decl{matrixAction_add} & Operator-action additivity.\\
242 \decl{matrixAction_gram_union} & Action refinement invariance.\\
243 \decl{streamedAction_union} & Streamed accumulation over disjoint blocks.\\
244 \decl{quadraticForm_add} & Quadratic-form additivity in the matrix.\\
245 \decl{quadraticForm_gram_eq_energy} & Gram form equals factor energy.\\
246 \decl{quadraticForm_gram_nonneg} & Positivity of the supplied Gram form.\\
247 \decl{quadraticForm_gram_union} & Statistic refinement invariance.\\
248 \decl{weightedSquares_mono} & Pointwise coefficientwise order.\\
249 \decl{weightedSquares_nonneg} & Positivity for nonnegative coefficients.\\
250 \decl{weightedSquares_tail_imp} & Pointwise tail-event implication.\\
251 \decl{enclosed_order} & A valid enclosure has ordered endpoints.\\
252 \decl{enclosed_add} & Additive interval composition.\\
253 \decl{enclosed_scale} & Nonnegative scaling.\\
254 \decl{enclosed_widen} & Valid interval widening.\\
255 \decl{enclosed_intersect} & Intersection of valid enclosures.\\
256 \decl{errorBound_iff_enclosed} & Absolute-error/enclosure equivalence.\\
257 \decl{errorBound_compose} & Analytic and arithmetic budget composition.\\
258 \decl{errorBound_accept} & Acceptance below a supplied tolerance.\\
259 \decl{enclosed_positive} & Positive lower endpoint proves positivity.\\
260 \decl{enclosed_monotone} & Supplied monotone transformation.\\
261 \bottomrule
262 \end{longtable}
263 }
264 
265 The exact-block, hierarchical-blocking, and streamed-action sections of the
266 main text map to the Gram theorems under the definitions above. The
267 error-ledger and acceptance sections map only to the arithmetic consequences
268 of already valid bounds. The matrix-to-tail bridge maps to pointwise
269 coefficient order only. The detailed machine-readable concordance includes
270 source filenames and implementation anchors.
271 
272 \section{Reproduction and trusted dependencies}
273 
274 The companion includes the pinned toolchain and dependency manifest, two
275 mathematical modules, a root import, an axiom audit, controls, and retained
276 build logs. From the companion directory, run:
277 \begin{verbatim}
278 lake exe cache get
279 lake build
280 lake env lean AxiomAudit.lean
281 \end{verbatim}
282 Reproduction requires the pinned compiler and dependencies. Compiler
283 binaries and the mathlib cache are not distributed in this package.
284 The retained runtime record includes an executable-location adapter and its
285 source. It did not modify the compiler or proof kernel.
286 
287 The positive and negative controls supplement the theorem build. The
288 axiom audit records each declaration's dependencies. Classical choice,
289 propositional extensionality, and quotient soundness are the reported
290 foundational dependencies. Any \decl{sorryAx} occurrence would indicate an
291 admitted proof. A clean admission scan alone does not establish acceptance.
292 The retained compiler logs and axiom output provide that evidence.
293 
294 \section{Remaining formal obligations}
295 
296 An end-to-end formal certificate would also require:
297 \begin{enumerate}[nosep,topsep=4pt]
298  \item Gaussian whitening and central, signed, and noncentral reductions
299  under their exact hypotheses.
300  \item Spectral decomposition and a proved connection between the input
301  matrix, its factor, and coefficient intervals.
302  \item Probability monotonicity under a common measurable coupling.
303  \item Exponential tilting and the transform/payoff inversion identity.
304  \item Support, alias, and omitted-mode bounds with their rank and
305  moment-generating-function domain conditions.
306  \item Exact interval semantics for input literals, directed rounding,
307  roots, complex transforms, logarithms, and transcendental operations.
308  \item A verified implementation-to-bound correspondence, including
309  input parsing and output endpoint conversion.
310 \end{enumerate}
311 These are separate obligations. The retained checks establish the finite
312 algebra and enclosure arithmetic listed in the inventory, not the
313 additional analytic or numerical layers.

Back to source controls

Back to COS Method