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{Assurance, reproducibility, and the completed scope}\label{sec:assurance}
2 The result has a mathematical input boundary, a formal program boundary, and an implementation boundary. These boundaries can be read directly from the declared functions and predicates. Rational factor-coded data determine the Gaussian model. Complete rational packet families determine the permitted decomposition. A successful formal program return determines the candidate gain and parameter arrays. The Python producer and a physical execution environment require additional correspondence evidence.
3 
4 \begin{longtable}{p{.23\linewidth}p{.40\linewidth}p{.27\linewidth}}
5 \toprule
6 Object & Established conclusion & Evidence role\\
7 \midrule
8 \endfirsthead
9 \toprule
10 Object & Established conclusion & Evidence role\\
11 \midrule
12 \endhead
13 Factor-coded model & Prior covariance PSD, innovation invertible at positive noise floor & Internal algebra and Gaussian semantics\\
14 Posterior kernel & Explicit Gaussian version disintegrates the forward law; canonical agreement evidence-a.e. & Internal measure-level proof\\
15 Joseph gain & A valid Gaussian approximation and residual-based $W_2$ bound & Common-noise coupling and matrix bounds\\
16 Exact packet cache & Correct residuals and energies at every iterate; same gains as recomputation & Initialization and preservation induction\\
17 Computed search fuel & Successful search under the positive-input hypotheses & Geometric contraction and computable sufficient fuel\\
18 Rounded verifier & Candidate validity and posterior tolerance follow from successful checking & Outward enclosure and inflation proofs\\
19 Parameter arrays & Enclose this approximation's parameters, with radii at most $\delta$ & Declared evaluator and precision theorem\\
20 Python instance & Exact emitted rational data can receive a Lean certificate & Compilation needed for that instance\\
21 Fresh publication runs & Specified examples and diagnostic assertions reproduced & Bounded executable evidence\\
22 Archived Lean release & 117 successful module receipts, 543 axiom-audited declarations & Preserved historical kernel evidence\\
23 \bottomrule
24 \end{longtable}
25 
26 \subsection{What was rechecked for this publication}
27 The standalone Core 1.0.0 archive was recovered and its SHA-256 compared with its separately delivered checksum. The source release and its history were retained intact. The fresh inventory checks the archived manifest, current source bytes, retained source snapshots, logs, dependency-source records, declaration locations, and axiom-report coverage. An independent parser finds the same 543 theorem and lemma declarations. Verbatim excerpts in the Lean companion are matched back to their actual source intervals.
28 
29 Fresh exact computations reproduce the coordinate and rotated returns, including their gains, score values and every output interval. Independent rational matrix calculations reconstruct the exact posterior and the Joseph covariance. They check the coupling cost, residual bound, cache identities, stopping thresholds, and the rounded-cache obstruction. The computation record states its finite domain and distinguishes producer checks from formal program theorems. The source archive remains byte-for-byte unchanged.
30 
31 The figures use exact input data and explicit formulas. Floating evaluation is used to draw curves and contours, with that visual role identified in their captions. No sampled scatter cloud is used as a proof of a Gaussian identity. Archived benchmark timings are marked as archived. Fresh timings of publication checks are not substituted into the original performance table.
32 
33 All three documents are compiled and rendered for page review. The audit records track any mathematical transcription corrections and the inspected page coverage. Build warnings and PDF structure checks address layout, references, links and glyphs. These checks verify the publications as artifacts; they do not extend the solver's formal scope.
34 
35 The original release records a clean rebuild after removing active project caches while reusing pinned Mathlib caches. It preserves successful source and log receipts, corrected failures, and recorded compiled-output hashes. Compiled output payloads and the portable runtime are not included in the source archive. A fresh source audit therefore cannot recompute absent compiled-output hashes. Fresh Lean compilation was unavailable for this publication edition. The companion provides the exact pinned reproduction route and keeps this limitation explicit.
36 
37 \subsection{Interpreting cost evidence}
38 The controlled benchmark contains seven models with dimensions at most eight, using five measured repetitions after warmup. Cached and recomputed selective runs use matching tolerances, backend and stopping conditions and return identical gains. Their iterative work differs because the cache updates only the selected packet. Precomputation, final interval verification, parameter representation, export and proof checking remain parts of a full execution.
39 
40 The archived measurements support a reduction in selective iteration cost. They do not establish overall superiority to the efficient full Richardson baseline. Operation counters describe the tested implementation's scalar arithmetic and comparisons. They do not constitute a formal bit-complexity theorem or a prediction for large matrices. Exact rational numerator and denominator growth, memory use, model preparation and certificate evaluation would need to be included in a practical scale study.
41 
42 \fig{19_benchmark_costs.pdf}{Archived bounded cost comparison. The plotted measurements concern the seven declared small models and their original reference environment. Iterative cache savings and whole-producer cost are different quantities.}{fig:main-costs}
43 
44 \subsection{Extensions that preserve the completed result}
45 The first extension is a rounded selective cache. Its invariant must carry uncertainty about the semantic residual of the stored gain. A center-only update cannot reuse the exact equality $G_a=Q_aF(B)$ after independent rounding. The checked counterexample identifies the failed implication. A valid replacement could track residual enclosures and allocate update, selection and final-verification error budgets. That construction would require a new progress proof and a new origin statement.
46 
47 Sequential filtering is another extension. A repeated update needs a contract for how the returned representation becomes the next prior, including propagation of approximation error and data uncertainty. The present output arrays represent the returned Joseph law. Replacing them by centers or repeatedly treating an approximate prior as exact would add unstated obligations. The single-update theorem remains a reusable component for such a future composition.
48 
49 Changing packet geometry also requires a transition contract. The exact invariant uses one fixed complete orthogonal family. A new family can represent the same residual, but its cache must be reconstructed or transported with a proved relationship. Adaptive choice of a label within the fixed family is already covered. Adaptive replacement of the family is a separate operation.
50 
51 A universally refined host implementation would connect parsing, rational representation, code generation and execution to the defined Lean program. The current exporter provides explicit candidate data and checkable instance source. Its bounded diagnostics support that route without supplying a universal refinement theorem. Executable sampling and hardware floating-point implementations similarly need their own input, arithmetic and output contracts.
52 
53 \section{Conclusion}
54 Certified Inference Core 1.0.0 closes a precise finite-dimensional inference construction. Its exact cached packet computation has a maintained semantic invariant, a proved greedy trajectory, and computed finite fuel. Its final outward-rounded verifier connects the returned gain to a posterior-measure tolerance. Its parameter evaluator returns enclosing arrays for the same Gaussian approximation, with a prescribed radius bound. These are composed conclusions about one actual program result.
55 
56 The worked examples show the construction operating with rectangular observations and a singular prior. The rounded-cache counterexample supplies an equally useful boundary: the proof identifies which state equality an attractive alternative loses. Together, the positive result and the obstruction make the arithmetic contract inspectable. The extensive visual and Lean companions provide routes from the picture to the exact formula, and from the formula to the source declaration.
57 
58 \appendix
59 \section{Source and reproduction map}
60 The authoritative archive is \path{inputs/FD_Certified_Inference_Core_v1.0.0_Checked.zip}. Its SHA-256 is
61 \begin{center}\small\path{844ae280ea4be7e7c25906e00733f0130996b32aa110c53951df00f8c18fa488}.\end{center}
62 Extract it under \path{source}. The publication package includes all editable LaTeX, twenty figures, their common generator, fresh exact results, source maps, computation provenance, independent audit and page-review records. The intact archive contains the underlying formal modules, Python reference tools, historical receipts, failed attempts, benchmark records and runtime restoration metadata.
63 
64 The formal pins are Lean 4.34.0-rc2, compiler commit
65 \path{6a10ac8c22beadecabdbb0919c2b50214762f91d}, and Mathlib commit
66 \path{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.
67 The dependency manifest supplies the remaining pins. Read the original \path{README.md} and \path{RELEASE_SCOPE.md} before rebuilding. Original historical receipts should remain separate from newly generated evidence. The main theorem is in \path{Komorebi/CachedPacketOutput.lean}; its result predicate is in \path{Komorebi/PosteriorOutputSolver.lean}.
68 
69 \clearpage
70 \begin{thebibliography}{9}
71 \bibitem{core} Komorebi P. \emph{Certified Inference Core 1.0.0}. Checked source release, 12 September 2026. \path{FD_Certified_Inference_Core_v1.0.0_Checked.zip}.
72 \bibitem{nutini2015} J. Nutini, M. Schmidt, I. H. Laradji, M. Friedlander, and H. Koepke. Coordinate Descent Converges Faster with the Gauss-Southwell Rule Than Random Selection. \emph{Proceedings of Machine Learning Research} 37:1632--1641, 2015. \url{https://proceedings.mlr.press/v37/nutini15.html}.
73 \bibitem{nutini2022} J. Nutini, I. Laradji, and M. Schmidt. Let's Make Block Coordinate Descent Converge Faster: Faster Greedy Rules, Message-Passing, Active-Set Complexity, and Superlinear Convergence. \emph{Journal of Machine Learning Research} 23(131):1--74, 2022. \url{https://jmlr.org/papers/v23/18-045.html}.
74 \bibitem{wilson2021} J. T. Wilson, V. Borovitskiy, A. Terenin, P. Mostowsky, and M. P. Deisenroth. Pathwise Conditioning of Gaussian Processes. \emph{Journal of Machine Learning Research} 22(105):1--47, 2021. \url{https://jmlr.org/papers/v22/20-1260.html}.
75 \bibitem{daumas2007} M. Daumas and G. Melquiond. Certification of bounds on expressions involving rounded operators. \emph{arXiv:cs/0701186v2}, 24 May 2007. \url{https://arxiv.org/abs/cs/0701186v2}.
76 \end{thebibliography}

Back to source controls

Back to Certified Bayesian Inference