Self-Improving Intelligence

Download original file

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

Read the typeset paper

1 % New theoretical companion. Prior manuscripts are unchanged.
2 \documentclass[11pt,letterpaper]{article}
3 \usepackage[margin=1in,headheight=15pt]{geometry}
4 \usepackage[T1]{fontenc}
5 \usepackage[utf8]{inputenc}
6 \usepackage{newtxtext}
7 \usepackage{microtype}
8 \usepackage{amsmath,amsthm,mathtools}
9 \usepackage{newtxmath}
10 \usepackage{booktabs,array,longtable,tabularx,graphicx,tocloft}
11 \usepackage{enumitem,fancyhdr,titlesec,needspace,placeins}
12 \usepackage{xcolor}
13 \definecolor{ink}{HTML}{172A44}
14 \definecolor{muted}{HTML}{5B6778}
15 \usepackage[pdfencoding=auto,psdextra]{hyperref}
16 \usepackage{bookmark}
17 \hypersetup{hidelinks,pdftitle={Self-Improving Intelligence: Representation, Discovery, and Recursive Revision},pdfauthor={Komorebi P.},pdfsubject={A first-edition theory of representation discovery, recursive acquisition, and applicable revision certificates},pdfkeywords={recursive self improvement, general intelligence, representation discovery, repair, metaproductivity}}
18 \pagestyle{fancy}\fancyhf{}
19 \fancyhead[L]{\small\textsc{Self-Improving Intelligence}}
20 \fancyhead[R]{\small First edition, 2026}
21 \fancyfoot[C]{\thepage}
22 \renewcommand{\headrulewidth}{0.3pt}
23 \titleformat{\section}{\large\bfseries}{\thesection}{0.65em}{}
24 \titleformat{\part}[display]{\Large\bfseries}{\partname\ \thepart}{.4em}{}
25 \titlespacing*{\part}{0pt}{0pt}{1.6em}
26 \titleformat{\subsection}{\normalsize\bfseries}{\thesubsection}{0.65em}{}
27 \titlespacing*{\section}{0pt}{2.5ex plus .4ex}{1.2ex}
28 \titlespacing*{\subsection}{0pt}{1.8ex plus .3ex}{.8ex}
29 \setlength{\parindent}{1.2em}\setlength{\parskip}{.24em}
30 \setlength{\emergencystretch}{2em}
31 \clubpenalty=10000\widowpenalty=10000\displaywidowpenalty=10000
32 \setlength{\textfloatsep}{18pt plus 2pt minus 2pt}\raggedbottom
33 \setlist{leftmargin=1.5em,topsep=.4em,itemsep=.25em,parsep=0pt}
34 \setcounter{tocdepth}{1}\setlength{\cftbeforesecskip}{.2pt}\setlength{\cftbeforepartskip}{2pt}
35 \theoremstyle{plain}
36 \newtheorem{theorem}{Theorem}[section]
37 \newtheorem{proposition}[theorem]{Proposition}
38 \theoremstyle{definition}
39 \newtheorem{definition}[theorem]{Definition}
40 \newtheorem{counterexample}[theorem]{Counterexample}
41 \newtheorem{example}[theorem]{Example}
42 \newcommand{\X}{\mathcal X}\newcommand{\Z}{\mathcal Z}
43 \newcommand{\U}{\mathcal U}\newcommand{\Q}{\mathcal Q}
44 \newcommand{\Y}{\mathcal Y}\newcommand{\C}{\mathcal C}
45 \newcommand{\M}{\mathcal M}\newcommand{\E}{\mathbb E}
46 \newcommand{\Ffive}{\mathbb F_5}\newcommand{\TV}{d_{\mathrm{TV}}}
47 \newcommand{\img}[1]{\operatorname{im}(#1)}
48 \newcommand{\Eq}{\equiv_{\C}}\newcommand{\supp}{\operatorname{supp}}
49 \newcommand{\code}[1]{\texttt{\small #1}}
50 \newcolumntype{P}[1]{>{\raggedright\arraybackslash}p{#1}}
51 
52 \newcommand{\B}{\mathcal B}\newcommand{\Rcal}{\mathcal R}\newcommand{\Gcal}{\mathcal G}
53 \newcommand{\Safe}{\mathsf{Safe}}\newcommand{\Post}{\operatorname{Post}}\newcommand{\Pareto}{\operatorname{Pareto}}
54 \begin{document}
55 \hypersetup{pageanchor=false}
56 \begin{titlepage}\thispagestyle{empty}
57 \vspace*{.25in}
58 \noindent{\color{muted}\small\textsc{Operation Komorebi}\hfill\textsc{Theoretical research manuscript}}\par
59 \vspace{.65in}
60 \noindent{\color{ink}\fontsize{34}{39}\selectfont\bfseries Self-Improving\\Intelligence\par}
61 \vspace{.19in}
62 \noindent{\fontsize{17}{22}\selectfont Representation, Discovery,\\and Recursive Revision\par}
63 \vspace{.27in}\noindent{\color{ink}\rule{\textwidth}{.85pt}}\par
64 \vspace{.16in}
65 \noindent\textbf{Komorebi P.}\hfill\textit{First consolidated edition}\\
66 \noindent 8 October 2026\hfill Version 1.0.0\par
67 \vspace{.38in}
68 \noindent{\color{ink}\large\bfseries Abstract}\par\smallskip
69 \noindent Improving a solver is not the same as improving the procedure that produces its successors. This first edition develops a contract-relative account in which representations, experiments, repair languages, evidence, and costs remain explicit as discovery procedures change. Exact finite synthesis produces diagnostic policies with execution and complete-storage guarantees, including uncertainty about one fixed experiment model. A checked compiler shortcut avoids exhaustive search when a candidate attains proved lower bounds. A counterexample-guided learner then synthesizes an internal pruning rule. A further acquisition procedure constructs a proof-checked equation library that reduces later synthesis work while preserving the exact candidate and counterexample transcript. Repair-relative weight certificates extend the diagnostic method beyond singleton-success repairs. The final integration tracks which guarantees remain applicable when semantics, grammar order, repairs, witnesses, or resource prices change. A complete resource ledger separates preservation of meaning from reductions in particular event counts and from end-to-end improvement. The contribution is an integrated theoretical framework, conditional proofs, and executable finite witnesses. It does not establish general intelligence, autonomous invention of its trusted substrate, or indefinite recursive acceleration.
70 \vfill\noindent\rule{\textwidth}{.4pt}\par\smallskip
71 \noindent{\color{muted}\small\textbf{Scope.} Self-contained mathematical arguments and exact finite reference constructions. Prior experimental histories are not used as evidence for the proposed integrated system. First edition freezes this theoretical scope. Independent peer review and proof-assistant verification are not claimed.}
72 \end{titlepage}
73 \hypersetup{pageanchor=true}\pagenumbering{roman}
74 \begingroup\small\setlength{\parskip}{0pt}\tableofcontents\endgroup\clearpage
75 \section*{Reading the first edition}\addcontentsline{toc}{section}{Reading the first edition}
76 The central question is what has changed when a system becomes better at making itself better. More stored answers can improve a solver without improving its learning procedure. A richer repair language can make a correction expressible without making it discoverable. An improved search procedure can find useful corrections without establishing that its own descendants will search better still. The paper keeps these distinctions visible within one account.
77 
78 A conceptual reading can follow Sections~\ref{sec:introduction}--\ref{sec:world}, the interpretations after the formal results, and Part~\ref{part:architecture}. A mathematical reading proceeds through diagnosis and uncertain-model synthesis, then certified compiler revision, grammar synthesis, acquired search quotients, repair-relative certificates, sequential evidence, and recursive progress. Part~\ref{part:release-contract} binds the guarantees to their changing inputs and consolidates the resource ledger. The running instrument is finite and inspectable. Appendix~\ref{app:trace} gives a complete diagnostic trace, and the source package contains the parent and descendant compilers, frozen procedure, rule-synthesis, and equation-library records, exact checks, and an itemized review record.
79 
80 \paragraph{Relation to earlier work.}
81 \emph{Machine Understanding} specifies what representations must preserve across inquiry and explanation~\cite{understanding}. \emph{Stratified Recursive Improvement Closure} (SRIC) supplies the earlier distinction between task, improvement-process, and epistemic improvement, together with repair transport and evidence-preserving lineages~\cite{sric}. Neuralese and Operator-Symbolic Language (OSL) distinguish provisional latent computation from an explicit semantic interface~\cite{neuralese,osl}. This paper consolidates their theoretical roles. It neither reproduces their experimental histories nor imports a complete-system claim from them. Every formal statement used below is proved here or identified as a cited foundation.
82 
83 \paragraph{What is new in this manuscript.}
84 The proposed integration makes the improvement procedure itself a charged, transferable computational object. Its observations must support an appropriate repair, its decisions must fit one executable policy, and its acceptance must refer to a preserved evaluation contract. The finite constructions sharpen those obligations. Partition refinement, decision trees, dynamic programming, statistical concentration, and simulation arguments have classical foundations. Their appearance here is not a priority claim for the underlying mathematics.
85 
86 \paragraph{Conventions.}
87 The principal constructive models are finite and deterministic. A stochastic law appears only with an explicit probability model. A protected predicate means a declared operational constraint, not a proof of moral adequacy. An exact reference check verifies the implemented finite case. A proof supplies the general conditional argument. No benchmark score, test count, or version number substitutes for the other.
88 
89 \begin{center}\small
90 \begin{tabularx}{\textwidth}{@{}lX@{}}\toprule
91 Symbol & Meaning\\\midrule
92 $S$, $U$, $L$ & A target solver, an improvement procedure, and a reusable library.\\
93 $\Xi$, $B$ & An evaluation contract and its resource allowance.\\
94 $\Rcal_\Xi(U,L;B)$ & Expected improvement produced by the procedure, not an oracle over its unselected candidates.\\
95 $B_0\subseteq X$ & Possible current states of a finite repair problem.\\
96 $e$, $r$, $P$ & An experiment, a terminal repair, and an executable diagnostic tree.\\
97 $F_h(B_0)$ & Nondominated execution/storage pairs for successful trees of depth at most $h$.\\
98 $\sigma$, $\tau$ & Correspondences of states and operations in a declared transfer.\\
99 $\mathcal K$, $W_{h,k}$ & A safe continuation set and states guaranteeing $k$ progress events within $h$ attempts.\\\bottomrule
100 \end{tabularx}\end{center}
101 \clearpage
102 \section*{First-edition scope and dependency guide}\addcontentsline{toc}{section}{First-edition scope and dependency guide}
103 This edition closes an editorial and mathematical scope, not the open problem of general intelligence. It develops one finite chain in which a solver, its diagnostic compiler, an internal search rule, and the representation used to acquire such rules are separate objects. Each generated object is accompanied by the assumptions needed to interpret it.
104 
105 \begin{center}\small
106 \begin{tabularx}{\textwidth}{@{}p{.23\textwidth}XX@{}}\toprule
107 Layer & Constructed or acquired here & Still supplied\\\midrule
108 Repair & Executable diagnostic tree & Experiment model and successful-repair meanings.\\
109 Compiler & Selected or pruned discovery procedure & Candidate skeletons, lower-bound proofs and witness checker.\\
110 Rule acquisition & Arithmetic pruning expression and counterexamples & Grammar, feature registry and teacher.\\
111 Acquisition representation & Checked equations and ordered representatives & Arithmetic semantics, primitive proof rules and equation learner.\\
112 Continuing validity & Replayed certificates and explicit invalidation & Dependency-complete registry and sound local checking base.\\\bottomrule
113 \end{tabularx}\end{center}
114 
115 The principal formal dependency runs from finite repair synthesis to transport and guarded compiler revision, then from sound equations to ordered-trace preservation, and finally to composition of the acquired rule with the diagnostic compiler. Repair-weight pruning is a separately scoped extension, not a consequence of the singleton certificate. Statistical lineage evidence and resource inequalities add independent premises to any claim of repeated improvement.
116 
117 \paragraph{How to interpret the demonstrations.}
118 The finite programs generate or acquire the indicated objects. Their control problems and arithmetic languages are analytical constructions. Exact checks test the implemented domains; prose proofs establish the general conditional statements. No historical agent experiment supplies a missing premise. A smaller event count is not a universal runtime result, and a generated rule is not evidence that its teacher or proof language invented itself.
119 
120 \paragraph{Review route.}
121 Read Sections~\ref{sec:contract}, \ref{sec:synthesis}, \ref{sec:ordered-quotient}, \ref{sec:meta-chain}, \ref{sec:certificate-life}, and \ref{sec:integrated-ledger} for the connected core. The supplied statement review identifies the premises and proof route for every formal result. The source map records the actual depth of reference checking. Open questions in Section~\ref{sec:limits} remain open research within the program rather than unfilled requirements for this edition.
122 \clearpage\pagenumbering{arabic}
123 \part{The object that improves}
124 \section{From a better answer to a better investigator}\label{sec:introduction}
125 A system encounters a failure, changes its representation, and succeeds on the next attempt. Something useful has happened. The system may have learned a fact, recovered a missing variable, or selected a more suitable operation. Yet the next unfamiliar failure may leave it no better equipped than before. It has a repaired answer without a reusable account of repair.
126 
127 A stronger change would preserve the way the failure was investigated. The system might discover that its representation merged two situations with different future consequences. It might learn to seek an observation that separates those situations, to reject an inadequate family of repairs, or to reuse a diagnostic method in another notation. The object retained is then not merely a solution. It is part of a procedure for acquiring solutions.
128 
129 The recursive question begins one step further out. Can the system improve that procedure, use the revised procedure to construct another improvement, and retain a defensible comparison across those changes? The question is not answered by putting an agent's source code in its own context. Editability is an affordance. Productive revision is a property of what the permitted edits actually achieve.
130 
131 We take general intelligence as a motivating problem rather than a theorem premise. A broad reasoner should acquire useful capabilities across substantially different tasks without receiving their solutions inside an uncharged interpreter. Chollet's account of skill-acquisition efficiency emphasizes scope, priors, and experience rather than demonstrated skill alone~\cite{chollet}. Our narrower contribution concerns one possible mechanism behind such acquisition: reusable procedures for diagnosing failures, choosing informative actions, constructing corrections, and preserving their scope.
132 
133 \subsection{Three distinct achievements}
134 \emph{Task improvement} changes how well a solver performs a declared task. \emph{Process improvement} changes how effectively an improvement procedure produces useful solvers from comparable starting conditions. \emph{Epistemic improvement} changes how reliably the evaluation process distinguishes genuine gains from misleading evidence. This separation is inherited from SRIC~\cite{sric}. A system can advance on one axis without advancing on the others.
135 
136 A larger archive, for example, can improve retrieval while the procedure that extends the archive remains unchanged. A stronger checker can reject more invalid proposals while producing no additional valid proposals. A faster search may exploit a defect in its evaluation. None of these possibilities makes improvement meaningless. They identify the claim that must be tested.
137 
138 Recursive improvement also differs from sustained acceleration. A sequence of positive gains can converge to a finite limit. A sequence of better algorithms can consume increasing development costs. A procedure can improve on one task family and deteriorate on another. The substantive claim is not that a feedback loop exists, but that the loop produces useful and transferable changes under a stable comparison.
139 
140 \subsection{The route developed here}
141 The paper moves from representational failure to a finite repair problem, from that problem to a compiled procedure, and from the procedure to transferable and statistically accountable improvement. It then treats the succession of procedures as another finite control problem. This last step makes a common quantifier visible: the system needs one policy that can carry its claims forward, not a different hypothetical policy for every desired property.
142 
143 The route does not require every useful correction to be formally proved beneficial on all future tasks. Exact semantic certificates and statistical performance evidence have different jobs. Nor does it require each system to invent its own computational substrate. A finite search language may be supplied. The theory must disclose what that language already makes possible and what the learner actually selects or extends.
144 
145 \begin{figure}[!ht]\centering
146 \includegraphics[width=.96\linewidth]{figures/two_loops.pdf}
147 \caption{The inner process repairs a solver. The outer process changes how repair is attempted. Arrows indicate proposed information flow, not an implemented neural agent.}\label{fig:loops}
148 \end{figure}
149 
150 \section{Related work and the proposed contribution}\label{sec:related}
151 Learning how to learn has a substantial history. Learned optimizers can acquire update rules from optimization problems~\cite{andrychowicz}. Model-Agnostic Meta-Learning trains parameters from which a small number of updates can adapt to a new task~\cite{maml}. These approaches show why adaptation mechanisms deserve direct study. Neither the phrase meta-learning nor the presence of an outer objective, by itself, establishes an indefinitely improving outer procedure.
152 
153 DreamCoder couples learned program libraries to neural search guidance~\cite{dreamcoder}. Its relevance is the interaction between a language for expressing solutions and the ability to search that language. SEAL instead learns to produce adaptation data and update directives whose value is evaluated after the resulting parameter update~\cite{seal}. These are different places at which an improvement process can become learnable.
154 
155 The G\"odel-machine formulation treats a self-rewrite as admissible after a proof of usefulness within encoded assumptions~\cite{goedel}. The Darwin G\"odel Machine uses empirical evaluation and an archive of modified coding agents~\cite{dgm}. They should not be conflated. A proof-based criterion and a benchmark-based criterion support different guarantees and have different costs.
156 
157 More recent systems sharpen the distinction between a task agent and its modifier. Hyperagents makes both roles editable and studies transfer of improvement strategies~\cite{hyperagents}. Its reported experiments include improvements to modification procedures and transfer across tested domains. The archived variants and their selection protocol remain part of the evaluation setup. The general expressiveness of the editable program is not itself evidence that efficient discovery occurs on every computable task.
158 
159 The September 2026 AIDE$^2$ preprint studies repeated modification of a research agent's harness and reports transfer beyond its selection tasks~\cite{aide}. Its separate comparison of a discovered agent as an outer-loop improver is explicitly inconclusive relative to the strong reference. This distinction is directly relevant: improvements in research performance and improvements in driving the next improvement loop are related hypotheses, not interchangeable observations. These public works are research context. Their empirical findings are not treated as evidence for the architecture proposed here.
160 
161 Causal abstraction provides a formal account of mechanism-preserving interpretation~\cite{geiger}. Adaptive data analysis studies why repeated access to evaluation information can invalidate ordinary statistical reasoning~\cite{dwork}. Both are necessary neighbors. A self-improver must know what its representations mean and what its evidence permits it to conclude.
162 
163 
164 \subsection{What this paper adds to that discussion}
165 The intended contribution is an integrated realization contract. A candidate improvement identifies its target, information access, experiment family, repair language, controller, retained evidence, and charged resources. It also identifies the comparison under which the procedure itself is said to improve. The exact results concern finite cases of that contract. The architectural hypotheses concern whether learned proposal and acquisition mechanisms can satisfy it economically on wider tasks.
166 
167 This is not a claim that program libraries, recursive search, causal abstraction, or guarded updates originated with Komorebi. The aim is to connect them without allowing the cost or uncertainty of one stage to disappear inside another. A valid final repair is weaker than a valid procedure for finding it. A transferable repair is weaker than a transferable investigation. A safe accepted edge is weaker than a lineage with a continuing path to further improvement.
168 
169 \section{A protected comparison for improvement procedures}\label{sec:contract}
170 Let $S$ denote a solver implementation, $U$ an improvement procedure, and $L$ the library available to that procedure. The distinction is functional rather than physical. They may occupy one executable program. Their different roles are retained so that changes can be attributed rather than hidden in a single checkpoint name.
171 
172 \begin{definition}[Improvement contract]\label{def:contract}
173 A contract $\Xi$ specifies a distribution $\mathcal H$ of starting-solver/task pairs, an initial information and library boundary, permitted observations and modifications, a resource allowance $B$, protected predicates, and an evaluation rule $J_\tau(S)\in[0,1]$. The improvement procedure returns one selected descendant or the unchanged baseline. Selection must use only the admitted development information. The final evaluation is not available as an oracle for choosing retrospectively among all candidates.
174 \end{definition}
175 
176 Write $U(S,\tau,L;B)$ for the selected result, including the procedure's randomness where applicable. Its productivity is
177 \begin{equation}\label{eq:productivity}
178 \Rcal_\Xi(U,L;B)=\E_{(S,\tau)\sim\mathcal H}
179 \big[J_\tau(U(S,\tau,L;B))-J_\tau(S)\big].
180 \end{equation}
181 Invalid execution and out-of-budget behavior receive the treatment fixed by $\Xi$, not an exclusion chosen after seeing the outcome. The score may be a primary coordinate of a larger profile. Resource, validity, and group-specific constraints need not be folded into one scalar.
182 
183 The value in~\eqref{eq:productivity} lies in $[-1,1]$. A procedure that may return the baseline need not achieve a nonnegative true value: noisy selection can still choose a worse descendant. A nonnegative certificate requires additional evidence. The mere existence of a fallback does not make every selector good at using it.
184 
185 \subsection{Fixed-library and full-system comparisons}
186 A comparison of $\Rcal_\Xi(U',L;B)$ with $\Rcal_\Xi(U,L;B)$ isolates process change at a common library. A comparison with $(U',L')$ measures the combined descendant. Both are useful, but they answer different questions. A crossed comparison of $(U,L)$, $(U',L)$, $(U,L')$, and $(U',L')$ can expose interaction between procedure and library. There is no general additive decomposition that makes their contributions independent.
187 
188 The same discipline applies to base models, training histories, tools, and stored controllers. A changed foundation model is a changed component. A foreign-agent test must supply a valid adapter or charge discovery of one. Calling two targets unfamiliar does not make them distributionally independent of the development process.
189 
190 \begin{counterexample}[More knowledge without a better improver]\label{ex:library}
191 Consider four equally likely task names. A fixed procedure returns a stored solution when one exists and otherwise leaves the solver unchanged. A library containing one answer yields a smaller expected gain than a library containing all four. The procedure has not changed. Holding the library fixed gives identical productivity for the two copies of the procedure. The full system improved, but this example contains no improvement of the improvement rule.
192 \end{counterexample}
193 
194 \subsection{What persists across a recursive step}
195 A lineage state can be written schematically as
196 \[
197 Z_t=(S_t,U_t,L_t,E_t,\Xi_t,\rho_t),
198 \]
199 where $E_t$ records evidence and rejected alternatives, and $\rho_t$ records remaining resources and scope. A proposed modification may target any admitted subset. A comparison across different $\Xi_t$ needs a declared bridge. It cannot be justified merely because both scores are called accuracy.
200 
201 The public record should distinguish which changes were selected by the system, which were supplied by an external designer, and which were only proposed. A successful finite search within a fixed grammar is a genuine computational result. It is not evidence that the grammar was invented, that a broader domain was covered, or that the outer search process improved itself.
202 
203 \section{A small world with reusable diagnostic structure}\label{sec:world}
204 Consider eight cells with exactly one latent defect, indexed by $j\in\{0,\ldots,7\}$. The solver must repair that cell while preserving the others. Its old representation retains only the number of defects, so every episode initially looks identical.
205 
206 A diagnostic query names a subset $A$ and returns $\mathbf 1\{j\in A\}$. The reference language contains eight singleton queries and three bit-coordinate queries. Repair $r_i$ succeeds exactly when $i=j$. Because repair is irreversible within the episode, a procedure may commit only when every surviving possibility justifies its choice. Otherwise it may continue investigating or abstain.
207 
208 The model is fully declared. Setting each known cell as the defect on a calibration copy would permit learning the complete query table in $8(8+3)=88$ observation calls. The code instead generates that table from the analytical specification and records it as supplied information. It does not claim to have executed those calibrations or inferred a hidden environment.
209 
210 Equality-first testing asks whether $j=0$, then $j=1$, and so on. Its worst case needs seven queries, identifying the last cell by elimination. The three bit-coordinate queries need only three. Each procedure then performs one repair. Both complete binary trees have eight leaves and fifteen stored records. Faster execution has not made the controller free.
211 
212 
213 \clearpage\part{Discovering and transporting repair}
214 \section{A residual constrains a diagnosis}\label{sec:diagnosis}
215 A residual records disagreement between a prediction and an observation, between a proposed operation and a required invariant, or between two routes of translation. It is evidence against a conjunction of assumptions. It does not uniquely identify which assumption failed.
216 
217 For example, an unexpected output can arise because a state variable was discarded, a transition was modeled incorrectly, the observation was noisy, or an action had a side effect omitted from the model. These explanations can agree on the current discrepancy and disagree about the next useful experiment. An automatic instruction to enlarge the representation after every error would confuse missing information with faulty dynamics.
218 
219 Let a hidden case $\theta$ determine a set $\mathcal R(\theta)$ of successful repairs. The set may have several members. Diagnosis need only obtain enough information to choose a repair in the appropriate set. It need not identify every hidden property of $\theta$.
220 
221 \begin{proposition}[Feedback indistinguishability limits repair]\label{prop:indistinguishable}
222 Suppose two cases have disjoint successful-repair sets and induce transcript laws $P_0,P_1$ under a fixed admitted investigation protocol. A repair selector observes only the transcript and independent private randomness. Under equal prior probabilities, its average probability of successful repair is at most
223 \[
224 \frac{1+\TV(P_0,P_1)}2.
225 \]
226 In particular, identical transcript laws rule out certain success in both cases.
227 \end{proposition}
228 \begin{proof}
229 From the selected repair construct a binary decision: report case zero if the repair belongs to $\mathcal R(0)$, and case one otherwise. Success in case zero implies a correct decision. Success in case one also implies a correct decision because the two repair sets are disjoint. Thus repair success is at most the success of this binary test. For a randomized test with probability $f(o)\in[0,1]$ of reporting zero, the latter success is
230 \[
231 \tfrac12\big(1+\E_{P_0}f-\E_{P_1}f\big)
232 \leq\tfrac12(1+\TV(P_0,P_1)).
233 \]
234 The inequality follows by summing the positive differences of the two finite probability laws. The same argument applies to any measurable transcript space with the usual total-variation definition.
235 \end{proof}
236 
237 The bound concerns the entire transcript, not each observation marginal in isolation. Correlations between observations can identify a case even when every separate marginal is uninformative. Randomized action selection is already covered when it is part of the declared protocol and its observable record.
238 
239 Nor does the bound identify the most informative protocol. The learner must choose experiments before receiving their outcomes. A protocol that distinguishes the cases may exist while being inadmissible, too expensive, or absent from the current language. The finite synthesis below makes those possibilities separate outcomes.
240 
241 \subsection{Repair sufficiency is not full identification}
242 Suppose $\mathcal R(\theta_1)=\{a,c\}$ and $\mathcal R(\theta_2)=\{b,c\}$. The cases are distinct, yet repair $c$ works in both. A method can stop without learning which case occurred. Conversely, pairwise overlap of repair sets does not guarantee one repair for an entire uncertainty set. The three sets $\{a,b\}$, $\{b,c\}$, and $\{a,c\}$ intersect pairwise and have empty total intersection. The stopping condition must refer to the whole surviving set.
243 
244 This matters for representation discovery. A useful latent state may preserve exactly those distinctions needed for future repair decisions rather than every property of the underlying process. Whether that state remains sufficient after new repair operations become available is a separate question.
245 
246 \subsection{Repairing a failed representation}
247 Let $X$ be a finite set with deterministic operations $F_u:X\to X$ and output labels $q(x)$. Begin with a partition $P_0$ that preserves both the old retained labels and $q$. Define the next partition by splitting a block whenever two states in it have successors in different current blocks under some permitted operation. Equivalently,
248 \[
249 x\equiv_{P_{t+1}}y
250 \quad\Longleftrightarrow\quad
251 x\equiv_{P_t}y\ \text{ and }\
252 F_u(x)\equiv_{P_t}F_u(y)\ \text{for every }u.
253 \]
254 The construction uses a complete transition description. Having a few observed contradictions does not give a learner that table for free.
255 
256 \begin{proposition}[Least stable refinement of a retained representation]\label{prop:refinement}
257 The splitting construction stabilizes after at most $|X|-|P_0|$ strict refinements. Its final partition is the coarsest refinement of $P_0$ on which every $F_u$ has a well-defined quotient operation. It preserves every finite continuation of the retained labels and outputs.
258 \end{proposition}
259 \begin{proof}
260 A strict refinement increases the number of nonempty blocks, which is bounded by $|X|$. At a fixed point, equivalent states have equivalent successors, so the quotient operations are well-defined. Induction on word length then preserves all retained labels after every finite word. For minimality, let $R$ be any stable partition refining $P_0$. If $R$ refines $P_t$, stability of $R$ implies that $R$-equivalent states have successors in the same $P_t$ blocks, so they remain together in $P_{t+1}$. Induction shows that $R$ refines every $P_t$ and hence the terminal partition.
261 \end{proof}
262 
263 This is a standard partition-refinement argument expressed as a repair of an old representation. It is not necessarily the smallest representation for the outputs alone: $P_0$ may retain distinctions that are no longer needed. Discarding those distinctions requires a different contract. The continuation and cost perspectives are developed more fully in \emph{Machine Understanding}~\cite{understanding}.
264 
265 A counterexample pair is useful because it proves that a current block is too coarse under the stated transition model. It does not specify how a learned encoder can acquire the missing coordinate from its actual inputs. The mathematical quotient and its realizable acquisition procedure remain separate objects.
266 
267 \section{One investigation, one repair, and two resource bounds}\label{sec:synthesis}
268 We now give a finite model in which that acquisition problem can be decided exactly. The result is deliberately restricted, but it charges the complete investigation rather than only a selected final answer.
269 
270 \begin{definition}[Finite repair experiment model]\label{def:repairmodel}
271 A model has a finite nonempty state set $X$, a finite experiment set $\mathcal E$, and a finite repair set $\mathcal A$. Experiment $e$ is allowed on a domain $D_e\subseteq X$, changes the state by $f_e:D_e\to X$, and reports $o_e:D_e\to O_e$. Its execution cost $c_e\geq0$ is fixed and known. Repair $a$ has fixed cost $c_a\geq0$ and succeeds on a declared set $G_a\subseteq X$. All costs are in one stated unit. A nonempty set $B_0\subseteq X$ records the possible current states.
272 \end{definition}
273 
274 A chosen experiment must be uniformly allowed: $B_0\subseteq D_e$. After observing $o$, the possible \emph{post-experiment} states are
275 \begin{equation}\label{eq:post}
276 B_{e,o}=\{f_e(x):x\in B_0,\ o_e(x)=o\}.
277 \end{equation}
278 Only nonempty branches are retained. A terminal repair is justified when $B_0\subseteq G_a$. If the original state or an earlier obligation matters, it must be retained as an immutable tag in $X$. Merely changing the current state into a known state is not recovery of its history.
279 
280 A diagnostic program is a finite rooted tree. An internal record names an experiment and branches on its possible report. A leaf names a repair justified on that branch's surviving states. We count one storage record per node of the complete tree. Shared subroutines, compressed code, and graphs with merged suffixes belong to other storage models. The present count is chosen because it is exact and unambiguous.
281 
282 Let $W(P,B_0)$ be the largest execution cost of a complete path, including its terminal repair. Let $M(P)$ be the number of stored tree records. These costs are not independently minimized. A single tree has to realize both.
283 
284 For horizon $h$, let $\mathcal F_h(B_0)$ be the nondominated attainable pairs $(w,m)$. A pair dominates another when it is no larger in either coordinate and strictly smaller in at least one. Let $T(B_0)=\{(c_a,1):B_0\subseteq G_a\}$. Then
285 \begin{align}\label{eq:pareto}
286 \mathcal F_0(B_0)&=\Pareto T(B_0),\\
287 \mathcal F_h(B_0)&=\Pareto\left(T(B_0)\cup
288 \bigcup_{e:B_0\subseteq D_e}
289 \left\{\left(c_e+\max_o w_o,\ 1+\sum_o m_o\right):
290 (w_o,m_o)\in\mathcal F_{h-1}(B_{e,o})\ \forall o\right\}\right).
291 \nonumber
292 \end{align}
293 An empty child frontier makes that experiment unavailable for a successful complete tree. An empty union is not a zero-cost solution.
294 
295 \begin{theorem}[Exact finite repair synthesis with compiled storage]\label{thm:synthesis}
296 For every finite model, nonempty $B_0$, and integer $h\geq0$, recurrence~\eqref{eq:pareto} yields exactly the nondominated cost pairs of successful diagnostic trees of depth at most $h$. Every retained pair has an executable witness. A work/storage allowance $(b,m)$ is feasible if and only if some retained pair is componentwise at most $(b,m)$.
297 \end{theorem}
298 \begin{proof}
299 At horizon zero only a justified terminal repair can succeed, giving $T(B_0)$. Assume the claim at $h-1$. A successful tree at horizon $h$ either stops immediately or has one uniformly allowed first experiment. Its child at each possible report is successful on exactly the post-experiment support in~\eqref{eq:post}. The execution cost is the root cost plus the worst child cost. The storage is the root record plus the sum over every child, including children not traversed in a particular execution. Conversely, choosing a successful child for each report constructs a successful root tree with those costs. Replacing a dominated child by a dominating one never increases the root maximum or sum. Thus Pareto pruning loses no feasible allowance. Induction proves both completeness and witness construction.
300 \end{proof}
301 
302 The theorem is an application of finite dynamic programming, not an efficient general solution to scientific discovery. Its state subsets and child combinations may grow exponentially. It assumes the transition, observation, legality, and success tables are correct. It also does not include the cost of constructing those tables in its online path cost. Acquisition of the model, compiler execution, and validation are separately charged development resources.
303 
304 \subsection{A more informative question can be a worse repair question}
305 \begin{counterexample}[Entropy reduction need not minimize repair work]\label{ex:entropy}
306 There are four equally likely cases. Repair $a$ succeeds in $\{0,1,2\}$ and repair $b$ succeeds in $\{3\}$. A balanced query separates $\{0,1\}$ from $\{2,3\}$. Another query separates $\{0,1,2\}$ from $\{3\}$. Both cost one unit and leave the state unchanged. The balanced query has the larger entropy reduction, but its second branch still needs another observation. The unbalanced query supports a correct repair after one observation in every case. Maximizing information about the entire hidden case is not the same objective as minimizing the cost of a successful correction.
307 \end{counterexample}
308 
309 \begin{figure}[!h]\centering
310 \includegraphics[width=.94\linewidth]{figures/repair_partition.pdf}
311 \caption{Two equally priced questions about four cases. The balanced split leaves one branch with incompatible repairs. The repair-aligned split identifies a valid action immediately. The figure represents exact sets, not measured agent behavior.}\label{fig:repair}
312 \end{figure}
313 
314 The example suggests a learning target more specific than general curiosity. A useful acquisition policy should distinguish alternative \emph{decisions} when needed, preserve unresolved alternatives when they matter later, and avoid spending work on irrelevant details merely because those details are easy to predict.
315 
316 \subsection{What a compiled witness proves}
317 The reference implementation returns a concrete tree together with its cost pair. A separate interpreter checks its branch coverage, the domains of its experiments, the success of each leaf, and both resource counts. The checker does not infer that the environment model is true. It checks the relation between a specified model and the proposed procedure. This is the same reason an OSL semantic check and a learned Neuralese realization need separate evidence~\cite{osl,neuralese}.
318 
319 \section{Investigating uncertainty in the experiment model}\label{sec:uncertain}
320 The first synthesis theorem assumes that the experiment table is known. This is a substantial informational premise. A reasoner may know which experiments it can request while being uncertain about their outcomes, side effects, or interpretation. Optimizing one guessed table can produce a perfectly checked procedure for the wrong instrument.
321 
322 A useful first extension retains several explicit possibilities rather than replacing uncertainty by one convenient estimate. Let $\Theta$ be a finite nonempty set of candidate models with a common state set $X$, experiment names, repair names, and nonnegative costs. Model $\theta$ specifies $D_e^\theta$, $f_e^\theta$, $o_e^\theta$, and $G_a^\theta$. The unknown model is fixed during an investigation. The initial information is a nonempty set $B\subseteq\Theta\times X$. The procedure observes reports, not the model label or the hidden physical state.
323 
324 An experiment is allowed only when it is allowed under every pair still possible. Its update is
325 \begin{equation}\label{eq:model-support}
326 B_{e,o}=\{(\theta,f_e^\theta(x)):(\theta,x)\in B,\ x\in D_e^\theta,\ o_e^\theta(x)=o\}.
327 \end{equation}
328 The model tag remains unchanged. Observations can exclude a model, but the algorithm cannot switch the underlying model between steps merely because doing so produces a convenient worst case. A terminal repair $a$ is justified when $x\in G_a^\theta$ for every $(\theta,x)\in B$.
329 
330 This is a finite form of planning under model uncertainty. Robust dynamic programming provides an established neighboring literature~\cite{nilim}. The present construction is not an application of a rectangular transition-uncertainty assumption. It explicitly remembers a fixed model label, including correlations between that model's predictions at different times.
331 
332 \begin{theorem}[Repair synthesis under a fixed unknown model]\label{thm:uncertain-synthesis}
333 Construct a finite repair model on $\widetilde X=\Theta\times X$ by
334 \[
335 \widetilde f_e(\theta,x)=(\theta,f_e^\theta(x)),\quad
336 \widetilde o_e(\theta,x)=o_e^\theta(x),\quad
337 \widetilde G_a=\{(\theta,x):x\in G_a^\theta\},
338 \]
339 with the corresponding tagged domains and the common action costs. Applying Theorem~\ref{thm:synthesis} to this model gives exactly the nondominated work/storage pairs of report-dependent trees that succeed for every initial pair in $B$, within the declared horizon. Every retained tree is valid for the actual system whenever its model and initial state belong to $B$.
340 \end{theorem}
341 \begin{proof}
342 A tree receives the same experiment names and report alphabet in both descriptions. For each experiment and report, its possible tagged successor states are exactly~\eqref{eq:model-support}. Its terminal repair is valid on the tagged support exactly when it is valid for every retained model/state pair. Consequently the report histories, path costs, branch counts, and stopping conditions agree node by node. Induction on tree depth gives a cost-preserving correspondence of all successful trees. The finite synthesis theorem then supplies the frontier and its witnesses. If the actual pair starts in $B$, each actual observation leaves its actual successor in the updated support, so the executed terminal repair is valid for that pair.
343 \end{proof}
344 
345 This theorem decides a finite robust investigation problem. It does not learn an arbitrary model class or guarantee that the class contains the truth. Its negative result is also contract-relative. An empty frontier may mean that the admitted experiments cannot resolve the uncertainty, that a needed calibration is unavailable, or that the horizon is too short. It is not evidence that every possible experiment would fail.
346 
347 \subsection{One hidden bit and two sensor conventions}
348 \begin{counterexample}[Known-model repair without a common unknown-model policy]\label{ex:orientation}
349 Let $x\in\{0,1\}$ be the cell requiring repair and let $\theta\in\{0,1\}$ be a fixed sensor convention. A nondestructive query reports $o=x\oplus\theta$ at cost one. Repair $r_i$ succeeds exactly when $x=i$ and costs one. If $\theta$ is known, one query followed by the appropriate repair always succeeds. If all four $(\theta,x)$ pairs are initially possible, report zero leaves $(0,0)$ and $(1,1)$, while report one leaves $(0,1)$ and $(1,0)$. Repeating the same query gives no further information. No finite tree using only this query can guarantee a repair, although each known model admits a two-unit procedure.
350 \end{counterexample}
351 
352 Add a permitted reference measurement that reports $\theta$, leaves $x$ unchanged, and costs two. The procedure can calibrate, make the ordinary query, and choose $r_{o\oplus\theta}$. Its worst-case work is four and its complete binary tree has seven records. Either measurement alone leaves both repairs possible. The two measurements are therefore both necessary in this example, regardless of their order. The executable reference construction returns exactly $(4,7)$ at horizons at least two.
353 
354 The reference measurement is an added information channel. It is not a renamed latent coordinate and not a free inference from the original report. Its authority, reliability, and cost belong to the model. If the physical reference is faulty, the exact guarantee no longer follows. The same issue would arise if a learner excluded the true sensor convention after an unreliable observation.
355 
356 \begin{figure}[htbp]\centering
357 \includegraphics[width=.97\linewidth]{figures/uncertain_sensor.pdf}
358 \caption{An ordinary reading can identify the repair under a known sensor convention yet fail under two possible conventions. A separately specified reference measurement resolves the missing distinction. The figure is an analytical model, not a calibration experiment on an agent.}\label{fig:uncertain}
359 \end{figure}
360 
361 \subsection{Model refinement should be driven by repair relevance}
362 There is no general need to identify the whole model before acting. Several retained models may agree on a successful repair even while disagreeing about irrelevant outputs. The tagged support retains this possibility because its stopping condition is a common successful repair, not a singleton model label. Conversely, a calibration that removes many candidate models can still leave the decisive repair ambiguity intact.
363 
364 A model learner therefore has two different targets. It can seek a more accurate description, or it can seek enough justified information to produce an affordable valid repair. The former can support the latter, but the two costs need not be minimized by the same investigation. The learner should retain the unresolved alternatives that matter to future decisions rather than certify an entire environment from one successful correction.
365 
366 The finite construction also makes the cost of caution visible. The tagged state set can have $|\Theta||X|$ members, and the support search can be substantially larger than a search under one assumed model. Representation refinement, model acquisition, and compiler improvement are consequently coupled research problems. A more reliable model can increase the computational burden of planning until a better discovery procedure exploits its structure.
367 
368 \section{Selecting a better procedure without hiding an oracle}\label{sec:selection}
369 The finite compiler can itself be the object modified by an outer process. One candidate may change the experiment order. Another may change the cost model, add a repair constructor, or select a different representation for the uncertainty set. Their effects should not all be described as the same kind of learning.
370 
371 For a fixed finite collection $\{U_1,\ldots,U_N\}$, suppose a declared assessment gives estimates $\widehat R_i$ of true productivities $R_i$. This assessment can be exact on a fully specified finite distribution or statistical under additional assumptions. Choosing a candidate must use the assessment actually available at selection time, not a hidden final score inspected afterward.
372 
373 \begin{proposition}[Selection under uniform assessment error]\label{prop:selection}
374 If $|\widehat R_i-R_i|\leq\varepsilon$ for every candidate and $\hat\imath$ maximizes $\widehat R_i$, then
375 \[
376 R_{\hat\imath}\geq \max_iR_i-2\varepsilon.
377 \]
378 If a baseline is included and the selected candidate's estimated advantage exceeds $2\varepsilon+\gamma$, its true advantage exceeds $\gamma$.
379 \end{proposition}
380 \begin{proof}
381 For a true maximizer $i^*$,
382 $R_{\hat\imath}\geq\widehat R_{\hat\imath}-\varepsilon
383 \geq\widehat R_{i^*}-\varepsilon
384 \geq R_{i^*}-2\varepsilon$.
385 Apply the same two error bounds to the selected candidate and the baseline for the second assertion.
386 \end{proof}
387 
388 The uniform premise is the essential obligation. A small error for each candidate considered in isolation does not automatically control a candidate selected after adaptive access to the same evaluation record. Section~\ref{sec:evidence} addresses an explicit alternative based on conditional validity.
389 
390 \subsection{Changing the selector and changing the language}
391 An improved selector over a fixed candidate family can produce higher gains without making any previously impossible repair expressible. Conversely, a richer language can increase the best achievable gain while a weak selector never finds the new repair. These are distinct forms of headroom, already separated in the earlier SRIC treatment~\cite{sric}.
392 
393 For a fixed budget, let $R^*_{\mathcal G}$ be the largest productivity among procedures expressible in a declared language $\mathcal G$, with installed data and interpreter costs held fixed. The gap $R^*_{\mathcal G}-R(U)$ is search or selection headroom \emph{within that language}. Comparing $R^*_{\mathcal G'}$ with $R^*_{\mathcal G}$ concerns expressibility and resources. Neither upper envelope is automatically available to the learner.
394 
395 A zero observed gain from one selector update is not a proof of saturation. A genuine saturation statement needs either a complete finite search or an upper bound close enough to the incumbent value. Otherwise the failure may reflect the proposer, the evidence channel, the search allowance, or the evaluation.
396 
397 \subsection{The compiled instrument improver}
398 In the eight-cell instrument, the supplied language admits both singleton and bit queries. Recurrence~\eqref{eq:pareto} can construct a depth-three diagnosis. The exported program replaces the equality-first diagnostic policy in an otherwise unchanged repair system. It does not contain the hidden defect index of the next episode.
399 
400 Under a cap of three diagnostic calls and one repair call, the equality-first procedure certifies and repairs the first three cells, then abstains on the other five. On the uniform finite case distribution, its productivity from a zero-success baseline is $3/8$. The depth-three procedure certifies all eight cases, giving productivity $1$. These are exact properties of stipulated procedures. The compiler selected a better procedure within a supplied finite language. It did not invent the language, learn a general visual representation, or improve the compiler that performed this search.
401 
402 That last distinction is deliberate. This first construction improves the diagnostic procedure, not its compiler. Part~\ref{part:discovery} then changes the compiler, using certified early termination to construct the same optimal diagnostic controllers with fewer model-record reads. The finite selector that installs that compiler remains supplied. An archive entry saying that a descendant is more reflective supplies none of these separate claims.
403 
404 \section{Transporting an investigation, not merely its result}\label{sec:transport}
405 A repair can commute with a representation map even when the procedure used to discover it cannot be transferred. The investigation may depend on an unavailable observation, on a source-specific reset, or on the precise meaning of a stopping condition. A transport contract must include those actions and their evidence.
406 
407 Consider source and target finite repair models. Let $\sigma:X\to X'$ be a bijection, $\tau:\mathcal E\to\mathcal E'$ a bijection of experiments, $\psi:\mathcal A\to\mathcal A'$ a bijection of repairs, and $\eta_e:O_e\to O'_{\tau(e)}$ a bijection of report labels. Assume
408 \begin{align}\label{eq:transport}
409 \sigma(D_e)&=D'_{\tau(e)}, &
410 \sigma f_e(x)&=f'_{\tau(e)}\sigma(x),\\
411 \eta_e(o_e(x))&=o'_{\tau(e)}(\sigma x), &
412 \sigma(G_a)&=G'_{\psi(a)},\nonumber
413 \end{align}
414 and matching execution costs. These assumptions concern supplied semantics. Their discovery or learned approximation is an additional problem.
415 
416 \begin{theorem}[Exact transport of diagnostic procedures]\label{thm:transport}
417 Under~\eqref{eq:transport}, relabeling every experiment, branch, and repair transports successful diagnostic trees bijectively between the source support $B_0$ and target support $\sigma(B_0)$. Execution cost, complete tree storage, and depth are preserved. In particular,
418 \[
419 \mathcal F_h(B_0)=\mathcal F'_h(\sigma(B_0)).
420 \]
421 The same conclusion holds for every selected tree, not only a cost-optimal tree.
422 \end{theorem}
423 \begin{proof}
424 A terminal repair is valid on $B_0$ exactly when its image is valid on $\sigma(B_0)$. For an internal experiment, domain preservation gives uniform admissibility. Transition and observation preservation yield
425 \[
426 \sigma(B_{e,o})=B'_{\tau(e),\eta_e(o)}.
427 \]
428 Apply induction to every child. The report bijection preserves the number of children, the maximum execution cost, and the sum of stored child records. Inverse maps give the converse correspondence. The equality of frontiers follows because costs and dominance are unchanged.
429 \end{proof}
430 
431 The theorem covers a complete explanation of how the repair is found. It is stronger than equality of the repaired output but weaker than a claim that any learned representation admits such a correspondence. A known map costs something to store and execute. In the toy instrument, an arbitrary cell permutation requires a label adapter. A permutation of eight names is not discovered merely by allocating an eight-row table.
432 
433 \subsection{Approximate performance transfer}
434 Suppose a source comparison gives productivity advantage $\Delta$ to $U'$ over $U$. Let $\widetilde U',\widetilde U$ be actual transported target procedures. If each procedure's productivity differs from its source value by at most $\varepsilon$, then
435 \begin{equation}\label{eq:gaintransport}
436 \Rcal'(\widetilde U')-\Rcal'(\widetilde U)
437 \geq\Delta-2\varepsilon.
438 \end{equation}
439 This follows by subtracting the two inequalities. A common source of the premise is an exact task correspondence plus a bounded evaluation-law shift. For any fixed gain function in $[-1,1]$, changing the task law by total variation $\delta$ changes its expectation by at most $2\delta$. A further pointwise gain discrepancy $\eta$ therefore gives $\varepsilon=\eta+2\delta$.
440 
441 This elementary estimate does not certify admissibility or sure success. A rare unauthorized action can have small average loss and still violate a zero-tolerance constraint. Such constraints require their own preservation check. The same is true of uncharged translation work: an equal-output target procedure can fall outside the budget after the adapter is added.
442 
443 \begin{counterexample}[Output transfer with no transferable investigation]\label{ex:unavailable}
444 A source can inspect a hidden bit for one unit and then choose one of two disjoint successful repairs. The target has the same hidden states and repair effects, but no operation that reveals the bit. The final repair meanings correspond exactly. The source diagnostic policy does not transport, and no target policy can guarantee success from the two-state uncertainty set. The missing object is an information channel, not a better translation of the repair names.
445 \end{counterexample}
446 
447 \section{Growing a repair language without losing its old scope}\label{sec:grammar}
448 A persistent discrepancy can be a limitation of the candidate language rather than the search procedure. Repeatedly optimizing coefficients cannot produce a nonlinear term in a language that expresses only affine functions. Reordering uninformative experiments cannot separate two cases whose transcripts are always identical. A learner must distinguish an unsuccessful search from a certified absence of a suitable expression.
449 
450 A conservative extension embeds each old program into a new language with the same meanings on the old domain. That semantic property is valuable, but it does not imply nonregression under a fixed resource allowance. The new interpreter may consume more time, memory, or evidence before executing the embedded old program.
451 
452 \begin{proposition}[The resource price of conservative extension]\label{prop:extension}
453 Suppose an embedding preserves every old procedure's successful behavior and adds at most $d\geq0$ execution work and $s\geq0$ stored records. Every old allowance $(b,m)$ is then feasible in the new language under allowance $(b+d,m+s)$. Feasibility at the unchanged allowance follows only when the embedded procedure fits that allowance. Semantic conservativity alone supplies no such guarantee.
454 \end{proposition}
455 \begin{proof}
456 Embed a witness for the old allowance. By hypothesis its behavior is preserved and its costs are bounded by the shifted pair. The unchanged-budget assertion requires the corresponding inequalities. For the final claim, an old one-unit procedure can be embedded with identical output into a new interpreter requiring two units of startup work. It remains semantically available but cannot execute within the old one-unit allowance.
457 \end{proof}
458 
459 A practical extension should retain a directly executable old path when possible, then route only justified cases through the new machinery. The routing operation also has a cost and an information requirement. A context-dependent grammar is not a solution if deciding the context already requires solving the original problem.
460 
461 \subsection{Error localization and new constructors}
462 The useful role of packets and residuals is to make this diagnosis structured. A packet can declare a domain, a retained distinction, an uncertainty set, an operation interface, and unresolved conditions. A residual identifies which preservation equation or evidence constraint failed. A constructor adds a new kind of candidate repair. The theory does not assume that a packet is an independent physical component or that its name supplies a new algorithm.
463 
464 \clearpage\part{Improving the procedure that discovers repairs}\label{part:discovery}
465 \section{A certificate can remove the need for exhaustive search}\label{sec:compiler-change}
466 The compiled tree in the first example is an improved diagnostic policy. This section changes the procedure that constructs such trees. The distinction is concrete: the parent and descendant receive the same new problem table and return equally valid optimal controllers, but they need not perform the same amount of discovery work.
467 
468 The parent is the exact frontier compiler of Theorem~\ref{thm:synthesis}. It examines a finite set of support/horizon states and combines successful subtrees. That generality is useful, but it can do unnecessary work when one inexpensive candidate already meets a proved global lower bound. A descendant compiler can first propose such a candidate, check it independently, and stop only if its checked cost proves that further search cannot improve either protected resource coordinate.
469 
470 This combines a proposal mechanism with a decisive rejection or acceptance condition. Synthesis from partial programs and counterexamples has established precedents~\cite{sketch}. The particular addition here is a certificate that can close an \emph{optimality} search, rather than merely establish that one candidate is valid. Neither the proposal template nor the lower-bound argument is assumed to have been invented by the system.
471 
472 \subsection{The scope in which a short proof is decisive}
473 Consider $n\geq1$ possible immutable cases. Every admitted query is total, nondestructive, binary-valued, and costs one unit. Every available repair costs one unit and succeeds on exactly one case. At least one repair is available for each case. The target is certain successful repair from the complete set of $n$ possibilities. A literal controller stores one record per query or repair node. Redundant unary query nodes are permitted but have their full costs.
474 
475 \begin{theorem}[Checked lower-bound closure of a diagnostic search]\label{thm:optimality-stop}
476 Every successful controller in this scope has worst-case execution work at least
477 \[
478 1+\lceil\log_2 n\rceil
479 \]
480 and storage at least $2n-1$. If an independently checked candidate attains both bounds and respects the requested horizon, its cost pair is the entire nondominated frontier. Returning this candidate is therefore equivalent in the protected work/storage objective to completing the exhaustive synthesis.
481 \end{theorem}
482 \begin{proof}
483 Every case produces one deterministic query history. Two different cases cannot terminate at the same repair leaf because no repair succeeds in both. Thus there are at least $n$ nonempty leaves. A tree of binary query depth $d$ has at most $2^d$ leaves, so $d\geq\lceil\log_2 n\rceil$. Every path also executes a unit-cost repair. For storage, let $l$ be the number of leaves and let $i_1,i_2$ count unary and binary internal nodes. Counting edges in a finite rooted tree gives $i_1+2i_2=i_1+i_2+l-1$, hence $i_2=l-1$. Total records are $2l-1+i_1\geq2n-1$. A successful candidate attaining both coordinatewise lower bounds dominates every other attainable cost pair. Its independent validity check and horizon check make it a feasible witness, so the Pareto frontier contains only that pair.
484 \end{proof}
485 
486 The immutable-case premise is essential. An experiment that resets every physical state into one safely repairable state can defeat a case-identification lower bound when only the current state matters. Multiple cases admitting a common repair can do the same. The guard must therefore verify the actual contract before applying the bound. This is not a universal theorem that diagnosis always requires identifying the hidden state.
487 
488 A candidate that is valid but misses one lower bound does not close the search. Nor does failure of the proposal rule prove that no optimum exists. In both cases the descendant falls back to the general compiler. The certificate licenses an early return, not an early claim of impossibility.
489 
490 \begin{figure}[htbp]\centering
491 \includegraphics[width=.96\linewidth]{figures/certified_compiler.pdf}
492 \caption{The descendant changes discovery control flow. A checked candidate must attain both global lower bounds before the compiler can stop early. Failure of a guard, proposal, or bound check invokes the unchanged exact compiler. The sequential reference implementation charges unsuccessful preliminary work.}\label{fig:compiler}
493 \end{figure}
494 
495 \subsection{The inexpensive proposal is not the proof}
496 The reference proposer repeatedly chooses a query whose two current branches have the smallest maximum cardinality, breaking ties by the installed query order. It searches the public observation table rather than recognizing privileged names such as ``bit zero.'' It constructs a tree recursively, stopping when a unique justified repair remains. It aborts a proposed branch when the remaining binary depth cannot distinguish its cases.
497 
498 Balancing is a supplied heuristic. It need not minimize repair work in general, as Counterexample~\ref{ex:entropy} already shows. It is useful in the narrower singleton-repair scope because the required distinctions coincide with case identification. Even there, a locally balanced split need not extend to a globally optimal tree for an arbitrary query library. Correctness comes from the finished witness and the lower bound, not from the heuristic's name.
499 
500 The checker reconstructs every possible support, checks all reports, and independently replays every initial case. A fabricated terminal label, missing branch, insufficient horizon, or altered repair effect is rejected. This is a finite model checker authored within the project. It is not a proof of the physical observation table or an independent proof-assistant kernel.
501 
502 \section{The cost of certifying a better compiler}\label{sec:compiler-cost}
503 The unit used in the following comparison is a consumed record of the supplied transition/report table. A repeated access counts again. The unit is chosen because it is explicit and can be instrumented in the unchanged parent compiler and the descendant. It is not a claim to count every Python operation, allocation, set-membership test, processor instruction, or unit of energy.
504 
505 Both procedures start with cold search caches and the same structurally validated table. Shared input-shape validation is recorded separately. The descendant additionally charges its semantic guard, candidate construction, and completed witness check. The parent charges its complete frontier search and the same witness-checking procedure for its returned frontier. Model acquisition, source storage, and the finite procedure-selection stage remain separate ledger entries.
506 
507 \begin{proposition}[Read cost of the certified binary-family shortcut]\label{prop:compiler-work}
508 Let $n=2^k$ with $k\geq1$. Suppose there are $q$ total unit-cost binary immutable queries, and the balanced proposer produces a perfect depth-$k$ tree. In the stipulated implementation, the semantic guard reads every query row once, the proposer scans all $q$ queries at each internal support, and verification performs one support reconstruction and one complete case replay. The total number of transition/report record reads is
509 \begin{equation}\label{eq:compiler-reads}
510 R_{\mathrm{shortcut}}=nq(k+1)+2nk.
511 \end{equation}
512 The usual hidden-cell family with all singleton queries and $k$ coordinate queries satisfies the premise, including after arbitrary cell relabeling, report-bit flips, or reordering of the query list.
513 \end{proposition}
514 \begin{proof}
515 The guard uses $nq$ reads. At each of the $k$ query levels, the current supports partition the $n$ cases, so scanning all queries uses $nq$ reads per level. Every case traverses $k$ query nodes in the support reconstruction and again in the independent replay, contributing $2nk$. Summing gives~\eqref{eq:compiler-reads}. In the hidden-cell family, every nonsingleton support reached by coordinate splits is a subcube. A remaining coordinate divides it equally, while a singleton query cannot give a smaller maximum branch. Thus the balancing rule chooses an equal split until singleton leaves are reached. When a two-case support admits a singleton tie, either split reaches singleton leaves. Relabeling the cases or reversing report names preserves all branch cardinalities and this argument.
516 \end{proof}
517 
518 The result is about a particular implemented access pattern. Caching rows, recognizing trusted structure symbolically, or using another cost unit changes the formula. A specialized cube compiler supplied with certified coordinate semantics can avoid the general search too. The result does not establish superiority to that informed comparator or to every available synthesis algorithm.
519 
520 \subsection{Some verification work cannot disappear}
521 \begin{proposition}[A table-access floor for universal scope certification]\label{prop:table-floor}
522 Suppose a deterministic validator receives an arbitrary table of $N\geq1$ independently variable records only through individual record reads. It must accept every table whose records all satisfy a fixed per-record predicate and reject every table with a violating record. Assume each record position admits both a satisfying and a violating value. On every accepted table, the validator must read all $N$ positions at least once.
523 \end{proposition}
524 \begin{proof}
525 Suppose it accepts a satisfying table while leaving position $j$ unread. Change only that position to a violating value. Every record the validator reads has the same value, so determinism gives the same sequence of reads and the same acceptance. This contradicts rejection of every table containing a violation. Therefore no accepted table can have an unread position.
526 \end{proof}
527 
528 In the compiler's unrestricted table interface, an unread entry could contain a destructive transition or an additional report value. The full semantic scope cannot be certified merely by recognizing a few apparently balanced rows. Trusted construction metadata or a proof from a different representation can change the interface and reduce this cost, but that metadata then becomes a charged assumption or a separate proof object.
529 
530 This identifies a useful bottleneck. Improving search can make model access and verification dominate the remaining computation. It does not make every stage improve at the same rate. Nor does it establish that this bottleneck is permanent, since a learned representation might eventually support cheaper certificates. Such a representation would need its own acquisition and soundness argument.
531 
532 \section{A bounded selection of a better discovery procedure}\label{sec:method-selection}
533 We now make the persistent change explicit. The candidate catalogue contains the unchanged parent compiler, a guarded first-nontrivial-query proposer with exact fallback, and a guarded balanced proposer with exact fallback. The guard, proposal constructors, lower-bound proof, checker, and fallback are supplied. The selection procedure runs each candidate on the four-cell and eight-cell development problems, with the same tables and cold caches. It selects the candidate with the smallest total number of charged record reads and writes a policy record before evaluating any additional problems.
534 
535 The developmental totals are $10{,}256$ reads for the parent, $10{,}380$ for the guarded first-query rule, and $488$ for the guarded balanced rule. The selector therefore installs the balanced rule. These totals concern a fixed, fully enumerated development catalogue. They do not imply a statistical generalization guarantee over an unknown problem distribution. The selected artifact changes the control flow of future compilations without containing the hidden state of a future repair episode.
536 
537 \begin{center}\begin{tabular}{@{}rrrr@{}}\toprule
538 Cases & Parent compiler reads & Descendant reads & Returned $(\text{work},\text{storage})$\\\midrule
539 2 & 16 & 16 & $(2,3)$\\
540 4 & 352 & 88 & $(3,7)$\\
541 8 & 9,904 & 400 & $(4,15)$\\
542 16 & 576,128 & 1,728 & $(5,31)$\\\bottomrule
543 \end{tabular}\end{center}
544 
545 Every paired entry includes complete checking of the returned controller. The sixteen-cell problem is evaluated only after the policy record is fixed. Additional cold cases remove singleton queries, restrict the initial support to six possibilities, reverse operation order, and change cell and report labels. These vary the finite structure available to the compiler. They are not evidence of transfer to an unrelated scientific domain.
546 
547 Under a common cap of $2{,}000$ table reads, the descendant returns a checked optimal sixteen-cell controller. The parent reaches the cap without returning its complete frontier. Its outcome is recorded as \emph{incomplete within the allowance}, not as a proof that no controller exists. Without that cap, the parent also returns the same optimal cost pair. The difference lies in discovery work rather than repair validity or online diagnostic depth.
548 
549 \begin{figure}[htbp]\centering
550 \includegraphics[width=.9\linewidth]{figures/compiler_read_cost.pdf}
551 \caption{Charged transition/report record reads on the exact binary family, including witness checking. The vertical axis is logarithmic. Both compilers return the same optimal online work and stored tree size. These deterministic algorithm counters are not measured agent-learning performance or total CPU instructions.}\label{fig:compiler-cost}
552 \end{figure}
553 
554 \subsection{What was selected and what remains supplied}
555 The persisted policy chooses a proposal rule from a fixed catalogue. It is not a stored solution to the next hidden-cell episode. It therefore modifies an improvement procedure rather than only adding another repaired answer. The compiler accepts arbitrary supplied tables, applies its semantic guard, and retains the exact fallback outside the shortcut's demonstrated scope.
556 
557 This is nevertheless a restricted form of process learning. The catalogue does not invent a new lower-bound theorem or discover a new programming primitive. It does not improve the selector that searched the catalogue. A second call with the same candidates and the same criterion returns the same selected rule. One genuine improvement of a discovery procedure is not an indefinite sequence of improving outer procedures.
558 
559 The distinction gives the next research target a concrete form. A learned proposer would need to generate useful shortcut templates or representations not simply chosen from this fixed list, while the checker verifies their stated scope. A learned evaluator would need to identify when existing cost or success measurements omit a consequential requirement. Such changes would alter additional parts of the realization and need their own preserved comparison.
560 
561 \subsection{Fallback protects meaning, not free execution}
562 \begin{counterexample}[A semantically protected shortcut with a slower fallback]\label{ex:slow-fallback}
563 Give the compiler four immutable cases and only four singleton queries. The horizon permits the three-query equality tree. A balanced proposal produces a valid controller but cannot attain the two-query information lower bound, since the query library does not supply the needed split. The descendant therefore performs its preliminary guard and proposal work and then runs the exact parent. It returns the same frontier but consumes more table reads. Semantic nonregression has not established work nonregression.
564 \end{counterexample}
565 
566 The counterexample is included in the shipped comparison. The declared development objective prefers the shortcut on its development family, not on every possible input. Changing the mixture of structured and fallback cases can change which procedure is preferable. Attributing all gains to the new procedure while excluding its failed proposal attempts would invalidate the comparison.
567 
568 There is a conditional way to bound this risk through scheduling rather than prediction. The following result is intentionally separate from the sequential implementation above.
569 
570 \Needspace{16\baselineskip}
571 \begin{proposition}[Bounded slowdown from a certified two-worker race]\label{prop:race}
572 Suppose a parent and a shortcut worker can be paused after each unit of a common work measure and resumed without losing progress. Each may announce completion only after producing a result certified for the same target. Alternate one unit of each worker and stop at the first certified completion. If their standalone completion costs are $D_0,D_1\in\mathbb N_{>0}\cup\{\infty\}$ and at least one is finite, at most $2\min\{D_0,D_1\}$ worker units are executed. If each dispatched unit costs at most an additional $c\geq0$ scheduler units in the same measure, total charged work is at most $2(1+c)\min\{D_0,D_1\}$.
573 \end{proposition}
574 \begin{proof}
575 After $2d$ dispatched worker units, each worker has received exactly $d$ units of progress. Set $d$ to the smaller finite standalone completion cost. That worker has completed its certification by this point, so the race has stopped no later. Multiplying the number of dispatches by the maximum combined work per dispatch gives the overhead bound.
576 \end{proof}
577 
578 The theorem does not provide resumability for an arbitrary compiler, bound the memory occupied by both workers, or make their setup free. The present reference compiler uses sequential fallback, not this race. The companion suite checks the abstract schedule bound separately on finite worker tapes. A systems implementation would need to include state checkpointing, dispatch cost, shared-resource contention, and both workers' storage before claiming this guarantee.
579 
580 Taken together, the results distinguish three achievements: a heuristic frequently proposes a good answer, a certificate establishes that the answer closes the search, and an implementation retains an affordable fallback when the heuristic fails. None of these can substitute for the others.
581 
582 \subsection{A complete receipt for the sixteen-cell compilation}
583 The selected policy is evaluated on a fresh sixteen-cell table after its bytes are fixed. The new table has twenty query rows: sixteen singleton queries and four coordinate queries. The next hidden defect is not supplied to either compiler. Both methods construct a complete controller that will work for any of the sixteen cases.
584 
585 The descendant's recorded access account is
586 \begin{center}\begin{tabular}{@{}lr@{}}\toprule
587 Compiler stage & Consumed transition/report records\\\midrule
588 Semantic scope guard & 320\\
589 Proposal construction across four levels & 1,280\\
590 Support reconstruction by the checker & 64\\
591 Independent replay of all cases & 64\\\midrule
592 Total & 1,728\\\bottomrule
593 \end{tabular}\end{center}
594 The separate common input-shape validation consumes another 320 records before the measured compilation begins. It is not included in the $2{,}000$-read compiler allowance. Counting that shared setup on both sides gives 2,048 reads for the descendant and 576,448 for the parent. No particular implementation is permitted to hide its extra guard inside an uncharged setup step.
595 
596 The three-candidate development comparison itself consumed 21,124 model-record reads. It is part of the cost of selecting the descendant, not part of one later compilation. For the declared sixteen-cell workload the per-use read saving is 574,400, so those developmental reads are recovered within one use in that same narrow accounting unit. This does not repay an unspecified human research cost, prove a wall-clock speedup on every machine, or charge the creation of the candidate templates. Source sizes and measured runtimes are recorded separately rather than silently converted into model-record reads.
597 
598 The result concerns cheaper discovery of equally valid controllers. It does not establish an improved selector or an independently discovered compiler catalogue.
599 
600 \clearpage\part{Learning a compiler's rejection rule}\label{part:rule-learning}
601 \section{A failed search representation can itself be repaired}\label{sec:search-features}
602 The preceding selector chooses among three supplied compiler strategies. It changes which algorithm will be used, but does not compose a new decision rule. We now move one step inside a compiler. A small learner constructs a predicate that tells the compiler when it can stop inspecting an unpromising query. The learned object is neither a hidden-cell answer nor a completed diagnostic tree. It is an operation on the compiler's own partial information, reused while constructing trees for further problems.
603 
604 The construction is deliberately restricted. Its experiment tables, compiler skeleton, primitive arithmetic language, and correctness argument remain supplied. Within that boundary, the learner is not given the complete predicate as one named strategy. It first encounters a representation that cannot express its assigned distinction, adds a specified missing feature, and synthesizes a formula from counterexamples. A structural certificate then determines whether the formula may safely prune later searches.
605 
606 This separates three questions that are easy to conflate: whether the examples determine a suitable formula, whether the formula is valid outside those examples, and whether executing it actually reduces the relevant cost. The reference construction answers each under a different explicit contract.
607 
608 \begin{figure}[!ht]\centering
609 \includegraphics[width=.95\linewidth]{figures/rule_synthesis_pipeline.pdf}
610 \caption{One complete bounded improvement. A feature conflict justifies exposing the supplied capacity feature. Counterexamples select a composed arithmetic expression. A narrow structural check links that expression to a proved scope, after which it can skip rows inside later compilations. The grammar, teacher, scope proof, and compiler skeleton remain outside the learned component.}\label{fig:rule-pipeline}
611 \end{figure}
612 
613 \subsection{The information available inside a search}
614 A compiler is considering a binary query on a support of $m$ possible immutable cases. It reads the query's public model rows in a fixed order. After a prefix, $a$ of the inspected cases have report zero and $b$ have report one. There are $m-a-b$ rows left to read. If this query is the first of at most $d\geq1$ remaining queries, either child can contain at most
615 \[
616 C=2^{d-1}
617 \]
618 cases when distinct cases need distinct repair leaves. The local cardinality premise $m\leq2C$ is checked before a root is investigated. An overfull support cannot fit the remaining binary depth, even before any rows of the proposed query are read.
619 
620 The initial search representation contains $(a,b,m)$ but omits $C$. This can lose a distinction relevant to the search itself. For example, $(a,b,m)=(0,3,4)$ cannot have a completion whose two branch sizes are at most two. It can have a completion with branch sizes $(1,3)$ when the allowed child capacity is four. The read prefix is the same. The permitted future investigation is different.
621 
622 \begin{proposition}[Feature sufficiency for a search decision]\label{prop:search-feature}
623 Let $\mathcal P$ be a finite set of search contexts, let $r:\mathcal P\to Z$ be their available feature map, and let $\ell:\mathcal P\to\{0,1\}$ be the required decision label. A deterministic rule $f:Z\to\{0,1\}$ satisfying $fr=\ell$ exists if and only if $\ell$ is constant on each nonempty fibre of $r$. A pair in one fibre with different labels rules out every such rule, irrespective of its program length.
624 \end{proposition}
625 \begin{proof}
626 If $f$ exists, equal features have the same output under $f$ and hence the same label. Conversely, assign to each attained feature value its common label. This is well defined when the fibre condition holds. Values outside the image of $r$ can be assigned arbitrarily. A conflicting pair violates necessity for every possible $f$.
627 \end{proof}
628 
629 The criterion is elementary factorization, not a new general learning theorem. Its role is to distinguish insufficient information from inadequate search effort. In the finite construction, exhaustive search for a larger formula over $(a,b,m)$ cannot fix the conflict. The supplied feature registry contains the remaining-depth capacity $C$. Exposing it resolves this particular obstruction. Computing $C$ from an already known depth is not a physical experiment and does not identify the next episode's hidden defect.
630 
631 \begin{counterexample}[The same prefix requires different rejection decisions]\label{ex:missing-capacity}
632 For the two contexts $(a,b,m,C)=(0,3,4,2)$ and $(0,3,4,4)$, the initial feature vector $(a,b,m)$ is identical. In the first, three cases already occupy a child with capacity two. In the second, assigning the remaining case to the other child gives a capacity-feasible completion. Thus the predicate ``no capacity-feasible completion exists'' cannot be computed from the initial features alone. Adding the capacity makes this specific decision representable. It does not establish that the actual query library can distinguish every resulting child.
633 \end{counterexample}
634 
635 This is a small instance of representational revision inside a discovery algorithm. The target of learning is not only a model of the external task. It is a model of which search continuations remain possible under the compiler's own constraints. A richer representation is useful because a named counterexample requires it, rather than because extra variables are assumed to improve intelligence in general.
636 
637 \section{Composing a rule from primitive syntax}\label{sec:grammar-learning}
638 The enlarged feature vector is $(a,b,m,C)$. The reference language has six integer atoms, $a,b,m,C,0,1$, three binary arithmetic operations, $\max$, $\min$, and addition, and the five comparisons $>,<,\geq,\leq,=$. A candidate is a Boolean comparison with at most five syntax nodes. No general program execution is admitted. The interpreter evaluates only these finite arithmetic trees.
639 
640 Integer atoms have size one. A binary arithmetic expression has size three. A comparison of two atoms has size three, while a comparison with one arithmetic child has size five. For commutative arithmetic, operand pairs are generated in one fixed order. This produces 180 size-three formulas and 3,780 size-five formulas, or 3,960 candidates in all. Different syntaxes can express the same function. No semantic deduplication is assumed in these counts.
641 
642 This is a bounded instance of syntax-guided synthesis, in which the candidate language and a semantic requirement are specified separately~\cite{sygus}. Counterexamples guide the choice of candidate. Learning invariants from examples, counterexamples, and implication constraints is also an established research direction~\cite{ice}. The present learner does not implement the full ICE framework and makes no claim to discover general loop invariants. It learns one rejection expression under a supplied search contract.
643 
644 \subsection{What the teacher knows}
645 Development uses the 198 count-prefix contexts with $C\in\{1,2,4\}$, $2\leq m\leq2C$, and $a,b\geq0$, $a+b\leq m$. For each context, the teacher enumerates the possible numbers of report-one cases among the unread rows. It labels the context as reject precisely when no such completion can put at most $C$ cases in either branch. The teacher therefore solves a small finite feasibility problem. It is not reading a label generated by the final formula.
646 
647 After each returned counterexample, the learner retains that context and its label. It selects the earliest formula in the fixed syntax enumeration that agrees with every retained example. The finite teacher either returns another disagreement or checks the formula against the complete developmental domain. The definition of that domain, the generation of its labels, and all rejected candidates are part of the development account.
648 
649 \begin{theorem}[Finite counterexample refinement within a grammar]\label{thm:grammar-refinement}
650 Let $\mathcal G$ be a finite nonempty set of deterministic candidate programs, let $\mathcal P$ be a finite domain, and let $\ell$ be its specified labeling. Suppose a teacher either returns a point where the proposed program differs from $\ell$ or certifies agreement on all of $\mathcal P$. A learner that proposes only candidates consistent with every retained counterexample rejects each proposed program at most once. It returns a correct program on $\mathcal P$, or certifies that none in $\mathcal G$ meets the labeling, after at most $|\mathcal G|$ teacher calls. With a fixed total order and the earliest-consistent selection rule, any returned program is the earliest one that agrees on the entire domain.
651 \end{theorem}
652 \begin{proof}
653 A counterexample removes the current program because it must be included in the constraints for every later proposal. Hence that program cannot be proposed again. A program agreeing with $\ell$ on all of $\mathcal P$ is never removed by a valid counterexample. There are only $|\mathcal G|$ candidates, so after at most that many distinct proposals the teacher has accepted one or all candidates are excluded. If a returned program were preceded by a globally correct program in the fixed order, the earlier program would remain consistent and would have been selected instead. This proves the ordering assertion.
654 \end{proof}
655 
656 The result concerns the declared finite domain. It is not a generalization bound and supplies no efficiency guarantee for obtaining the teacher's answers. A teacher timeout is not a certificate. If the grammar does not contain a suitable program, enlarging the grammar changes the search problem and its cost.
657 
658 \subsection{The synthesized expression and its provenance}
659 The reference learner encounters three disagreements. Its first candidate, $a>a$, fails on a prefix with too many ones. The next proposed candidate, $b>a$, rejects a prefix that can still be completed. The third, $b>C$, misses a prefix with too many zeros. The fourth teacher proposal is
660 \begin{equation}\label{eq:learned-prune}
661 \rho(a,b,m,C)=\mathbf 1\{\max(a,b)>C\}.
662 \end{equation}
663 The formula uses five syntax nodes and passes all 198 developmental contexts. The enumeration generates all 3,960 AST roots and considers 190 of them, including candidates rejected directly by retained examples. There are 282 retained-example checks, 210 full-domain teacher comparisons, 344 completion-count checks to construct the labels, and 1,898 interpreted syntax-node visits in the learner's recorded comparisons. The full grammar has 19,440 literal node occurrences. Shared in-memory subexpressions can reduce actual storage, so this last quantity is not a measured byte count.
664 
665 These numbers describe an exact finite synthesis, not a statistical training cohort. The formula is serialized and frozen before evaluation on larger supports, additional capacities, and changed row and query orders. No new episode's defect index or solved controller is placed in the formula. It contains only the reusable relation between two observed prefix counts and remaining capacity.
666 
667 The learner discovers the composition of supplied primitives. It does not invent addition, maximum, the teacher, the resource model, or the eventual safety proof. This boundary is important: enumerating a finite grammar is more expressive than choosing among the earlier three named compiler policies, but it remains a bounded search space chosen in advance.
668 
669 \section{When an unfinished read can close a search branch}\label{sec:prefix-pruning}
670 A finite fit is insufficient grounds for deleting possibilities from a later search. Pruning is stronger than proposing. A bad proposal can be rejected by a finished-witness checker. A bad pruning rule can remove the only successful controller and leave nothing for that checker to inspect. We therefore attach the generated expression to a separate scope argument.
671 
672 \begin{proposition}[Exact obstruction to a capacity-feasible completion]\label{prop:prefix-capacity}
673 Let $C,m,a,b$ be integers with $C\geq1$, $2\leq m\leq2C$, $a,b\geq0$, and $a+b\leq m$. A binary completion of the remaining $m-a-b$ reports with both final branch counts at most $C$ exists if and only if $\max(a,b)\leq C$. Consequently, a prefix satisfying $\max(a,b)>C$ can be rejected before its remaining rows are read, without rejecting any completion that satisfies these two capacity constraints.
674 \end{proposition}
675 \begin{proof}
676 Counts do not decrease as rows are read, so $a>C$ or $b>C$ makes a feasible completion impossible. Conversely, suppose $a,b\leq C$. Let $r=m-a-b$. There are $C-a$ available places in the zero branch and $C-b$ in the one branch. Both are nonnegative and their sum is $2C-a-b\geq r$. Distribute the $r$ remaining cases between these two capacities, filling either branch up to its capacity and putting any remainder in the other. This gives the required completion. The argument concerns possible report assignments, not whether an installed query has that assignment.
677 \end{proof}
678 
679 The theorem applies to arbitrary positive integer capacities. The connection to query depth uses $C=2^{d-1}$. An actual search separately checks that both observed branches are nonempty, since a redundant unary query cannot be part of a controller attaining the minimal literal storage. It also verifies all later subtrees. Capacity feasibility is necessary, not sufficient, for actual repair solvability.
680 
681 \begin{figure}[!ht]\centering
682 \includegraphics[width=.90\linewidth]{figures/prefix_capacity.pdf}
683 \caption{An exact count-prefix model with eight cases and child capacity four. A prefix outside the square $a,b\leq4$ cannot be completed within that capacity. Prefixes also satisfy $a+b\leq8$. Surviving the count test does not guarantee that the installed query library can separate the children. The dotted arrow is one unfinished read that can stop immediately after its fifth equal report.}\label{fig:prefix-capacity}
684 \end{figure}
685 
686 \subsection{A deliberately narrow certificate checker}
687 The executable gate accepts only ASTs that normalize by swapping a comparison's sides or maximum's arguments to $\max(a,b)>C$. It rejects other finite-consistent formulas rather than claim to prove arbitrary arithmetic identities. Thus the universal justification is the preceding prose proof, coupled to a project-local structural checker and a runtime scope guard. This is not a Lean certificate or an independent theorem-proving service.
688 
689 \begin{counterexample}[Agreement on training prefixes does not establish scope]\label{ex:prune-extrapolation}
690 The formula $\max(a,b)>\min(C,4)$ agrees with~\eqref{eq:learned-prune} on every developmental context because every developmental capacity is at most four. At $(a,b,m,C)=(0,5,16,8)$ it rejects, while a completion with final branch sizes $(8,8)$ exists. A larger input has not merely changed the frequency of familiar cases. It has reached a scope on which the bounded-cap formula was never justified. The structural gate does not accept that formula.
691 \end{counterexample}
692 
693 This counterexample also separates candidate selection from admissibility. A learner may prefer a formula for reasons of fit or cost. The compiler may install it as a pruning rule only under the corresponding proof obligation. Changing the rule's semantics, the available features, or the repair-success contract requires revisiting that obligation.
694 
695 \subsection{The same search with fewer model-row reads}
696 The reference compiler first checks the immutable, unit-cost, binary-query and singleton-repair scope of Theorem~\ref{thm:optimality-stop}. It then conducts an ordered depth-first feasibility search at the information lower depth $d_0=\lceil\log_2|B_0|\rceil$. The full-scan version reads every current row of a candidate query before rejecting an overfull child. The streaming version consults the certified prefix rule after each read. Both use the same query order, report order, remaining depth, and stopping rules. If a root has capacity-feasible children but a child cannot be completed using the actual library, the search backtracks to the next root.
697 
698 A successful controller is separately checked and attains both lower bounds. When no controller exists at $d_0$, a requested horizon equal to $d_0$ permits a genuine finite infeasibility result. A longer requested horizon instead invokes the unchanged general compiler. Failure of the initial scope guard also invokes that compiler. Exhaustion of a model-read allowance returns incomplete, never infeasible merely because the allowance ran out.
699 
700 \begin{theorem}[Semantics-preserving streaming pruning]\label{thm:streaming-pruning}
701 Under the checked binary immutable singleton-repair scope, fixed query and row orders, and identical search and fallback rules described above, replacing full root scans by the certified predicate~\eqref{eq:learned-prune} returns the same first successful lower-depth controller, or the same exhaustive failure at that depth. With unlimited completion of any required common fallback, both compilers return the same protected frontier. The streaming version uses no more transition/report model-row reads, and the difference is exactly the number of unread suffix rows skipped at rejected roots. Scope checks and final witness verification are included identically in both read accounts.
702 
703 Within a root scan, after a prior prefix has passed, the predicate can be evaluated by comparing only the newly incremented count with $C$. This lowering preserves every rejection decision.
704 \end{theorem}
705 \begin{proof}
706 By Proposition~\ref{prop:prefix-capacity}, every root rejected early would be rejected after its full scan. A root not rejected early has its complete rows read and produces the same two child supports in the same order. Induction on remaining depth therefore gives the same child searches, backtracking choices, first completed controller, and lower-depth failure. Nonempty binary splits strictly reduce support, and the depth decreases, so the finite search terminates. Any successful tree can omit redundant unary roots without losing case information in this immutable unit-cost scope. The search consequently covers all relevant lower-depth controllers. The checked lower bounds justify the same optimal frontier on success. Identical failure conditions invoke the same exact fallback on the same problem.
707 
708 At every visited root, either the same rows are read or one suffix of rows that cannot affect the rejection decision is omitted. All descendant supports actually entered are identical. Summing omitted suffix lengths gives the stated read difference. This excludes timeouts, under which the methods can finish at different allowances but neither asserts false infeasibility.
709 
710 For the lowering, both prior counts are at most $C$, since otherwise the scan would already have stopped. One report increments exactly one count. The unchanged count remains at most $C$, so the maximum exceeds $C$ exactly when the incremented count does. This implication requires the stated loop invariant.
711 \end{proof}
712 
713 The read comparison isolates one alteration to one compiler. It is not a claim that every new search order beats the earlier balanced proposer, nor that fewer table reads imply shorter processor runtime. Interpreting a five-node formula at each prefix adds work. The supplied lowering replaces that interpretation by one integer comparison, but it too has a cost. The code records both versions and checks that they choose identical trees.
714 
715 \begin{counterexample}[Local capacity without a completing query library]\label{ex:local-capacity}
716 Four cases admit singleton repairs. The only available query divides them into $\{0,1\}$ and $\{2,3\}$ and leaves the state unchanged. At depth two, the root satisfies the $2/2$ capacity test. Repeating the only query cannot separate either pair, so no successful depth-two tree exists. Accepting the first capacity-feasible root as a finished certificate would be wrong. The streaming compiler searches its children, records the failure, and concludes infeasibility only after exhausting the actual library.
717 \end{counterexample}
718 
719 \section{Pruning depends on what counts as a repair}\label{sec:repair-cover}
720 The singleton scope is not cosmetic. A repair procedure need not determine the hidden case if one action succeeds on several cases. A change to the repair language can therefore invalidate the interpretation of raw case counts as required leaves, even when the experiment model is unchanged.
721 
722 Let $B$ be a finite nonempty immutable-case support and let $G_r\subseteq B$ be each repair's success set restricted to it. Define $\kappa(B)$ to be the smallest number of repair-success sets whose union covers $B$. Set $\kappa(B)=\infty$ when no such cover exists. This number concerns the repaired objective, not the number of hidden states. Computing it can itself be expensive.
723 
724 \begin{proposition}[Repair-relative leaf requirements]\label{prop:repair-cover}
725 For finite immutable cases with binary deterministic queries, any certain successful diagnostic tree of query depth at most $d$ has at least $\kappa(B)$ nonempty repair leaves. Consequently $\kappa(B)\leq2^d$ is necessary for success, and literal tree storage is at least $2\kappa(B)-1$. These conditions are not sufficient for success under a specified query library.
726 \end{proposition}
727 \begin{proof}
728 Every initial case reaches one repair leaf. The set of cases reaching that leaf is contained in its repair's success set. The success sets of the attained leaves therefore cover $B$, so the number of leaves is at least $\kappa(B)$. A binary tree of depth $d$ has at most $2^d$ leaves. The edge-count argument from Theorem~\ref{thm:optimality-stop} gives at least twice the number of nonempty leaves minus one literal records, with any unary nodes adding further storage. The preceding one-query example has $\kappa(B)=4$ and $d=2$, satisfying both numerical lower bounds while lacking a completing tree. Thus the necessary conditions are not sufficient.
729 \end{proof}
730 
731 For singleton repairs, $\kappa(B)=|B|$, recovering the earlier argument. With a universal repair, $\kappa(B)=1$ even when many cases remain unknown. The executable streaming path retains the easier singleton guard rather than quietly substituting a hard cover computation whose cost would be uncharged. The broader proposition indicates how a different pruning contract could be developed, not a hidden extension of the present code.
732 
733 \begin{counterexample}[A successful repair language can make identification unnecessary]\label{ex:scope-repair-change}
734 Keep the four-case query table but add one unit-cost repair that succeeds in every case. The exact optimum is now one repair call and one stored record, with no queries. A compiler that carries over the old ``four cases require four distinct leaves'' assumption can discard this optimum. The reference guard rejects the changed singleton scope and the general compiler returns the zero-query solution. The old theorem remains true. Its premise no longer describes the new language.
735 \end{counterexample}
736 
737 This is the preservation problem in recursive revision. A learned optimization acquires authority from a contract. Subsequent language growth can change that contract. Keeping the old formula while discarding its premise is not improvement. A retained shortcut should therefore carry its feature definition, semantic assumptions, recognized proof form, and fallback behavior together.
738 
739 \section{What the synthesized compiler actually gains}\label{sec:synthesized-cost}
740 The learner freezes~\eqref{eq:learned-prune} after the small development domain. It is then used on the hidden-cell query family through 64 cases. The primary comparison is between the full-scan ordered search and the same ordered search with prefix pruning. It therefore isolates the effect of the generated rule. The earlier balanced wrapper is retained as a separate comparison, not silently treated as identical to this full-scan baseline.
741 
742 \begin{center}\small
743 \begin{tabular}{@{}rrrrr@{}}\toprule
744 Cases & Full-scan reads & Streaming reads & Rows avoided & Added comparisons\\\midrule
745 2 & 12 & 12 & 0 & 2\\
746 4 & 66 & 65 & 1 & 25\\
747 8 & 308 & 277 & 31 & 141\\
748 16 & 1,384 & 1,129 & 255 & 681\\
749 32 & 6,192 & 4,641 & 1,551 & 3,137\\
750 64 & 27,744 & 19,457 & 8,287 & 14,209\\\bottomrule
751 \end{tabular}\end{center}
752 
753 All listed compilers include the semantic scope guard and final witness check. The common input-shape validation is separately recorded and identical. For example, the 64-case query table has 70 queries and its shared shape check consumes 4,480 model rows for each method before the reported compilation allowance. The final controllers have the same literal trees in the primary comparison. Their execution and storage costs are unchanged: seven online units and 127 stored records in the 64-case case.
754 
755 \begin{figure}[!ht]\centering
756 \includegraphics[width=.92\linewidth]{figures/synthesized_read_cost.pdf}
757 \caption{Transition/report model-record reads for the same ordered compiler before and after installing the synthesized prefix rule. Scope and final witness checks are charged in both curves. Common input-shape validation is separately reported. The vertical axis is logarithmic. The plot is an exact finite cost comparison, not a timing ratio or evidence of a broad neural-learning gain.}\label{fig:synthesized-cost}
758 \end{figure}
759 
760 \subsection{A resource improvement is not a universal speedup}
761 In the interpreted version, each prefix evaluates five AST nodes. The checked lowering uses one integer comparison instead. Relative to a baseline that already performs the complete-root capacity test, a conservative extra-work account charges every new prefix comparison without crediting any removed end-of-scan check. At 64 cases this adds 14,209 comparisons while avoiding 8,287 model rows. At two cases no row is avoided and the new comparisons are pure overhead.
762 
763 If a model-row read has declared price $w>0$ and a new comparison has price one, the additional per-use saving under this conservative two-unit account is
764 \[
765 \Delta(w)=w\,(R_{\mathrm{full}}-R_{\mathrm{stream}})-N_{\mathrm{compare}}.
766 \]
767 For the 64-case row it is positive when $w>14209/8287$. At $w=1$ it is negative. The price is a modeling choice, not a measured statement about Python or a physical machine. Interpreted AST visits, installed code, grammar construction, labels, and development search remain additional recorded coordinates. No weighted sum is presented as a universal cost of intelligence.
768 
769 If development has total charged cost $D$ in a chosen common accounting unit and the same future use has saving $\Delta(w)>0$, $N$ repetitions repay that cost only when $N\Delta(w)>D$. This is the amortization argument already used earlier, applied to the learned compiler rule. It does not authorize ignoring development because deployment might eventually repeat often.
770 
771 \subsection{Transport and negative controls}
772 The formula contains counts and a remaining-depth capacity rather than cell names or query identifiers. Renaming cases and flipping binary report meanings preserve the capacity predicate. A complete search uses the model rows to determine its actual branches, and its witness is checked anew. Reordering queries can change which equally optimal controller is encountered first. Reordering rows can change how early an impossible prefix becomes visible. Correctness is preserved under the certified scope, but the number of saved reads need not be invariant.
773 
774 A four-case equality-only library provides another boundary. It has no controller at the information lower depth, so a larger requested horizon invokes the general compiler. The new method can spend preliminary work before that fallback. On a changed language with a universal repair, the semantic guard rejects the pruning scope and the general optimum is recovered. These are specified behaviors, not successes relabeled after observing the results.
775 
776 
777 
778 \subsection{The precise recursive claim}
779 The first construction improved a diagnostic controller. The second selected a better compiler from named policies. The present construction synthesizes and installs an internal decision rule that changes how future controllers are discovered. It also records a representational obstruction within that compiler and a permitted feature refinement that removes it. This is a bounded inductive program-synthesis step, not neural training or a renamed cache of solved episodes.
780 
781 The construction does not demonstrate that the grammar enumerator becomes better at inventing later grammars, that the learner discovers its own theorem checker, or that its task family becomes generally intelligent. The primitive operations, teacher, feature registry, scope proof, and search skeleton are substantial prior structure. The gain nevertheless occurs at the claimed location: future searches omit work because of a reusable expression composed from evidence, and the conditions under which that omission remains justified are checked rather than presumed.
782 
783 
784 \clearpage\part{Improving how discovery rules are acquired}\label{part:meta-acquisition}
785 \section{The next retained object is a search representation}\label{sec:meta-acquisition}
786 Part~\ref{part:rule-learning} changes a decision inside the diagnostic compiler. Its counterexample-guided learner still traverses a fixed list of arithmetic candidates. A further change is possible without pretending that the learner invents its own computational foundations: it can acquire a reusable representation of that candidate space, then use the representation to reduce the work of synthesizing later rules.
787 
788 The new object is neither a completed diagnostic tree nor the target expression $\max(a,b)>C$. It is a library of checked equations and an ordered map from grammar expressions to earlier equivalent representatives. Learning the library does not require the labels of a later synthesis task. Once the representation has been constructed and validated, subsequent tasks still begin with empty task-specific counterexample sets.
789 
790 This direction has direct precedents. Equality saturation represents equivalent expressions and supports program optimization and synthesis~\cite{egg}. Ruler automatically infers rewrite rules and uses equality saturation within that inference process~\cite{ruler}. The present implementation is intentionally smaller. It uses a typed arithmetic language, finite proposals, a local derivation checker, and ordered enumeration rather than an e-graph. It does not claim a new rewrite-inference paradigm or superiority to those systems. Its purpose is to make one additional level of the improvement process executable and to connect the acquired search representation to the paper's unchanged semantic and resource contracts.
791 
792 \subsection{Four objects and two meanings of success}
793 Let $\Gcal=(p_0,\ldots,p_{N-1})$ be a finite ordered grammar of pure, total expressions. A target task supplies contexts $z\in D$ and desired values $f(z)$. An ordinary learner uses counterexamples to find the first grammar expression that agrees with all of $D$. A separate equational learner observes expressions on a development probe set and proposes equations. A checker admits only equations supported by a derivation in the declared arithmetic theory.
794 
795 There are therefore two distinct successes. A task candidate may agree with a complete finite target domain while remaining unjustified outside it. An equational certificate may establish agreement for every integer substitution, even though it says nothing about whether the resulting program solves a particular task. The latter can safely reduce the former search, but cannot manufacture its missing target evidence.
796 
797 \section{Learning equations without confusing probes with proofs}\label{sec:equation-learning}
798 The reference language uses exact integers, the total operations $+$, $\min$, $\max$, and the comparisons $<$, $\le$, $>$, $\ge$, and $=$. A finite schema language contains 135 terms built from variables $x,y$, small integer literals, Boolean literals, and at most one binary operation. The proposer evaluates those schemas on the nine contexts $(x,y)\in\{1,2,3\}^2$.
799 
800 Two schemas with the same probe vector become a proposed equation, not an accepted rule. This produces 1,068 proposals. The supplied proof procedure proves 336 using integer arithmetic identities. The other 732 are not admitted. Failure of that limited procedure is not a theorem that an equation is false.
801 
802 The derivation interface has six elementary rule kinds: commutativity where valid, addition of zero, idempotence of minimum and maximum, reversal of an order comparison, reflexive comparison, and exact evaluation of literal constants. It also checks replacement at an explicit subtree position. A proof of an equation contains two derivations ending in the same expression. A separate replayer checks every position, side condition, and endpoint. This is a project-local equational checker, not a proof-assistant kernel or a general arithmetic decision procedure.
803 
804 \begin{counterexample}[A probe-equivalent rule that fails on a new input]\label{ex:probe-equation}
805 On the development inputs $x\in\{1,2,3\}$, the terms $\max(x,1)$ and $x$ agree. At $x=0$ they differ. The proposed equation is not admitted by the proof checker. By contrast, $\max(x,0)=x$ holds on all nonnegative integers but not on all integers. A checker using the stronger integer-wide contract may fail to admit a rule that would be valid under a narrower natural-number contract. Rejection, counterexample, and scope restriction remain different outcomes.
806 \end{counterexample}
807 
808 \subsection{What the learner contributes and what it is given}
809 The proposer generates the equations from evaluations rather than receiving the final equation list. The library is serialized before the later task targets are evaluated. The primitive syntax, probe schedule, arithmetic axioms, proof search, and normalization engine remain supplied. Their presence does not negate the acquired representation. It does prevent describing the construction as discovery of integer arithmetic or autonomous improvement of the equational learner itself.
810 
811 The complete accepted library occupies 69,518 bytes in its stated compact JSON serialization. This is a serialization measurement, not an estimate of an optimal theory description. It contains redundant equations. A supplied full normalizer is retained as a stronger comparison, so the results do not depend on comparing only against deliberately repeated syntax.
812 
813 \section{A certified quotient preserves the investigation's evidence}\label{sec:ordered-quotient}
814 Write $\llbracket p\rrbracket(z)$ for an expression's value in context $z$. Let $n(p)$ be a deterministic representation produced by finitely many checked substitutions of valid equations. We only require
815 \[
816  n(p)=n(q)\quad\Longrightarrow\quad
817  \llbracket p\rrbracket(z)=\llbracket q\rrbracket(z)
818  \quad\text{for every admitted }z.
819 \]
820 The reverse implication is unnecessary. Distinct normal forms may denote the same function. Missing such an equivalence wastes an optimization opportunity but does not remove a valid candidate.
821 
822 \begin{theorem}[Sound ordered quotienting from checked equations]\label{thm:certified-quotient}
823 Assume the expression language is pure and total, every admitted schema equation is valid for all well-typed substitutions in the common semantic domain, and each normalization terminates after valid contextual replacements. For each $p_i$, keep its earliest grammar representative
824 \[
825  \rho(i)=\min\{j:n(p_j)=n(p_i)\}.
826 \]
827 Then $\rho(i)\le i$, $p_i$ and $p_{\rho(i)}$ agree on every admitted context, and every pointwise specification realizable in $\Gcal$ is realizable in its retained representatives. No confluence or complete semantic-equivalence decision procedure is required.
828 \end{theorem}
829 \begin{proof}
830 A schema identity remains true under a well-typed substitution. Purity and totality make replacement inside any expression context preserve its value. Induction over a finite derivation gives equality between an expression and its normalized result. Two expressions with the same result therefore have equal values by transitivity. The defining set for $\rho(i)$ contains $i$, giving existence and $\rho(i)\le i$. Replacing a satisfying expression by its representative preserves every pointwise requirement. The argument uses the soundness of each actual derivation, not uniqueness or completeness of normalization.
831 \end{proof}
832 
833 In the reference implementation, a successful rewrite must decrease a size-and-structural-order measure. Rewriting introduces no free variables or literals outside the finite input-and-library vocabulary, and never increases size. Only finitely many terms lie below the initial size over that vocabulary, so there is no infinite decreasing rewrite sequence. The index keeps the original earliest AST, not the normalized AST. This preserves the reference learner's output convention and its program interpreter cost on every teacher proposal.
834 
835 \begin{theorem}[Preservation of ordered counterexample-guided acquisition]\label{thm:cegis-quotient}
836 Consider a learner that scans a finite ordered grammar, retains every counterexample, tests candidates against those examples in a fixed order, and submits only consistent candidates to a deterministic teacher. The teacher returns the first disagreement in a fixed complete finite context order, or accepts. Under Theorem~\ref{thm:certified-quotient}, scanning only the earliest representatives produces exactly the same submitted ASTs, counterexamples, and final accepted AST or grammar-exhaustion outcome. With the original AST interpreter retained, it performs no more retained-example evaluations or interpreter-node visits. Its teacher calls and teacher-evaluation work are unchanged. Quotient construction, storage, and dispatch costs are separate.
837 \end{theorem}
838 \begin{proof}
839 Consider a removed expression $p_i$ and its earlier representative $p_j$. If the reference learner accepted $p_j$, it never reaches $p_i$. Otherwise a retained example refuted $p_j$, either before its teacher call or as a result of that call. That example is still retained when $p_i$ is reached. Semantic equality means the same example refutes $p_i$, so the reference learner never submits $p_i$ to the teacher. Deleting that unsuccessful consistency check leaves the sequence of proposals unchanged. Induction over the ordered scan gives the same candidate AST at every teacher call. The deterministic teacher then supplies the same first counterexample or acceptance. Removed candidates contribute only nonnegative evaluation work, while submitted expressions and their evaluations remain identical. If the finite grammar is exhausted, both learners have rejected the same possible behaviors.
840 \end{proof}
841 
842 The theorem concerns an extensional target and a fixed candidate order. A teacher that accepts based on source identity, or a learner that forgets old counterexamples, does not satisfy it. Nor does equality of return values make two candidates equal in execution cost, memory use, or causal side effects. To preserve a different resource-constrained objective, one must keep appropriate nondominated representatives or include those observables in the equivalence contract. The reference deliberately preserves the first original AST rather than selecting an uncharged cheaper replacement.
843 
844 \subsection{Cold reacquisition and additional finite task families}
845 The 3,960-expression grammar reduces to 1,362 retained representatives. Reacquiring the original capacity predicate starts with no task counterexamples and no installed copy of the answer. The original scan considers 190 candidates, while the quotient scan considers 76. Both submit the same four candidate ASTs, receive the same three counterexamples, and return the identical five-node expression. Retained-example checks fall from 282 to 112. Total interpreter-node visits in that task fall from 1,898 to 1,376. Teacher comparisons remain 210.
846 
847 The frozen quotient is next used for nine finite targets involving sums, extrema, comparisons, and equality, followed by a parity target that is not expressible on its complete declared domain. These are changed target functions in the same arithmetic language, not a statistical sample of unrelated research domains. The first nine use all 256 contexts in $\{0,1,3,5\}^4$. The parity control uses all contexts in $\{0,1,2,3\}^4$, so more than one even value is present.
848 
849 \begin{center}\small
850 \begin{tabular}{@{}lrr@{}}\toprule
851 Finite target & Original interpreter visits & Quotient interpreter visits\\\midrule
852 Sum exceeds capacity & 4,611 & 3,517\\
853 Minimum below threshold & 7,762 & 5,553\\
854 Maximum equals a value & 26,407 & 10,116\\
855 Sum equals a value & 29,357 & 12,311\\
856 Parity outside the grammar & 54,045 & 18,728\\\midrule
857 Complete ten-target batch & 196,384 & 85,162\\\bottomrule
858 \end{tabular}
859 \end{center}
860 
861 Every submitted candidate and counterexample trace agrees exactly between the two learners. The parity target produces grammar exhaustion in both. A bounded grammar's failure is not a proof that the target function is uncomputable.
862 
863 \begin{figure}[!ht]\centering
864 \includegraphics[width=.94\linewidth]{figures/meta_acquisition_cost.pdf}
865 \caption{Repeated task-synthesis evaluations are reduced while the teacher trace remains fixed. Values are exact interpreter-node counts in the stated finite cases. Equation discovery, checking, quotient construction, and stored library costs are not included in these bars and are reported separately.}\label{fig:meta-acquisition-cost}
866 \end{figure}
867 
868 \subsection{The stronger normalizer and the cost of preparing the shortcut}
869 A supplied full arithmetic normalizer retains 1,352 representatives, ten fewer than the learned library. It therefore removes at least as much semantic redundancy under this implementation's normal-form relation. The learned library is not claimed to outperform that stronger prior. This control identifies the result as automatic acquisition of a useful search representation from the supplied reasoning substrate, not a new best-in-class synthesis algorithm.
870 
871 The library-development ledger records 1,215 probe evaluations, 3,519 probe interpreter-node visits, 1,068 proposed equations, and 584 successful checked axiom steps. Proof search also attempts proposals it cannot establish. Applying the admitted library to the whole grammar costs 19,440 normalizer-node visits and 518,140 schema-match attempts, with 4,798 successful replacements. Grammar generation, proof search, bookkeeping, and serialization remain distinct charged phases. These event counts do not encode every Python instruction.
872 
873 Let $C_{\rm prepare}$ be the complete preparation cost in a declared common resource model, including failed proposals and certificate checking, and let $d_t$ be the subsequent saving on task $t$ after including dispatch. Reuse is beneficial in that model exactly when
874 \[
875  \sum_{t=1}^{T}d_t>C_{\rm prepare}.
876 \]
877 This is the earlier amortization identity applied to acquisition itself. The reference does not convert unlike counters into a universal wall-clock claim. Even one setup coordinate, 518,140 schema matches, exceeds the 522 interpreter-node visits saved in one cold capacity-rule run. A short workload or an expensive matcher can make the full modification undesirable.
878 
879 \subsection{A cached proof representation has a scope}
880 The quotient records the grammar's contents, order, and declared integer semantics. Loading a cache requires checking those bindings and reconstructing its representative map from the admitted proofs. Adding syntax or changing order requires rebuilding the index. Extending the grammar can still reuse an equation library when every substituted operation is pure, total, and retains the relevant types and meanings.
881 
882 \begin{counterexample}[The same operator spelling with changed semantics]\label{ex:semantic-cache}
883 The identity $x+0=x$ is valid for ordinary addition. Suppose a revised interpreter uses the same printed symbol but executes $a\mathbin{\oplus}b=a+b+1$. Then $x\mathbin{\oplus}0\ne x$. A cache certified for the former interpreter cannot be imported merely because its expression strings still parse. A semantic identifier helps detect ordinary version mismatch, but an identifier falsely attached to a changed implementation is not itself proof of faithful execution.
884 \end{counterexample}
885 
886 \section{A repair-relative certificate that can be updated cheaply}\label{sec:weighted-pruning}
887 The singleton pruning result remains valid within its original scope. To move beyond that scope, the compiler must account for what a repair can accomplish, not merely count hidden cases. An exact minimum repair cover can be expensive. A feasible lower-bound witness is often enough to exclude an impossible branch.
888 
889 Let $X$ be a finite immutable state set and let $S_r\subseteq X$ be the success set of repair $r$. Choose nonnegative rational weights $w_x$ satisfying
890 \begin{equation}\label{eq:repair-weights}
891  \sum_{x\in S_r}w_x\le1\quad\text{for every permitted repair }r.
892 \end{equation}
893 This is a feasible dual weight assignment for unweighted set cover. We use only its elementary weak-duality property, not an assumption that the best assignment has been found~\cite{williamson}.
894 
895 \begin{proposition}[Repair-relative weight and prefix obstruction]\label{prop:weighted-cover}
896 Suppose a total immutable deterministic binary diagnostic tree succeeds on nonempty support $B$ and has $L$ reachable leaves and maximum query depth $h$. Under~\eqref{eq:repair-weights},
897 \[
898  \sum_{x\in B}w_x\le L\le2^h.
899 \]
900 At a candidate query root with $h\ge1$ remaining query levels, if the cases already read into either outcome branch have weight greater than $2^{h-1}$, no assignment of its unread reports can make that branch repairable within the remaining depth. This implication is valid even when one repair succeeds in several states.
901 \end{proposition}
902 \begin{proof}
903 Immutable deterministic execution partitions $B$ into its nonempty reachable leaf supports. Each leaf support is contained in the success set of its chosen repair. Nonnegativity and~\eqref{eq:repair-weights} give weight at most one for every leaf, so summing gives the first inequality. A binary tree of depth at most $h$ has at most $2^h$ leaves, by induction on $h$. At a candidate root, each child has at most $h-1$ query levels. Unread cases can only add nonnegative weight to an outcome branch, so a prefix already exceeding its leaf capacity cannot be rescued by any completion.
904 \end{proof}
905 
906 \begin{theorem}[Streaming search with a checked repair-weight witness]\label{thm:weighted-streaming}
907 Fix total immutable binary unit-cost experiments, unit-cost repairs with arbitrary fixed success sets, an ordered initial support, a repair order, an experiment order, a finite query horizon, and a weight vector satisfying~\eqref{eq:repair-weights}. Consider depth-first search that first checks for a common successful repair and otherwise explores informative query roots in that order, rejecting child supports whose weight exceeds their remaining binary leaf capacity. Replacing each complete root scan by a scan that stops on the first overweight prefix preserves the exact first returned tree or finite-horizon infeasibility result. It never increases model-record reads during search. These statements do not establish a Pareto-optimal storage frontier or free weight arithmetic.
908 \end{theorem}
909 \begin{proof}
910 Proposition~\ref{prop:weighted-cover} shows that an overweight support has no successful tree at its depth. A root stopped on an overweight prefix would still be rejected after a complete scan because all further contributions are nonnegative. Every root not stopped early is partitioned identically, with the same row and outcome orders. Induction over depth and the ordered root scan therefore yields identical first successful children and identical returned trees. A query with one reachable outcome leaves the immutable support unchanged, so deleting such a query never destroys the existence of a depth-bounded successful tree. The search over the remaining roots and repairs is finite and complete for existence. Early stopping deletes only unread suffixes of roots the complete scan also rejects, proving the read comparison. The final witness checker and weight-scope checker remain required and are charged separately.
911 \end{proof}
912 
913 \subsection{Constructing a feasible witness without solving the whole cover problem}
914 A simple supplied constructor processes states in order. It raises the current state's weight by the smallest remaining slack among repairs containing that state, and updates those repair loads. An uncovered state may receive a finite weight of one. Every step preserves nonnegativity and all repair constraints. The result is checked independently by resumming every repair's weight. It can be a weak certificate. In particular, the all-zero assignment is always feasible and excludes nothing.
915 
916 For example, on three cases with success sets $\{1,2\}$, $\{2,3\}$, and $\{1,3\}$, the ordered greedy constructor returns total weight one. The feasible fractional assignment $w_1=w_2=w_3=1/2$ has total $3/2$ and proves that at least two leaves are required. Thus the supplied constructor does not optimize the bound. Both assignments are valid and neither creates a missing experiment.
917 
918 The construction is not itself learned in this revision. It is a semantic extension showing how the compiler can continue when successful repair no longer means exact state identification. A learner may later propose a stronger weight assignment, but the same inequalities would still govern admission. The work of producing and checking those weights cannot be hidden inside one cheap predicate call.
919 
920 \subsection{Paired repairs change the task, not just its notation}
921 Consider $2g$ possible hidden cases divided into $g$ pairs, where $g$ is a power of two. One repair succeeds on both members of each pair. The query language contains equality questions and bits of the pair index. The greedy weight constructor gives weight one to the first member of each pair and zero to the second, with total weight $g$. A depth $\log_2g$ tree is both necessary and sufficient, so the diagnostic-plus-repair work is $1+\log_2g$ and a full binary witness uses $2g-1$ records.
922 
923 \begin{center}\small
924 \begin{tabular}{@{}rrrrr@{}}\toprule
925 Hidden cases & Repair groups & Full scan reads & Streaming reads & Work / records\\\midrule
926 4 & 2 & 20 & 18 & 2 / 3\\
927 8 & 4 & 152 & 120 & 3 / 7\\
928 16 & 8 & 864 & 608 & 4 / 15\\
929 32 & 16 & 4,416 & 2,864 & 5 / 31\\\bottomrule
930 \end{tabular}
931 \end{center}
932 
933 These columns count search reads only. For the 32-case problem, each method additionally pays 1,152 scope-table reads and 256 witness-checking reads, giving 5,824 versus 4,272 total model reads. Weight construction, repair-success-set checks, rational additions, and comparisons have their own ledger. The streaming search makes 2,941 capacity comparisons rather than 1,073. Both methods return the identical literal tree.
934 
935 This is not a generalization score obtained by making the task easier. The comparison is between two discovery procedures on the same paired-repair task. The difference between that task and the earlier singleton task explains why the earlier cardinality certificate would be invalid here.
936 
937 \begin{figure}[!ht]\centering
938 \includegraphics[width=.93\linewidth]{figures/repair_relative_classes.pdf}
939 \caption{Eight hidden cases need only four repair distinctions when each repair succeeds on a pair. The displayed weights certify a four-leaf lower bound. They do not claim that every feasible weight assignment is optimal or that every query library can realize the bound.}\label{fig:repair-relative}
940 \end{figure}
941 
942 \begin{counterexample}[A newly admitted repair invalidates the old lower-bound certificate]\label{ex:weight-invalidation}
943 In an eight-case paired model, the original weights have total four. Add a repair that succeeds on every case. Its weight load is four, violating~\eqref{eq:repair-weights}. The old certificate must be rejected. Recomputing a feasible assignment gives total one, and the compiler returns the universal repair with no query, work one, and one stored record. The success of that repair does not retrospectively validate the obsolete weight assignment.
944 \end{counterexample}
945 
946 A capacity-feasible prefix still does not guarantee that available experiments can distinguish the required repair classes. The implementation retains a model with only a constant report: its cover weights fit a nominal depth bound, but no successful tree exists. A lower-bound certificate is a reason to reject some candidates, not a generator of a missing experiment.
947 
948 \section{One chain from acquired equations to an improved investigator}\label{sec:meta-chain}
949 The levels can now be connected without substituting one kind of evidence for another. The equational learner produces a checked library. The library prepares an ordered search representation. That representation reduces the repeated evaluation work of acquiring the earlier pruning rule and other finite targets. The rule's separate scope certificate then permits its use in the diagnostic compiler. Each stage retains the predecessor's semantic comparison.
950 
951 \begin{proposition}[Composition of acquisition and compiler preservation]\label{prop:meta-chain}
952 Assume the ordered quotient satisfies Theorem~\ref{thm:cegis-quotient}, the resulting task expression passes the unchanged compiler-scope checker, and the original and optimized compilers satisfy the common-domain premises of Theorem~\ref{thm:streaming-pruning}. If all stages complete, quotient-guided rule acquisition followed by optimized compilation returns the same learned expression and the same diagnostic controller as ordinary rule acquisition followed by the reference ordered compilation. In a common additive resource model, writing $K$ for extra preparation cost, $A,A'$ for the two acquisition costs, and $D,D'$ for the two compilation costs, the composite saves work exactly when
953 \[
954  (A-A')+(D-D')>K.
955 \]
956 The semantic conclusion does not imply the cost inequality, and a budget interruption does not imply infeasibility.
957 \end{proposition}
958 \begin{proof}
959 Theorem~\ref{thm:cegis-quotient} gives the same acquired AST and teacher transcript. Passing the unchanged scope checker places that expression in the stated compiler-preservation theorem, which gives the same returned controller. The reference total is $A+D$ and the modified total is $K+A'+D'$. Subtracting gives the displayed necessary and sufficient cost condition. Neither semantic theorem bounds $K$ or assigns exchange rates among distinct resource units. An interrupted finite search has not exhausted its candidates and therefore cannot use completeness to infer infeasibility.
960 \end{proof}
961 
962 \subsection{The recursive achievement and its next boundary}
963 The retained change is now used to produce future discovery rules more economically in a specific evaluation coordinate. It is not merely a better diagnostic result. The learner's search representation has changed, while the pointwise target, oracle transcript, and final generated program remain fixed. This is a bounded meta-improvement with an explicit implementation and cost boundary.
964 
965 It does not require that a useful self-improver invent every foundational component. It does require us to locate those foundations honestly. Here the schema proposer, primitive axioms, checking engine, and ordered-quotient construction are given. The acquired equation library and grammar quotient are generated. A supplied stronger normalizer can outperform the learned library, and a short workload can fail to repay its preparation cost. Extending the result to learned physical semantics, larger generated languages, uncertain arithmetic, or repeated improvements of the library learner itself requires additional work.
966 
967 \subsection{The boundary of the first edition}
968 The finite construction now covers repair discovery, compiler revision, synthesized pruning, acquired search representations, and repair-relative scope extension. Part~\ref{part:release-contract} consolidates their dependency and resource contracts. A first edition need not claim that general intelligence follows or that the outermost learner has become unboundedly self-improving. Those are distinct research questions. The completed scope is the explicit finite chain and the evidence required to interpret it.
969 
970 \clearpage\part{Keeping a revision's guarantees applicable}\label{part:release-contract}
971 \section{A certificate belongs to a changing realization}\label{sec:certificate-life}
972 A proof can remain mathematically correct while ceasing to justify an installed shortcut. The equation library was proved for pure, total integer expressions. The ordered quotient was constructed for one grammar order. A repair-weight certificate was checked against particular success sets. A resource comparison assigned costs to specified events. None of those objects is licensed to retain its old interpretation after every component bearing the same name has changed.
973 
974 This is the final integration problem for the first edition. The earlier sections provide distinct certificates for the outputs of different stages. A continuing system must also identify which of those certificates remain applicable after a revision. The appropriate response is not to repeat every discovery from scratch, nor to regard an old passing record as timeless. It is to retain the actual dependencies, reject unsupported reuse, and recheck the affected obligations before relying on them again.
975 
976 \subsection{A declared dependency graph}
977 Let an artifact state be $a=(a_1,\ldots,a_d)$. Its components may include operation semantics, a grammar and its order, an equation library, experiment tables, repair-success sets, a returned controller, and a resource model. A finite directed acyclic graph has one vertex $v$ for each claimed guarantee. Its incoming vertices $\operatorname{pa}(v)$ identify guarantees used as premises. Its direct dependency set $D_v\subseteq\{1,\ldots,d\}$ identifies the artifact components used directly. Each vertex carries a witness $w_v$ and a local verification rule.
978 
979 The dependency declaration must be \emph{semantically complete}: the meaning of the claim and the local rule is determined by the components in $D_v$ and the stated parent claims. Hidden environment assumptions cannot be left outside this declaration merely because the implementation does not know how to check them. They can instead be recorded as explicit external premises. Verifier soundness, the interpretation of primitive arithmetic, and the faithfulness of the supplied model to an external process are not established by naming them in a registry.
980 
981 Suppose a revision replaces $a$ by $a'$. Mark a vertex directly stale whenever one of its declared component values differs. Let $\Delta$ be the union of those vertices and all their descendants in the dependency graph. Equivalently, in a topological order, mark $v$ whenever
982 \[
983  a|_{D_v}\ne a'|_{D_v}
984  \quad\text{or}\quad
985  \operatorname{pa}(v)\cap\Delta\ne\varnothing.
986 \]
987 Here equality refers to the declared artifact value, not merely an unchanged version label. This procedure is conservative. A changed premise may leave the conclusion true, but the old evidence is not reused without a further argument.
988 
989 \begin{theorem}[Dependency-complete reuse across a revision]\label{thm:certificate-reuse}
990 Assume a finite acyclic dependency graph, semantically complete direct dependencies, and sound local verification rules. Suppose the old witnesses establish every old claim from the declared external premises. After a revision, the old claims outside $\Delta$ remain established by their old witnesses. If every vertex in $\Delta$ is re-established in topological order using the revised artifact values and already established parent claims, all revised claims hold. If an affected vertex is not re-established, no dependent claim is justified by this reuse rule alone. These statements are conditional on the external premises applicable to the revised realization.
991 \end{theorem}
992 \begin{proof}
993 A vertex outside $\Delta$ has unchanged direct inputs and no parent in $\Delta$. Inducting through a topological order, its parents remain established with the same meanings, so dependency completeness leaves its old verification argument applicable. For an affected vertex, assume its parents have already been established in the revised realization. Soundness of the newly checked local rule then establishes its revised claim. A second induction yields the result when every affected vertex is re-established. Without that step, the rule has an unsupported premise and supplies no conclusion along that dependency. This is a limitation of the reuse argument, not a proof that the dependent claim is false.
994 \end{proof}
995 
996 The argument is elementary induction over declared dependencies. Its role here is to connect the exact preservation results to their continued use. It does not compute the complete dependency graph from arbitrary source code. A dependency cycle requires an additional justified rule, such as an independently proved invariant. The finite replayer in this edition rejects an unsupported cycle rather than interpreting mutual assertions as evidence.
997 
998 \begin{counterexample}[An unchanged name hides a changed premise]\label{ex:incomplete-dependency}
999 A stored claim asserts that two binary values $u$ and $v$ agree. Initially both are zero. A registry records only $u$ as a dependency and continues to validate that its stored value is zero. Change $v$ to one without changing $u$. The declared check still passes, but the claimed equality is false. Recording and replaying the incomplete registry cannot repair its omitted premise. Dependency completeness is a mathematical assumption, not a consequence of serialization or a checksum.
1000 \end{counterexample}
1001 
1002 \subsection{The scopes that actually have to be carried}
1003 The implemented constructions require different bindings. An equation witness includes the supported arithmetic semantics and the local derivation rules. A quotient includes the equation library and the full ordered grammar. Exact candidate-trace preservation additionally requires the extensional teacher, fixed context order, and retained counterexamples. The compiler rule has its own integer-prefix and singleton-repair scope. Weighted pruning instead checks every repair-success set and the nonnegative weights. A returned tree must be checked against the actual experiment effects, observations, repair meanings, and horizon.
1004 
1005 Cost and evidence claims add other dependencies. A reduction in model reads is not a price-independent reduction in total work. An audit comparing a frozen candidate cannot be carried unchanged to a new candidate merely because the score field has the same name. Statistical independence and commitment order may depend on events outside the program's observation boundary. The manifest must state whether those conditions are guaranteed by the controlled construction, supplied by a trusted interface, or not established.
1006 
1007 The reference certificate manager therefore has several outcomes. A claim is \emph{valid} when its declared inputs match and its local evidence is replayed successfully. It is \emph{stale} when a direct input changed, \emph{blocked} when a required parent is unavailable or different, \emph{rejected} when its local record fails, and \emph{missing} when no witness was supplied. A timeout is not successful replay. Nor is a valid resource assessment necessarily favorable: the assessment may correctly report a negative saving.
1008 
1009 The reference manager uses exact canonical snapshots for direct input comparisons and content identifiers for linking parent evidence. Those identifiers aid integrity checks. They do not establish who produced a witness or whether an external assumption is true. The manager and dependency registry are supplied components. This edition does not claim that the learner derived its own trusted verification base.
1010 
1011 \subsection{A repair-language change through the complete record}
1012 The first-edition demonstration checks the retained equation library, its ordered quotient, the capacity rule's supported form, a repair-weight witness, a returned weighted diagnostic tree, and a conditional resource assessment. The equation and diagnostic branches remain distinct. A valid capacity expression is not silently substituted for the weighted compiler's separate certificate.
1013 
1014 In the 32-case paired-repair example, the accepted weight total is sixteen and the returned controller has work five and 31 records. Add a repair that succeeds in every case. The old weight certificate becomes stale, and direct rechecking confirms that it fails the new repair constraint. Its dependent controller and cost claims cannot rely on it through the old chain. The arithmetic equations and ordered grammar quotient remain applicable because their declared premises have not changed.
1015 
1016 Rebuilding the weight witness gives total one. The compiler then returns a universal repair with work one and one record. The new controller is checked against the new repair language. The old cost comparison is deliberately not reissued: a claim about the work of producing the former controller does not become a claim about this different search simply because both controllers are valid. The appropriate repair of that claim is a new comparison under a stated workload.
1017 
1018 Changing only the resource prices has the opposite pattern. The semantic certificates remain applicable, while the cost conclusion needs to be recomputed. Changing the grammar order invalidates the ordered quotient and its recorded acquisition lineage, not the independently proved arithmetic identities. These cases illustrate selective invalidation without equating it with a complete theory of arbitrary self-modification.
1019 
1020 \section{One resource ledger for the complete improvement}\label{sec:integrated-ledger}
1021 The manuscript's numerical comparisons concern several different units. A model-record read, an interpreter-node visit, an arithmetic comparison, a stored tree record, and a serialized byte are not interchangeable. The purpose of a complete ledger is to preserve those distinctions until a specific execution or economic model justifies a conversion.
1022 
1023 \begin{small}\begin{longtable}{@{}P{.25\textwidth}P{.34\textwidth}P{.33\textwidth}@{}}\toprule
1024 Phase & Recorded object or event & What the count does not supply\\\midrule\endhead
1025 Model and language acquisition & Supplied experiment tables, grammar, feature registry, primitive axioms & An executed calibration of an unknown physical process, or free discovery of those foundations.\\
1026 Equation acquisition & 1,068 proposals, 336 admitted equations, 584 successful checked axiom steps & Proof completeness, a generally optimal equation set, or uncharged failed attempts.\\
1027 Search representation & 3,960 grammar expressions, 1,362 representatives, 518,140 schema-match attempts & Free preparation, hardware-time units, or superiority to the 1,352-representative supplied normalizer.\\
1028 Task-rule acquisition & 1,898 versus 1,376 interpreter-node visits for the capacity rule & All preparation costs, or a different teacher transcript. The retained four proposals agree.\\
1029 Compiler execution & Query-model reads, weight arithmetic, capacity comparisons, scope checks, witness replay & A universal conversion of avoided reads into elapsed time.\\
1030 Installed information & Equation-library serialization of 69,518 bytes, original programs, quotient records & Minimal description length, physical peak memory, or a byte-free interpreter.\\
1031 Online repair & Experiment and repair calls, plus complete stored tree records & Only the visited path's storage, or the cost of discovering the controller.\\
1032 Revision management & Bound snapshots, witness checks, parent comparisons, and replacement evidence & Free invalidation detection or a trusted explanation of undeclared external assumptions.\\\bottomrule
1033 \end{longtable}\end{small}
1034 
1035 The exact per-phase records remain in the source package. The table does not add unlike events into one total. In particular, retained storage is normally a capacity coordinate. Treating it as an additive expense requires a stated storage-duration or installation convention. Peak memory combines by its own rule, not by automatically summing all sizes ever observed.
1036 
1037 \subsection{Which gains survive a change of resource prices?}
1038 Fix an additive ledger with $d\ge1$ named event types. Let $K\in\mathbb R_{\ge0}^d$ be extra setup, let $s_i\in\mathbb R^d$ be the old-minus-new per-use event vector for workload type $i$, and let $n_i$ be its nonnegative integer multiplicity. The net event saving is
1039 \begin{equation}\label{eq:vector-saving}
1040  \Delta(n)=\sum_i n_i s_i-K.
1041 \end{equation}
1042 A price vector $w\in\mathbb R_{\ge0}^d$ specifies conversions into one declared additive resource measure. Its priced saving is $w\cdot\Delta(n)$. The prices are modeling assumptions, not learned hardware laws inferred from the event counts.
1043 
1044 \begin{proposition}[Resource dominance and declared price uncertainty]\label{prop:resource-prices}
1045 For a fixed ledger and workload, $w\cdot\Delta(n)\ge0$ for every nonnegative price vector $w$ if and only if $\Delta(n)$ is componentwise nonnegative. If admissible prices form the convex hull of a nonempty finite set $W_0$, then
1046 \[
1047  \min_{w\in\operatorname{conv}(W_0)}w\cdot\Delta(n)
1048  =\min_{w\in W_0}w\cdot\Delta(n).
1049 \]
1050 Thus strict improvement throughout that price set holds exactly when every listed vertex gives a strictly positive margin. The claims concern the same workflow, workload, and complete additive ledger.
1051 \end{proposition}
1052 \begin{proof}
1053 Componentwise nonnegativity makes every nonnegative weighted sum nonnegative. If coordinate $j$ is negative, the $j$th coordinate vector is a nonnegative price vector giving a negative sum, proving the converse. Every point of the specified convex hull is a convex combination of its listed points. Linearity makes its priced saving the same combination of their savings, which cannot be smaller than their minimum. A listed minimizer attains that minimum, proving the equality and the strict criterion.
1054 \end{proof}
1055 
1056 This is ordinary linear accounting, not a new optimization principle. It prevents a system from asserting a price-independent gain after improving only one coordinate. The deterministic workload count must also be separated from an expectation over future tasks. Proposition~\ref{prop:amortization} addresses the latter under its stated assumptions. Changing the task mixture can change both the amount and the sign of an improvement.
1057 
1058 \begin{counterexample}[One valid controller, opposite resource conclusions]\label{ex:price-change}
1059 For the 32-case weighted-search comparison, the old-minus-new search-event vector is
1060 \[
1061  (1552,\ 1552,\ -1868)
1062 \]
1063 in model-record reads, rational additions, and capacity comparisons. Scope checking and final witness checking are equal for both procedures and cancel in this particular difference. Prices $(1,1,1)$ give a saving of 1,236 units. Prices $(1,0,1)$ give a loss of 316 units, and prices $(0,0,1)$ give a loss of 1,868 units. The identical returned controller remains valid in every comparison. None of the price choices was measured as a universal property of a processor.
1064 \end{counterexample}
1065 
1066 The zero setup in that isolated execution comparison is not a statement that preparing the whole improvement was free. For an explicitly hypothetical additional setup charge of 2,000 comparison units and prices $(1,1,1)$, one use loses 764 units while two uses save 472. The purpose of this small calculation is to expose the dependence on the declared ledger. The actual equation-discovery, proof-search, quotient-construction, and revision-management records must be included when assessing the entire first-edition workflow.
1067 
1068 \clearpage\part{Evidence and recursive continuation}
1069 \section{Evidence that survives candidate selection}\label{sec:evidence}
1070 A self-improvement procedure has an unusual incentive to find weaknesses in its own measurements. It searches repeatedly, retains favorable results, and changes the way later candidates are generated. A validation number can therefore become part of the training information even when it is never called a training label. This is a central issue in adaptive data analysis~\cite{dwork}.
1071 
1072 The correct distinction is between development evidence used to generate a candidate, selection evidence used to choose among candidates, and final evidence used to assess the selected procedure. A private test repeatedly consulted by an outer selector is still selection information for that outer process. Keeping it hidden from the inner solver does not make it independent of the entire lineage.
1073 
1074 A practical record should identify what was frozen before each assessment, which outputs were exposed, and which claim the assessment supports. When a procedure changes a checker, both the checker change and the candidate it would approve cannot receive their only justification from the new checker's own approval. That restriction does not forbid improving evaluators. It prevents the target of validation from silently changing the validation standard in the same step.
1075 
1076 \begin{proposition}[Conditional error budgets across an adaptive lineage]\label{prop:lineage}
1077 Let $\mathcal H_{t-1}$ be the information available before attempt $t$. Suppose the event $A_t$ that attempt $t$ accepts a false improvement claim satisfies
1078 \[
1079 \Pr(A_t\mid\mathcal H_{t-1})\leq\delta_t
1080 \quad\text{almost surely},
1081 \]
1082 for deterministic $\delta_t\geq0$ with $\sum_{t\geq1}\delta_t\leq\delta$. Then
1083 \[
1084 \Pr\big(\exists t\geq1:A_t\big)\leq\delta.
1085 \]
1086 The candidate-generating process and the time at which attempts stop may depend on the earlier history.
1087 \end{proposition}
1088 \begin{proof}
1089 Taking expectations gives $\Pr(A_t)\leq\delta_t$. The union bound gives the result for any finite number of attempts. The infinite statement follows from continuity of probability for the increasing finite unions. A history-dependent stop can only reduce the set of attempts whose acceptance events occur.
1090 \end{proof}
1091 
1092 No independence between attempts is needed. The conditional premise is stronger than a marginal guarantee for a candidate considered before adaptive selection. It must be justified by the actual sampling or verification mechanism. A budget such as $\delta_t=\delta/[t(t+1)]$ is summable, but writing that schedule does not make an invalid test conditionally valid.
1093 
1094 \subsection{One sufficient fresh-audit construction}
1095 Freeze a candidate and its comparator using the prior history. Draw $n_t$ fresh evaluation cases conditionally independently from the declared distribution and record paired score differences $Y_i\in[-1,1]$. Let $\Delta_t$ be their conditional mean and $\widehat\Delta_t$ their average. The bounded-variable concentration inequality gives
1096 \[
1097 \Pr\left(\widehat\Delta_t-\Delta_t\geq r\mid\mathcal H_{t-1}\right)
1098 \leq \exp(-n_tr^2/2).
1099 \]
1100 Consequently, accepting a claim $\Delta_t\geq\gamma$ only when
1101 \begin{equation}\label{eq:audit}
1102 \widehat\Delta_t-\sqrt{2\log(1/\delta_t)/n_t}\geq\gamma
1103 \end{equation}
1104 meets the preceding conditional error requirement for that claim. This is a fixed-sample sufficient construction. The candidate and $n_t$ may depend on past data, but $n_t$ is fixed before this audit is examined. Inspecting the same sample repeatedly and stopping at a favorable value requires a time-uniform method or a separately justified spending rule. Time-uniform concentration is an established subject~\cite{howard}.
1105 
1106 Formula~\eqref{eq:audit} can be conservative and expensive. It is included to make the premise operational, not as a claim that this test is optimal. If evaluator randomness, shared tasks, or dependence between runs changes the sampling unit, the analysis must change with it. Thousands of messages from one trained lineage do not automatically become thousands of independent improvement trials.
1107 
1108 \begin{counterexample}[Reused evidence can reward memorization]\label{ex:reuse}
1109 A task has $N$ equally likely names and an externally fixed binary answer for each. After the answers on a development subset become available, a candidate stores them and gives the wrong answer on every other name. It is perfect on that subset and has true accuracy equal only to the subset's fraction of the task universe. An outer loop that keeps selecting by the same subset can improve its reported score without improving beyond the information it has exposed. Renaming the subset a holdout does not restore independence.
1110 \end{counterexample}
1111 
1112 \subsection{Proof obligations and performance evidence}
1113 A semantic proof can establish that a proposed operation preserves a specified relation. A program checker can establish that a finite tree respects the supplied domains and budgets. A fresh performance comparison can support usefulness on a declared task law. None of these establishes the truth of every environmental premise. Their evidence types should remain separate in an improvement receipt.
1114 
1115 The constructive tests shipped with this paper are deterministic finite enumerations. They are not samples from an AGI population, and they do not use~\eqref{eq:audit} to manufacture confidence intervals. Their role is to check the implementations of the stated finite arguments.
1116 
1117 \section{Sequential evidence for an improved discovery procedure}\label{sec:anytime}
1118 The deterministic compiler comparison above can be checked on its whole declared family. A learned discovery procedure evaluated on fresh stochastic tasks would need another kind of evidence. It may also be expensive enough that the auditor would like to inspect results sequentially and stop once the evidence is adequate. The fixed-sample rule in Section~\ref{sec:evidence} does not automatically justify that stopping policy.
1119 
1120 We give a small time-uniform alternative whose finite arithmetic is directly inspectable. Before an audit begins, freeze the candidate procedure, its comparator, their installed information, the task law, the common resource cap, and a paired score $Y_t\in[-1,1]$. Timeouts and invalid outcomes must have a stipulated score rather than disappear from the sample. Fix a proposed improvement margin $\gamma\in[0,1)$.
1121 
1122 The null condition is
1123 \begin{equation}\label{eq:anytime-null}
1124 \E[Y_t\mid\mathcal H_{t-1}]\leq\gamma
1125 \quad\text{for every audit step }t,
1126 \end{equation}
1127 where $\mathcal H_{t-1}$ includes all information available before the next score. Conditionally independent cases from a fixed task law with mean at most $\gamma$ satisfy this condition. An auditor cannot change the task distribution toward favorable cases and retain that interpretation without a new argument.
1128 
1129 Choose a nonnegative bet $\lambda_t$, measurable from $\mathcal H_{t-1}$, with $\lambda_t\leq1/(1+\gamma)$. Define
1130 \begin{equation}\label{eq:anytime-capital}
1131 E_0=1,\qquad E_t=E_{t-1}\bigl(1+\lambda_t(Y_t-\gamma)\bigr).
1132 \end{equation}
1133 The variable $E_t$ is an evidence process, not a posterior probability that the candidate is better. Predictability means choosing the bet before observing the score to which it is applied.
1134 
1135 \begin{theorem}[An anytime-valid paired improvement audit]\label{thm:anytime}
1136 Under~\eqref{eq:anytime-null} and the stated predictable bet constraints, $E_t$ is a nonnegative supermartingale. For every $\delta\in(0,1)$,
1137 \[
1138 \Pr\left(\sup_{t\geq0}E_t\geq1/\delta\right)\leq\delta.
1139 \]
1140 Consequently an audit may reject the stated null at its first crossing of $1/\delta$, while choosing its stopping time from the observed audit history. The result does not require a predetermined number of cases or independence beyond the conditional-mean premise.
1141 \end{theorem}
1142 \begin{proof}
1143 Since $Y_t-\gamma\geq-(1+\gamma)$, every factor in~\eqref{eq:anytime-capital} is nonnegative. Conditional expectation and predictability give
1144 \[
1145 \E[E_t\mid\mathcal H_{t-1}]
1146 =E_{t-1}\bigl(1+\lambda_t(\E[Y_t\mid\mathcal H_{t-1}]-\gamma)\bigr)
1147 \leq E_{t-1}.
1148 \]
1149 Let $\tau$ be the first threshold crossing. For a finite $N$, the stopped process at $\tau\wedge N$ still has expected value at most one, by induction on the stopped conditional expectations. On $\{\tau\leq N\}$ its value is at least $1/\delta$, while it is nonnegative otherwise. Therefore $\Pr(\tau\leq N)\leq\delta$. Letting $N$ increase proves the result for any crossing time.
1150 \end{proof}
1151 
1152 This is the elementary nonnegative-supermartingale method underlying time-uniform evidence, not a new general concentration theorem~\cite{howard}. The contribution here is its explicit paired comparison and its placement within the recursive resource and information contract. In particular, an audit observation is a complete comparable attempt by each discovery procedure, not an arbitrary message emitted within one attempt.
1153 
1154 \subsection{Why seeing the outcome before choosing the bet fails}
1155 \begin{counterexample}[Hindsight betting creates false evidence]\label{ex:hindsight-bet}
1156 Let $Y_t$ be independent fair signs and $\gamma=0$. Choose $\lambda_t=1$ when the current sign is positive and zero otherwise. This invalid rule doubles $E_t$ on a positive score and leaves it unchanged on a negative one. Within four scores it crosses the threshold four whenever at least two scores are positive, an event of probability $11/16$. This exceeds the nominal bound $1/4$. Each individual bet lies in the numerical range $[0,1]$. What fails is predictability.
1157 \end{counterexample}
1158 
1159 A data-dependent stopping rule is allowed by the theorem. A data-dependent choice that looks at the \emph{current} outcome before staking on that outcome is not. The software can validate the numerical range of a bet, but it cannot infer the provenance of an externally supplied bet from that number alone. A usable audit receipt must record the commitment order and the sampling contract.
1160 
1161 The same issue arises when a candidate is edited after seeing an audit result. The resulting process no longer evaluates one frozen procedure under its original interpretation. It can start a new comparison, debit a new conditional error budget, and retain the earlier result as development evidence. It cannot silently reuse the old evidence process as though the candidate had not changed.
1162 
1163 \subsection{Evidence across recursive generations}
1164 For attempt $j$, condition on the complete earlier lineage, freeze its candidate, and initialize a fresh valid audit at $E_0^{(j)}=1$ with error allowance $\delta_j$. If $\sum_j\delta_j\leq\delta$, Proposition~\ref{prop:lineage} bounds the probability of ever accepting a false margin claim by $\delta$. Each audit can stop sequentially, and the next candidate may depend on completed earlier audits. The premise remains conditional validity for each actual attempt.
1165 
1166 Exact certificate checks and sequential evidence still have different jobs. A table-defined compiler can be checked for admissibility and optimality on its formal input without making a claim about a population of tasks. A stochastic audit can support a productivity comparison on that population without proving every generated program correct. The recursive system needs both whenever its claim combines semantic validity and statistical usefulness.
1167 
1168 The new reference suite enumerates finite rational null paths and confirms the crossing bound in those cases. It also checks the hindsight counterexample. No live learner was evaluated with this test, and the deterministic compiler counts are not retroactively presented as independent random samples.
1169 
1170 \section{The complete cost of becoming a better improver}\label{sec:cost}
1171 A procedure can save work on each future task and still be a poor investment when its discovery and validation are expensive. Conversely, a costly method can be worthwhile when it is reused sufficiently often. Both observations are ordinary resource accounting. They become especially important when a claimed improvement shifts work from inference into training, into a translator, or into an external oracle.
1172 
1173 Use a resource vector rather than an unexplained token total:
1174 \[
1175 C=(C_{\rm model},C_{\rm search},C_{\rm validate},C_{\rm install},
1176 C_{\rm execute},C_{\rm store}).
1177 \]
1178 These coordinates need not share units. Model construction may involve environment observations. Search and validation may involve processor work. Installation may require conversion or compilation. Execution work concerns one deployment. Storage concerns the retained library and complete controller. A scalar comparison needs declared conversion weights or a common physical budget, not an arbitrary sum of unlike quantities.
1179 
1180 For the hidden-cell instrument, a compiled tree has fifteen records even though a successful depth-three run visits only four. The bit-query API is installed for both procedures in the matched comparison. Its table representation, if used, occupies $n(n+\log_2n)$ Boolean entries for the chosen power-of-two family. The reported three-versus-seven diagnostic comparison does not imply that inspecting a large subset costs one machine instruction in every implementation. It uses one sensor call as its stipulated unit.
1181 
1182 \begin{proposition}[Amortization of a reusable process improvement]\label{prop:amortization}
1183 In a fixed additive resource unit, suppose installing a new procedure has incremental cost $C\geq0$ relative to the old one, and its expected per-use saving on an unchanged task distribution is $d>0$. If there are $N$ uses and no additional costs or changes in the task law, its expected cumulative saving is $Nd-C$. It is strictly resource-improving exactly when $N>C/d$.
1184 \end{proposition}
1185 \begin{proof}
1186 Linearity of expectation gives expected total use savings $Nd$, without requiring independence between uses when each has the stated expectation. Subtract the fixed incremental cost and solve the strict inequality.
1187 \end{proof}
1188 
1189 The formula is not a prediction of future demand. Distribution drift, maintenance, growing context, retrieval overhead, or a changed interface can alter $d$ or add costs. The value of the repair library depends on whether later problems actually admit its operations.
1190 
1191 \subsection{Larger search spaces can lower productivity}
1192 \begin{counterexample}[More expressibility with worse fixed-budget discovery]\label{ex:dilution}
1193 A search language has $N$ candidates, exactly one useful. A procedure samples uniformly with replacement $B\geq1$ times and recognizes usefulness perfectly after each sample. Its probability of finding the useful candidate is $1-(1-1/N)^B$. Adding an additional useless candidate preserves every old expression and strictly decreases this probability. The best attainable repair is unchanged, while the implemented discovery procedure becomes worse under the same sampling budget.
1194 \end{counterexample}
1195 
1196 This does not argue against grammar growth. It identifies what the learner must improve alongside growth: proposal probabilities, indexing, modular reuse, or informative pruning. The search space and the search distribution are different parts of the agent.
1197 
1198 An archive has a related ambiguity. The best true value among retained artifacts cannot decrease when an old artifact remains available under the same score. But a deployed selector can perform worse as retrieval becomes harder. The monotonicity of a hypothetical maximum is not the monotonicity of actual use. Resource-limited archive management belongs inside the recursive system rather than outside its reported budget.
1199 
1200 \section{A finite certificate for repeated improvement}\label{sec:recursion}
1201 A valid local change can destroy the ability to make another valid change. A new representation may discard the evidence needed to verify future proposals. A controller may consume the remaining budget while preserving the current task score. A shortcut can bypass an interface on which later transports depend. Recursive continuation therefore needs its own object.
1202 
1203 Let $Z$ be a finite set of complete lineage configurations. A configuration includes the currently selected solver and improver, retained libraries and evidence, the active comparison contract, and relevant resource state. The following theorem assumes this configuration is observed. Unknown configurations require belief-state modeling or a different synthesis result. No unrestricted introspection is inferred.
1204 
1205 Each $z$ has a finite set of authorized attempts $A(z)$. An attempt has a nonempty set $\Post(z,a)$ of possible successor configurations. This can represent all outcomes of a stochastic proposal or an abstract uncertainty set. A safe set $\Safe\subseteq Z$ encodes the declared semantic, evidence, authority, and resource conditions. A pause or terminal state may have a zero-progress self-loop. Actual expensive attempts must debit resources in $Z$, or the model must explicitly state their replenishment.
1206 
1207 Define
1208 \[
1209 K_0=\Safe,\qquad
1210 K_{n+1}=\{z\in K_n:\exists a\in A(z),\ \Post(z,a)\subseteq K_n\}.
1211 \]
1212 The descending finite sequence reaches a fixed point $\mathcal K$. It is the set from which some policy keeps every successor safe indefinitely. This can include doing nothing forever. Safety alone is not recursive improvement.
1213 
1214 For each transition, a progress mark $p(z,a,z')\in\{0,1\}$ is supplied by a checked criterion. A mark of one means the specified process-improvement claim has been established under the same comparison. It is not assigned merely because a file changed. Define
1215 \begin{align}\label{eq:progress}
1216 W_{0,0}&=\mathcal K, & W_{0,k}&=\varnothing\quad(k>0),\\
1217 W_{h,k}&=\{z\in\mathcal K:\exists a\in A(z),\ \Post(z,a)\subseteq\mathcal K,\nonumber\\[-2pt]
1218 &\hspace{34mm} z'\in W_{h-1,\max\{0,k-p(z,a,z')\}}
1219 \quad\forall z'\in\Post(z,a)\}.\nonumber
1220 \end{align}
1221 Here $h$ is the number of remaining attempts and $k$ the number of still-required progress events. A pause action lets a policy that finishes early use the remaining horizon without changing the result.
1222 
1223 \begin{theorem}[Common-policy recursive progress]\label{thm:progress}
1224 A configuration belongs to $W_{h,k}$ if and only if there exists one authorized policy that keeps all outcomes in $\mathcal K$ and guarantees at least $k$ checked progress events within $h$ attempts. A policy depending on the current configuration and the remaining pair $(h,k)$ suffices. The finite recurrence gives a witness when feasible and a complete negative answer within the stated model when infeasible.
1225 \end{theorem}
1226 \begin{proof}
1227 At horizon zero, zero remaining progress is possible exactly in $\mathcal K$, and positive remaining progress is impossible. Assume the claim for $h-1$. A policy at $z$ must choose one initial action before its outcome is known. Every possible successor must remain in $\mathcal K$ and must admit a continuation meeting the remaining target $\max\{0,k-p\}$. By induction these conditions are exactly the memberships in~\eqref{eq:progress}. Conversely, choose a witnessing first action and a witnessing continuation for each observed successor. The resulting policy works on every path. Induction proves necessity, sufficiency, and the stated memory requirement. Finiteness makes the construction terminating.
1228 \end{proof}
1229 
1230 The use of one first action is important. The weaker claim that every possible outcome has some favorable action, selected after secretly learning that outcome, is not an implementable policy. Likewise, independently feasible semantic, resource, and evaluation certificates must refer to the same attempt and successor relation.
1231 
1232 The theorem is complete only for its finite catalogue and its information boundary. It does not create a promising next candidate or identify the true productivity of an arbitrary program. Its progress labels may come from exact finite evaluation or from a separate evidence layer. With probabilistic labels, the conclusion about actual progress holds on the event that the relevant certificates are valid. Proposition~\ref{prop:lineage} can bound failure of that event under its own assumptions.
1233 
1234 \subsection{Safe rejection can prevent a worst-case progress guarantee}
1235 \begin{counterexample}[Repeated opportunity is not bounded sure progress]\label{ex:retry}
1236 At a safe configuration, an attempt either produces a genuine improvement or rejects the candidate and returns to the same configuration. Both outcomes are possible at every attempt. A safe pause is also available. For every finite $h$, there is a path with $h$ consecutive rejections, so no policy guarantees one improvement within $h$ attempts. With an independent positive success probability, eventual success can nevertheless occur with probability one. The worst-case finite theorem and that probabilistic statement answer different questions.
1237 \end{counterexample}
1238 
1239 \subsection{Why local improvement does not imply recursive viability}
1240 A second finite example has a proposal that raises the current score but deletes the only retained witness needed to validate any subsequent proposal. Its destination lies outside $\Safe$ when witness availability is protected. If witness availability is omitted, it may remain safe but have no productive continuation. The result depends on the contract, not the flattering name assigned to the edit.
1241 
1242 This is a compact version of the closure perspective in SRIC~\cite{sric}. The present contribution is to connect that perspective to a concrete diagnostic tree, a resource witness, and a specified productivity comparison rather than treating closure as a free consequence of successful self-modification.
1243 
1244 \section{Acceleration is an additional hypothesis}\label{sec:acceleration}
1245 Recursive improvement can be meaningful without being indefinitely accelerating. Its measured pace depends on useful gains, the cost of finding and checking them, available opportunities, and the chosen scale of evaluation. A normalized task score has a ceiling. A changing suite can continually introduce new headroom, but its successive normalized scores are not automatically comparable.
1246 
1247 \begin{proposition}[A fixed-margin ceiling on a fixed score]\label{prop:ceiling}
1248 Suppose a lineage has a fixed measure $R_t\in[a,b]$, every accepted progress event increases it by at least $\gamma>0$, and all other transitions are nondecreasing in that same measure. Then the number of progress events is at most
1249 \[
1250 \left\lfloor\frac{b-a}{\gamma}\right\rfloor.
1251 \]
1252 An infinite sequence of positive increments is compatible with bounded total improvement when no common positive lower bound is imposed.
1253 \end{proposition}
1254 \begin{proof}
1255 After $k$ progress events, telescoping and nondecrease give $R_t\geq R_0+k\gamma\geq a+k\gamma$. Since $R_t\leq b$, the bound follows. For the second assertion, start at zero and use increments $2^{-t}$ for $t\geq1$. Every increment is positive and their partial sums remain below one.
1256 \end{proof}
1257 
1258 If nonprogress transitions can decrease the measure, the first bound need not hold: repeatedly falling and recovering can generate arbitrarily many positive increments. Those recoveries are not unlimited cumulative progress. A moving evaluator creates a different problem. It may be appropriate, but it requires bridges to preserve the meaning of the comparison.
1259 
1260 A simple accounting model can express the additional conditions for acceleration. Let $g_t$ be an expected useful gain and $c_t>0$ the complete cost of the corresponding discovery and acceptance cycle. Improvement productivity per unit resource is $g_t/c_t$. Raising $g_t$ alone does not raise that ratio when $c_t$ rises faster. A larger reachable repair set is similarly insufficient when proposal quality falls or validation becomes the limiting cost.
1261 
1262 SRIC's bottleneck perspective is useful here: improving one stage can expose another stage as the dominant limitation~\cite{sric}. The next bottleneck might be information acquisition rather than proposal generation, or evidence quality rather than repair expressibility. A theory of acceleration would need to specify how those bottlenecks move and which resources support their resolution. A claim of universal acceleration does not follow from the existence of one productive cycle.
1263 
1264 
1265 \clearpage\part{A bounded route toward general intelligence}\label{part:architecture}
1266 \section{A proposed learned architecture}\label{sec:architecture}
1267 The mathematical contracts do not specify a complete learning algorithm. They do identify the components that a credible algorithm must make learnable and the evidence required when those components change. The intended architecture has one active solver, a recurrent working state, a persistent library of typed operations, an acquisition policy, a proposal mechanism, and an admission procedure. These are roles in one realized computation, not a requirement for a separate large model for every role.
1268 
1269 \subsection{What would learn}
1270 Let $r_\phi$ encode the retained state, $G_{\theta,a}$ describe proposed operations, $\pi_\omega$ choose observations or experiments, and $p_\psi$ propose candidate programs or parameter updates. A development episode can modify $\phi,\theta,\omega,\psi$ through a declared learning rule. A persistent program library can also change by adding, replacing, or removing checked operators. Temporary deliberation without a retained modification is not called a new learned generation here.
1271 
1272 The learning signals need separate purposes. Prediction losses train anticipation of future outputs. Intervention-consistency losses test whether the proposed operations match their intended effects. Acquisition rewards favor useful reductions of repair uncertainty after charging experiment cost. Proposal rewards evaluate the actual selected descendant rather than fluency of its rationale. Preservation checks protect specified older capabilities or interfaces. There is no universal set of weights that turns these distinct obligations into one sufficient scalar objective.
1273 
1274 A latent computation may suggest that a particular variable matters. A typed checkpoint should then declare the variable's domain, the operations it supports, the evidence used to infer it, and the continuations on which it was checked. Its translator must not read the answer that the checkpoint claims to predict. Its complexity is charged. OSL is a proposed semantic consumer for such checkpoints, while Neuralese concerns the learned latent producer~\cite{osl,neuralese}. This paper does not implement their complete learned bridge.
1275 
1276 \begin{proposition}[Local operation agreement preserves finite continuation]\label{prop:continuation}
1277 Let $D$ be invariant under every source operation $F_a$, let $q:D\to Z$, and suppose
1278 \[
1279 qF_a=G_aq\quad\text{on }D
1280 \]
1281 for every admitted $a$. If the required output satisfies $y=\bar yq$ on $D$, then for every finite operation word $w$,
1282 \[
1283 qF_w=G_wq,\qquad yF_w=\bar yG_wq.
1284 \]
1285 \end{proposition}
1286 \begin{proof}
1287 The empty word gives the identity. Assume the relation holds for a prefix. Domain invariance allows application of the next local equation, giving $qF_aF_w=G_aqF_w=G_aG_wq$. Induction establishes the first identity and composing with $\bar y$ gives the second.
1288 \end{proof}
1289 
1290 The proposition is a specification for meaningful reuse, not a method for learning $q$ or $G_a$. Invariance matters because an unchecked operation can leave the domain where the equations hold. Output preservation matters because commuting hidden states need not retain the task variable. Actual causal use matters because a probe can decode an appropriate state that the solver does not use.
1291 
1292 \subsection{What a complete attempt would do}
1293 A bounded iteration would begin with an observed task failure and an explicit set of plausible causes. The active acquisition policy chooses an admitted experiment. Its result updates those causes and the current state. A proposer supplies a candidate repair or a new constructor when the old language is insufficient. A separate execution checks the candidate's declared interface, resource usage, and behavior. A selected candidate is assessed on evidence not used to construct it. If admitted, its actual changes and scope are stored, including the procedure that found it.
1294 
1295 A later outer attempt may change the acquisition policy, proposer, or selection code. It must then be assessed as an improver from comparable starting conditions, not only as the latest solver. An improvement may be retained provisionally for a particular domain rather than promoted globally. Failed hypotheses remain useful evidence when their assumptions and reasons for rejection are preserved.
1296 
1297 Candidate evaluation can use the same kind of mathematical tools as the proposer without sharing the candidate's unchecked assumptions. Independence here means a specified information and authority separation, not a mystical absence of common software or training ancestry. External audit data and the authority to redefine a protected score are not supplied to a candidate as editable inputs for the same transaction.
1298 
1299 \subsection{A learned policy is not an unconstrained interpreter}
1300 A sufficiently powerful interpreter can hide the entire solution behind a small label. The remedy is not to forbid interpreters by definition. It is to state their installed information, runtime, storage, and access. This is the resource lesson of \emph{Machine Understanding}~\cite{understanding}. The diagnostic tree is intentionally explicit so that this accounting can be performed exactly in the worked case.
1301 
1302 Nor should neural implementation be required simply for appearance. A library of executable operators and a learned experiment selector can be a meaningful adaptive system. Conversely, updating a large weight tensor does not automatically establish a useful representation, a causal mechanism, or a transferable improvement procedure. The architecture is evaluated by its realized operations and the origin of their improvement.
1303 
1304 \section{The compiled diagnostic improvement}\label{sec:worked}
1305 We can now state the exact mathematical achievement of the running example. It is deliberately smaller than the full learned architecture, but complete enough to expose the relevant distinctions.
1306 
1307 For $n=2^k$ cells, assume a single defective cell, binary reports, singleton queries, and $k$ bit-coordinate queries. All queries leave the cell unchanged and cost one diagnostic call. A correct final repair costs one additional call. Distinct cells require distinct terminal repairs. There are no false repair commits. A literal tree record contains one experiment or repair identifier plus its child references.
1308 
1309 \begin{theorem}[Optimal diagnosis in the hidden-cell family]\label{thm:cells}
1310 Every certain diagnosis needs at least $k$ binary queries in the worst case. The bit-query procedure attains this bound and uses $2n-1$ records in a full binary tree. Any procedure using singleton queries alone needs at least $n-1$ queries in the worst case, and equality-first testing attains that bound with the same number of tree records. Thus their worst total execution costs, including repair, are $k+1$ and $n$.
1311 \end{theorem}
1312 \begin{proof}
1313 A binary tree of depth less than $k$ has fewer than $2^k=n$ leaves. Every successful leaf can identify at most one cell because its repair must be correct for every remaining case. Therefore depth at least $k$ is required. The $k$ coordinate bits identify every cell and give a complete binary tree with $n$ leaves and $n-1$ internal nodes. For singleton tests, an adversary can answer no on each tested cell while at least two untested cells remain. Fewer than $n-1$ distinct singleton queries therefore cannot guarantee identification. Equality-first testing uses one leaf for each positive answer and one final leaf for the last remaining cell, again totaling $2n-1$ records. Adding the terminal repair gives the claimed work counts.
1314 \end{proof}
1315 
1316 \begin{figure}[!ht]\centering
1317 \includegraphics[width=.92\linewidth]{figures/diagnostic_cost.pdf}
1318 \caption{Exact total execution costs for the power-of-two cell family. Singleton testing requires $n-1$ diagnostic queries, while the admitted bit queries require $\log_2 n$. A final repair adds one call to each plotted curve. Both full trees have $2n-1$ stored records. The curves omit separately charged model acquisition, compilation, and adapters.}\label{fig:cost}
1319 \end{figure}
1320 
1321 \subsection{What is actually compiled}
1322 The reference compiler receives an observation table and the set of successful terminal repairs. It computes the frontier in Theorem~\ref{thm:synthesis} and returns an optimal tree under a chosen work/storage allowance. At $n=8$ it returns a four-call, fifteen-record witness. A separately coded interpreter checks every initial cell and every branch. The reference comparison constructs the equality-first baseline independently, rather than comparing the compiler to a weakened version of its own output.
1323 
1324 The selected tree is an executable diagnostic policy for future episodes. It is not a saved answer for the calibration case. In a new episode, the hidden cell is unavailable to the policy. Only reports from its queries determine the branch and eventual repair. A cell permutation supplies a controlled foreign interface when the query sets, terminal repairs, and adapter are transported together. Theorem~\ref{thm:transport} explains that transfer. The tests do not claim that the adapter was learned without correspondence data.
1325 
1326 \subsection{The measured object is a procedure}
1327 Under the earlier four-call cap, the equality-first improver repairs $3/8$ of the uniform eight-cell cases and otherwise abstains. The compiled improver repairs all cases. The repaired solvers themselves are simple: each now knows the correct cell-specific operation. What improved is the procedure that acquires that case-specific correction. The library and sensor language are unchanged.
1328 
1329 This original controller-level construction does not by itself improve the compiler. The compiler and acquisition constructions in Parts III--V provide the additional changes to compilation and rule acquisition. Each comparison retains its own starting procedure, supplied information, and cost unit. Their coexistence does not convert the original eight-cell demonstration into evidence of indefinite self-improvement.
1330 
1331 \subsection{Controls that expose the boundary}
1332 Removing the bit-query family changes the synthesis problem and restores the singleton lower bound. Omitting the adapter breaks foreign-label replay even when the tree shape is unchanged. Deliberately choosing an incorrect leaf causes the independent checker to reject the certificate. Reducing the allowed tree records below fifteen rules out the certain eight-cell solution in this literal binary-tree model. These are failures of distinct requirements, not reasons to reinterpret the target after a run.
1333 
1334 The repair-aligned query example in Section~\ref{sec:synthesis} supplies a different control. There the compiler need not identify the exact hidden case. It should stop when one repair works for every surviving case. This prevents full identification from being hard-coded as the universal objective of inquiry.
1335 
1336 \section{Generality requires more than semantic relabeling}\label{sec:generality}
1337 The exact transport theorem is useful because it proves what is preserved when a correspondence exists. It is not evidence that the system can discover correspondences efficiently across arbitrary tasks. A relabeled hidden-cell world remains the same informational problem. Transfer from diagnosis to theorem discovery, planning, or empirical model construction needs additional argument.
1338 
1339 A credible generality study would vary several things separately: the state distinctions needed for future behavior, the allowed experiment language, the repair constructors, the information available to the learner, and the resource costs. It would also separate unfamiliar instances of a known schema from unfamiliar combinations of schemas and from an operation family that the old language cannot express.
1340 
1341 The proposed mechanism is not that every task reduces to binary cell location. It is that many tasks can expose a useful pattern: a currently retained representation fails to support a consequential distinction, an experiment can discriminate among causes, and a reusable operation can resolve the resulting class of failures. Whether that pattern is broad enough and economical enough to contribute to general intelligence is a research hypothesis.
1342 
1343 \subsection{The next decisive learning comparison}
1344 The most informative next study would compare a parent and descendant improvement procedure on the same family of fresh starting solvers. It would hold installed libraries and base-model access fixed in the primary contrast, then add a separate full-system contrast that includes any learned library. A stronger ordinary program-library learner should be included, since library learning itself is established~\cite{dreamcoder}.
1345 
1346 The development system would be allowed to acquire or revise an encoder, experiment selector, and operator library in bounded simulated environments. Evaluation would include longer continuations, new operator compositions, and changed observation formats. Each change should have an explicit semantic target and a resource ledger. Removing acquisition adaptation, repair reuse, or recurrent state separately would locate which mechanism produces a gain. Those are proposed experiments, not results reported in this paper.
1347 
1348 The desired endpoint is not merely that the descendant solves more familiar cases. It is that its acquired improvement procedure produces better valid repairs on unfamiliar cases within the same budget, and that the gain survives adequate controls for retained answers, installed adapters, and selection leakage. A subsequent generation must repeat that comparison rather than inherit its predecessor's claim by name.
1349 
1350 \subsection{What would count against the central hypothesis}
1351 The obstruction-guided procedure may be no better than an ordinary search method given the same information. Its apparent advantage may vanish after charging its diagnostic model and checker. Its recovered operators may fail on longer compositions. A learned selector may memorize surface labels instead of identifying the causal distinction. A larger repair language may dilute search enough to erase its representational advantage. These outcomes would identify where the proposed integration fails or requires stronger assumptions.
1352 
1353 A negative result on a restricted task family would not prove that general intelligence is impossible. A positive result would not prove AGI either. Both would help determine whether the proposed mechanism earns its place in a larger architecture.
1354 
1355 \section{Open problems beyond the first edition}\label{sec:limits}
1356 The exact core rests on finite models, supplied semantics, bounded horizons, and explicit information. Several important extensions remain.
1357 
1358 \paragraph{Learning the experiment model.}
1359 The tagged-model theorem accounts for a fixed unknown member of a supplied finite class, including paid calibration. It does not construct that class from open-ended experience or guarantee that it contains the true process. Safe learning with noisy, misspecified, or changing observation models remains open in this framework. Model uncertainty must not be replaced by a guessed deterministic table merely to preserve an exact theorem.
1360 
1361 \paragraph{Discovering a repair language.}
1362 Both the original compiler and the selected shortcut use a supplied repair language. The earlier selector chooses within a supplied catalogue of compiler templates. Part~\ref{part:rule-learning} additionally synthesizes a primitive arithmetic rule after exposing a missing feature. Its grammar, feature registry, teacher, and proof gate remain supplied. Open-ended constructor discovery needs a representation of candidate meanings, a method for proposing them, and evidence that the new language preserves old operations while making new problems tractable. Expressibility of all computable programs is not an efficient search strategy.
1363 
1364 \paragraph{Acquiring stronger search representations.}
1365 Part~\ref{part:meta-acquisition} changes the candidate space used to acquire future discovery rules. The new equations and quotient are generated, while their arithmetic meanings and proof machinery are supplied. A stronger supplied normalizer remains a useful comparator. Learning effective proof search, choosing cheaper rule subsets, and adapting the representation when a language changes are distinct next questions. A finite-consistent equation is not automatically a valid optimization.
1366 
1367 \paragraph{Transfer without a supplied correspondence.}
1368 The exact policy-transport theorem assumes its maps. Learning them introduces gauge ambiguity, underidentification, lossy observations, and potential answer leakage. The Neuralese-to-OSL bridge remains a separate learned realization problem, not a solved consequence of writing a commuting square~\cite{neuralese}.
1369 
1370 \paragraph{Improving evaluation without changing the question.}
1371 An evaluator can be genuinely defective. Correcting it requires retaining evidence of the defect, specifying the new scope, and distinguishing a change in estimated performance from a change in the underlying target. A fully unrestricted evaluator rewrite would remove the stable comparison on which the reported improvement depends.
1372 
1373 \paragraph{Noisy and distributed recursive synthesis.}
1374 The finite progress theorem uses fully observed configurations and worst-case successor sets. Useful systems may need probabilistic service, partial observation, or several decision centers. Separate success probabilities do not automatically yield one policy that satisfies all constraints. A noisy extension must state both the risk accepted and the evidence supporting its transition law.
1375 
1376 \paragraph{Long-run productivity.}
1377 Repeated finite improvements do not determine the eventual learning curve. A richer task distribution, increasing resources, changing architectures, or new scientific observations may create further headroom. Those changes should be modeled and charged rather than absorbed into a claim of autonomous acceleration. The current paper does not settle whether general-purpose recursive improvement has increasing, constant, or diminishing returns.
1378 
1379 \subsection{Authority and bounded implementation}
1380 The formal permission to modify a local program is not authorization to change external services, access private data, or remove an institution's controls. Proposed deployments would require an explicit scope of authority and a justified handling of affected parties. The reference package does not connect to services, modify other agents, train a neural model, or conduct autonomous external research. It constructs and checks finite mathematical objects in a local process.
1381 
1382 Similarly, stopping and refusal are legitimate outcomes when required evidence or resources are missing. An improvement claim must not become a reason to suppress those outcomes. A preserved archive can retain unsuccessful attempts without promoting them into operating authority. These commitments follow the evidence-preserving lineage perspective rather than a presumption that continued self-modification is always desirable.
1383 
1384 \section{Conclusion}\label{sec:conclusion}
1385 A better solver, a better repair procedure, and a better process for discovering repair procedures are different objects. They can interact productively, but the interaction needs an explicit realization. General intelligence motivates the search for transferable discovery methods. It is not a premise from which those methods follow.
1386 
1387 The finite theory keeps the relevant obligations in one chain. An investigation must acquire enough information to choose a successful repair, without necessarily identifying every hidden detail. Its execution and stored controller must fit the same resource witness. A transfer must preserve observations and admissibility, not only an output. A language extension changes which lower bounds remain valid. An adaptive lineage must retain the evidential meaning of its accepted gains and a continuing policy for any promised progress.
1388 
1389 The constructive sequence now reaches the acquisition of discovery rules. A compiler produces better diagnostic trees. A guarded strategy reduces the search needed to find such trees. A learner composes an internal rejection predicate. A further learned equation library prepares a smaller search representation for reacquiring that predicate and other targets. Exact teacher-transcript preservation identifies what has not changed: the required evidence and the final selected AST. The additional improvement concerns repeated evaluation work, not a newly supplied answer.
1390 
1391 Correctness and productivity remain different. A supplied full normalizer can remove more redundancy than the learned library. Preparation can cost more than a short workload saves. Streaming avoids some model reads while adding comparisons. A repair that succeeds on several cases can make an old identification bound unsound. These are not peripheral caveats. They determine what the acquired modification is and when it is worth using.
1392 
1393 The finite constructions demonstrate specific changes in discovery behavior under declared semantics. They do not establish learned physical meaning, efficient search over every computable procedure, or an indefinitely improving sequence of outer learners. Their positive contribution is an auditable connection between representations, generated rules, checked equivalences, resource use, and recursive revision. A claim about becoming better at improvement can now be located at a particular level, checked against its predecessor, and refused when its evidence or cost contract is missing.
1394 
1395 
1396 The first edition also makes those claims revisable without making their premises disposable. A changed repair language can invalidate a weight bound while leaving the equation library sound. A changed resource price can reverse a cost conclusion without altering one controller transition. The dependency-complete reuse theorem states when old witnesses remain applicable, and the resource proposition states when an event saving is independent of a selected price model. Their role is to keep one actual, inspectable chain of reasoning and computation attached to every claimed gain.
1397 
1398 \appendix
1399 \section{A complete diagnostic trace}\label{app:trace}
1400 Take $n=8$ and hidden defect $j=5$, whose binary digits are $101$. One optimal tree uses the three queries
1401 \[
1402 A_0=\{1,3,5,7\},\qquad A_1=\{2,3,6,7\},\qquad A_2=\{4,5,6,7\}.
1403 \]
1404 The precise order may differ among equally optimal compiled trees. For this order, the supports are
1405 \[
1406 \{0,\ldots,7\}\xrightarrow{1}\{1,3,5,7\}
1407 \xrightarrow{0}\{1,5\}\xrightarrow{1}\{5\}.
1408 \]
1409 The terminal repair is $r_5$. The path uses three diagnostic calls and one repair call. The complete tree stores all eight repair leaves and seven query nodes, not merely this path.
1410 
1411 Equality-first testing asks about cells zero through five before it obtains a positive report. It uses six diagnostic calls on this particular case, then one repair. Under the three-diagnostic cap it abstains after three negative reports. The cap is fixed before the episode, not shortened for the baseline after observing which cell is defective.
1412 
1413 For a target relabeling $\sigma(i)=3i+1\pmod8$, the defect has target label $\sigma(5)=0$. Each query becomes $\sigma(A_r)$ and the terminal repair becomes $r'_{\sigma(5)}$. Reports and tree shape agree with the source, but the label adapter is part of the transported interface. Applying the old numeric repair label five directly in the target would be incorrect. This is why syntactic resemblance does not replace a semantic map.
1414 
1415 \subsection{A repair problem that should stop before full identification}
1416 In the four-case example, the support $\{0,1,2\}$ admits repair $a$ immediately. A compiler that insists on identifying the precise case would spend unnecessary work. The successful stopping condition is the existence of one action whose success set contains the whole support. Conversely, the support $\{2,3\}$ admits no common repair in that example. A leaf chosen there without another observation is invalid even though either repair succeeds in one of its cases.
1417 
1418 \section{Reference computations and evidence scope}\label{app:checks}
1419 The package implements the finite experiment model, the two-resource recurrence, tree reconstruction, and a separate replay checker. It also implements stable partition refinement and finite recursive-progress synthesis. Exact test groups compare selected constructions with separately coded enumerations on small domains. Integer and rational arithmetic are used for mathematical acceptance checks. Plotting converts exact analytical quantities to display coordinates only.
1420 
1421 The verification program records its exact domains, input and output hashes, command, interpreter, duration, and outcomes. The source audit inventories formal statements and checks labels, citations, and their proof environments. The build uses LaTeX and the supplied vector figures. A clean rebuild is compared by extracted PDF text, not claimed to be byte-identical across environments.
1422 
1423 These checks are authored within this project. Alternative algorithms provide implementation cross-checks, not independent peer review. No test count establishes a universal claim outside its implemented domain. The proofs in the manuscript provide the conditional general arguments. No Lean certificate, trained agent, learned semantic bridge, or automated research run is included.
1424 
1425 \subsection{A precise reading of the finite demonstration}
1426 The observation and success tables are supplied analytical semantics. The compiler selects a tree without access to the next episode's hidden index. The checker separately receives that index when exhaustively verifying all possible episodes. That division prevents a policy from consulting hidden state during replay. It does not make the supplied model an empirically learned object.
1427 
1428 The main generated files are the compiled cell-tree certificate, a report of source and transported replays, the cost frontiers, and the exact check results. All can be regenerated locally. The README records the commands and the review notes record any failures or limitations encountered during preparation.
1429 
1430 \section{Claim map and the scope of the first edition}\label{app:claimmap}
1431 \begin{small}\begin{longtable}{@{}p{.30\textwidth}p{.62\textwidth}@{}}\toprule
1432 Claim & What the present manuscript supplies\\\midrule\endhead
1433 Feedback can support a repair & A transcript-discrimination bound and a common-repair stopping condition. No automatic causal diagnosis is inferred.\\
1434 A representation supports continuation & A least stable refinement and explicit operation equations. Learning the representation is additional.\\
1435 A repair can be found within a budget & An exact finite work/storage recurrence and a checkable tree. It requires a supplied finite experiment model.\\
1436 A discovery procedure transfers & A correspondence preserving complete investigation semantics and costs. Discovering that correspondence is additional.\\
1437 A pruning rule is learned & A finite grammar synthesis, a witnessed feature conflict, and a separate scope proof. The teacher and grammar are supplied.\\
1438 A compiler skips work safely & Streaming root rejection preserves the controller and avoids counted rows. Predicate work remains charged.\\
1439 A candidate procedure is better & A selection bound under uniform assessment error and a protected productivity comparison. The error premise must be established.\\
1440 A lineage preserves credible gains & Conditional error spending and an explicit distinction between development, selection, and audit evidence.\\
1441 A lineage can improve repeatedly & An exact finite common-policy criterion for marked progress. Marks require separate valid evidence.\\
1442 The process accelerates & Not established. A fixed-score ceiling and cost accounting expose additional requirements.\\
1443 The system is generally intelligent & Not established. Generality and learned discovery remain research targets across unfamiliar structures.\\The synthesis procedure improves & A checked equation library removes redundant candidate evaluations while preserving teacher proposals. Preparation costs remain separate.\\
1444 One repair covers several cases & A feasible repair-weight certificate replaces singleton counting. Its validity is rechecked after a repair-language change.\\
1445 A composed gain is affordable & The actual acquisition, compilation, checking, and preparation costs must fit one common resource model.\\
1446 Old certificates survive a change & Only dependency-complete unchanged obligations can be reused without new evidence. Affected descendants require re-establishment.\\
1447 A gain is independent of prices & Componentwise event dominance, or a strictly positive margin on the declared finite price polytope, supplies the precise criterion.\\
1448 \bottomrule
1449 \end{longtable}\end{small}
1450 
1451 \clearpage\addcontentsline{toc}{section}{References}
1452 \begin{thebibliography}{99}\fontsize{9.5}{11.2}\selectfont\setlength{\itemsep}{3pt}\setlength{\parskip}{0pt}
1453 \bibitem{understanding} Komorebi P. \emph{Machine Understanding: Representation, Explanation, and Transfer}. Operation Komorebi, first consolidated edition, v1.0.0, 8 October 2026.
1454 \bibitem{sric} Komorebi P. \emph{Stratified Recursive Improvement Closure: Obstruction, Descent, Transport, and Evidence-Preserving Lineages}. Formal theory draft v2.4, Block 23, 3 September 2026. The reviewed source is identified in the package source map. Cited for theoretical structure, not as empirical evidence for this manuscript's architecture.
1455 \bibitem{neuralese} Komorebi P. \emph{Neuralese}. Operation Komorebi, Final Research Edition v1.0, 2026. Section 12 specifies the proposed semantic and continuation interface.
1456 \bibitem{osl} Komorebi P. \emph{Operator-Symbolic Language}. Operation Komorebi, Final Research Edition v1.0, 2026. Explicit semantic and operational interface.
1457 \bibitem{chollet} F. Chollet. On the Measure of Intelligence. 2019. \url{https://arxiv.org/abs/1911.01547}.
1458 \bibitem{andrychowicz} M. Andrychowicz, M. Denil, S. Gomez, M. W. Hoffman, D. Pfau, T. Schaul, B. Shillingford, and N. de Freitas. Learning to learn by gradient descent by gradient descent. 2016. \url{https://arxiv.org/abs/1606.04474}.
1459 \bibitem{maml} C. Finn, P. Abbeel, and S. Levine. Model-Agnostic Meta-Learning for Fast Adaptation of Deep Networks. \emph{PMLR} 70:1126--1135, 2017. \url{https://proceedings.mlr.press/v70/finn17a.html}.
1460 \bibitem{dreamcoder} K. Ellis et al. DreamCoder: Growing generalizable, interpretable knowledge with wake-sleep Bayesian program learning. 2020. \url{https://arxiv.org/abs/2006.08381}.
1461 \bibitem{seal} A. Zweiger, J. Pari, H. Guo, E. Aky\"urek, Y. Kim, and P. Agrawal. Self-Adapting Language Models. 2025. \url{https://arxiv.org/abs/2506.10943}.
1462 \bibitem{goedel} J. Schmidhuber. Goedel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements. 2003, revised 2006. \url{https://arxiv.org/abs/cs/0309048}.
1463 \bibitem{dgm} J. Zhang, S. Hu, C. Lu, R. Lange, and J. Clune. Darwin Godel Machine: Open-Ended Evolution of Self-Improving Agents. 2025. \url{https://arxiv.org/abs/2505.22954}.
1464 \bibitem{hyperagents} J. Zhang et al. Hyperagents. 2026. \url{https://arxiv.org/abs/2603.19461}. Public manuscript accessed 8 October 2026.
1465 \bibitem{aide} D. Srikanth, B. Zhao, D. Xu, Y. Wu, and Z. Jiang. Recursive self-improvement of AI research agents. Preprint, 22 September 2026. \url{https://arxiv.org/abs/2609.26457}. The outer-loop comparison is qualified in Section 3.6.
1466 \bibitem{geiger} A. Geiger et al. Causal Abstraction: A Theoretical Foundation for Mechanistic Interpretability. \emph{Journal of Machine Learning Research} 26(83):1--64, 2025. \url{https://jmlr.org/papers/v26/23-0058.html}.
1467 \bibitem{dwork} C. Dwork, V. Feldman, M. Hardt, T. Pitassi, O. Reingold, and A. Roth. Preserving Statistical Validity in Adaptive Data Analysis. 2014, revised 2016. \url{https://arxiv.org/abs/1411.2664}.
1468 \bibitem{howard} S. R. Howard, A. Ramdas, J. McAuliffe, and J. Sekhon. Time-uniform Chernoff bounds via nonnegative supermartingales. \emph{Probability Surveys} 17:257--317, 2020. \url{https://doi.org/10.1214/18-PS321}.
1469 
1470 \bibitem{nilim} A. Nilim and L. El Ghaoui. Robust Control of Markov Decision Processes with Uncertain Transition Matrices. \emph{Operations Research} 53(5):780--798, 2005. \url{https://doi.org/10.1287/opre.1050.0216}. Cited as background on explicit model uncertainty, not as an identical uncertainty model.
1471 \bibitem{sketch} A. Solar-Lezama et al. Combinatorial sketching for finite programs. \emph{ASPLOS}, pp. 404--415, 2006. \url{https://doi.org/10.1145/1168857.1168907}.
1472 \bibitem{sygus} M. Raghothaman and A. Udupa. Language to Specify Syntax-Guided Synthesis Problems. 2014, revised 2016. \url{https://arxiv.org/abs/1405.5590}. Specification-language account of the syntax-guided synthesis framework introduced by Alur and colleagues in 2013.
1473 \bibitem{ice} P. Garg, C. L\"oding, P. Madhusudan, and D. Neider. ICE: A Robust Framework for Learning Invariants. In \emph{Computer Aided Verification}, LNCS 8559, pp. 69--87, 2014. \url{https://doi.org/10.1007/978-3-319-08867-9_5}.
1474 \bibitem{egg} M. Willsey, C. Nandi, Y. R. Wang, O. Flatt, Z. Tatlock, and P. Panchekha. egg: Fast and Extensible Equality Saturation. \emph{Proceedings of the ACM on Programming Languages} 5(POPL), 2021. \url{https://doi.org/10.1145/3434304}.
1475 \bibitem{ruler} C. Nandi, M. Willsey, A. Zhu, Y. R. Wang, B. Saiki, A. Anderson, A. Schulz, D. Grossman, and Z. Tatlock. Rewrite Rule Inference Using Equality Saturation. \emph{Proceedings of the ACM on Programming Languages} 5(OOPSLA), 2021. \url{https://doi.org/10.1145/3485496}. Author manuscript: \url{https://arxiv.org/abs/2108.10436}.
1476 \bibitem{williamson} D. P. Williamson and D. B. Shmoys. \emph{The Design of Approximation Algorithms}. Cambridge University Press, 2011. Chapter 1 develops set-cover relaxations and dual bounds. Author-hosted edition: \url{https://www.designofapproxalgs.com/}.
1477 \end{thebibliography}
1478 \end{document}

Back to source controls

Back to Self-Improving Intelligence