AVOC

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 An artifact can be correct and still be a poor computational investment. A probability estimate can be useful and still be invalid for the stream on which it is applied. A recovery protocol can preserve a logical checkpoint and still depend on an unverified external execution contract. AVOC develops these distinctions within a finite formal architecture for artifact planning. Its cumulative theory combines task sufficiency, stochastic and Bayesian information transport, exact checking for declared artifact languages, finite-horizon planning, robust quote bounds, rational finite-sample calibration, and recoverable state transitions. The latest recorder block connects complete executions of a source-generative lifecycle machine to its actual terminal sample prefixes and proves an unconditional bound on uncertified policy issuance. We present central definitions and proof mechanisms, worked exact examples, and a theorem-to-source map. We also explain a completion-order obstruction: honest and complete logging can turn independent attempted outcomes into biased reported prefixes. The publication is based on the preserved v0.41.0 sources and their archived Lean verification. Fresh source-inventory and exact Python checks are reported separately from compilation, which was not repeated for this edition.
3 \end{abstract}
4 
5 \section*{Reading contract}
6 This paper gives a mathematical exposition of the cumulative formal project, with explicit contracts for applying its results to external computational services. AVOC is the project name used throughout.
7 
8 There are three complementary documents. The main paper develops the definitions, central arguments, and precise scope. The visual guide works through concrete examples with exact Python-generated figures. The Lean companion identifies actual definitions and theorem declarations, explains their hypotheses, and gives the pinned reproduction workflow. All source files, review notes, figure programs, and the original formal archive accompany the publication set.
9 
10 The following evidence vocabulary is used throughout. A \emph{formal result} refers to a statement in the delivered Lean theory with archived positive-build and axiom evidence. A \emph{prose reconstruction} explains that argument in conventional notation. An \emph{exact example} is a rational or finite computation with an explicit tested family. An \emph{external premise} is an assumption about a provider, host, storage layer, cost conversion, or sampling process that is not derived from accepting a formal certificate. These categories are deliberately kept distinct.
11 
12 \tableofcontents
13 \clearpage
14 
15 \section{Introduction: correct artifacts and correct decisions}
16 \label{sec:intro}
17 A useful computational system must decide more than whether an answer is correct. It must decide whether to search for an answer, inspect an existing candidate, reuse a checked result, or stop. It must account for checking and acquisition costs. When those costs and outcomes are uncertain, it must distinguish a plausible ranking from a certified decision. When work is interrupted, it must preserve enough state to resume without silently charging or installing the same logical result twice.
18 
19 AVOC organizes these questions around three related objects: the semantics of an artifact, the value of an action, and the evidence supporting the action's quoted parameters. None can substitute for the others. An exact affine checker can establish that a stored factorization computes the desired map for all inputs. It cannot establish how likely a future provider is to return such a factorization. A confidence procedure can bound a failure event under a stated source law. It cannot establish that externally supplied log entries satisfy that law. A checkpoint theorem can establish idempotent acceptance of a logical commit. It cannot establish exactly-once execution of a physical operation.
20 
21 This separation makes the architecture compositional. The artifact layer supplies a declared semantic language and checker. The decision layer supplies a state space, finite admissible action sets, finite observation alternatives, rewards, and transitions. The state space itself need not be finite. The uncertainty layer supplies frozen quote bands and compatible realizations. The observation layer supplies finite source laws, scheduled calibration, and a recorder whose terminal samples are connected to those sources. The recovery layer specifies how typed evidence and logical accounting are retained across replay.
22 
23 \subsection{The central chain}
24 The central statistical composition has the following form. A finite rational probability space supplies per-identity latent Boolean sources satisfying the stated conditional fresh-outcome law. A predetermined finite schedule fixes the checkpoints and their error allowances. The source-generative recorder constructs terminal reports from those sources. A theorem identifies each observed sample list with the appropriate source prefix. Calibration then bounds failure of simultaneous scheduled probability-band validity. On the simultaneous-coverage event, every issued plan has the stated episode certificate. Outside that event a plan may be uncertified; the final theorem bounds the unconditional risk of that issuance.
25 
26 \fig{02_evidence_chain.pdf}{The dependency chain inside the declared model. Physical source integrity and durable host storage require their own justification. The chain is a source-based schematic, not a measurement.}{fig:chain}
27 
28 Writing $I$ for issuance and $C$ for the specified episode certificate, the resulting conclusion is
29 \[
30  \Prob(I\cap C^{\mathsf c})\leq\sum_{j\in J}\alpha_j.
31 \]
32 This is an unconditional probability over the original outcome space. It allows arbitrary dependence between scheduled checkpoints. It retains failed and unfinished runs in that space, with no plan issued on those runs. It does not assert a nominal bound conditional on issuance or completion, eventual issuance, or a productivity lower bound. The final recorder theorem derives the execution-to-prefix correspondence inside its generative model. The model's primitive source law remains an explicit premise.
33 
34 \subsection{What is established}
35 The paper selects a coherent path through a larger cumulative library. The first group of results explains when a context or stochastic observation preserves what a task or decision problem needs. The second supplies complete checking and cost comparisons for declared Boolean and affine artifact languages. The third proves finite planning and robust value guarantees under specified guards and tariffs. The fourth connects finite calibration, source laws, recorder executions, and optional policy issuance. The fifth preserves logical evidence and accounting under replay and recovery.
36 
37 The global Boolean synthesis result is global within its declared finite semantic universe and syntax tariff. The affine minimum-width result concerns the specified two-stage factorization class. The policy guarantee concerns expected finite-horizon value against a comparator with the same conservative reservation guards. These restrictions are part of the conclusions, rather than qualifications attached after the fact.
38 
39 \subsection{Relation to classical mathematics}
40 The formal development uses familiar mathematical principles: factorization through fibers, comparison of statistical experiments, finite conditional probability, dynamic programming, test inversion, union bounds, and linear algebra over a field. For example, composing a decision rule with a stochastic garbling proves the direction that a more informative observation cannot reduce attainable decision value. This belongs to the classical comparison-of-experiments tradition of Blackwell; the finite proof is given here and is not represented as a new general informativeness theorem.
41 
42 The publication's mathematical focus is the integration of explicit contracts: which representation preserves a task, which artifact checker is complete for its language, which cost model supports a claimed saving, which uncertainty bound supports a selected action, and which sampling contract makes the calibration applicable. We make no exhaustive historical novelty claim. The names Bellman and Bayesian refer to the established planning and conditioning constructions used in the source, not to newly discovered replacements for those theories.
43 
44 \subsection{A running computational example}
45 Consider an affine map over $\mathbb F_5$ with four inputs and four outputs, all-ones linear coefficient matrix, and offset $(1,2,3,4)$. The direct dense evaluation tariff is $4(2\cdot4+1)=36$. Its rank-one factorization has a $4\to1$ stage followed by a $1\to4$ stage, with tariff $9+12=21$. Thus each declared call saves $15$ arithmetic cost units. For $1{,}000$ calls the gross saving is $15{,}000$.
46 
47 The delivered exact-quote example gives warm inspection setup $133$ and cold generation setup $196$, both with success probability $1$. Their net values are $14{,}867$ and $14{,}804$. These numbers are exact within the declared model. They are not wall-clock measurements, energy savings, or an empirical result about an external generation service. Later examples introduce uncertainty and show how certification can change an action, or lead a conservative planner to stop.
48 
49 \fig{03_rank_one_costs.pdf}{The rank-one affine example under its declared dense arithmetic tariff. Both the evaluation saving and the acquisition setup must enter the comparison.}{fig:rankcost}
50 
51 The example gives one intelligible route through the whole architecture. The semantic certificate establishes the factorization. The tariff establishes a per-call saving. The quote identity binds that saving to a specified source, call count, checker, provider, and environment. The planner compares admissible acquisition actions. The recorder and calibration address the probability parameters only under their own source contracts. A recovery checkpoint retains a confirmed logical result without treating every replay as a fresh acquisition.

Back to source controls

Back to AVOC