Certified Bayesian Inference

Download original file

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

Read the typeset paper

1 \section{An exact selective iteration with a preserved cache}
2 \label{sec:solver-cache}
3 
4 The posterior certificate becomes an algorithm when it is paired with a gain
5 construction that is guaranteed to reach a passing certificate. The canonical
6 construction in Core 1.0.0 performs exact rational selected-packet updates. It
7 retains enough residual information to choose the next update without rebuilding
8 the complete residual after every step. Its final certificate and parameter
9 representation use outward-rounded dyadic arithmetic. These are separate stages
10 with separate correctness arguments.
11 
12 Throughout this section, the state dimension and observation dimension are finite.
13 The supplied rational model has
14 \[
15  P=LL^{\mathsf T},\qquad R=NN^{\mathsf T}+\sigma I,
16  \qquad \sigma>0,
17 \]
18 and observation operator $H$. Put
19 \[
20  S=HPH^{\mathsf T}+R,\quad v=y-Hm,\quad
21  F(B)=PH^{\mathsf T}-BS,\quad E(X)=\Frob{X}^{2}.
22 \]
23 The output packet family $(Q_a)_{a\in A}$ consists of rational self-adjoint,
24 mutually orthogonal projectors with sum $I$. The input family $(D_b)_{b\in D}$
25 has the same properties on the observation space. The output family controls
26 selection and cache maintenance. The input family participates in the independent
27 final certificate. No commutation relation between $S$ and the input projectors
28 is assumed.
29 
30 Preprocessing forms three model-dependent constants:
31 \begin{equation}
32  \tau=\frac{1}{\sigma+\tr S},\qquad T=I-\tau S,
33  \qquad w=\frac{\sigma+\lVert v\rVert^{2}}{\sigma^{2}}.
34  \label{eq:solver-kernel}
35 \end{equation}
36 All are rational. They are the fields of the record
37 \path{Komorebi.CachedPosterior.Kernel}, produced by
38 \path{Komorebi.CachedPosterior.prepare}. The correctness theorems use this actual
39 preparation, rather than an arbitrary record whose fields happen to have the same
40 names. A wrong transition matrix or weight would invalidate the correspondence
41 between the stored score and the posterior certificate.
42 
43 \begin{definition}[Cache validity]
44 A cache state is a tuple $c=(B,(G_a),(e_a),t)$ satisfying
45 \begin{equation}
46  G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a.
47  \label{eq:solver-invariant}
48 \end{equation}
49 The cached score is $s(c)=tw$.
50 \end{definition}
51 
52 Validity is an exact equality invariant. It does not mean that a stored residual
53 is approximately near a true residual, nor that its energy is merely an upper
54 bound. Initialization evaluates $F(B_0)$ once, projects it onto every output
55 packet, computes every energy, and sums them. The theorem
56 \path{initialState_valid} follows directly from the definitions. It requires no
57 prediction about future iterates.
58 
59 Orthogonal complete packets account for the whole energy:
60 \[
61  \sum_{a\in A}E(Q_aF)=E(F).
62 \]
63 Consequently a valid cache has $t=E(F(B))$ and
64 \begin{equation}
65  s(c)=E(F(B))\frac{\sigma+\lVert v\rVert^2}{\sigma^2}=a(B).
66  \label{eq:solver-score}
67 \end{equation}
68 The right-hand side is the exact residual score used by the posterior error
69 certificate. The declarations \path{total_eq_residual_energy} and
70 \path{score_eq} establish these two identifications. The total is therefore a
71 meaningful global stopping signal even though only one of its summands changes
72 in an iteration.
73 
74 For a selected label $a$, the executed update is
75 \begin{align}
76  B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\
77  G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a),
78  &t'&=t-e_a+e'_a.
79  \label{eq:solver-cache-step}
80 \end{align}
81 This is the definition \path{Komorebi.CachedPosterior.step}. It computes the new
82 selected residual from the old selected residual and the precomputed transition.
83 It retains unselected entries and updates the scalar total by a difference. The
84 implementation does not define its new state by recomputing $F(B')$ and projecting
85 that matrix onto every packet.
86 
87 \begin{proposition}[Preservation by the executed update]
88 If the output packets satisfy the stated projector assumptions, $c$ is valid,
89 and the kernel is \path{prepare M}, then the state in
90 \eqref{eq:solver-cache-step} is valid.
91 \end{proposition}
92 \begin{proof}
93 By cache validity, $G_a=Q_aF(B)$, so the gain update is the exact packet step
94 $B'=B+\tau Q_aF(B)$. Expand its residual:
95 \[
96  F(B')=F(B)-\tau Q_aF(B)S.
97 \]
98 Multiplication on the left by the selected projector gives
99 \[
100  Q_aF(B')=Q_aF(B)-\tau Q_a^2F(B)S
101           =G_a(I-\tau S)=G_aT.
102 \]
103 For $b\ne a$, mutual orthogonality gives $Q_bQ_a=0$ and hence
104 $Q_bF(B')=Q_bF(B)=G_b$. This proves every residual equality in the new cache.
105 Its energy equalities hold because the selected energy is evaluated from its new
106 residual and the remaining residual-energy pairs are retained. Finally, replacing
107 one term in a finite sum changes that sum by exactly $-e_a+e'_a$. Thus
108 $t'=\sum_b e'_b$. All three clauses of validity are preserved.
109 \end{proof}
110 
111 This proof is realized by \path{step_valid}, using the algebraic identities
112 \path{selected_residual} and \path{unselected_residual}. The declarations
113 \path{step_other_residual} and \path{step_other_energy} expose the unchanged
114 entries independently. The distinction between proving an invariant for an
115 executed update and postulating it for a desired state is decisive: the later
116 termination theorem uses the invariant at every state visited by the program.
117 
118 The locality is on the output side. For an input projector $D_b$,
119 \[
120  F(B')D_b=F(B)D_b-\tau Q_aF(B)SD_b.
121 \]
122 The factor $SD_b$ can mix input directions. The source declaration
123 \path{input_packet_effect} makes this effect explicit. Complete input packets
124 can still account for certificate energy, but an input packet decomposition does
125 not by itself make the iteration independently local in both indices.
126 
127 \section{Selection, exact trajectory equality, and finite fuel}
128 \label{sec:solver-termination}
129 
130 The algorithm chooses a largest stored output energy. Its finite scan has a seed
131 label and an ordered list. It replaces the incumbent label only when a scanned
132 label has strictly greater energy. On an equality it preserves the incumbent.
133 This tie rule appears in the definition \path{winner}, whose comparison is
134 \path{e a < e b}. The scan may contain repeated labels. Completeness requires
135 that every output label occurs in the scan, while the seed supplies an inhabitant
136 of the label type. The proof counts the cardinality of the finite label type,
137 not the length of a possibly repeated scan.
138 
139 \path{winner_ge_initial} and \path{winner_ge_member} prove that the final winner
140 has energy at least that of the seed and of every scanned label. Under complete
141 coverage, \path{selectPacket_max} therefore supplies a genuine maximum over all
142 output packet energies. The argument does not prescribe a fixed schedule. The
143 maximum is selected again from the current state after every update.
144 
145 \begin{proposition}[Exact selection and gain equality]
146 For a valid cache, cached selection returns the same label as a scan of the
147 recomputed energies $E(Q_aF(B))$. Starting from an initialized cache and using the
148 prepared kernel, its gain after $n$ updates equals the recomputed greedy gain after
149 $n$ updates, for every $n\in\N$.
150 \end{proposition}
151 \begin{proof}
152 Each stored energy equals the corresponding recomputed energy by
153 \eqref{eq:solver-invariant}. Both scans therefore receive the same energy
154 function, the same seed, the same list, and the same strict comparison. Their
155 outputs are equal, including ties. This is \path{chosen_eq}. The cache gain update
156 then equals the recomputed greedy step by \path{advance_gain}.
157 
158 The initial gains agree at $n=0$. Suppose they agree at $n$. The cache at that
159 index is valid by repeated application of \path{step_valid}. Equality of
160 selection and equality of the gain step give equality at $n+1$. Induction proves
161 the entire trajectory identity. The formal statements are
162 \path{trajectory_valid} and \path{trajectory_gain}.
163 \end{proof}
164 
165 This is stronger than convergence to the same limit. At a fixed index, the two
166 rational gain matrices are identical. As a result, the convergence proof for the
167 recomputed greedy algorithm transfers directly to the cached execution.
168 
169 Write $A_{\mathrm{count}}=|A|$ for the positive number of output labels, and set
170 \begin{equation}
171  \rho=1-\frac{\sigma}{\sigma+\tr S},\qquad
172  q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}.
173  \label{eq:solver-rates}
174 \end{equation}
175 The model factorization and positive noise floor imply that $S$ is positive
176 semidefinite with quadratic lower bound $\sigma$. Its trace is nonnegative, and
177 $\sigma+\tr S$ is a valid positive spectral cap. Thus $0\le\rho<1$, $0\le q<1$,
178 and $0\le r<1$. No eigenvalue oracle is needed to construct these rational
179 constants.
180 
181 The transition contracts every residual matrix:
182 \[
183  E(XT)\le qE(X).
184 \]
185 If label $a$ is updated, its residual energy contracts by this inequality and
186 all other output residuals remain unchanged. Orthogonal energy accounting gives
187 \[
188  E(F(B'))\le E(F(B))-(1-q)e_a.
189 \]
190 Because $a$ is a maximum, $e_a\ge E(F(B))/A_{\mathrm{count}}$. It follows that
191 \begin{equation}
192  E(F(B'))\le rE(F(B)),\qquad
193  a(B_n)\le r^na(B_0).
194  \label{eq:solver-geometric}
195 \end{equation}
196 The energy share is \path{selected_energy_share}; one-step contraction is
197 \path{greedy_energy_contract}; and the score estimate is
198 \path{greedy_score_geometric}. The estimate allows singular $P$, arbitrary initial
199 rational $B_0$, rectangular $H$, and rational rotated packets under the same
200 projector assumptions.
201 
202 A convergent sequence alone would not define a terminating program with an
203 explicit natural-number budget. The source supplies a logarithm-free fuel:
204 \begin{equation}
205  N=\left\lceil
206  \frac{a(B_0)}{(\varepsilon/2)^2(1-r)}
207  \right\rceil_{\N},\qquad \varepsilon>0.
208  \label{eq:solver-fuel}
209 \end{equation}
210 Here $\lceil\cdot\rceil_{\N}$ is the natural-number ceiling used by
211 \path{toleranceFuel}. The canonical \path{adaptiveFuel} evaluates this expression
212 from the actual model, initial gain, tolerance, and number of labels.
213 
214 \begin{lemma}[Rational fuel sufficiency]
215 For $0\le r<1$ and $n\ge N$, the geometric envelope obeys
216 $r^na(B_0)\le\varepsilon^2/4$.
217 \end{lemma}
218 \begin{proof}
219 The source first proves
220 \[
221  r^n\bigl(1+n(1-r)\bigr)\le1.
222 \]
223 At the induction step, the inequality
224 $r(1+(n+1)(1-r))\le1+n(1-r)$ reduces to nonnegativity of
225 $(n+1)(1-r)^2$. The natural ceiling in \eqref{eq:solver-fuel} gives
226 $a(B_0)\le n(\varepsilon/2)^2(1-r)$. Multiplying by the nonnegative
227 $r^n$ and applying the preceding bound yields the required squared tolerance.
228 The proof remains valid when the contraction factor is zero. The source
229 statements are \path{geometric_bernoulli}, \path{geometric_fuel_sufficient}, and
230 \path{greedy_score_at_fuel}.
231 \end{proof}
232 
233 This fuel is conservative. The geometric rate is substantially sharper than the
234 reciprocal envelope used to obtain a simple rational fuel, and the executed search
235 can stop much earlier. Neither the large natural fuel nor its existence is a
236 claim about a practical time or memory budget.
237 
238 \path{search} tests the exact cached score against $\varepsilon^2/4$ at the current
239 state. If the test fails and fuel remains, it advances once and decrements fuel.
240 At fuel zero it still tests the last permitted state. This convention permits
241 success after exactly $N$ updates. \path{search_score} proves that every returned
242 state passes the score condition. \path{search_origin} proves that a returned
243 state is an actual trajectory state at some $k\le N$. Finally,
244 \path{search_complete} proves that a passing score at the last permitted state
245 forces the search to return some state, possibly earlier.
246 
247 Combining preserved validity, exact trajectory equality, and fuel sufficiency
248 therefore proves a finite successful cached search. There is no caller-supplied
249 claim that an iteration has converged. The computed budget and proved invariant
250 supply the necessary conclusion internally.
251 
252 \section{Independent final verification and precision fallback}
253 \label{sec:solver-verification}
254 
255 The exact cached score is used to select a gain and establish termination. The
256 successful gain is still sent to the independent certificate evaluator. That
257 evaluator reconstructs rounded packet residual obligations from the actual model
258 and gain. It does not accept the stored cache energies as certificate evidence.
259 This separation protects successful returns from an incorrect internal stopping
260 signal. The canonical route checks setup, constructs the outward-rounded
261 candidate, and executes its tolerance test. Construction and setup imply that
262 \path{checkCandidate} is true by theorem. A separate untrusted-candidate checker
263 can recompute exact residual obligations; that is distinct from the canonical
264 rounded construction route.
265 
266 The definition \path{solveCached} first checks a positive posterior tolerance,
267 valid model and packet setup, and complete scan coverage. It prepares the kernel,
268 initializes the cache, and runs the exact-score search with its computed fuel.
269 Only the returned gain is passed to \path{certifyGain}. Thus certificate evaluation
270 is outside the selective update loop. The definition makes one call to this final
271 verification procedure, although that procedure may try several precisions.
272 
273 The precision schedule consists of the caller's finite list of probes followed by
274 one computed fallback. The probes can be empty, repeated, or unordered. Successful
275 verification records the precision actually used. The appended fallback makes
276 finite success independent of a lucky externally chosen probe.
277 
278 Let $h_p=2^{-p}$. The dyadic evaluator propagates rational centers and outward
279 radii through its arithmetic graph. Its budget calculation supplies a nonnegative
280 coefficient $C_{\mathrm{ver}}(M,Q,D,B)$ independent of $p$, with
281 \begin{equation}
282  \widehat a_p(B)\le a(B)+C_{\mathrm{ver}}(M,Q,D,B)h_p.
283  \label{eq:solver-inflation}
284 \end{equation}
285 Here $\widehat a_p$ is the actual rounded candidate score. The full expression for
286 the coefficient is \path{scoreRoundCoeff}, built from packet residual energy and
287 innovation-vector magnitude and radius budgets. It bounds the entire score graph,
288 rather than rounding only its final exact answer. The theorem
289 \path{rounded_score_inflation} proves \eqref{eq:solver-inflation}.
290 
291 The common precision selector is the computable integer expression
292 \begin{equation}
293  \operatorname{precisionFor}(C,d)
294  =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1,
295  \qquad d>0,
296  \label{eq:solver-precision}
297 \end{equation}
298 where $\log^{\N}_2$ denotes the natural-number logarithm \path{Nat.log}, including its
299 specified value at zero. It is not a floating-point logarithm. For every precision
300 at least this selected count, \path{coefficient_mesh_le} gives $C2^{-p}\le d$.
301 The proof uses integer power and ceiling inequalities. The additional bit is a
302 sufficient choice, not a claim that the bit count is minimal.
303 
304 For final verification, the solver appends
305 \[
306  p_* = \operatorname{sufficientPrecision}(M,Q,D,B,\varepsilon^2/4).
307 \]
308 At its returned search state, $a(B)\le\varepsilon^2/4$. The fallback guarantees
309 inflation at most another $\varepsilon^2/4$, so
310 \[
311  \widehat a_{p_*}(B)\le\varepsilon^2/2\le\varepsilon^2.
312 \]
313 Positive $\varepsilon$ gives a positive inflation allowance. Valid model and
314 packet setup give the candidate check, while this inequality gives the tolerance
315 check. The declarations \path{certifyRounded_of_slack} and
316 \path{certifyGain_complete} establish that the fallback must succeed.
317 
318 The stricter search threshold supplies room for rounded verification. Searching
319 only until an exact score happened to equal $\varepsilon^2$ would leave no positive
320 allowance for an enclosing evaluator. The construction deliberately separates
321 progress from verification slack. Its inherited geometric fuel is computed for
322 $\varepsilon/2$, which is exactly the square-root tolerance corresponding to
323 $\varepsilon^2/4$.
324 
325 \begin{theorem}[Successful and complete cached gain construction]
326 For rational factor-coded model data with $\sigma>0$, valid complete rational
327 output and input packets, a seed and complete output scan, any positive rational
328 $\varepsilon$, any finite precision probe list, and any rational initial gain,
329 \path{solveCached} returns a candidate and verification precision. The candidate
330 and tolerance checks pass, and its gain is an actual greedy iterate at an index
331 within the computed fuel. Its Joseph Gaussian has Wasserstein distance at most
332 $\varepsilon$ from the explicit posterior version established by the Bayesian
333 semantics.
334 \end{theorem}
335 
336 The source assembles these conclusions through \path{solveCached_terminates},
337 \path{cached_solver_gain_origin}, and
338 \path{cached_solver_reaches_posterior_tolerance}. The semantic posterior used here
339 is the proved explicit Gaussian kernel version. Its agreement with Bayesian
340 conditioning is established through disintegration and almost-everywhere agreement
341 with canonical conditional versions, as discussed in the foundations. The theorem
342 at the supplied rational observation does not assert uniqueness of every possible
343 pointwise conditional version at an event of probability zero.
344 
345 The independent statement \path{solveCached_sound} is logically different from
346 termination. It says that any successful program return satisfies both Boolean
347 checks without requiring the caller to supply setup-validity proofs. A returned
348 candidate has passed the evaluator's checks. Valid input hypotheses are needed
349 to guarantee that a return exists; they are not external assumptions attached to
350 the meaning of an already successful return.
351 
352 \section{Parameter arrays and the meaning of a complete result}
353 \label{sec:solver-output}
354 
355 A useful posterior output contains more than a passing gain. For the returned
356 rational gain $B$, the parameter stage represents
357 \begin{align}
358  \mu_B&=m+B(y-Hm),\nonumber\\
359  V_B&=(I-BH)P(I-BH)^{\mathsf T}+BRB^{\mathsf T}.
360  \label{eq:solver-joseph-output}
361 \end{align}
362 These are the mean and Joseph covariance of the same Gaussian law certified by
363 the Wasserstein statement. The covariance is positive semidefinite under the model
364 hypotheses even when the prior is singular. The declaration
365 \path{approximation_eq_output_gaussian} identifies this parameterized Gaussian
366 with the approximation law used in the posterior theorem.
367 
368 The evaluator returns a ball for each mean coordinate and each covariance entry.
369 For exact rational entry $x$, a ball $(c,r)$ means $|x-c|\le r$. Its radius is an
370 arithmetic enclosure error for that parameter of the returned approximation.
371 The output tolerance $\delta>0$ bounds every such radius. It is independent of
372 the posterior Wasserstein tolerance $\varepsilon$.
373 
374 Each output arithmetic expression has a precision-independent budget coefficient.
375 The source sums all mean coefficients and all covariance coefficients to obtain
376 $C_{\mathrm{out}}$, defined by \path{outputCoefficient}. Every individual coefficient is
377 nonnegative and no greater than this sum. It chooses
378 \[
379  p_{\mathrm{out}}=\operatorname{precisionFor}(C_{\mathrm{out}},\delta)
380 \]
381 and evaluates the output graph at that precision. Since every entry radius is
382 bounded by its coefficient times $2^{-p_{\mathrm{out}}}$, the same integer
383 precision bounds all radii by $\delta$. The declarations \path{mean_coeff_le},
384 \path{covariance_coeff_le}, and \path{evaluate_radii_le} establish this argument.
385 \path{represent_spec} joins entrywise enclosure and the requested radius bound.
386 
387 The result record stores verification precision, the checked candidate, parameter
388 precision, and the evaluated arrays. Its contract \path{ResultValid} contains
389 seven clauses: the candidate check passes, the tolerance check passes, the
390 Wasserstein bound holds, the arrays enclose the returned approximation's parameters,
391 all radii are at most $\delta$, the reported parameter precision equals the actual
392 precision selector, and the arrays equal the actual evaluator at that precision.
393 The final two clauses make the reported representation part of the contract,
394 rather than allowing arbitrary arrays that happen to satisfy a looser description.
395 
396 \begin{theorem}[Complete first-release output]
397 Under the valid-input hypotheses above and $\delta>0$,
398 \path{Komorebi.CachedPosterior.runCached} returns a result satisfying
399 \path{ResultValid}. Every successful return is sound even without setup-validity
400 proofs supplied by the caller. A nonpositive output-radius tolerance is rejected.
401 \end{theorem}
402 
403 These are precisely \path{runCached_terminates}, \path{runCached_sound}, and
404 \path{runCached_rejects_nonpositive_output_tolerance}. The complete contract is
405 finite-dimensional inference for one observation update. It includes singular
406 priors, rectangular observation operators, gain origin, computable iteration fuel,
407 verification precision, and parameter precision.
408 
409 Two interpretations must remain separate. The intervals enclose the parameters
410 of the certified Joseph Gaussian. They do not certify another Gaussian obtained
411 by treating interval centers as exact mean and covariance. In particular, rounded
412 covariance centers are not independently proved positive semidefinite. Likewise,
413 $\delta$ is not a coordinate error bound against the exact posterior. The
414 Wasserstein guarantee compares laws; the interval guarantee encloses the parameters
415 of one of those laws. A theorem combining either guarantee with a new operation
416 must account for that operation explicitly.
417 
418 The program is mathematically finite for every positive rational pair
419 $(\varepsilon,\delta)$ under its declared assumptions. A reference implementation
420 can still encounter a time, memory, or user-supplied resource cap. The Python tools
421 report \path{RESOURCE_LIMIT} when their caps are reached. Such a cap is a limit of
422 the execution environment, not a counterexample to the finite-success theorem.
423 The result contract also contains no sampler and no guarantee for an external
424 floating-point implementation.
425 
426 \section{A complete coordinate execution}
427 \label{sec:solver-coordinate}
428 
429 The coordinate fixture has a two-dimensional state and one-dimensional
430 observation:
431 \[
432  P=\begin{pmatrix}4&0\\0&1\end{pmatrix},\quad H=\begin{pmatrix}1&1\end{pmatrix},
433  \quad R=1,\quad m=\begin{pmatrix}0\\0\end{pmatrix},\quad y=1.
434 \]
435 It is represented by $L=\operatorname{diag}(2,1)$, $N=0$, and $\sigma=1$.
436 The two output projectors select the coordinate axes, and the single input
437 projector is $1$. Start with $B_0=0$, seed $0$, scan $[0,1]$, probes $[4,12]$,
438 $\varepsilon=1/20$, and $\delta=1/1000$.
439 
440 Here $S=6$, $\tau=1/7$, $T=1/7$, and $w=2$. The initial residual is $(4,1)^{\mathsf T}$,
441 with packet energies $16$ and $1$. Updating one coordinate multiplies its residual
442 by $1/7$ and its energy by $1/49$. The other coordinate remains exactly unchanged.
443 The maximum-energy schedule therefore alternates between labels $0$ and $1$.
444 The complete pre-update trace is
445 \begin{center}
446 \begin{tabular}{rrrrr}
447 \toprule
448 Updates already made & Selected label & $e_0$ & $e_1$ & $t$\\
449 \midrule
450 0 & 0 & $16$ & $1$ & $17$\\
451 1 & 1 & $16/49$ & $1$ & $65/49$\\
452 2 & 0 & $16/49$ & $1/49$ & $17/49$\\
453 3 & 1 & $16/2401$ & $1/49$ & $65/2401$\\
454 4 & 0 & $16/2401$ & $1/2401$ & $17/2401$\\
455 5 & 1 & $16/117649$ & $1/2401$ & $65/117649$\\
456 \bottomrule
457 \end{tabular}
458 \end{center}
459 
460 After six updates, each coordinate has been selected three times. The geometric
461 sum in its gain gives
462 \[
463  B_6=\begin{pmatrix}228/343\\57/343\end{pmatrix},\qquad
464  F(B_6)=\begin{pmatrix}4/343\\1/343\end{pmatrix},\qquad
465  a(B_6)=\frac{34}{117649}.
466 \]
467 The strict search threshold is $\varepsilon^2/4=1/1600$. At the previous state,
468 $a(B_5)=130/117649>1/1600$, while $a(B_6)<1/1600$. Thus six is the actual update
469 count for this stopping rule. The formal fuel is $410093$; the program uses only
470 six of these allowed updates. This large difference illustrates the conservative
471 fuel construction, not an ambiguity in the observed trace.
472 
473 At verification precision $4$, the rounded score is $25/16$ and the attempt fails.
474 At precision $12$, it is $481/1048576$, which is below the required final threshold
475 $\varepsilon^2=1/400$. The solver therefore returns verification precision $12$.
476 A failed coarse enclosure is a failed certificate attempt, not evidence that the
477 gain itself is inaccurate. Sufficiently high precision bounds the enclosure inflation.
478 
479 The exact posterior mean is $(2/3,1/6)^{\mathsf T}$, while the returned Joseph mean
480 is the gain $B_6$ because $m=0$ and $y=1$. Parameter output uses precision $32$.
481 Its mean centers are
482 \[
483  \begin{pmatrix}2854963683/4294967296\\89217615/536870912\end{pmatrix}
484 \]
485 with radius $1/4294967296$ in each coordinate. The covariance centers are
486 \[
487  \begin{pmatrix}
488  5726720411/4294967296 & -1431643597/2147483648\\
489  -1431643597/2147483648 & 3579145495/4294967296
490  \end{pmatrix},
491 \]
492 and the corresponding radii are
493 \[
494  \begin{pmatrix}
495  1/536870912&7/4294967296\\
496  7/4294967296&1/536870912
497  \end{pmatrix}.
498 \]
499 Every radius is smaller than $1/1000$. These fractions describe output arithmetic,
500 not uncertainty intervals for model estimation. They enclose exactly the Joseph
501 mean and covariance at $B_6$.
502 
503 The exact rational matrix enclosed by those covariance balls is
504 \[
505  V_{B_6}=\frac{1}{117649}
506  \begin{pmatrix}156868&-78432\\-78432&98041\end{pmatrix}.
507 \]
508 It can be checked directly by substituting $B_6$ into
509 \eqref{eq:solver-joseph-output}. Another useful check starts from the exact
510 posterior covariance
511 $V_* = \left(\begin{smallmatrix}4/3&-2/3\\-2/3&5/6\end{smallmatrix}\right)$.
512 If $B_*=(2/3,1/6)^{\mathsf T}$ is the exact gain, expansion of the Joseph
513 expression gives
514 \[
515  V_{B_6}=V_*+6(B_6-B_*)(B_6-B_*)^{\mathsf T}.
516 \]
517 The gain discrepancy is
518 $B_*-B_6=(2/1029,1/2058)^{\mathsf T}$, which produces the displayed matrix.
519 This second calculation checks the sign of the off-diagonal entries and explains
520 why the approximate covariance has an additional positive semidefinite term.
521 The posterior accuracy certificate concerns the complete mean-covariance law,
522 while the dyadic output stage faithfully represents these rational parameters.
523 The larger output budget can still choose many more bits than the smallest
524 possible entrywise enclosure would require. Its purpose is a guaranteed common
525 precision, not an optimal encoding of this particular covariance.
526 
527 The module \path{GeneratedCachedCoordinate.lean} defines this actual model,
528 initial cache, six-step cache trajectory, final gain, certificate, and result.
529 Its declarations check the computed fuel, final gain, exact and rounded scores,
530 each of the six chosen labels, solver return, parameter precision, every displayed
531 center and radius, and the full output return. Its theorem \path{output_valid}
532 applies \path{runCached_sound} to the proved return. This is a checked finite
533 program example, while the universal termination theorem covers all valid inputs
534 in the declared class.
535 
536 An earlier recomputed selective solver verified after each update and could stop
537 at five updates with a passing rounded certificate. That is a different stopping
538 policy. The canonical cached solver first waits for the stricter exact-score
539 margin and then performs final verification. A recomputed baseline using this
540 same strict margin returns the same six-step gain. Comparisons between cached and
541 recomputed execution must align their stopping policy before comparing work.
542 
543 \section{A singular rotated execution}
544 \label{sec:solver-rotated}
545 
546 The rotated fixture makes the prior singular and the packets non-coordinate:
547 \[
548  P=J=\begin{pmatrix}1&1\\1&1\end{pmatrix},\quad H=I,
549  \quad R=I,\quad m=0,\quad y=\begin{pmatrix}1\\-1\end{pmatrix}.
550 \]
551 It uses the rectangular prior factor $L=(1,1)^{\mathsf T}$, zero noise factor,
552 and $\sigma=1$. Both output and input packet families are
553 \[
554  Q_+=\frac12\begin{pmatrix}1&1\\1&1\end{pmatrix},\qquad
555  Q_-=\frac12\begin{pmatrix}1&-1\\-1&1\end{pmatrix}.
556 \]
557 These project onto the common and antisymmetric directions. They are rational,
558 self-adjoint, orthogonal, and complete. The prior has rank one, but the innovation
559 matrix $S=I+J$ is positive definite because of the positive noise floor.
560 
561 Take $B_0=0$, seed $0$, scan $[0,1]$, probes $[4,12]$, $\varepsilon=1/4$, and
562 $\delta=1/1000$. Here $\tr S=4$, $\tau=1/5$, and
563 $T=I-(I+J)/5$. The initial residual is $J$, entirely in the $Q_+$ output packet.
564 Since $JS=3J$, each selected update multiplies this residual by $2/5$. The
565 $Q_-$ residual remains zero. Thus every selected label is $0$ and
566 \[
567  (e_+,e_-)=(4(4/25)^n,0),\qquad B_n=\frac{1-(2/5)^n}{3}J.
568 \]
569 The first four pre-update energy pairs are $(4,0)$, $(16/25,0)$,
570 $(64/625,0)$, and $(256/15625,0)$.
571 
572 After four updates,
573 \[
574  B_4=\frac{203}{625}J,\qquad F(B_4)=\frac{16}{625}J,
575  \qquad a(B_4)=\frac{3072}{390625}.
576 \]
577 The score weight is $w=3$, because $\lVert y\rVert^2=2$. The strict margin is
578 $\varepsilon^2/4=1/64$. At the previous state the score is $768/15625>1/64$;
579 after the fourth it is below $1/64$. The computed fuel is $4267$. Precision $4$
580 produces score $435/64$ and fails; precision $12$ produces $9111/1048576$ and
581 passes the final threshold $1/16$.
582 
583 The exact posterior mean is zero because $Jy=0$, and the returned approximation's
584 mean is also zero. Its Joseph covariance is
585 \[
586  V_{B_4}=\frac{130379}{390625}J.
587 \]
588 The exact posterior covariance is $J/3$. Both laws remain supported in the prior's
589 one-dimensional common-direction subspace. This example therefore combines a
590 singular prior, rotated packet selection, a nontrivial covariance approximation,
591 and a zero mean without using an inverse of the singular prior covariance.
592 
593 At output precision $32$, each mean center is zero with radius $1/2147483648$.
594 Every covariance entry has center $179191533/536870912$ and radius
595 $7/4294967296$. All output radii satisfy $\delta=1/1000$. The equality of these
596 centers reflects the exact common-direction structure of the returned Joseph
597 covariance. It does not turn the rounded center matrix into the object of the
598 posterior theorem.
599 
600 \path{GeneratedCachedRotated.lean} checks the same kinds of finite obligations as
601 the coordinate module: fuel, chosen labels, gain, scores, actual return, parameter
602 precision, arrays, and \path{ResultValid}. The example is particularly useful for
603 testing whether a presentation has accidentally assumed an invertible prior or
604 coordinate-only packets. Neither assumption belongs to the solver contract.
605 
606 \section{The rounded-cache counterexample and the separate rounded solver}
607 \label{sec:solver-rounding-boundary}
608 
609 Exact cache validity cannot be reused unchanged after independently rounding its
610 components. The release contains a scalar counterexample with
611 $P=H=R=1$, $\sigma=1$, $m=0$, $y=1$, and $B_0=0$. Then $S=2$, $\tau=1/3$,
612 $w=2$, and the first exact update is
613 \[
614  B_1=1/3,\qquad F(B_1)=1/3.
615 \]
616 The naive route separately rounds the gain center and residual center downward
617 to zero fractional bits. Both become zero. It then computes the stored energy
618 from the rounded residual, obtaining a stored score of zero.
619 
620 The actual residual at its stored gain is instead
621 \[
622  F(0)=1,
623  \qquad a(0)=2.
624 \]
625 Thus the state claims exact internal convergence while its true residual is
626 nonzero. The equality $G=QF(B)$ has been destroyed by rounding independently
627 related quantities. The source module \path{CachedRoundingBoundary.lean} proves
628 \path{naive_score_zero}, \path{true_score_two}, and \path{naive_cache_invalid}.
629 For $\varepsilon=1/10$ and probe $[12]$, it also proves
630 \path{naive_final_verification_rejected}: \path{certifyGain} returns no candidate.
631 
632 This result identifies both a failure and a protection. The naive rounded cache
633 cannot support the exact-cache termination proof. The independent final verifier
634 still rejects its false stopping signal, preserving the meaning of successful
635 returns. The example does not rule out a rounded selective cache with propagated
636 error bounds. Such a construction needs an enclosure relation, an error budget
637 for each selected update, and a selection argument that tolerates uncertain
638 energies. Those obligations are a separate extension.
639 
640 Core 1.0.0 already retains a different, completed rounded solver. Its update is a
641 genuinely rounded full-gain Richardson step. It neither claims exact selective
642 cache invariants nor selects a largest cached packet. Its declarations expose
643 the whole-update defect instead. If $\widetilde B_{n+1}$ is the rounded update
644 and $B_{n+1}^{\mathrm{ideal}}$ is the exact full step at the current gain, then
645 \[
646  F(\widetilde B_{n+1})=F(\widetilde B_n)T
647  -(\widetilde B_{n+1}-B_{n+1}^{\mathrm{ideal}})S.
648 \]
649 This is \path{rounded_residual_step}. The defect is explicitly included in the
650 tracking and termination argument.
651 
652 Writing $d$ for the number of gain entries and $h_t=2^{-t}$, the source establishes
653 an all-iteration tracking bound
654 \[
655  E(\widetilde B_n-B_n^{\mathrm{exact}})
656  \le\frac{6d h_t^2}{(1-q)^2}.
657 \]
658 Its residual-score comparison has the form
659 \[
660  a(\widetilde B_n)\le2a(B_n^{\mathrm{exact}})+C_{\mathrm{round}}h_t^2,
661  \qquad
662  C_{\mathrm{round}}=
663  \frac{12dE(S)w}{(1-q)^2}.
664 \]
665 The source names are \path{roundedGain_tracking}, \path{roundoffScoreCoeff}, and
666 \path{rounded_score_compare}. The first term is ideal progress. The second is a
667 precision-dependent floor. Both are needed.
668 
669 The chosen update precision \path{updateAccuracy} places the floor below
670 $\varepsilon^2/8$. The rounded fuel \path{roundedFuel} drives the exact full-step
671 score below $(\varepsilon/4)^2=\varepsilon^2/16$. The factor of two in the
672 comparison therefore gives another $\varepsilon^2/8$, so the actual rounded
673 iterate reaches score at most $\varepsilon^2/4$. The same independent final
674 precision fallback can certify it. \path{solveRounded_terminates} proves finite
675 successful return, and \path{rounded_solver_gain_origin} identifies the result
676 as an actual rounded iterate within its declared fuel.
677 
678 There are consequently two completed branches: exact selective updates with an
679 exact cache, and genuinely rounded full-gain updates with an explicit perturbation
680 bound. A rounded selective cache combining their advantages remains an extension.
681 No proof for one branch is presented as a theorem about the other.
682 
683 \section{Measured work, execution boundaries, and extensions}
684 \label{sec:solver-performance}
685 
686 The cached representation reduces the work needed to maintain packet residuals
687 relative to recomputing every packet at every selected update. It stores the
688 projected residual matrices and energies, retains unselected objects, and updates
689 the total by one scalar difference. Selection still scans the stored energies.
690 The amount of storage depends on the number and shape of the represented packet
691 matrices. Rational numerator and denominator growth also matters in execution.
692 The algebraic locality theorem alone is not a formal bit-complexity estimate.
693 
694 The archived bounded benchmark compares cached selective, recomputed selective,
695 and full Richardson reference implementations on seven cases of dimensions at
696 most eight. All use exact fraction arithmetic, the same zero-skipping matrix
697 backend, the same strict exact-score stopping margin, and common requested
698 posterior and output tolerances. All include setup, final rounded certification,
699 and parameter output. The recomputed and cached selective branches return
700 identical candidates. The full baseline maintains a full residual by recurrence
701 and avoids unnecessary packet scans.
702 
703 One warmup precedes five repetitions with rotating method order. Archived median
704 producer times and selective-iteration ratios are
705 \begin{center}
706 \begin{tabular}{lrrrr}
707 \toprule
708 Case & Cached ms & Recomputed ms & Full ms & Iteration ratio\\
709 \midrule
710 coordinate & 2.38 & 2.46 & 2.33 & $1.94$\\
711 rotated & 4.38 & 4.45 & 4.28 & $2.16$\\
712 sparse4 & 13.84 & 14.52 & 13.79 & $2.51$\\
713 dense4 & 16.34 & 17.96 & 16.34 & $3.11$\\
714 sparse8 & 171.98 & 174.30 & 169.87 & $4.62$\\
715 dense8 & 200.69 & 235.15 & 195.44 & $5.61$\\
716 conditioned4 & 19.16 & 21.36 & 17.46 & $3.08$\\
717 \bottomrule
718 \end{tabular}
719 \end{center}
720 The final column is recomputed-selective iteration time divided by cached
721 iteration time. It excludes setup, verification, and output. The producer columns
722 include these stages and exclude export and Lean checking. These are archived
723 reference measurements, rather than fresh timing measurements from this
724 publication session.
725 
726 The cache improves selective iteration in these cases, yet these measurements
727 establish no overall advantage over the efficient full baseline. Several cases
728 require substantially more selective updates than full updates. The dense8 case,
729 for example, takes $67$ cached selective updates and $9$ full updates. Final
730 certification and output account for a large part of total production cost. The
731 bounded result supports a narrower conclusion: preserving a packet cache avoids
732 unnecessary selective recomputation, while end-to-end performance depends on more
733 than the selective update loop.
734 
735 Every method-case pair also exported an explicit final candidate certificate,
736 for $21$ checked benchmark outputs. Their archived Lean checks certify those
737 explicit rational gains and posterior tolerances. They do not certify the Python
738 timing trace, counters, or numeric parameter arrays from the benchmark runs. The
739 two generated coordinate and rotated modules have the stronger finite-program and
740 output-array checks described above. A universal theorem about the mathematical
741 output evaluator is also distinct from a universal refinement theorem for a
742 Python implementation of that evaluator.
743 
744 The archived per-instance Lean checking measurements range from seconds to tens
745 of seconds and dominate millisecond producer times. Each includes a fresh pinned
746 Lean process, import, elaboration, and kernel checking with common dependencies
747 already compiled. The dependency build is accounted for separately. One checking
748 time per export cannot reliably rank small differences. The source reports preserve
749 these distinctions, rather than combining an iteration ratio with an unrelated
750 claim of total acceleration.
751 
752 The producer/exporter boundary is similarly precise. Python parses user data,
753 executes a reference algorithm, and emits a Lean instance containing explicit
754 rational data. Successful checking establishes the statement about that emitted
755 instance. A universal theorem identifying arbitrary parser input with the emitted
756 model is outside this release. The output record is a mathematical representation
757 with checked arithmetic semantics, rather than a claim about every external file
758 format or hardware arithmetic instruction.
759 
760 The most direct extensions now have concrete obligations. A rounded selective
761 cache must propagate residual and energy enclosures and prove progress under its
762 actual selection rule. Approximate maximum selection needs a quantitative energy
763 share bound. A changing packet hierarchy must preserve global accounting across
764 refinement and coarsening. Uncertain model inputs need their own error budget in
765 both the certificate and the posterior semantics. Sequential filtering must
766 account for repeated updates and transport of earlier approximation error.
767 Large-scale performance work must measure preprocessing, final certification,
768 output representation, rational bit growth, memory, and checking cost as well as
769 iteration kernels.
770 
771 These extensions do not leave the first-release theorem unfinished. The closed
772 contract remains exact rational, finite-dimensional, single-update Gaussian
773 inference with complete fixed packets, positive tolerances, a terminating gain
774 construction, independent dyadic verification, and enclosed parameters of the
775 certified Joseph law. The rounded-cache counterexample and bounded performance
776 result make the limits of that contract inspectable and give specific targets for
777 the next stage of development.

Back to source controls

Back to Certified Bayesian Inference