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 \begin{abstract}
2 We present a certified finite-dimensional Gaussian inference construction that connects an executable packet solver to a posterior measure and to an explicit arithmetic output contract. Model data are exact rational factors. The prior covariance may be singular, and the observation operator may be rectangular. A positive noise floor makes the innovation covariance invertible. The canonical solver maintains an exact cache of orthogonal output-packet residuals, selects a largest-energy packet, and updates only that packet. Its trajectory agrees with the recomputed greedy trajectory. A geometric residual bound supplies computable finite fuel. After an exact stopping test establishes a strict verification margin, an outward-rounded dyadic verifier certifies a Wasserstein tolerance. The final result also contains enclosing mean and covariance intervals for the Joseph Gaussian at the returned gain, with prescribed maximum radii. We give the underlying algebra, proof composition, worked executions, arithmetic distinctions, and verification boundaries. A checked scalar counterexample shows that independently rounding the gain and cached residual centers does not preserve the exact-cache invariant. The integrated result is complete for one observation update under its declared hypotheses. Sequential filtering, a rounded selective cache, executable sampling, and a universally refined host implementation are separate extensions.
3 \end{abstract}
4 
5 \section*{Reading contract}
6 This traditional paper develops the mathematics and the exact program contract. The extended visual guide follows two concrete models through the same chain, with twenty figures generated by Python from exact data or explicit mathematical relationships. The Lean companion gives actual source excerpts, hypotheses, dependency maps, archived evidence, and pinned reproduction instructions. Editable LaTeX, figure programs, exact example outputs, audit reports, and the intact formal release accompany all three documents.
7 
8 The formal baseline is \path{FD_Certified_Inference_Core_v1.0.0_Checked.zip}. Its archived build belongs to 12 September 2026. This publication edition separates that evidence from the fresh source and Python checks performed while preparing the papers. The compiler and pinned dependency runtime were not available for a fresh Lean build here. No finite test, source inventory, or rendered page is described as a new kernel check.
9 
10 \clearpage\tableofcontents\clearpage
11 \section{The result and its role}
12 An approximate inference program needs a conclusion about the object it returns. A small internal residual, a visually plausible covariance, and a successful numerical routine address different obligations. In this construction, a single result joins them through exact statements. The gain returned by the permitted iteration defines a Gaussian approximation. A certificate controls its distance from a proved posterior version. Parameter intervals enclose the mean and covariance of that same approximation. The result ties its reported arrays to the actual outward-rounded evaluator.
13 
14 The problem is one Gaussian observation update. Write the prior as
15 \[
16 X\sim\mathcal N(m,P),\qquad Y=HX+\eta,
17 \]
18 where the centered Gaussian noise $\eta$ is independent of $X$. The representation uses rational factors
19 \[
20 P=LL^{\mathsf T},\qquad R=NN^{\mathsf T}+\sigma I,
21 \qquad \sigma>0.
22 \]
23 All data supplied to the executable construction, including $m,H,L,N,\sigma$ and the observation $y$, are rational. Finite state and observation index types determine the matrix shapes. There is no requirement that $H$ be square or that $P$ be invertible. The innovation matrix is
24 \[
25 S=HPH^{\mathsf T}+R.
26 \]
27 Its positive noise floor supports the inverse used in the exact posterior semantics. The executable iterative solver avoids computing that inverse to construct its returned gain.
28 
29 For a rational gain $B$, the Joseph approximation has mean and covariance
30 \begin{align*}
31 m_B&=m+B(y-Hm),\\
32 P_B&=(I-BH)P(I-BH)^{\mathsf T}+BRB^{\mathsf T}.
33 \end{align*}
34 Its covariance is positive semidefinite by construction. The approximation is a measure, rather than a collection of unqualified decimal entries. The exact gain $K=PH^{\mathsf T}S^{-1}$ identifies the familiar Gaussian posterior parameters. Later sections prove that this explicit Gaussian kernel disintegrates the actual forward joint law. This gives a posterior version defined at every supplied observation. Agreement with Mathlib's canonical conditional kernel is an evidence-almost-everywhere statement, as is appropriate for conditional distributions.
35 
36 \begin{theorem}[Publication contract of the canonical solver]\label{thm:publication-contract}
37 Fix a finite-dimensional rational factor-coded model with $\sigma>0$, and complete, mutually orthogonal self-adjoint rational output and input packet families. Supply an output-packet seed and a finite scan containing every output label. Let $\epsilon,\delta>0$ be rational. An arbitrary rational initial gain and an arbitrary finite list of requested precision probes are permitted.
38 
39 The canonical program \path{Komorebi.CachedPosterior.runCached} returns a result $r$. If $B$ is its candidate gain and $\Pi_y$ is the explicitly proved Gaussian posterior version, then
40 \[
41 \Wtwo(\Pi_y,\mathcal N(m_B,P_B))\leq\epsilon.
42 \]
43 The candidate and tolerance predicates hold. The reported mean and covariance intervals enclose $m_B$ and $P_B$, respectively, and every reported radius is at most $\delta$. Its parameter precision is the program's computed output precision, and its arrays equal the declared evaluator at that precision.
44 
45 Any successful return of the same program is sound without caller-supplied validity proofs: its internal admission and verification steps imply the same result predicate. The positive-input hypotheses above establish guaranteed successful termination.
46 \end{theorem}
47 \begin{proof}[Proof composition]
48 The source declaration \path{Komorebi.CachedPosterior.runCached_terminates} obtains a successful certified gain from \path{cached_solver_reaches_posterior_tolerance}. That theorem combines initialization, cache preservation, greedy-trajectory equivalence, finite fuel, and a sufficient fallback verification precision. The Gaussian semantic bridge converts its residual certificate into the Wasserstein conclusion. The output theorem \path{represent_spec} provides parameter enclosure and the radius bound at positive $\delta$. The definition of the result record supplies both reported-evaluator equalities. The separate source declaration \path{runCached_sound} derives these properties from an actual successful return. The mathematical steps are developed in the following chapters and traced to their exact declarations in the companion.
49 \end{proof}
50 
51 The two tolerances have different purposes. The parameter tolerance $\delta$ is an enclosure radius for the parameters of the returned approximation. It is not an entrywise error against the exact posterior covariance. The law tolerance $\epsilon$ compares the whole approximation with the posterior in $W_2$. Neither conclusion certifies a Gaussian formed by discarding every interval radius and using its centers as exact parameters. Such a replacement would need a separate perturbation argument, including a positive-semidefinite covariance obligation.
52 
53 \fig{01_contract_chain.pdf}{The complete contract links an exact rational model, a permitted cached iterate, rounded verification, a posterior-measure guarantee, and enclosing parameter arrays. The two output tolerances belong to different conclusions.}{fig:main-contract}
54 
55 \subsection{Why the packet representation matters}
56 The residual is $F(B)=PH^{\mathsf T}-BS$. Orthogonal output projectors $Q_a$ split it into components $G_a=Q_aF(B)$. Completeness makes the sum of their squared Frobenius energies equal the energy of the full residual. Selecting a largest-energy component therefore chooses a block containing a definite fraction of the remaining error.
57 
58 The exact cache retains these components, their energies, and their total. For a selected label $a$, the update changes $B$ by $\tau G_a$, changes $G_a$ by right multiplication with $I-\tau S$, and leaves every other cached component unchanged. The proof of that last statement uses orthogonality of the output projectors. It is an algebraic locality result. Keeping unrelated cache entries untouched is justified by their semantic invariant.
59 
60 The fixed packet family is part of the model of execution. It can represent coordinate blocks or rotated subspaces. The theorem is not restricted to a preferred coordinate basis. Changing the family during the run, however, changes the state invariant and is outside this solver's proved trajectory theorem. The singular rotated worked example demonstrates a non-coordinate packet family without making a claim about changing hierarchies.
61 
62 \subsection{Arithmetic is part of the statement}
63 The cached branch uses exact rational gain updates and exact rational cache scores. It does not independently round the selected gain and cached residual during iteration. Final certificate evaluation and parameter representation use outward-rounded dyadic operations. Those rounded operations have explicit enclosure and inflation bounds. A separately preserved solver uses rounded full-gain updates and has its own convergence theorem. These are distinct verified branches.
64 
65 The naive rounded-cache counterexample explains the distinction. In a scalar model, exact gain and residual both equal $1/3$ after one step. Rounding both centers independently to zero fractional bits makes both stored values zero. The stored residual score then says zero, although the true residual at the stored gain has score two. The independent final interval verifier rejects that candidate. Sound final verification survives, but the invalid cache cannot supply the exact-cache progress proof.
66 
67 \subsection{Relation to established methods}
68 Maximum-energy packet selection has a direct optimization interpretation. For the quadratic objective
69 \[
70 \phi(B)=\tfrac12\tr(BSB^{\mathsf T})-\langle B,PH^{\mathsf T}\rangle_{\mathrm F},
71 \]
72 the gradient is $BS-PH^{\mathsf T}=-F(B)$. The selected packet has largest projected-gradient norm. This is a block Gauss--Southwell mechanism, and the residual cache is maintained by exact linear identities. Greedy coordinate and block selection are established methods \cite{nutini2015,nutini2022}. Pathwise Gaussian conditioning and Wasserstein approximation analysis also have substantial prior literature \cite{wilson2021}. Formally checked interval reasoning for rounded arithmetic is an established methodology \cite{daumas2007}.
73 
74 The contribution presented here is the integrated formal construction: a specified executable trajectory, maintained semantic cache, computable fuel, sufficient verification precision, posterior guarantee, and interval output tied to the actual returned record. The paper proves this construction under its declared hypotheses. It makes no global priority claim or competitive-performance claim from the small archived benchmark.
75 
76 \subsection{Evidence and reproduction}
77 The archived release records successful compilation of 117 active modules and axiom reports for 543 named theorem or lemma declarations. Its allowlist is \path{propext}, \path{Classical.choice}, and \path{Quot.sound}. Those counts include support lemmas and benchmark certificates. They count different forms of evidence rather than independent mathematical discoveries.
78 
79 The original source release contains successful receipts, source snapshots, logs, dependency records, exact diagnostic outputs, and preserved failures. It excludes the portable compiler and compiled dependency runtime. Fresh publication checks can verify retained source and log hashes and reproduce exact Python examples. Archived compiled-output hashes remain recorded values when the corresponding binaries are absent. The Lean companion states precisely which evidence was replayed here and which remains archived.
80 
81 The reference Python producer accepts exact rational strings and rejects raw JSON floating-point numbers. Its successful status is provisional until the emitted explicit Lean instance is compiled. A checked instance certifies the rational data present in that source. It does not prove a universal JSON-parser or Python-exporter refinement. The resource-capped producer may fail with a resource limit even when the ideal mathematical solver has finite fuel. These distinctions make the delivered object reproducible and its authority inspectable.

Back to source controls

Back to Certified Bayesian Inference