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{Finite-horizon planning with admissible actions}
2 \label{sec:planning}
3 
4 An artifact decision changes both what is available and what can be afforded.
5 Inspection can turn an untried cached artifact into a ready artifact, but a
6 rejection also spends its inspection fee. Generation can create a candidate,
7 but deployment must wait for a checked success. A controller therefore needs
8 an action set that depends on the current state, rather than a fixed menu with
9 inadmissible actions assigned convenient scores.
10 
11 \begin{definition}[Guarded rational system]
12 Let $S$ be a state space, $A(s)$ a finite nonempty set of actions, and $O$ a
13 finite observation space. A guarded system consists of a rational reward
14 $r(s,a)$, a transition $T(s,a,o)$, and rational probabilities $P(o\mid s,a)$
15 satisfying
16 \[
17  P(o\mid s,a)\geq0,\qquad \sum_{o\in O}P(o\mid s,a)=1.
18 \]
19 Its finite-horizon Bellman values are
20 \begin{align}
21  V_0(s)&=0,\label{eq:bellmanzero}\\
22  Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\
23  V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
24 \end{align}
25 \end{definition}
26 
27 Here $h$ in $Q_h$ counts \emph{continuation} steps. Choosing an acquisition
28 action and then deploying a successful artifact requires two total actions,
29 so its first-action score is $Q_1$, not $Q_0$. This indexing also applies to
30 \texttt{robustChoice md h s} in the formal source.
31 
32 The state space need not be finite. Rational Bayesian beliefs are one intended
33 instance. Only each feasible action set and the observation space are finite.
34 The finite maximum exists even when there is no asserted efficient procedure
35 for finding it. The mathematical selector and the executable evaluator are
36 separate constructions.
37 
38 \begin{theorem}[Optimality over complete adaptive plans]
39 Every horizon $H$ has a legal deterministic observation tree attaining
40 $V_H(s)$. Every other legal deterministic observation tree has value at most
41 $V_H(s)$. If each admissible transition preserves an invariant, the attaining
42 tree preserves that invariant on every branch.
43 \end{theorem}
44 \begin{proof}
45 At horizon zero, the empty tree has value zero. At horizon $h+1$, choose an
46 action attaining the finite maximum in \eqref{eq:bellman}; after each observation,
47 attach an optimal horizon-$h$ tree at the successor state. Induction proves
48 equality of the resulting expected value and the Bellman value. For an arbitrary
49 legal tree, induction bounds each child value by the corresponding optimal
50 continuation. Multiplication by nonnegative probabilities, summation, and the
51 maximum over admissible first actions give the upper bound. Invariant
52 preservation follows by the same tree induction. The invariant argument applies
53 to every observation branch, including a branch of probability zero.
54 \end{proof}
55 
56 This is a prose reconstruction of
57 \path{safe_optimal_plan_exists},
58 \path{optimalPlan_value}, and \path{planValue_le_value} in
59 \path{AVOC/GuardedControl.lean}. The competitors are complete adaptive
60 observation trees. They need not use the same subsequent choices as the selected
61 controller. The comparator nevertheless uses the same state, information,
62 action guards, and transition model. An oracle with additional information is a
63 different optimization problem.
64 
65 \subsection{Warm inspection and cold generation}
66 
67 The lazy staged controller makes this structure concrete. Its state records
68 warm and cold statuses, remaining budget, reserved spending, original credit,
69 and a terminal flag. Each artifact status is untried, failed, or ready. The
70 action list always contains stop. Inspection and generation require an untried
71 status and enough budget. Deployment requires the matching ready status.
72 Stopping or deploying ends the episode.
73 
74 An acquisition transition pays its setup fee whether its Boolean report is true
75 or false. A true report changes the corresponding status to ready. A false
76 report changes it to failed. Acquisition rewards are negative setup fees,
77 deployment rewards are nonnegative gross values, and stopping has reward zero.
78 This prevents three easy accounting mistakes: assuming unsuccessful acquisition
79 is free, treating a quote as an already available artifact, and deploying before
80 checked success.
81 
82 \begin{example}[The artifact-backed rank-one comparison]
83 The exact quote model retained in \path{AVOC/RobustQuoteExamples.lean} has
84 warm setup $133$, cold setup $196$, success probability $1$ for both, and gross
85 deployment value $15000$ for each over $1000$ calls. With initial credit $196$
86 and two total actions available,
87 \[
88  Q_1(\mathrm{inspectWarm})=15000-133=14867,
89  \qquad
90  Q_1(\mathrm{generateCold})=15000-196=14804.
91 \]
92 Warm inspection is better by $63$ in this exact model. At one total action,
93 acquisition has only its negative immediate reward, and stopping is preferable
94 when neither artifact is ready. The deployment opportunity creates the change
95 between these two horizons.
96 \end{example}
97 
98 This example has actual bounded artifact witnesses in the retained source.
99 The gross value is the symbolic execution saving for the protected workload,
100 not a measured dollar return or a wall-clock benchmark. The singleton evidence
101 makes all quote uncertainty radii vanish, so the robust lower-Q selector
102 recovers the inherited exact selector. The relevant declarations are
103 \path{exact_recovers_v037},
104 \path{exact_all_local_radii_zero}, and
105 \path{artifact_refines_deterministic_fields}.
106 
107 \subsection{An executable evaluator and its cost boundary}
108 
109 The executable planner enumerates admissible first actions and observation
110 branches, recursively evaluates continuations, and chooses a best score. Under
111 the formal \path{Realizes} relation, its returned score equals the mathematical
112 Bellman value. A full catalogue enumeration and a verified admissibility check
113 connect the staged workflow to that evaluator. In particular,
114 \path{WorkflowPlanner.model_realizes} and
115 \path{executable_policy_source_safe} connect actual staged transitions,
116 source-bound artifacts, and the selected policy.
117 
118 The planner's work counter counts defined recursive evaluator nodes. A branching
119 cap permits reserving an abstract planning allowance, and truncated lookahead
120 has a source-backed policy regret bound. This counter is not a rational-bit
121 complexity bound. It does not include all host parsing, catalogue scans,
122 reservation arithmetic, storage operations, or physical invocation cost.
123 Consequently, a proved allowance in that model cannot by itself establish a
124 time bound for the complete service.
125 
126 \section{Quote uncertainty and certified lower-Q selection}
127 \label{sec:quotes}
128 
129 Quotes carry more than a success estimate. A protected identity records the
130 artifact kind, exact source signature, workload call count, cost model, provider,
131 checker, environment, and schema. A setup band has natural endpoints. Gross
132 and probability bands have rational endpoints, with probability endpoints in
133 $[0,1]$ and nonnegative gross lower endpoints. A submitted quote validates only
134 when it equals the protected approved quote. Changing either identity or any
135 band changes the evidence.
136 
137 For kind $k\in\{w,c\}$, write
138 \[
139  c_k\in[c_k^-,c_k^+],\qquad
140  g_k\in[g_k^-,g_k^+],\qquad
141  p_k\in[p_k^-,p_k^+].
142 \]
143 The formal nominal model reserves $c_k^+$, credits $g_k^-$, and uses $p_k^-$.
144 A compatible realization supplies exact values inside these bands. In the true
145 comparison system, rewards and report probabilities use those exact values,
146 but the state transitions and action guards remain those of the nominal model.
147 In particular, setup reservations continue to use the upper setup bound.
148 
149 This common guard matters. If the true setup is $1$ and the upper quoted setup
150 is $3$, a budget of $2$ still makes the acquisition inadmissible for both systems
151 in the theorem. The comparator does not obtain an extra feasible action by
152 knowing the smaller true fee. A theorem against that larger feasible set would
153 require a different comparison argument.
154 
155 \subsection{From primitive bands to value bounds}
156 
157 Let $w_c(k)=c_k^+-c_k^-$, $w_g(k)=g_k^+-g_k^-$, and
158 $w_p(k)=p_k^+-p_k^-$. The source uses the uniform quantities
159 \begin{align}
160  \varepsilon&=w_c(w)+w_c(c)+w_g(w)+w_g(c),\\
161  \delta&=2\bigl(w_p(w)+w_p(c)\bigr),\\
162  M&=c_w^++c_c^++g_w^++g_c^+.
163 \end{align}
164 They bound reward error, Boolean-row $L^1$ error, and nominal one-step reward
165 magnitude respectively. For an acquisition of kind $k$, the sharper local
166 reward error is $w_c(k)$ and its row error is $2w_p(k)$. For deployment of kind
167 $k$, the local reward error is $w_g(k)$ and its row error is zero. Stop has zero
168 primitive errors.
169 
170 \begin{lemma}[Bernoulli row error and expectation transport]
171 For Bernoulli parameters $p,q$,
172 \[
173  \sum_{o\in\{0,1\}}|P_p(o)-P_q(o)|=2|p-q|.
174 \]
175 If $|W(t)|\leq B$, then replacing an observation row $P$ by $\widehat P$
176 changes its expected continuation by at most
177 \[
178  \left|\sum_o(P(o)-\widehat P(o))W(T(s,a,o))\right|
179  \leq B\sum_o|P(o)-\widehat P(o)|.
180 \]
181 \end{lemma}
182 \begin{proof}
183 The two Bernoulli row differences are $p-q$ and $q-p$, which have equal
184 absolute values. For the second statement, apply the triangle inequality to the
185 finite sum and use the uniform bound on each continuation value.
186 \end{proof}
187 
188 Induction on the Bellman recursion gives $|\widehat V_h(s)|\leq hM$ for the
189 nominal value. The source's accumulated value radius and local Q radius are
190 \begin{align}
191  D_h&=\sum_{j=0}^{h-1}(\varepsilon+\delta jM),\label{eq:value-radius}\\
192  \rho_h(a)&=D_h+\varepsilon_a+\delta_a hM,\label{eq:local-radius}\\
193  \Gamma_h&=D_h+\varepsilon+\delta hM.\label{eq:global-radius}
194 \end{align}
195 The Bellman residual is zero here because the nominal tables are exact Bellman
196 values. The broader model-error framework also allows a supplied table with a
197 proved nonzero residual, but no residual term is silently introduced in these
198 quote results.
199 
200 \begin{theorem}[Value and Q enclosures]
201 For every compatible realization, every state, and every continuation horizon,
202 \begin{align}
203  |V_h(s)-\widehat V_h(s)|&\leq D_h,\\
204  |Q_h(s,a)-\widehat Q_h(s,a)|&\leq\rho_h(a)\leq\Gamma_h.
205 \end{align}
206 Thus $L_h(s,a)=\widehat Q_h(s,a)-\rho_h(a)$ and
207 $U_h(s,a)=\widehat Q_h(s,a)+\rho_h(a)$ enclose the true Q value.
208 \end{theorem}
209 \begin{proof}
210 At horizon zero the value error is zero. In a single backup, insert and subtract
211 the expectation of the nominal continuation under the true row. The reward
212 error contributes at most $\varepsilon_a$, the continuation-value error at most
213 $D_h$, and row transport at most $\delta_a hM$. Taking a maximum over the same
214 feasible action set is nonexpansive in the uniform score error. Therefore
215 $D_{h+1}\leq D_h+\varepsilon+\delta hM$, whose accumulated upper bound is
216 \eqref{eq:value-radius}. The local Q statement follows from the same inserted
217 expectation before taking a maximum.
218 \end{proof}
219 
220 The reconstructed argument follows \path{value_error},
221 \path{local_q_error}, \path{value_between}, and
222 \path{q_between} in \path{AVOC/RobustQuotePlanning.lean}. The primitive
223 steps are \path{reward_close}, \path{probability_l1_le}, and
224 \path{expectation_transport}.
225 
226 \subsection{What the robust selector optimizes}
227 
228 The executable robust choice maximizes $L_h(s,a)$ over feasible actions. It is
229 a maximizer of a \emph{certified surrogate lower bound}. It is not asserted to
230 solve the exact minimax problem over all compatible realizations. A bound can
231 be valid and substantially below the actual worst-case score.
232 
233 \begin{proposition}[Distinct-competitor dominance]
234 If $a$ is feasible and
235 \[
236  U_h(s,b)\leq L_h(s,a)\quad
237  \text{for every feasible }b\ne a,
238 \]
239 then $a$ is optimal in every compatible realization.
240 \end{proposition}
241 \begin{proof}
242 For a distinct competitor, chain the three inequalities
243 $Q_h(s,b)\leq U_h(s,b)\leq L_h(s,a)\leq Q_h(s,a)$.
244 The comparison with $a$ itself is reflexive.
245 \end{proof}
246 
247 This is \path{competitor_dominance_sound} in
248 \path{AVOC/CalibrationBridge.lean}. Excluding self-comparison is essential
249 for a useful non-singleton certificate. The older sufficient condition compares
250 every feasible upper score, including the chosen action's own upper score, to
251 its lower score. That older condition is sound but forces the chosen radius to
252 be zero. The formal declaration
253 \path{self_comparison_forces_zero_radius} records this limitation.
254 
255 \begin{example}[A deliberately conservative abstract quote fixture]
256 The retained uncertainty example assigns zero setup to both kinds, warm gross
257 $200$, cold gross $60$, warm success band $[3/5,1]$, and exact cold success $1$.
258 Start with both statuses untried and use $h=1$, hence two total actions. The
259 nominal scores are warm $120$, cold $60$, and stop $0$. Here
260 $\varepsilon=0$, $\delta=4/5$, $M=260$, and $D_1=0$. The local warm radius
261 is $208$, while the cold and stop radii are zero:
262 \[
263 \begin{array}{c|r|r|r}
264  \text{action}&\widehat Q_1&\rho_1&L_1\\\hline
265  \mathrm{inspectWarm}&120&208&-88\\
266  \mathrm{generateCold}&60&0&60\\
267  \mathrm{stop}&0&0&0
268 \end{array}
269 \]
270 The lower-Q rule chooses cold although warm's exact compatible Q range is
271 $[120,200]$. This is a clear example of conservatism in the certified envelope.
272 It does not show that cold is the exact maximin choice.
273 \end{example}
274 
275 The source proves the widths, local radii, and numerical order through
276 \path{uncertain_warm_local_radius},
277 \path{uncertain_cold_local_radius}, and
278 \path{uncertainty_changes_numerical_order}. The displayed first-action
279 ranking is a direct reconstruction at the stated initial state and horizon.
280 This fixture is \emph{abstract quote planning}, not an artifact-backed saving
281 example. Its protected rank-one source has dense cost $36$ per call and the
282 fixture has one call, so gross values $200$ and $60$ cannot come from bounded
283 execution savings for that source. The separate $1000$-call example above is
284 the artifact-backed comparison. These two roles must remain distinct.
285 
286 \subsection{Whole-policy regret, not only first-action quality}
287 
288 Let $a_h(s)$ maximize $L_h(s,a)$ and let $a^*$ maximize the true $Q_h$.
289 Then
290 \begin{align*}
291  V_{h+1}(s)-Q_h(s,a_h(s))
292  &\leq U_h(s,a^*)-L_h(s,a_h(s))\\
293  &\leq U_h(s,a^*)-L_h(s,a^*)\\
294  &\leq 2\Gamma_h.
295 \end{align*}
296 The comparison controls the Bellman loss of the actual choice at each state.
297 The policy is rebuilt at every remaining horizon with the same frozen evidence.
298 
299 \begin{theorem}[Expected frozen-policy regret]
300 For a horizon $H$, let $J_H^{\rm lower}(s)$ be the expected value of the complete
301 adaptive policy induced by robust lower-Q selection. Under any compatible
302 realization,
303 \[
304  0\leq V_H(s)-J_H^{\rm lower}(s)
305  \leq\sum_{h=0}^{H-1}2\Gamma_h.
306 \]
307 The comparator is the true optimal legal adaptive plan with the same
308 conservative reservation guards.
309 \end{theorem}
310 \begin{proof}
311 Write the regret at a node with $h+1$ remaining steps as its local Bellman loss
312 plus the expected regret of the selected continuation. The local term is at
313 most $2\Gamma_h$. By induction, every child regret is bounded by the common
314 sum $\sum_{j<h}2\Gamma_j$. Taking the expectation leaves that constant unchanged
315 because probabilities sum to one. This yields the cumulative upper bound.
316 Nonnegativity follows because the selected complete tree is legal and $V_H$
317 dominates the value of every legal tree.
318 \end{proof}
319 
320 This is the argument implemented by \path{plan_regret_le} in
321 \path{AVOC/GuardedPolicyRegret.lean} and
322 \path{robust_policy_regret} in \path{AVOC/RobustQuotePlanning.lean}.
323 Ordinary finite sums simplify the displayed bound to
324 \[
325  \varepsilon H(H+1)+\frac{\delta M}{3}H(H-1)(H+1).
326 \]
327 This last closed form is a prose algebraic consequence of the source's sums,
328 not a newly compiled Lean declaration. The envelope is deliberately broad and
329 may be vacuous for a particular application. It remains a valid certificate.
330 The regret is an expected policy-value difference. It does not bound every
331 realized sequence of successes and failures.
332 
333 \section{Exact finite-grid calibration}
334 \label{sec:calibration}
335 
336 Probability bands need an evidence rule. The implemented rule is an exact
337 rational finite-grid cell-envelope construction. It should not be relabeled as
338 an exact inversion of binomial tails or as a Clopper--Pearson interval. Its proof
339 uses a different and simpler exclusion budget.
340 
341 Let $K$ be the number of successes in $n$ Bernoulli trials with rational
342 parameter $p\in[0,1]$. Define
343 \[
344  b_{n,k}(p)=\binom nk p^k(1-p)^{n-k},\qquad 0\leq k\leq n.
345 \]
346 Choose a positive integer grid size $m$ and nonnegative rational allowance
347 $\alpha$. The grid cells have endpoints
348 \[
349  \ell_i=\frac{i}{m},\qquad u_i=\frac{i+1}{m},\qquad 0\leq i<m.
350 \]
351 For observed count $k$, the envelope of its point mass over cell $i$ is
352 \[
353  B_{n,k,i}=\binom nk u_i^k(1-\ell_i)^{n-k}.
354 \]
355 Retain the cell exactly when
356 \[
357  B_{n,k,i}>\frac{\alpha}{n+1}.
358 \]
359 Return the closed interval spanning all retained cells. If there are no retained
360 cells, return $[0,1]$. The returned interval is therefore always a valid band.
361 The construction performs exact rational arithmetic and strict comparison.
362 Boundary cells cover $0$ and $1$ as well as interior parameters.
363 
364 \begin{theorem}[Finite-sample grid coverage]
365 If $K$ has the binomial count law $b_{n,k}(p)$, the returned interval $I(K)$ obeys
366 \[
367  \Prob\{p\notin I(K)\}\leq\alpha.
368 \]
369 This holds for every rational $p\in[0,1]$, without assuming that $p$ is a grid
370 point.
371 \end{theorem}
372 \begin{proof}
373 Some grid cell contains $p$. In that cell, $p\leq u_i$ and
374 $1-p\leq1-\ell_i$, hence $b_{n,k}(p)\leq B_{n,k,i}$. If $p$ is outside the
375 returned interval, the containing cell could not have been retained: any
376 retained cell lies inside the hull. Therefore
377 $B_{n,k,i}\leq\alpha/(n+1)$, and the mass of this excluded count $k$ is at most
378 that threshold. There are $n+1$ possible counts, so summing their failure masses
379 gives at most $\alpha$. If no cells were retained, the returned full band cannot
380 exclude $p$ and the conclusion is immediate.
381 \end{proof}
382 
383 The source proves the grid cover, the cell envelope, excluded-count mass, and
384 final sum as \path{grid_covers}, \path{mass_le_envelope},
385 \path{excluded_mass_le}, and \path{missMass_le} in
386 \path{AVOC/FiniteCalibration.lean}. This proves finite-sample validity of the
387 algorithm itself within the exact rational binomial model. It does not infer the
388 sampling model from a list of reported outcomes.
389 
390 \begin{example}[Ten successes are evidence, not certainty]
391 For $n=10$, $m=10$, and $\alpha=1/10$, ten successes retain cells
392 $\{6,7,8,9\}$ and return $[3/5,1]$. Ten failures retain
393 $\{0,1,2,3\}$ and return $[0,2/5]$. These endpoint calculations are explicit
394 Lean theorems. By contrast, the empirical singleton $\{K/n\}$ has no such
395 coverage property. At $n=1$ and $p=1/2$, both possible singletons exclude the
396 true parameter, so its miss probability is $1$.
397 \end{example}
398 
399 The relevant declarations include \path{ten_successes_lower},
400 \path{ten_successes_upper}, \path{ten_failures_lower},
401 \path{ten_failures_upper}, and
402 \path{empirical_singleton_counterexample}. Nothing here says the true
403 parameter has posterior probability $9/10$ of lying inside an observed band.
404 The guarantee concerns repeated-data failure probability under the specified
405 law.
406 
407 \subsection{Predetermined schedules and data-dependent selection}
408 
409 A schedule is a finite set $J$ of checkpoints. Each checkpoint fixes an
410 identity stratum, sample size $n_j$, grid $m_j>0$, true parameter $p_j$, and
411 nonnegative error allocation $\alpha_j$. Its count statistic has the stated
412 binomial marginal. Counts can be dependent, including different prefixes of
413 one source and checkpoints that share other underlying randomness.
414 
415 \begin{theorem}[Scheduled and selected failure bounds]
416 Let $B_j$ be the event that checkpoint $j$'s interval excludes $p_j$. Then
417 \[
418  \Prob\Bigl(\bigcup_{j\in J}B_j\Bigr)
419  \leq\sum_{j\in J}\alpha_j.
420 \]
421 For any data-dependent selector $j(\omega)\in J$,
422 \[
423  \Prob\{\omega\in B_{j(\omega)}\}\leq\sum_{j\in J}\alpha_j.
424 \]
425 \end{theorem}
426 \begin{proof}
427 For each outcome $\omega$, the indicator of a union is at most the sum of the
428 individual indicators. Multiply by the nonnegative rational weight of
429 $\omega$ and sum over the finite probability space. Interchange the two finite
430 sums to obtain the union bound. Each checkpoint has failure mass at most its
431 allocated $\alpha_j$ by finite-grid coverage. Finally, selected failure implies
432 failure of at least one scheduled checkpoint, so it is a subset of the union.
433 This last inclusion holds pointwise even if selection sees all outcomes.
434 \end{proof}
435 
436 This reconstructs \path{finite_union_le},
437 \path{scheduled_binomial_failure_le}, and
438 \path{selected_binomial_failure_le} in
439 \path{AVOC/CalibrationSchedule.lean}. Neither checkpoint independence nor
440 an independent selector is required. Predetermination is required: the theorem
441 does not authorize creating arbitrary new checkpoints after viewing the data.
442 It is finite scheduled selection, rather than an unrestricted anytime
443 confidence sequence.
444 
445 \begin{example}[Why the schedule's total allowance is necessary]
446 Take a fair Boolean outcome $\omega$ and two checkpoint bad events
447 $B_0=\{\omega=0\}$ and $B_1=\{\omega=1\}$. Each has probability $1/2$.
448 Selecting $j(\omega)=\omega$ makes selected failure certain. The total allowance
449 $1/2+1/2=1$ remains valid, while either single checkpoint's allowance fails.
450 This is the exact obstruction proved by
451 \path{fairBool_adaptive_exceeds_single_budget}.
452 \end{example}
453 
454 \section{From source laws to actual terminal samples}
455 \label{sec:recorder}
456 
457 The count-law obligation is substantial. Fair marginals do not imply a binomial
458 sum. Two identical fair bits each have parameter $1/2$, but their two-bit count
459 is either zero or two and never one. The source contains this obstruction as
460 \path{correlatedPair_not_product}.
461 
462 The primitive model uses a finite rational probability space and, for each
463 identity $k$, a finite latent Boolean vector of length $N_k$. Its success
464 parameter $p_k$ is fixed. The fresh-outcome contract states that after agreement
465 with any specified pattern on a previously revealed set of positions, a fresh
466 position's joint success mass is $p_k$ times that history mass. In notation,
467 \[
468  \Prob\{H\text{ matches and }X_i=1\}=p_k\Prob\{H\text{ matches}\},
469  \qquad i\text{ fresh}.
470 \]
471 The multiplication-only form is meaningful for histories of mass zero and does
472 not divide by them. Induction determines the mass of every full pattern, then
473 summing patterns by success count gives its binomial law. Truncation yields the
474 same law for each fixed prefix.
475 
476 The formal steps are \path{conditional_implies_product},
477 \path{count_fiber_eq_binomial}, and
478 \path{prefix_count_fiber_eq_binomial} in
479 \path{AVOC/ObservationStream.lean}. This derives the count law from a
480 primitive source law. The primitive source law itself remains an explicit
481 model assumption.
482 
483 \subsection{Pending intents and immutable terminal events}
484 
485 The new lifecycle recorder separates a pending-intent list from a terminal log.
486 A single global natural-number operation-ID namespace covers both lists and
487 all identities. Pending entries store an ID and identity. Terminal entries
488 store an ID, identity, and success, rejection, or fault. An unfinished outcome
489 cannot be inserted as a terminal event.
490 
491 \begin{center}
492 \begin{tabularx}{\linewidth}{@{}lX@{}}
493 \toprule
494 Command situation & Defined result\\\midrule
495 Fresh begin & Append one pending ID and identity.\\
496 Exact pending begin replay & Return the same state.\\
497 Begin replay after matching completion & Return the same state without reopening.\\
498 Matching fresh finish & Remove the pending ID and append one terminal event.\\
499 Exact terminal replay & Return the same state.\\
500 Changed identity or terminal outcome & Reject the command.\\
501 Finish without matching intent & Reject the command.\\
502 Unfinished terminal outcome & Reject the command.\\
503 \bottomrule
504 \end{tabularx}
505 \end{center}
506 
507 These cases resolve a concrete inherited obstruction. If an immutable log stores
508 an unfinished event under an ID, later adding success under that ID changes the
509 event and must be rejected. A pending registry therefore cannot simply be an
510 unfinished terminal record. The declaration
511 \path{inherited_unfinished_terminal_conflict} proves the mismatch, rather
512 than relying on a narrative explanation.
513 
514 \begin{theorem}[Pure recorder lifecycle invariant]
515 Every successful run from the empty state has unique pending IDs, unique
516 terminal IDs, disjoint pending and terminal IDs, and no unfinished terminal
517 entries. An accepted terminal event occurs once and remains once throughout
518 every later successful continuation. Terminal history grows by suffix append.
519 \end{theorem}
520 \begin{proof}
521 For a begin step, the transition first checks both uses of the ID. It either
522 returns the unchanged state for a matching replay, rejects conflicting reuse,
523 or appends a fresh pending entry. For a finish step, exact replay is unchanged;
524 otherwise successful completion requires an unused terminal ID and a matching
525 pending entry. Removing that pending ID and appending its terminal event
526 preserves uniqueness and disjointness. Unfinished outcomes are rejected before
527 these cases. Induction over a successful command list preserves the invariant.
528 Every successful step leaves the log unchanged or appends one event, which
529 proves retention under continuation.
530 \end{proof}
531 
532 The source declarations are \path{run_wellFormed},
533 \path{runFrom_log_prefix}, and
534 \path{accepted_terminal_retained_once} in
535 \path{AVOC/ObservationRecorder.lean}. A success adds true once to its
536 identity's samples, a rejection adds false once, and a fault adds no sample.
537 False outcomes count toward sample readiness just as true outcomes do.
538 
539 \subsection{A source-generative recorder and whole-run refinement}
540 
541 The raw recorder accepts externally supplied terminal labels. The generative
542 recorder instead has begin, report, and fault commands. A fresh report constructs
543 its true or false label from the next latent Boolean of its identity. A replay
544 checks the terminal log first and reuses the stored outcome, consuming no new
545 source bit. A fresh report with an exhausted source rejects. Faults and begins
546 consume no source bit. Reporting after a fault conflicts with the immutable
547 terminal event.
548 
549 Every accepted generative step emits an ordinary recorder command and an
550 effective reveal marker. Whole-run induction proves that the emitted commands
551 reproduce the actual raw recorder state and that the reveal state equals the
552 inherited reveal machine on its effective trace. In particular, for every
553 identity,
554 \begin{equation}
555  \mathrm{samples}_k(\mathrm{terminalLog})
556  =\mathrm{source}_k.\mathrm{take}
557      \bigl(|\mathrm{samples}_k(\mathrm{terminalLog})|\bigr).
558  \label{eq:recorder-prefix}
559 \end{equation}
560 
561 This is \path{run_refines} and \path{run_samples_eq_take} in
562 \path{AVOC/RecorderReveal.lean}. The source-prefix correspondence is a
563 derived invariant of the defined machine, not an additional equality asserted
564 for each observed raw event. It still does not establish that an arbitrary
565 external success label came from this latent source. A parser can check the
566 label's syntax without checking its physical or statistical origin.
567 
568 \begin{example}[Replay and faults do not create new evidence]
569 Let an identity's source be $[\mathrm{true},\mathrm{false}]$. Begin ID $7$, report
570 ID $7$, then report ID $7$ again. The sample list is $[\mathrm{true}]$ and the
571 remaining source begins with false. Begin ID $8$ and finish it as a fault. The
572 sample list stays unchanged. Begin and report ID $9$. It appends false, yielding
573 $[\mathrm{true},\mathrm{false}]$. A further fresh report rejects after source
574 exhaustion, while a replay of ID $7$ remains possible. The replay supplies no
575 extra success and the fault supplies no concealed binary observation.
576 \end{example}
577 
578 This is an illustrative execution of the defined transitions. The retained
579 formal examples \path{replay_fault_exhaustion_example} and
580 \path{exhausted_fresh_report_rejected} provide closely related checked
581 instances. Reusing a different ID for the same physical operation is a separate
582 identity problem. Global ID uniqueness alone cannot rule it out.
583 
584 \section{Unconditional calibrated policy issuance}
585 \label{sec:issuance}
586 
587 The recorder-to-policy endpoint reads counts from the actual terminal log.
588 Rejected whole runs supply no counts. Successful runs with \emph{any} pending
589 operation also supply no counts, even when the pending identity is unrelated to
590 the selected checkpoint. A fully resolved run still needs enough success or
591 rejection reports for both selected checkpoints. A checkpoint always reads the
592 first predetermined $n_j$ reports, so later reports cannot change that count.
593 
594 When both selected counts are available, the endpoint constructs their exact
595 learned probability bands and installs them for a fresh frozen policy episode.
596 Setup and gross memberships are supplied deterministic premises. The warm and
597 cold selectors may depend on all outcomes but must select checkpoints with the
598 specified warm and cold true parameters. Changing a probability band does not
599 authorize changing an outstanding operation's evidence.
600 
601 \begin{theorem}[Recorder-to-policy bad-issuance bound]
602 Assume finite rational latent sources satisfy the primitive conditional laws;
603 the finite schedule, grids, and nonnegative allowances are predetermined;
604 scheduled prefix lengths fit within their sources; selected strata match the
605 specified true probabilities; and deterministic setup/gross memberships hold.
606 Then
607 \begin{equation}
608  \Prob\{\text{a plan is issued and lacks its episode certificate}\}
609  \leq \sum_{j\in J}\alpha_j.
610  \label{eq:issuance}
611 \end{equation}
612 The episode certificate supplies a compatible realization with the stated exact
613 parameters, value and Q enclosures, and expected whole-policy regret for every
614 finite horizon under frozen quotes.
615 \end{theorem}
616 \begin{proof}
617 The primitive conditional law yields binomial prefix count laws at all scheduled
618 checkpoints. The generative run refinement gives \eqref{eq:recorder-prefix}.
619 Whenever gated counts are available, taking the fixed first $n_j$ reports
620 therefore gives the corresponding latent prefix count. On the event where all
621 scheduled bands cover their true parameters, either the gates suppress issuance
622 or both selected learned bands contain the correct parameters. Combine those
623 memberships with the supplied deterministic memberships to construct a
624 compatible realization. The deterministic frozen-episode theorem then supplies
625 the policy certificate. Thus bad issuance is a subset of the scheduled band
626 failure union, whose probability is bounded by the total allowance.
627 \end{proof}
628 
629 The final declarations are \path{recorder_episode_coverage} and
630 \path{recorder_issued_failure_le} in
631 \path{AVOC/RecorderPolicy.lean}. Success of execution, absence of pending
632 intents, availability of enough samples, log-prefix equality, and the binomial
633 count law are not separately supplied premises to that final theorem. They are
634 derived or checked by its machine and gates. The primitive source laws and
635 deterministic memberships are still supplied.
636 
637 The probability in \eqref{eq:issuance} ranges over the original outcome space,
638 including rejected, unresolved, and insufficient-data runs. There is no claim
639 that a plan will be issued, that any operation finishes, or that collection is
640 cheap. If the issuance probability is $q>0$, the generic conditional implication
641 is only
642 \[
643  \Prob\{\text{uncertified}\mid\text{issued}\}
644  \leq \min\left(1,\frac{\sum_j\alpha_j}{q}\right).
645 \]
646 The same nominal allowance need not hold after conditioning on issuance.
647 
648 \subsection{Completion conditioning can select a biased population}
649 
650 \begin{example}[Predictable availability still biases completed runs]
651 Let $(X_1,X_2)$ be independent fair bits. Reveal $X_1$, and reveal $X_2$ by the
652 deadline only if $X_1=1$. Availability of the second report depends on the past,
653 not on $X_2$. Completion probability is $1/2$. Conditional on completion,
654 $X_1=1$ with probability one, and the two-bit count has probability zero of
655 being zero. A genuine two-trial binomial count with parameter $1/2$ has zero
656 count probability $1/4$.
657 \end{example}
658 
659 This is kernel-checked in \path{AVOC/ObservationCensoring.lean}, including
660 \path{deadline_second_retention_predictable},
661 \path{deadline_conditioned_first_success}, and
662 \path{deadline_conditioned_count_not_binomial}. It shows why one cannot
663 replace the original law by the law conditioned on enough reports arriving.
664 
665 A direct interval illustration uses ten independent fair bits and issues an
666 interval only when all ten are true. Its issuance probability is $2^{-10}$.
667 The implemented $n=m=10$, $\alpha=1/10$ interval is then $[3/5,1]$, which excludes
668 $1/2$. Conditional on issuance, failure is certain. Unconditional bad issuance
669 is only $2^{-10}$ and satisfies the allowance. This finite calculation is an
670 illustrative consequence of the checked interval endpoints and the elementary
671 product law, not a new Lean declaration.
672 
673 \subsection{Complete logs do not fix outcome-dependent completion order}
674 
675 Conditioning and ordering are different obstructions. Suppose two independent
676 fair attempts start together. Success takes one unit of time and rejection
677 takes two; resolve ties by the initiation ID. Record every final outcome and
678 wait until all intents have resolved. The completion order is
679 \[
680 \begin{array}{c|c|c}
681 \text{initiation outcomes}&\text{completion-order outcomes}&\text{mass}\\\hline
682 (0,0)&(0,0)&1/4\\
683 (0,1)&(1,0)&1/4\\
684 (1,0)&(1,0)&1/4\\
685 (1,1)&(1,1)&1/4
686 \end{array}
687 \]
688 The first completed bit succeeds with probability $3/4$. No report was missing,
689 no terminal event was forged, and no operation remains pending. Nevertheless,
690 the first-completed prefix is not a fair source prefix.
691 
692 For the implemented interval, the stronger retained finite experiment starts
693 twenty independent fair attempts and lets all successes complete before all
694 rejections. If there are at least ten successes, the first ten completed reports
695 are all true. Their interval is $[3/5,1]$ and excludes $1/2$. That event has mass
696 \[
697  \frac{1}{2^{20}}\sum_{k=10}^{20}\binom{20}{k}
698  =\frac{308333}{524288}>\frac{1}{10}.
699 \]
700 Thus actual interval failure exceeds its nominal allowance despite complete,
701 fully resolved lifecycle records. The exact Python evidence is preserved under
702 \path{results/v0.41.0/review_completion_order.py} and its JSON receipt. It is
703 a finite computational obstruction with an explicit rational derivation here,
704 not a newly kernel-checked theorem.
705 
706 The generative theorem assigns the next latent bit in report order and assumes
707 that source's conditional law. Independent outcomes in initiation order do not
708 automatically satisfy that assumption after outcome-dependent reordering. A
709 physical deployment must justify its report-order contract, for example through
710 an initiation-indexed sampling policy or a proved alternative coupling. The
711 current release leaves that physical coupling open.
712 
713 \section{Checked recovery and durable accounting}
714 \label{sec:recovery}
715 
716 Recovery must distinguish a recorded intention from a completed paid result.
717 The robust quote recovery model binds a commit to its sequence, complete
718 pre-state, selected action, quote evidence, outcome tag, and post-state. Fresh
719 acknowledgment checks those bindings and checks that the supplied typed outcome
720 realizes the action through the runtime's \path{confirm} transition. It then
721 requires the computed successor's store view to equal the recorded durable
722 post-state. An unfinished intent is rejected rather than interpreted as a
723 negative observation or permission to repeat paid work.
724 
725 \begin{proposition}[Fresh acknowledgment and replay]
726 A successful fresh acknowledgment advances the sequence by one and yields
727 the successor certified by \path{confirm}. It preserves the runtime safety
728 invariant. Repeating that accepted commit at the resulting matching checkpoint
729 returns the same checkpoint.
730 \end{proposition}
731 \begin{proof}
732 Each failed identity, sequence, pre-state, outcome, evidence, or post-state
733 comparison returns an error. A successful fresh branch therefore exposes all
734 those equalities and a successful \path{confirm}. The successor invariant
735 follows from \path{confirm_safe}. At the resulting checkpoint, the recorded
736 last commit, next sequence, and actual store view match the duplicate branch,
737 which returns the state unchanged.
738 \end{proof}
739 
740 These are \path{acknowledge_fresh_contract},
741 \path{acknowledge_safe}, and \path{acknowledge_idempotent} in
742 \path{AVOC/RobustQuoteRecovery.lean}. Duplicate acknowledgment recognizes
743 the already accepted commit and checkpoint. It does not freshly validate every
744 field of an independently supplied outcome argument on that replay branch.
745 This is appropriate for state replay but must not be described as new checking
746 of a second physical result.
747 
748 The \path{prepare} constructor selects the robust action and binds current
749 evidence into its intent. Acknowledgment alone does not prove that an arbitrary
750 supplied commit was originally produced by \path{prepare}. If the conclusion
751 needs provenance of the planner's choice, that provenance must be supplied or
752 established by the enclosing protocol. Fresh acknowledgment proves the exact
753 checked transition contract, not an unstated origin claim.
754 
755 Probability bands are frozen within the episode. Replacing them for a fresh
756 episode preserves the source and protected identity fields but changes the
757 approved evidence. An old intent cannot be acknowledged under the changed
758 evidence. The explicit declaration
759 \path{new_bands_obstruct_old_acknowledgement} in
760 \path{AVOC/CalibrationBridge.lean} prevents calibration from silently
761 rewriting an active durable operation.
762 
763 \subsection{Prepaid evaluation and upgrade journals}
764 
765 The separate durable-upgrade machine has a journal containing the current
766 upgrade state, one optional pending ticket, and closed tickets. A ticket binds
767 a campaign-local key, its complete parent state, and a proposal. Beginning a
768 funded fresh ticket charges its protected evaluation tariff immediately.
769 Repeating the same ticket is unchanged. Finishing it charges no second
770 evaluation tariff, and switching occurs only according to the checked upgrade
771 decision. Abandoning clears the pending ticket while retaining its already
772 charged evaluation expenditure.
773 
774 The upgrade authority supplies checker soundness and sound lower and upper
775 utility bounds for one fixed workload, objective, and unit convention. These
776 are explicit obligations in \path{AVOC/VerifiedUpgrade.lean}. Receiving a JSON
777 utility bound or an approval flag does not prove them.
778 
779 In particular, a failed or abandoned evaluation is not a free trial. The
780 complete parent state includes spending, so reusing a ticket based on an old
781 active version but ignoring changed expenditure is rejected. The formal
782 declarations \path{begin_keeps_active},
783 \path{finish_evaluation_unchanged}, and
784 \path{abandon_keeps_current} make these distinctions explicit.
785 
786 For a successful paid trace with total evaluation debit $e$ and switching debit
787 $u$, the formal accounting identities are
788 \begin{align}
789  \mathrm{evaluationSpent}_{\rm final}
790  &=\mathrm{evaluationSpent}_{\rm initial}+e,\\
791  \mathrm{switchSpent}_{\rm final}
792  &=\mathrm{switchSpent}_{\rm initial}+u.
793 \end{align}
794 From a safe initial journal, their sum stays within protected credits.
795 Successful replay also cannot decrease the protected utility of the active
796 version. These are \path{paid_trace_exact_accounting},
797 \path{paid_trace_no_overspend}, and
798 \path{replay_utility_nondecreasing} in
799 \path{AVOC/DurableUpgradeLaws.lean}.
800 
801 Restoration replays supplied commands from a specified initial version and
802 compares the result with the actual checkpoint. A successful restoration equals
803 that checkpoint. Provided the specified initial version satisfies the
804 authority's contract, restoration also inherits the safety certificate. This checks consistency
805 between two supplied records. It cannot authenticate their physical origin or
806 detect coordinated replacement of both the journal and checkpoint.
807 
808 \subsection{What recovery establishes about external execution}
809 
810 The lifecycle recorder is a pure finite snapshot reducer. Its once-only
811 terminal history is not exactly-once external execution. It neither invokes
812 an operation nor persists a crash-safe transaction. The recovery models give
813 checked state-transition and replay contracts, while the retained runtime and
814 storage adapters have their stated bounded evidence and external trust
815 assumptions. Filesystem durability, endpoint authentication, physical identity,
816 and reliable observation delivery are not consequences of a pure transition
817 function.
818 
819 A rejected pure batch supplies no final export. That is an all-or-nothing
820 reduction result, not rollback of physical work already performed before
821 rejection. A fault closes an intent without supplying a binary sample. It does
822 not establish that retrying the corresponding paid operation is safe or free.
823 Conservative reserved spending remains a protected model quantity rather than
824 an automatic identity with actual billed expenditure.
825 
826 The completed chain is therefore precise: under the declared finite source
827 model, the lifecycle machinery derives trustworthy prefix correspondence;
828 fixed scheduled calibration bounds bad issuance; on the simultaneous-coverage
829 event, every issued frozen episode has the proved value and policy guarantees;
830 outside that event, uncertified issuance has mass at most the scheduled total
831 allowance; and the checked recovery machines preserve their specified state
832 and accounting contracts. Physical source coupling,
833 universal host/storage refinement, multi-episode accumulation, and measured
834 productivity remain separate obligations.

Back to source controls

Back to AVOC