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{Representations, tasks, and retained distinctions}
2 \label{sec:representations}
3 
4 AVOC begins with an operational question about information: which distinctions must a retained artifact preserve so that a specified task can still be performed? The answer depends on the task. A representation that is adequate for one query can fail for another, and a representation that answers the current query can fail to support future controlled transitions. The formal development separates these obligations before assigning costs or probabilities.
5 
6 \begin{definition}[Deterministic refinement and task sufficiency]
7 Let $X$ be a raw state space and let $\phi:X\to Z$ and $T:X\to Y$ be functions. We write
8 \[
9  \phi\succeq T
10  \quad\Longleftrightarrow\quad
11  \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
12 \]
13 More generally, $\phi\succeq\psi$ means that $\psi$ factors through $\phi$. The relation is called refinement. The representation $\phi$ is task sufficient for $T$ when $\phi\succeq T$. Two representations are information equivalent when each refines the other.
14 \end{definition}
15 
16 The decoder is part of the assertion. It may be computationally expensive, and its existence alone supplies no efficient implementation. Refinement is reflexive, using the identity decoder, and transitive, by composition of decoders. Thus it is a preorder. Information equivalence is the associated equivalence relation. Neither relation compares the byte length, acquisition cost, or evaluation time of the representations.
17 
18 \begin{theorem}[Exact fiber criterion]
19 \label{thm:fiber-criterion}
20 Suppose $Y$ is nonempty. Then $\phi$ is sufficient for $T$ if and only if
21 \[
22  \phi(x)=\phi(y)\quad\Longrightarrow\quad T(x)=T(y)
23  \qquad(x,y\in X).
24 \]
25 In particular, a single pair with $\phi(x)=\phi(y)$ and $T(x)\ne T(y)$ proves insufficiency.
26 \end{theorem}
27 \begin{proof}
28 If $T=d\circ\phi$, equality of the two representations gives equality after applying $d$. Conversely, fix a default $y_0\in Y$. For every reachable $z\in\phi(X)$ choose $x_z$ with $\phi(x_z)=z$ and set $d(z)=T(x_z)$. Set $d(z)=y_0$ on unreachable representation states. The fiber hypothesis ensures that $T(x_z)=T(x)$ whenever $z=\phi(x)$, so $d(\phi(x))=T(x)$. The nonempty-codomain hypothesis supplies the default on unreachable states. The formal proof uses classical choice for the representatives.
29 \end{proof}
30 
31 The target $T$ itself is sufficient for $T$. Every sufficient representation refines $T$, by definition. Consequently $T$ is a canonical coarsest sufficient representation in this information preorder. A sufficient representation is task minimal when $T$ also refines it, and hence task minimality is exactly information equivalence with $T$. This is a statement about retained distinctions, rather than a theorem that the target can be computed cheaply or stored in a shortest file.
32 
33 \begin{proposition}[Finite data processing]
34 For a finite sample $D\subseteq X$, let $c_D(\phi)=|\phi(D)|$ denote the number of reached representation states. If $\phi\succeq\psi$, then
35 \[
36  c_D(\psi)\le c_D(\phi).
37 \]
38 \end{proposition}
39 \begin{proof}
40 Choose $d$ with $\psi=d\circ\phi$. Then $\psi(D)=d(\phi(D))$, and the image of a finite set under a function has cardinality at most that of the original set.
41 \end{proof}
42 
43 The finite sample serves only to count reached states. Sufficiency in Theorem~\ref{thm:fiber-criterion} is quantified over all of $X$. Agreement on a sample is therefore a different kind of evidence unless that sample exhausts the domain.
44 
45 \begin{example}[A task must be declared before compression]
46 Let $X=\{0,1\}^3$ and let $T(x_1,x_2,x_3)=x_1\wedge x_2$. The representation $\phi(x)=T(x)$ is sufficient for this target, although it discards $x_3$ and many distinctions among the first two coordinates. The representation $\psi(x)=x_1\oplus x_2$ is insufficient: $(0,0,0)$ and $(1,1,0)$ have the same $\psi$ value and different $T$ values. No decoder can repair this collision. Conversely, retaining all three coordinates refines $T$ but retains more information than this task requires.
47 \end{example}
48 
49 \subsection{Query families and joint targets}
50 
51 Suppose a family of tasks is given by $T_q:X\to Y$, indexed by $q\in Q$. Define the joint target
52 \[
53  T_{\mathrm{joint}}(x)=(T_q(x))_{q\in Q}\in Y^Q.
54 \]
55 Then $\phi$ is sufficient for the joint target if and only if it is sufficient for each individual task. The forward direction evaluates the decoded answer vector at $q$. For the reverse direction, choose a decoder $d_q$ for each query and define $d(z)(q)=d_q(z)$. The formal theorem permits an arbitrary query index type, and the simultaneous decoder selection uses classical choice.
56 
57 This distinction matters for reuse. An artifact can be minimal for one fixed target while a later target requires a distinction that the artifact discarded. A reusable library therefore needs a declared target family or an exact semantic key. Enlarging that family changes the sufficiency obligation. The framework does not infer the full future query family from the fact that past tasks succeeded.
58 
59 \section{Information value and finite Bayesian evidence}
60 \label{sec:information-value}
61 
62 An information ordering becomes a decision ordering only after specifying a prior, available actions, and utility. The source treats the prior and utility as declared mathematical inputs. In probabilistic applications the prior is normalized and nonnegative. Some structural decision identities need less and are proved even for arbitrary rational weights.
63 
64 \begin{definition}[Deterministic experiment value]
65 Let $\Omega$ be finite, $A$ be a finite nonempty action set, $b:\Omega\to\Q$ be a prior, and $u:\Omega\times A\to\Q$ be utility. For an observation $\phi:\Omega\to Z$ and policy $\pi:Z\to A$, define
66 \[
67  J_b(\phi,\pi)=\sum_{\omega\in\Omega}b(\omega)u(\omega,\pi(\phi(\omega))).
68 \]
69 When $Z$ is finite, write $J_b^*(\phi)=\max_{\pi:Z\to A}J_b(\phi,\pi)$.
70 \end{definition}
71 
72 \begin{theorem}[Deterministic information-value monotonicity]
73 If $\phi\succeq\psi$, then $J_b^*(\psi)\le J_b^*(\phi)$. If the acquisition costs satisfy $c_\phi\le c_\psi$, then
74 \[
75  J_b^*(\psi)-c_\psi\le J_b^*(\phi)-c_\phi.
76 \]
77 \end{theorem}
78 \begin{proof}
79 Let $d$ decode $\psi$ from $\phi$. Any coarse policy $\pi$ lifts to $\pi\circ d$. For every world the lifted policy chooses exactly the same action, so its decision value is unchanged. A maximizing coarse policy exists because the policy space is finite and nonempty. Its lifted value is at most the best fine value. Subtracting the stated costs gives the second inequality.
80 \end{proof}
81 
82 More information can increase gross decision value while decreasing net value if it costs more. The theorem's cost hypothesis is therefore essential to its domination conclusion. It also supplies a practical pruning rule: an experiment that is coarser and no cheaper can be removed from a finite decision menu without losing an optimum.
83 
84 \subsection{Stochastic observations and garbling}
85 
86 \begin{definition}[Finite rational channel]
87 A channel from $\Omega$ to a finite observation alphabet $O$ consists of rational entries $E(o\mid\omega)\ge0$ with $\sum_o E(o\mid\omega)=1$ for every $\omega$. Given a second channel $K(y\mid o)$, their composite is
88 \[
89  (EK)(y\mid\omega)=\sum_o E(o\mid\omega)K(y\mid o).
90 \]
91 The composite is a garbling of $E$.
92 \end{definition}
93 
94 The unnormalized signal-action score and policy value are
95 \[
96  S_E(o,a)=\sum_\omega b(\omega)E(o\mid\omega)u(\omega,a),
97  \qquad J_b(E,\pi)=\sum_o S_E(o,\pi(o)).
98 \]
99 This form avoids dividing by the evidence mass. In particular, it remains well defined on observations whose predictive probability is zero.
100 
101 \begin{theorem}[Finite stochastic information-value monotonicity]
102 Every deterministic policy on $EK$ is weakly dominated in value by some deterministic policy on $E$. Consequently the best deterministic value of $EK$ is at most that of $E$.
103 \end{theorem}
104 \begin{proof}
105 For each fine observation $o$, select $a_o\in A$ maximizing $S_E(o,a)$. Such a selection exists because $A$ is finite and nonempty. For a coarse policy $\pi$, expand the channel composition and rearrange finite sums:
106 \[
107  J_b(EK,\pi)=\sum_o\sum_y K(y\mid o)S_E(o,\pi(y)).
108 \]
109 Every inner score is at most $S_E(o,a_o)$. Nonnegativity and normalization of the row of $K$ give
110 \[
111  \sum_y K(y\mid o)S_E(o,\pi(y))\le S_E(o,a_o).
112 \]
113 Summing over $o$ proves domination by the fine policy $o\mapsto a_o$. Taking a best coarse policy yields the optimal-value comparison.
114 \end{proof}
115 
116 \begin{example}[Information has a price]
117 For two equally likely worlds, let the action predict the world and let utility be $1$ for a correct prediction and $0$ otherwise. A constant observation gives value $1/2$. Revealing the world gives value $1$. If revelation costs $1/8$, its net value is $7/8$, exceeding the free constant experiment's $1/2$. If it costs $3/4$, its net value is $1/4$. The information order is unchanged across these two cases, while the preferred paid experiment changes.
118 \end{example}
119 
120 \subsection{Exact Bayesian updates}
121 
122 A rational belief is a nonnegative vector $b$ on finite $\Omega$ with $\sum_\omega b(\omega)=1$. For a channel $E$, define the predictive mass
123 \[
124  p(o)=\sum_\omega b(\omega)E(o\mid\omega).
125 \]
126 For $p(o)>0$, the posterior is $b_o(\omega)=b(\omega)E(o\mid\omega)/p(o)$. The total updater in the source uses $b_o=b$ when $p(o)=0$. This fallback is normalized and has zero coefficient in predictive expectations. Nonnegativity of every summand implies that each Bayes numerator also vanishes on such an impossible observation. Hence, with the total-update convention, the division-free identity
127 \[
128  p(o)b_o(\omega)=b(\omega)E(o\mid\omega)
129 \]
130 holds on every branch. It follows that
131 \[
132  \sum_o p(o)\sum_\omega b_o(\omega)u(\omega,\pi(o))=J_b(E,\pi).
133 \]
134 Posterior-predictive evaluation and the unnormalized decision formula therefore agree exactly.
135 
136 For any nonnegative likelihood weight $L$, write
137 \[
138  M_b(L)=\sum_\omega b(\omega)L(\omega),\qquad
139  C_L(b)(\omega)=\frac{b(\omega)L(\omega)}{M_b(L)}
140 \]
141 when $M_b(L)>0$. Given nonnegative $L_1,L_2$ and positive successive evidence masses, the source proves
142 \[
143  M_b(L_1)M_{C_{L_1}(b)}(L_2)=M_b(L_1L_2),\qquad
144  C_{L_2}(C_{L_1}(b))=C_{L_1L_2}(b).
145 \]
146 These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires the appropriate joint likelihood model. In particular, multiplying likelihoods is justified by a stated factorization of the evidence law, rather than merely by the existence of two reports.
147 
148 \subsection{Compression must preserve the likelihood}
149 
150 \begin{theorem}[Conditioning commutes with exact compression]
151 Let $\phi:\Omega\to Z$ map between finite spaces, and define the pushforward belief $\bar b(z)=\sum_{\phi(\omega)=z}b(\omega)$. Suppose $L=\bar L\circ\phi$ for a nonnegative likelihood $\bar L:Z\to\Q$, and the evidence mass is positive. Then
152 \[
153  \phi_*C_L(b)=C_{\bar L}(\phi_*b).
154 \]
155 Such an exact $\bar L$ exists if and only if $L$ is constant on every fiber of $\phi$.
156 \end{theorem}
157 \begin{proof}
158 Grouping the normalizer by fibers gives $M_b(L)=M_{\bar b}(\bar L)$. On each fiber $\phi^{-1}(z)$, the likelihood can be factored outside the sum. Thus
159 \[
160  \sum_{\phi(\omega)=z}\frac{b(\omega)L(\omega)}{M_b(L)}
161  =\frac{\bar b(z)\bar L(z)}{M_{\bar b}(\bar L)}.
162 \]
163 The factorization criterion is Theorem~\ref{thm:fiber-criterion} applied to the rational-valued target $L$.
164 \end{proof}
165 
166 A prior compression that merges worlds with different likelihoods has no exact coarse likelihood for that observation. A later evidence update can consequently reveal a distinction that the compressed state no longer represents. This is the evidence version of the collision obstruction.
167 
168 \begin{example}[Rare evidence can reverse a posterior completely]
169 Under the uniform prior on $\{0,1\}$, take $L_0=(\varepsilon,0)$ and $L_1=(0,\varepsilon)$ with rational $\varepsilon>0$. The two likelihoods differ pointwise by at most $\varepsilon$, and both evidence masses equal $\varepsilon/2$. Their posteriors are respectively $(1,0)$ and $(0,1)$, with full $L^1$ distance $2$. Arbitrarily small positive likelihood perturbations therefore do not imply uniform pointwise posterior stability without an additional evidence condition. The later model-error chapter uses weighted continuation comparisons rather than identifying nearby posterior points as the same controller state.
170 \end{example}
171 
172 \section{Sufficiency for controlled futures}
173 \label{sec:control-sufficiency}
174 
175 For a one-shot task, refinement preserves sufficiency by decoder composition. A state abstraction for a controlled process has a second obligation: its fibers must remain compatible with the process's transitions. This extra obligation changes the mathematical behavior of refinement.
176 
177 \begin{definition}[Deterministic control sufficiency]
178 Let $A_0$ be a finite nonempty set of admissible actions, let $f:S\times A_0\to S$ be transition, and let $r:S\times A_0\to\Q$ be reward. A representation $\phi:S\to Z$ is control sufficient if, whenever $\phi(s)=\phi(t)$, every admissible action satisfies
179 \[
180  r(s,a)=r(t,a),\qquad \phi(f(s,a))=\phi(f(t,a)).
181 \]
182 The global action set is common to all states in this definition.
183 \end{definition}
184 
185 Define the finite-horizon values by
186 \[
187  V_0(s)=0,\qquad Q_n(s,a)=r(s,a)+V_n(f(s,a)),\qquad
188  V_{n+1}(s)=\max_{a\in A_0}Q_n(s,a).
189 \]
190 
191 \begin{theorem}[Exact preservation of controlled value]
192 If $\phi$ is control sufficient, then $V_n$ is constant on every fiber of $\phi$ for every $n\in\N$. The same is true of $Q_n(\cdot,a)$ for each admissible $a$, and Bellman-optimal action sets coincide within each fiber.
193 \end{theorem}
194 \begin{proof}
195 At horizon zero the values vanish. If $V_n$ is fiber constant and $\phi(s)=\phi(t)$, control sufficiency gives equal rewards and equal represented successors. Hence $Q_n(s,a)=Q_n(t,a)$ for every admissible $a$. Taking the maximum over the common action set proves equality of $V_{n+1}$. The action-value equality also makes all inequalities defining optimal action membership identical at $s$ and $t$.
196 \end{proof}
197 
198 \begin{example}[A finer representation can fail dynamic closure]
199 Consider $S=\{0,1,2\}$, one action, zero reward, and transitions $f(0)=0$, $f(1)=2$, $f(2)=2$. The constant representation is control sufficient. The finer representation with fibers $\{0,1\}$ and $\{2\}$ refines that constant representation, but it merges states $0$ and $1$ whose successors fall into different fine fibers. It is therefore not control sufficient. This example is retained as an explicit formal counterexample to arbitrary refinement monotonicity.
200 \end{example}
201 
202 The exact repair is simple: a refinement of a control-sufficient representation remains control sufficient if the finer representation is itself transition closed. Reward equality is inherited through the coarse decoder, while successor equality must be supplied for the fine representation. For models with state-dependent action sets, exact action feasibility is an additional obligation, handled by the guarded control interfaces later in the paper.
203 
204 \subsection{Projected stochastic laws}
205 
206 Let $S$ be finite and replace deterministic transition by rational probability rows $P_a(s,s')\ge0$ with $\sum_{s'}P_a(s,s')=1$. The stochastic Bellman recursion is
207 \[
208  V_0(s)=0,\qquad Q_n(s,a)=r(s,a)+\sum_{s'}P_a(s,s')V_n(s'),\qquad
209  V_{n+1}(s)=\max_{a\in A_0}Q_n(s,a).
210 \]
211 Equality of entire raw transition rows is sufficient for compression, but can demand more than the abstract process needs. The appropriate condition compares their projected laws.
212 
213 \begin{definition}[Projected stochastic control sufficiency]
214 A representation $\phi:S\to Z$ is projected stochastically sufficient if equal represented current states have equal immediate rewards and, for every admissible $a$ and every rational fiber-constant function $W:S\to\Q$,
215 \[
216  \sum_{s'}P_a(s,s')W(s')=\sum_{s'}P_a(t,s')W(s')
217  \quad\text{whenever }\phi(s)=\phi(t).
218 \]
219 \end{definition}
220 
221 When $Z$ is finite, this expectation condition is equivalent to equality of the mass sent to every abstract fiber:
222 \[
223  \sum_{\phi(s')=z'}P_a(s,s')=\sum_{\phi(s')=z'}P_a(t,s')\qquad(z'\in Z).
224 \]
225 To prove necessity, use the indicator of the fiber as $W$. To prove sufficiency, group the expectation by fibers and factor out the common value of $W$ on each nonempty fiber. Empty fibers contribute zero. These arguments explain why raw states may have distinct next-state probabilities while having identical controlled abstract behavior.
226 
227 \begin{theorem}[Exact stochastic quotient]
228 Suppose $\phi:S\to Z$ is surjective and projected stochastically sufficient, with $S,Z$ finite. Choose a representative $s_z$ of every fiber, and define
229 \[
230  \bar r(z,a)=r(s_z,a),\qquad
231  \bar P_a(z,z')=\sum_{\phi(s')=z'}P_a(s_z,s').
232 \]
233 These quantities give a normalized rational stochastic control system, independent of the representative choices for admissible actions. For every finite horizon,
234 \[
235  \bar V_n(\phi(s))=V_n(s).
236 \]
237 \end{theorem}
238 \begin{proof}
239 Nonnegative fiber masses give nonnegative quotient probabilities; partitioning $S$ by the fibers shows that each quotient row sums to one. Sufficiency makes reward and projected mass unchanged when replacing $s_z$ by another representative. Inductively assume the value equality at horizon $n$. Then
240 \[
241  \sum_{z'}\bar P_a(\phi(s),z')\bar V_n(z')
242  =\sum_{s'}P_a(s,s')V_n(s'),
243 \]
244 by projected equality and fiberwise grouping. Immediate rewards agree, so every action backup agrees. Taking the maximum over the common action set proves the next horizon. The zero-horizon case is immediate.
245 \end{proof}
246 
247 This result concerns exact finite models with a specified reward and transition law. It neither discovers the correct abstraction automatically nor identifies a supplied rational model with a physical system. Its role is to certify the consequences of a declared abstraction once the one-step obligations have been established.
248 
249 \section{Artifacts, identities, and proof-carrying admission}
250 \label{sec:artifact-identities}
251 
252 An artifact's semantic content and its operational identity serve different purposes. Semantic equivalence permits replacement in a declared task language. Operational identity prevents a receipt for one statement, dependency set, environment, or generation from authorizing another.
253 
254 The concrete binding layer uses a small data-only propositional language. Formulas contain numbered atoms, truth, falsity, conjunction, disjunction, and implication. Derivations contain the corresponding introduction and elimination rules. Atoms are interpreted as arbitrary propositions under a valuation $v:\N\to\operatorname{Prop}$. A recursive inference function either returns a formula or rejects. It accepts data representing a derivation, rather than executable tactics or imported source code.
255 
256 \begin{theorem}[Checker soundness]
257 If the inference checker accepts derivation $p$ for target $F$ under context $\Gamma$, then every valuation satisfying $\Gamma$ satisfies $F$.
258 \end{theorem}
259 \begin{proof}
260 Induct on the derivation. A used assumption belongs to $\Gamma$ and is true by the context hypothesis. Conjunction introduction combines the two inductive conclusions, and its projections select the corresponding conclusion. Implication introduction applies the induction hypothesis in the extended context; implication elimination applies a proved implication to a proved premise. The two disjunction injections construct the appropriate alternative. Case elimination applies the matching branch proof after extending the context with the observed alternative. Falsity elimination follows from the impossible proposition. The checker's shape and equality tests ensure that the formulas in these rules match exactly.
261 \end{proof}
262 
263 This is soundness of the defined propositional checker. It is not a universal ingestion theorem for arbitrary Lean source. Dependencies remain assumptions in the checker context, and their truth must come from the surrounding certified workflow.
264 
265 \begin{definition}[Protected artifact identity]
266 An identity records a task name, a formula, its statement-byte snapshot, a list of dependencies with their formulas and artifact-byte snapshots, and an environment snapshot. An artifact contains that identity, a source-byte snapshot, and a data-only derivation. A ticket consists of a generation number together with an artifact. A receipt names the exact ticket and records an approval bit.
267 \end{definition}
268 
269 All byte snapshots in this model are exact strings. No finite hash is assumed injective. The validator checks four obligations: the pending artifact's identity equals the current identity, the receipt names the exact pending ticket, its approval bit is true, and the derivation checks for the current target under the current dependency context. The resulting validation theorem supplies the target proposition whenever the dependency propositions hold.
270 
271 A changed statement, dependency, environment, source snapshot, or ticket generation is rejected by the corresponding equality gate. Approval alone supplies no proof. Re-registering an identical payload still changes its generation, which prevents an old receipt from serving as authorization for a new registration.
272 
273 The finite slot model increments its generation on registration. Successful admission consumes the pending ticket; failed admission leaves it unchanged. A successfully consumed receipt cannot admit again because no pending ticket remains. These statements describe admission in the defined reducer. They do not establish exactly-once performance of external paid work, filesystem durability, or authentication of an external provider. The recovery chapters treat the separate accounting and persistence obligations.
274 
275 \section{Certified Boolean synthesis and semantic reuse}
276 \label{sec:boolean-synthesis}
277 
278 The Boolean backend provides a complete finite example of semantic checking, cost-aware replacement, and retained computation. Its restricted language is deliberate: strong universal conclusions are possible because both the input domain and semantics are explicit.
279 
280 \subsection{Programs and their declared work}
281 
282 Programs are finite abstract syntax trees built from Boolean literals, three input variables, negation, conjunction, disjunction, and exclusive-or. The input domain is the eight triples in $\{0,1\}^3$. Let $N(p)$ be the tree-node count: each literal or variable contributes one, negation adds one to its child, and a binary constructor adds one to the sum of its child counts.
283 
284 The instrumented evaluator evaluates both children of a binary operation. A structural induction proves that its output equals the ordinary evaluator and that its visit count is exactly $N(p)$ for every input. Thus node count is a valid eager-traversal meter for this interpreter. It is not a short-circuit meter, hardware runtime, memory-allocation count, or Boolean circuit size with shared subexpressions.
285 
286 \begin{theorem}[Complete Boolean equivalence check]
287 Let $\sigma(p)$ be the eight output bits of $p$, in the fixed lexicographic input order. Then
288 \[
289  \sigma(p)=\sigma(q)\quad\Longleftrightarrow\quad
290  \forall x\in\{0,1\}^3,\ p(x)=q(x).
291 \]
292 The executable checker comparing all eight outputs is sound and complete.
293 \end{theorem}
294 \begin{proof}
295 Equality of signatures gives equality at every entry. Every possible input occurs in the enumerated list, so every input is covered. Conversely, pointwise equality makes the two mapped output lists equal. This is exhaustive finite checking, not a sampled approximation.
296 \end{proof}
297 
298 \subsection{Bounded grammar search}
299 
300 The initial grammar layer has five atoms: two literals and three variables. If a layer is $L$, expansion retains $L$, adds all negations, and adds all ordered pairs under each of the three binary operations. Let $M_d$ count emitted list entries at depth $d$. The source proves
301 \[
302  M_0=5,\qquad M_{d+1}=2M_d+3M_d^2.
303 \]
304 The entries can contain duplicates. The node bound is $B_0=1$, $B_{d+1}=2B_d+1$, and every expression of height at most $d$ occurs in the depth-$d$ list. In particular $M_1=85$ and $M_2=21845$.
305 
306 The search retains an incumbent equivalent to a reference. A candidate replaces it only when the complete checker passes and the candidate has strictly fewer nodes. Induction over the examined list proves preservation of equivalence and nonincrease of node count. The returned incumbent has node count at most that of every equivalent examined candidate.
307 
308 Generation is reserved before a layer is constructed. The declared generation charge is the sum of the layer-entry counts through the chosen depth. A candidate comparison is conservatively charged
309 \[
310  T(r,d)=8\bigl(N(r)+B_d+1\bigr).
311 \]
312 The examined prefix is limited by both a user trial cap and the remaining budget divided by $T(r,d)$. Its generation plus examination charge is proved at most the supplied budget. If the generation charge does not fit, search returns the original reference and incurs zero modeled search charge. If the entire layer fits both limits, the result is optimal among equivalent expressions of height at most $d$. A partial prefix provides optimality only over that prefix.
313 
314 \begin{example}[A smaller artifact need not repay its discovery]
315 The reference $\neg(\neg x_1\vee\neg x_2)$ has six nodes. The equivalent conjunction $x_1\wedge x_2$ has three. The archived depth-one search examines the complete 85-entry layer under its stated limits and returns the conjunction, with modeled search charge $6890$. Each eager evaluation subsequently saves three visits. A large deployment can repay the exploration cost; a single evaluation cannot. The synthesis theorem supplies semantic safety and a budget bound even in the unprofitable case, and the promotion layer separately checks the campaign economics.
316 \end{example}
317 
318 \subsection{Compaction preserves the search optimum}
319 
320 Semantic entries carry an expression, its complete eight-bit signature, its node count, and equations certifying the two cached fields. The index retains at most one representative of each signature and keeps a smallest representative among inserted expressions. There are at most $2^8=256$ entries, regardless of the size of the submitted list.
321 
322 \begin{proposition}[Recursive semantic coverage]
323 For every depth $d$, recursively expanding the retained representatives and compacting again preserves the smallest equivalent node count obtainable from the full uncompressed grammar layer at that depth, with the same reference fallback.
324 \end{proposition}
325 \begin{proof}
326 Compaction gives every input expression an equivalent retained representative of no greater node count. Equivalence is a congruence for each grammar constructor. Replacing either child by a no-larger equivalent representative therefore preserves the result and does not increase its node count. Negation has the same property. Induction on depth supplies semantic and cost coverage of the full grammar by recursive representatives. Conversely, every retained representative originates in the full grammar. These two inclusions in semantic-cost coverage give equal selected optimum costs.
327 \end{proof}
328 
329 This is a precise example of reusable knowledge reducing subsequent construction. It is finite semantic compaction with a proof of optimum preservation. It does not establish that arbitrary learned representations preserve future optimization problems. The instrumented construction separately records emitted entries, total node mass, and index probes; its declared tariff excludes several host costs, including allocation and serialization.
330 
331 \subsection{From bounded search to a global cost certificate}
332 
333 A complete finite semantic algebra supports a stronger conclusion than searching a deeper finite layer. Let $D$ be a semantic domain with interpretations of the Boolean constructors. A cost function $c:D\to\N$ is a lower certificate if it satisfies the constructor inequalities
334 \begin{align*}
335  c(\text{literal }b)&\le1,& c(\text{variable }j)&\le1,\\
336  c(\neg s)&\le c(s)+1,&
337  c(s\mathbin{\circ}t)&\le c(s)+c(t)+1
338  \quad(\circ\in\{\wedge,\vee,\oplus\}).
339 \end{align*}
340 
341 \begin{theorem}[Attained global semantic minimum]
342 \label{thm:semantic-minimum}
343 Suppose $c$ satisfies those inequalities and, for every semantic state $s$, a witness expression $w_s$ has semantics $s$ and node count $c(s)$. Then for every expression $p$ with semantics $s$,
344 \[
345  N(w_s)=c(s)\le N(p).
346 \]
347 No expression-height bound appears in this conclusion. Two such attained cost certificates have identical cost functions.
348 \end{theorem}
349 \begin{proof}
350 Structural induction proves $c(\operatorname{sem}(p))\le N(p)$. The leaf inequalities give the base cases. For a unary constructor, use its inequality and the child's induction hypothesis. For a binary constructor, use its inequality and both child hypotheses. Applying this lower bound to any expression with semantics $s$ and using the attained witness proves global minimality. For two certificates, apply each one's lower bound to the other's witness, obtaining both inequalities between their costs.
351 \end{proof}
352 
353 For the three-input Boolean backend, $D$ consists of all 256 truth signatures. A proposed bank must have exactly 256 rows. Each row's stored expression is checked for its exact signature and claimed node count, and the bank is checked against every unary and binary constructor inequality. An accepted bank therefore carries the hypotheses of Theorem~\ref{thm:semantic-minimum}. Its query returns a globally node-minimal expression within this entire Boolean tree grammar, including all finite heights.
354 
355 The distinction is substantive. A bounded search is global only within its examined language fragment. A checked closure bank certifies a lower bound for every expression by structural induction and supplies witnesses attaining that bound. The universal conclusion remains specific to the grammar, three-input semantics, and eager tree-node tariff. It does not claim unrestricted program minimization or optimal implementation on physical hardware.
356 
357 \section{Exact affine artifacts and complete finite probes}
358 \label{sec:affine-semantics}
359 
360 The affine backend extends exact semantic certification to infinite input domains. Its complete finite test is possible because the represented functions have a fixed algebraic form.
361 
362 \begin{definition}[Dimension-indexed affine signature]
363 Over a ring $R$, a signature from dimension $n$ to dimension $m$ is a pair $(A,b)$ with $A\in R^{m\times n}$ and $b\in R^m$, denoting $x\mapsto Ax+b$. Dimensions are part of the type. Composition and pointwise addition are
364 \[
365  (B,c)\circ(A,b)=(BA,Bb+c),\qquad
366  (A,b)+(A',b')=(A+A',b+b').
367 \]
368 \end{definition}
369 
370 \begin{theorem}[Complete zero-and-basis probes]
371 Two affine signatures $f,g:R^n\to R^m$ are equal if and only if they agree at $0$ and at every standard basis vector $e_j$. Thus $n+1$ vector probes establish equality on all inputs. A mismatch in signatures has a mismatch among these probes.
372 \end{theorem}
373 \begin{proof}
374 The zero probe identifies the offsets because $f(0)=b_f$. At $e_j$, the output is the $j$th matrix column plus the offset. After canceling the now-equal offsets, equality of the basis probes identifies every column. Equal coefficients give equal evaluations for all inputs. The mismatch assertion is the contrapositive.
375 \end{proof}
376 
377 The theorem is algebraic completeness, rather than empirical interpolation from arbitrary function values. Its premise is that both candidates belong to the affine language over the stated ring. Adding a nonlinear primitive changes the language and invalidates this probe argument unless a new completeness theorem is supplied.
378 
379 \begin{example}[The zero probe is necessary]
380 Over $\Q$, consider scalar maps $f(x)=x$ and $g(x)=2x-1$. They agree at the single basis vector $x=1$, but $f(0)=0$ and $g(0)=-1$. Omitting the zero probe would accept a false affine equivalence. Over a field, equality of the linear matrices alone also leaves arbitrary affine offsets unconstrained.
381 \end{example}
382 
383 \subsection{Typed normalization and safe contextual replacement}
384 
385 Typed programs combine affine atoms, identities, sequential composition, and pointwise addition. Composition connects only matching intermediate dimensions. An independent recursive execution semantics and coefficient-normalization semantics are defined. Structural induction proves
386 \[
387  \operatorname{eval}(\operatorname{normalize}(p),x)=\operatorname{run}(p,x)
388  \qquad\text{for all }x.
389 \]
390 Hence two programs are equivalent if and only if their normal signatures coincide. Decidable coefficient comparison is a sound and complete checker when equality in $R$ is decidable, as it is for the rational and finite-field executable examples.
391 
392 One-hole typed contexts permit replacement at arbitrary nesting depth. Equivalence is preserved under composition and pointwise addition, so plugging equivalent programs into such a context preserves its semantics. A declared additive nonnegative primitive tariff, with $m$ charged for adding two $m$-dimensional outputs, also makes contextual cost monotone: a no-more-expensive replacement cannot increase the whole context's declared cost. This is a compositional guarantee for the explicit syntax and tariff.
393 
394 \section{Fusion, rank certificates, and retargeted reuse}
395 \label{sec:affine-cost}
396 
397 An exact normal form can improve verification without improving evaluation. The affine backend therefore checks semantics and cost separately. Its dense arithmetic tariff is
398 \[
399  D(n,m)=m(2n+1),
400 \]
401 charging $n$ multiplications, $n$ accumulations, and one bias addition per output row. The coefficient-composition tariff is
402 \[
403  C(n,m,k)=2knm+D(m,k).
404 \]
405 These are declared scalar-operation tariffs. They exclude bit complexity, memory traffic, allocation, and physical timing.
406 
407 \subsection{Fusion has an amortization threshold}
408 
409 Replacing a composed program by one dense atom with its normalized coefficients preserves every output. Its per-call execution tariff becomes $D(n,m)$. The source's no-slower selector retains the original program whenever that dense tariff is greater than its current execution cost. Normalization work is charged separately for campaign comparisons.
410 
411 \begin{example}[Beneficial and harmful fusion]
412 A dense $2\to3\to2$ chain has per-call tariff $D(2,3)+D(3,2)=29$. Its fused $2\to2$ map costs $10$ per call, and coefficient composition costs $38$. Thus $38+10q\le29q$ exactly when $q\ge2$, with strict savings exactly when $q\ge3$.
413 
414 In contrast, a $4\to1\to4$ bottleneck costs $D(4,1)+D(1,4)=21$ per call, while its dense fused $4\to4$ form costs $36$. Fusion remains semantically correct but loses its cheap intermediate bottleneck. The cost-aware selector therefore keeps the original chain in that comparison.
415 \end{example}
416 
417 The second case motivates retaining a factorized artifact. A dense semantic key can identify a function while a different execution representation realizes it more cheaply.
418 
419 \subsection{An upper factorization and a lower rank witness}
420 
421 Work over a field $R$. For reference $f=(A,b):R^n\to R^m$, a candidate supplies an intermediate width $k$, first and second affine signatures
422 \[
423  a(x)=Ux+u_0,\qquad d(y)=Vy+v_0,
424 \]
425 and matrices $L\in R^{k\times m}$, $H\in R^{n\times k}$. The checker verifies
426 \[
427  VU=A,\qquad Vu_0+v_0=b,\qquad LAH=I_k.
428 \]
429 The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
430 
431 \begin{theorem}[Certified minimum affine width]
432 \label{thm:affine-width}
433 An accepted candidate has $k=\operatorname{rank}(A)$. Every exact two-stage affine factorization of $f$ through width $\ell$ satisfies $k\le\ell$. Under the dense two-stage tariff,
434 \[
435  F(n,m,k)=D(n,k)+D(k,m),
436 \]
437 the accepted candidate is no more expensive than any such two-stage factorization.
438 \end{theorem}
439 \begin{proof}
440 The upper factorization gives $\operatorname{rank}(A)=\operatorname{rank}(VU)\le k$. The lower witness gives
441 \[
442  k=\operatorname{rank}(I_k)=\operatorname{rank}(LAH)\le\operatorname{rank}(A).
443 \]
444 Thus rank equals $k$. Any exact factorization through $\ell$ has $\operatorname{rank}(A)\le\ell$, by the same upper rank inequality. Finally,
445 \[
446  F(n,m,k)=k(2n+1)+m(2k+1)
447 \]
448 is increasing in $k$, so minimum width gives minimum tariff in this class.
449 \end{proof}
450 
451 Exact factorization alone does not prove minimum width. A redundant factorization can be correct while failing to supply a valid $LAH=I_k$. Conversely, a lower rank witness alone does not prove that the proposed affine implementation has the correct offset. Both directions are needed.
452 
453 \begin{example}[A checked rank-one bottleneck]
454 In the archived finite-field example over $\mathbf F_5$, $A$ is the $4\times4$ all-ones matrix and $b=(1,2,3,4)$. The first stage computes $y=x_1+x_2+x_3+x_4$. The second emits $(y+1,y+2,y+3,y+4)$. Taking $L$ to select the first output coordinate and $H$ to select the first input coordinate gives $LAH=(1)$. The width-one factorization is therefore exact and width minimal.
455 
456 Its tariff is $9+12=21$, compared with dense cost $36$, saving $15$ per call. The declared factor-checking charge is $105$. For this already atomic reference, the campaign inequality is exactly
457 \[
458  105+g\le15q,
459 \]
460 where $g$ is the declared generation work and $q$ the deployment count. With $g=0$, seven calls break even. Generation, validation, and deployment are all visible in this comparison.
461 \end{example}
462 
463 The menu selector compares three equivalent implementations: the current program, its dense fused atom, and the accepted minimum-width two-stage plan. Its selected tariff is exactly
464 \[
465  \min\{\operatorname{cost}(p),\ D(n,m),\ F(n,m,k)\}.
466 \]
467 This proves a minimum over the explicit menu, and also comparison with every exact two-dense-stage factorization. It does not prove a globally cheapest affine program in the larger language. Sparse schedules, sharing, special primitives, and hardware-specific algorithms have different admissible implementations or tariffs. An identity program already costs zero in this syntax and remains preferable to a paid dense factorization.
468 
469 \subsection{Reuse under a changed offset}
470 
471 Suppose a stored candidate has been validated for $(A,b)$ and a later target is $(A,b')$ with exactly the same linear matrix. Keep $U,u_0,V,L,H$ and replace only the second-stage offset by
472 \[
473  v_0'=b'-Vu_0.
474 \]
475 Then $VU=A$ is unchanged, $Vu_0+v_0'=b'$, and $LAH=I_k$ remains true. The same width and two-stage tariff are retained. A second retargeting overwrites the offset rather than accumulating prior offset changes.
476 
477 The import gate rechecks the entire stored certificate and exact equality of the current linear semantic key before constructing the retargeted checked record. It rejects invalid saved certificates and changed linear matrices. The current implementation is then compared with the reused plan, so a previously beneficial plan is not automatically preferred after other implementation changes.
478 
479 This is an exact reuse theorem for a specified invariant key. It shows which part of the calculation is reusable and which part must be adapted. Persisting a claimed certificate, trusting a previous receipt, or comparing a suggestive task label would not provide these hypotheses. The proof-carrying bank and the protected artifact workflow supply complementary mechanisms for making that distinction explicit.

Back to source controls

Back to AVOC