AVOC

Download original file

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

Read the typeset paper

1 \section{Evidence, reproduction, and the publication boundary}
2 \label{sec:publication-evidence}
3 The authoritative formal baseline for this edition is \path{AVOC_Formal_v0.41.0.zip}, with SHA-256
4 \begin{quote}\small\ttfamily
5 \detokenize{04efab87010b3b88c9a119275e190423a2465da32ba1e526edb7e6d2e0cd077e}.
6 \end{quote}
7 The original archive is preserved intact in the accompanying package. Its internal payload manifest was freshly checked for this edition: all $16{,}912$ listed payload digests match. The archive contains the mathematical source, interfaces, experiments, review records, failed attempts, and reproduction instructions. It excludes the Lean runtime and compiled project/dependency objects.
8 
9 \subsection{Archived formal evidence}
10 The v0.41.0 release record reports $222$ positive build targets, all passing under warnings-as-errors, and $2{,}268$ exact named theorem/lemma axiom reports. The allowed axiom union is \path{Classical.choice}, \path{Quot.sound}, and \path{propext}. There are $195$ non-audit mathematical modules; the latest block adds four modules and $69$ named theorem/lemma declarations. The $191$ inherited mathematical modules were checked byte-identical to the preceding release. The archive also records $135$ substantive negative proof rejections.
11 
12 These are different counts with different meanings. A build target may be an executable or audit target rather than a mathematical module. A named theorem/lemma count includes local infrastructure and explicit private helpers. It is not a count of independent discoveries. Negative-test success means that the incorrect test proposition was rejected for a substantive proof reason, not merely that a command exited unsuccessfully.
13 
14 The compiler pin is Lean 4.34.0-rc2, commit
15 \begin{quote}\small\ttfamily\detokenize{6a10ac8c22beadecabdbb0919c2b50214762f91d}.\end{quote}
16 The mathlib pin is
17 \begin{quote}\small\ttfamily\detokenize{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.\end{quote}
18 Nine exact dependency revisions are retained in \path{lake-manifest.json}. Local project objects were rebuilt from empty in the archived release. The external pinned caches were not rebuilt from every source. This distinction belongs to the reproducibility contract.
19 
20 \subsection{Fresh checks for this edition}
21 A fresh source inventory matches the actual $195$ mathematical modules and $2{,}268$ named declarations to the delivered registry. It checks the archived declaration-source digests and recorded source locations. Fresh exact Python computations reproduce the declared examples and finite recorder comparisons. The detailed tested families, assertions, input digests, outputs, and commands are included in the publication's \path{reviews} directory.
22 
23 No fresh Lean build or executable Lean comparison was performed for this publication edition. The compiler and exact portable dependency kit were unavailable in this session. The companion therefore uses archived kernel evidence together with fresh source-identity checks; it does not relabel that evidence as a new compilation. The Python comparisons remain bounded executable evidence and do not prove universal Python, parser, or storage refinement.
24 
25 \subsection{Assurance matrix}
26 \begin{longtable}{p{.24\linewidth}p{.37\linewidth}p{.30\linewidth}}
27 \toprule
28 Layer & Established statement & Application obligation \\
29 \midrule\endhead
30 Task context & Fiber criterion and decision-rule transport in the stated finite model & Identify the actual task and allowed rules \\
31 Artifact checker & Soundness/completeness for specified Boolean or affine syntax & Bind the checked input to the intended artifact \\
32 Cost comparison & Exact declared syntax/arithmetic tariffs and break-even calculations & Justify conversion to physical cost or reward \\
33 Frozen quote planner & Q/value enclosures, admissible robust choices, expected policy regret & True parameters and deterministic values belong to approved bands \\
34 Calibration & Finite rational cell-envelope coverage on fixed scheduled checkpoints & Source law, parameter strata, and predetermined schedule \\
35 Generative recorder & Unique logical IDs, immutable terminal retention, source-prefix refinement & Couple external operations and reporting order to the defined source \\
36 Recovery model & Confirmed logical evidence, selected installation, replay/accounting invariants & Input provenance and external execution/storage contracts \\
37 Host programs & Exact bounded tests and archived Lean endpoint comparisons & Universal parsing/host refinement, authentication, physical persistence \\
38 \bottomrule
39 \end{longtable}
40 
41 \subsection{The remaining research questions}
42 The principal statistical question is the coupling from physical attempts to reported samples. In the generative model, a fresh accepted report consumes the next latent bit. In a physical service, an attempted outcome can affect latency, retention, fault reporting, or whether a report appears at all. The completion-order counterexample proves that merely resolving every intent does not solve this problem. An initiation-indexed sampling contract is a plausible future target, but this paper does not claim to have proved it.
43 
44 \fig{10_completion_order_four_cases.pdf}{Every pair of attempted outcomes is logged and resolved, yet successes finishing first make the first reported bit successful with probability $3/4$. This exact finite counterexample concerns a physical interpretation of reported samples; it does not refute the formal generative-source theorem.}{fig:reportorder}
45 
46 A second question is controller composition. Current quotes are frozen within an episode. Updating bands during the same episode changes the policy and its dependency structure. Repeated episodes require explicit treatment of cumulative error, cost, and reward. The finite schedule theorem alone does not supply an unrestricted optional-stopping or continual-learning result.
47 
48 A third question is implementation assurance. The raw recorder accepts supplied labels; it does not authenticate their truth or execute a paid operation. An injective identity registry can prevent protected identity aliasing within its declared input contract, but a unique terminal ID does not prevent a caller from assigning two IDs to the same physical work. The inherited SQLite implementation relies on its database, operating-system, filesystem, and hardware contract. Its process-exit tests do not establish power-loss or distributed-system correctness.
49 
50 Finally, the present source laws are finite and rational, and the artifact backends use explicit languages and tariffs. Broader real-valued probability models, drift, dependence, scalable calibration, unrestricted stopping, larger artifact languages, and measured service workloads remain distinct extensions. None is needed to state the existing formal results accurately.
51 
52 \section{Conclusion}
53 AVOC supplies a checked finite route from artifact semantics and quoted uncertainty to admissible planning, calibrated policy issuance, and recoverable logical state. Its results are strongest when their interfaces are explicit. Correctness of an artifact, validity of a probability model, value of an action, and durability of external work are separate assertions, each with its own evidence.
54 
55 The recorder composition closes an operational step inside the formal model: the samples used by calibration are the actual terminal samples of a complete generative run. The completion-order counterexample identifies the next external step with equal clarity. Together they provide a usable publication boundary: a substantial verified architecture, exact explanatory examples, and an explicit physical-sampling problem that remains open.
56 
57 \appendix
58 \section{Source and document navigation}
59 The source root inside the original archive is \path{AVOC_Formal_v0.41.0}. Begin with \path{START_HERE.md}, \path{FORMAL_THEORY.md}, and \path{PROOF_BOUNDARY.md}. The full named declaration index is \path{THEOREM_INDEX.md}. Current reproduction instructions are in \path{REPRODUCE.md}; interface details are in \path{RECORDER_EXECUTABLE.md} and \path{OBSERVATION_EXECUTABLE.md}. Earlier source and verification records remain under \path{provenance}, \path{history}, and \path{results}.
60 
61 Publication review maps identify which source statements support each manuscript section. The separate Lean companion gives the module groups, actual theorem names and excerpts, archived evidence schema, and practical reproduction commands. Figure programs and exact test outputs make the visual examples independently reproducible. These navigation aids supplement the original source rather than replacing its hypotheses.
62 
63 \begin{thebibliography}{9}
64 \bibitem{avoc} Komorebi P. \emph{AVOC Formal v0.41.0}. Cumulative Lean/Python source and verification archive, 19 September 2026. Source, theory boundaries, declaration index, exact experiments, review records, and pinned reproduction instructions supplied with this edition.
65 \bibitem{blackwell} David Blackwell. \emph{Comparison of Experiments}. In Jerzy Neyman (editor), Proceedings of the Second Berkeley Symposium on Mathematical Statistics and Probability, University of California Press, 1951, pp. 93--102. \url{https://digicoll.lib.berkeley.edu/record/112749}. Historical context for comparison of observations; the finite rule-transport proof in this paper is self-contained.
66 \bibitem{lean} The Lean development team. \emph{Theorem Proving in Lean 4}, chapter ``Axioms and Computation.'' \url{https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation/}. Consulted 7 October 2026 for the distinction between foundational axioms, kernel reduction, and compiled computation. This documentation is not a replacement for the project's pinned compiler and audit receipts.
67 \bibitem{sqlite} SQLite development team. \emph{Atomic Commit in SQLite}. \url{https://www.sqlite.org/atomiccommit.html}. Official description of transaction mechanisms and hardware/flush assumptions, consulted 7 October 2026. Cited only for the external storage contract.
68 \end{thebibliography}

Back to source controls

Back to AVOC