Machine Native Reasoning: wider continuation

Download original file

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

Read the typeset paper

1 \chapter{From evidence to a reusable state}\label{ch:evidence}
2 \question{The first question is not how much state to store. It is which distinctions are accessible.}
3 Let $\Omega$ be a finite nonempty set of possible worlds. A world may include a physical state, a fixed model index, and an origin tag. An observation record is a function $r:\Omega\to H$. A target is a function $t:\Omega\to Y$. All codomains used below are nonempty. We work on attained records $r(\Omega)$, so no arbitrary interpretation of an impossible record is needed.
4 
5 \begin{proposition}[A record determines a target exactly on its fibres]\label{r:factor}
6 There exists $d:r(\Omega)\to Y$ with $d(r(\omega))=t(\omega)$ for every world if and only if
7 \[
8 r(\omega)=r(\omega')\ \Longrightarrow\ t(\omega)=t(\omega').
9 \]
10 \end{proposition}
11 \begin{proof}
12 Necessity follows because a function assigns one value to one input. For sufficiency, define $d(h)$ to be $t(\omega)$ for any world with $r(\omega)=h$. Such a world exists for attained $h$, and the hypothesis makes the choice immaterial. The resulting decoder satisfies the required equation.
13 \end{proof}
14 \source{Grounded Abstraction [GA], Proposition 3.2 and Theorem 3.4. Machine Understanding [MU], the representation and sender-access criteria. This is the shared elementary factorization argument, stated once.}
15 
16 The proposition is an information statement, not a runtime bound. The table defining $d$ could be large. Nor does the mere existence of $d$ teach a learner how to find it. A proof that a suitable decoder exists and a justified account of its acquisition remain separate.
17 
18 \section{The sensor used throughout the book}
19 Write a world as
20 \[
21 \omega=(b,s,n)\in\{0,1\}^3.
22 \]
23 The physical target bit is $b$. The sensor convention is $s$. The nuisance bit $n$ never affects the operations or outputs of the initial contract. The display is
24 \[
25 y=b\oplus s,
26 \]
27 where $\oplus$ is addition modulo two. A permitted control $f$ flips the physical bit and leaves $s,n$ unchanged. Consequently the next display is $1-y$.
28 
29 An agent given only $y$ can predict every future display under repeated flips: after $k$ flips it is $y\oplus(k\bmod2)$. It cannot determine the current physical bit. Worlds $(0,0,0)$ and $(1,1,0)$ share display zero and have different targets. The obstruction is the fibre of the available record, not a shortage of computational effort.
30 
31 Calibration is a separate, nondestructive observation $c(\omega)=s$. When calibration is permitted and trustworthy, the joint record $(y,s)$ determines $b=y\oplus s$. Adding a blank field called ``sensor convention'' does not provide this information. The observation operation, its interpretation, and its cost must be part of the contract.
32 
33 \begin{center}\begin{tabular}{llll}\toprule
34 Available record & Number of values & Determines display? & Determines physical bit?\\\midrule
35 $y$ & 2 & Yes & No\\
36 $(y,s)$ & 4 & Yes & Yes\\
37 $(b,s,n)$ & 8 & Yes & Yes, with unused detail\\\bottomrule\end{tabular}\end{center}
38 
39 \begin{figure}[ht]
40 \centering\includegraphics[width=\linewidth]{figures/sensor_chain.pdf}
41 \caption{One exact observation sequence. The last two worlds differ only in the nuisance bit. Knowing every hidden coordinate is unnecessary for the protected physical target.}
42 \end{figure}
43 
44 \section{One answer versus every permitted continuation}
45 Let $X$ be a finite nonempty state space, and fix an available record $r:X\to H$. Let $\mathcal A$ be a finite alphabet of total deterministic operations $F_a:X\to X$, and let $q:X\to Y$ be the protected output. A word $w=a_1\cdots a_k$ executes $a_1$ first. Thus $F_w=F_{a_k}\cdots F_{a_1}$, and the empty word denotes the identity.
46 
47 Define behavioral equivalence by
48 \[
49 x\sim x'\quad\Longleftrightarrow\quad q(F_wx)=q(F_wx')\text{ for every finite word }w.
50 \]
51 The empty word protects the present output. The other words protect its permitted future uses.
52 
53 \begin{theorem}[Evidence-initialized behavioral state]\label{r:behavior}
54 A finite predictor initialized only from $r(x)$, updated only by the operation names, and exact for all protected continuation outputs exists if and only if
55 \[
56 r(x)=r(x')\ \Longrightarrow\ x\sim x'.
57 \]
58 When it exists, $X/{\sim}$ supplies a predictor with the smallest possible number of initialized states. Its updates are $\bar F_a([x])=[F_ax]$ and its readout is $\bar q([x])=q(x)$.
59 \end{theorem}
60 \begin{proof}
61 If two initial records are equal, a deterministic predictor has the same initialized state. Applying the same subsequent operations produces the same predicted outputs. Exactness therefore requires behavioral equivalence.
62 
63 For the converse, equivalent states have equivalent successors: an output after $F_a$ followed by $w$ is one of the outputs in the defining family. Hence $\bar F_a$ is well defined. The empty word makes $\bar q$ well defined. The fibre premise gives a well-defined initializer $d(r(x))=[x]$. Induction on word length proves exactness. Finally, behaviorally distinct states cannot initialize the same predictor state, since some continuation separates their outputs. Every exact predictor therefore needs at least one initialized value for each class, and the quotient attains that number.
64 \end{proof}
65 \source{[GA], Theorem 3.4, and [MU], Theorem 4.1. The two source versions are consolidated, not counted as independent discoveries.}
66 
67 In the sensor, the display task has two behavioral states. Changing the protected output to $(y,b)$ yields four behavioral states. The old record still has only two values and cannot initialize the enlarged quotient. The new task has exposed a real information requirement.
68 
69 \section{Why a statistical law is not an observed record}
70 A parameter can determine a distinct probability law while every finite sample remains possible under several parameters. For instance, Bernoulli parameters $1/3$ and $2/3$ assign positive probability to every finite binary string. No estimator based on one such string can be certainly correct for both parameters. The laws differ, but their finite supports overlap.
71 
72 A correct uncertainty record can be the appropriate output in this setting. Calling the most probable world ``identified'' would silently replace an error-free claim with a probabilistic one. Chapter~\ref{ch:memory} gives the corresponding probability update explicitly.
73 
74 \section*{What is now available}
75 We have a criterion for an initialized predictive state, but no automatic guarantee that an arbitrary coordinate manipulation preserves it. The next chapter studies operations on a representation. Its input is a declared state map and operation family, not an assumed learned encoder.
76 
77 \chapter{Operations must survive their representations}\label{ch:operations}
78 \question{A representation is useful only to the extent that its intended operations remain meaningful.}
79 There are two different ways to change representation. An exact split representation retains the whole mathematical state in another space. A compression retains only part of it. The first can preserve arbitrary composition. The second needs additional conditions.
80 
81 \section{Exact packets and the hidden-return defect}
82 Let $V,Z$ be vector spaces over a field. Let $A:V\to Z$ be analysis and $S:Z\to V$ synthesis, with $SA=I_V$. Then $AS$ is an idempotent on $Z$. The map $\mathcal E(T)=ATS$ represents a full-state operator $T:V\to V$ on resolved coordinates. Direct multiplication gives
83 \[
84 \mathcal E(T)\mathcal E(U)=ATSAUS=ATUS=\mathcal E(TU).
85 \]
86 The resolved identity is $AS$ on the compatible image $A(V)$, not necessarily $I_Z$ on arbitrary coordinates.
87 
88 For a compression, reverse the splitting. Let $C:V\to Z$ and $R:Z\to V$ satisfy $CR=I_Z$, and put $P=RC$. The compressed operator is $\Phi(T)=CTR$.
89 
90 \begin{proposition}[Exact accounting of the discarded excursion]\label{r:packet}
91 For any endomorphisms $T,U$ of $V$,
92 \[
93 \Phi(TU)-\Phi(T)\Phi(U)=CT(I-P)UR.
94 \]
95 Thus compression preserves this composition precisely when the discarded excursion on the right vanishes. Full split encoding $T\mapsto ATS$ preserves composition without that extra condition.
96 \end{proposition}
97 \begin{proof}
98 Expand the product $\Phi(T)\Phi(U)=CTRCUR=CTPUR$ and subtract it from $CTUR$. The identity for full split encoding follows from $SA=I_V$ as computed above. These computations make no approximation and require no orthogonality.
99 \end{proof}
100 \source{Sufficient Resolution [SR], Theorems 2.1 and 2.3. The present proof reviews only these algebraic identities, not the complete forty-seven-page source or its full formal implementation.}
101 
102 \begin{counterexample}[A discarded coordinate returns]\label{ce:return}
103 Take $V=\mathbb R^2$, let $C(x_1,x_2)=x_1$, let $R(z)=(z,0)$, and let $T(x_1,x_2)=(x_2,x_1)$. The compressed one-step map is zero. Yet $T^2=I_V$, so $\Phi(T^2)=I_Z$, while $\Phi(T)^2=0$. The discarded second coordinate was not irrelevant to the two-step question.
104 \end{counterexample}
105 
106 This is the mathematical reason that a short successful readout is not enough. A representation may preserve what is visible now and lose a route by which hidden information becomes visible later. Packets identify the retained and residual components, but the decomposition alone does not prove the residual harmless.
107 
108 \section{A method can be transported without reconstructing everything}
109 Suppose source states $z\in Z$ have operations $F_a$, target states $u\in U$ have operations $G_{\tau(a)}$, and $T:Z\to U$ is a translation. The operation-name map $\tau$ is fixed. Let $q$ and $\bar q$ be matched readouts.
110 
111 \begin{theorem}[Forward transport of a reusable method]\label{r:transport}
112 If the source domain is invariant, and
113 \[
114 TF_a=G_{\tau(a)}T,\qquad q=\bar qT,
115 \]
116 then for every finite word $w$,
117 \[
118 TF_w=G_{\tau(w)}T,\qquad qF_w=\bar qG_{\tau(w)}T.
119 \]
120 \end{theorem}
121 \begin{proof}
122 The empty word gives $TI_Z=I_UT$. Assume the first equality for a prefix. Invariance allows the next local equality to be applied on its successor, yielding
123 $TF_aF_w=G_{\tau(a)}TF_w=G_{\tau(a)}G_{\tau(w)}T$.
124 Induction proves the first claim. Composition with the matched readout proves the second.
125 \end{proof}
126 \source{[MU], Theorem 6.1. The same local-to-continuation argument appears in OSL and Neuralese. No claim about a learned latent translator is imported.}
127 \boundary{The theorem is forward. It does not imply an inverse, matching of new target operations, cheap computation of $T$, or that the source solver causally uses the represented state.}
128 
129 The sensor representation $(y,s)$ translates to $(b,s)$ through $T(y,s)=(y\oplus s,s)$. Flipping the physical bit complements the first coordinate in either representation. The square commutes, and so does every repeated flip. The nuisance bit is never reconstructed because it has no role in this contract.
130 
131 \section{One quotient for several possible dynamics}
132 A stronger situation arises when the operator itself is uncertain. Let $V$ be a finite-dimensional vector space over a fixed field, and let $Y$ be a vector space over the same field. Let $T_a^\theta:V\to V$ be a finite family of candidate linear operators indexed by an action $a$ and a model $\theta$. Choose one model $\theta_0$ as the reference and put $A_a=T_a^{\theta_0}$. A model index $\theta$ is fixed during the initial comparison. Let $Q:V\to Y$ be the same linear readout for every candidate.
133 
134 Define $D_a^\theta=T_a^\theta-A_a$ and the propagated discrepancy space
135 \[
136 E=\Span\{A_wD_a^\theta v: v\in V,\ a,\theta,\ w\text{ finite}\}.
137 \]
138 It can be constructed by starting with the sum of the discrepancy ranges and repeatedly adding their images under the reference actions. In finite dimension this increasing sequence stops. Immediate invisibility $QD_a^\theta=0$ alone does not guarantee $QE=0$.
139 
140 \begin{theorem}[A common observable quotient]\label{r:common}
141 The following conditions are equivalent:
142 \begin{enumerate}
143 \item $QT_w^\theta=QA_w$ on all of $V$, for every fixed candidate $\theta$ and every word $w$.
144 \item $E\subseteq\ker Q$.
145 \item There is a vector space $Z$, a surjective linear map $r:V\to Z$, common linear updates $G_a:Z\to Z$, and a linear readout $\bar Q:Z\to Y$ with $rT_a^\theta=G_ar$ and $Q=\bar Qr$ for every $a,\theta$.
146 \end{enumerate}
147 Under these conditions, $V/E$ is a common quotient and also predicts the output when the candidate index changes between operations.
148 \end{theorem}
149 \begin{proof}
150 Assume the first condition. For every $a,\theta,w$, equality as operators on all of $V$ gives
151 \[
152 QA_wD_a^\theta=QT_w^\theta T_a^\theta-QA_wA_a=0.
153 \]
154 The last equality applies the premise to the word executing $a$ and then $w$. Spanning proves $E\subseteq\ker Q$.
155 
156 Conversely, $E$ is invariant under every $A_a$ by construction, and contains the entire range of each difference $D_a^\theta$. Hence $T_a^\theta E\subseteq E$, and every candidate induces the same map $G_a([v])=[A_av]$ on $V/E$. Since $QE=0$, the readout descends. This proves the third condition. Composing its equalities yields the first condition. The same induction permits a different $\theta$ at each step because the quotient map and update remain shared.
157 \end{proof}
158 \source{[GA], Theorem 13.1, ``Exact common quotient for structured model uncertainty.'' The all-initial-vectors hypothesis is retained.}
159 
160 For example, let $Q(x_1,x_2,x_3)=x_1$ and let every candidate act as
161 \[
162 T^\theta(x_1,x_2,x_3)=(x_1+x_2,x_2,\theta x_3).
163 \]
164 Then $E$ is contained in the third coordinate and remains invisible. The two-coordinate method $(x_1,x_2)\mapsto(x_1+x_2,x_2)$ is exact, although the hidden dynamics are not identified.
165 
166 The conclusion would be different if a later action moved the third coordinate into the first. That change enlarges $E$ beyond $\ker Q$. It invalidates the use of this quotient, not the theorem that justified the former one.
167 
168 
169 \section{An algebraic packet is not automatically a probability}
170 The previous sections concern linear representations. Bayesian correction will require more: a nonnegative state with a well-defined total mass. Those requirements belong to a declared domain, not to the spelling of its coordinates.
171 
172 Let $\mathcal K$ be a convex cone in a real vector space, and let $\lambda$ be linear and strictly positive on every nonzero member of $\mathcal K$. Its normalized states satisfy $v\in\mathcal K$ and $\lambda v=1$. A coordinate change can send $\mathcal K$ to a cone containing negative coordinates without changing those states' probability meaning. Conversely, an arbitrary signed component of a valid state need not itself be valid.
173 
174 \begin{proposition}[When complete packets are genuine probability components]\label{r:positive-packets}
175 Let $P_1,\ldots,P_m$ be linear maps with $\sum_iP_i=I$. If every $P_i$ preserves $\mathcal K$, each normalized $v\in\mathcal K$ has the mixture decomposition
176 \[
177  v=\sum_{i:w_i>0}w_i v_i,\qquad
178  w_i=\lambda P_iv\ge0,\quad \sum_iw_i=1,\quad v_i=P_iv/w_i\quad(w_i>0).
179 \]
180 Every zero-weight component is zero. If $\mathcal K=\mathbb R^d_{\ge0}$ and the $P_i$ are also idempotent, they must be disjoint diagonal coordinate selections. Orthogonal completeness alone does not imply a probability mixture.
181 \end{proposition}
182 \begin{proof}
183 Cone preservation places $P_iv$ in $\mathcal K$, so its mass is nonnegative. Strict positivity says that a member of this cone with zero mass is zero. Applying $\lambda$ to the complete decomposition gives $\sum_iw_i=\lambda v=1$. Dividing every nonzero component by its mass proves the mixture identity.
184 
185 On the nonnegative coordinate cone, preservation is equivalent to nonnegative matrix entries, as is seen by applying a matrix to every standard basis vector. Because the matrices sum to $I$, their nonnegative off-diagonal entries must all vanish. An idempotent diagonal entry satisfies $x^2=x$, hence is zero or one. The diagonal sums are one, so each coordinate is selected by exactly one map. Finally, completeness and orthogonality without positivity do not give the first premise, as the following example shows.
186 \end{proof}
187 \source{Large Signal Model Foundations [LSM], Proposition 30, physical page 40. Only this finite packet argument and the joint-closure result below are admitted from that source at this stage.}
188 
189 \begin{counterexample}[An exact detail component has negative probability mass]\label{ce:signed-packet}
190 For $p=(3/4,1/4)^\top$, the orthogonal average and detail projectors are
191 \[
192  P_{\rm av}=\tfrac12\begin{pmatrix}1&1\\1&1\end{pmatrix},\qquad
193  P_{\rm det}=\tfrac12\begin{pmatrix}1&-1\\-1&1\end{pmatrix}.
194 \]
195 They sum to the identity and produce $(1/2,1/2)^\top$ and $(1/4,-1/4)^\top$. The components reconstruct $p$ exactly, but the detail has zero total mass without being zero. Normalizing it as a belief is undefined. Clipping its negative entry and normalizing the resulting sum would instead produce $(3/5,2/5)^\top$, a different belief.
196 \end{counterexample}
197 
198 \begin{figure}[ht]
199 \centering\includegraphics[width=.92\linewidth]{figures/signed_packets.pdf}
200 \caption{Exact reconstruction and probability interpretation are different requirements. The signed detail is useful algebraically but is not a separate probability distribution. Values are from Counterexample~\ref{ce:signed-packet}.}
201 \end{figure}
202 
203 This distinction supplies the interface to the next chapter. A signal packet may describe a discrepancy, a coordinate, or a component of an operator. A belief represents nonnegative mass over alternatives. Moving between them requires a domain-preserving map. No learned signal architecture is inferred from this algebraic admission.
204 
205 \section*{What is now available}
206 We have a declared method that preserves the selected outputs. But a predictive quotient need not retain the relationships needed for new evidence. The next chapter changes the retained object from a current physical coordinate to a set or distribution of candidate worlds.
207 
208 \chapter{Memory that remains open to correction}\label{ch:memory}
209 \question{A useful memory preserves the distinctions by which its own conclusions can be revised.}
210 Let $t:\Omega\to Y$ be the current target. A candidate set $V\subseteq\Omega$ records worlds still possible. The empty set is allowed and means that the represented candidates contradict the admitted evidence. It is not a successful identification.
211 
212 Let $\mathcal E\subseteq\Pow(\Omega)$ contain $\Omega$ and be closed under intersection. In this chapter the world does not change when an evidence event is received. The update is $V\mapsto V\cap E$. Physical actions and their effects will return in Chapter~\ref{ch:inquiry}.
213 
214 \section{A state sufficient for every later filter}
215 Define the correction signature
216 \[
217 \Sigma(V)=\bigl(t(V\cap E)\bigr)_{E\in\mathcal E}.
218 \]
219 It records what each admitted future filter would leave of the possible target values.
220 
221 \begin{theorem}[Minimal exact memory for a correction contract]\label{r:memory}
222 Equality of $\Sigma$ is a congruence for every update $V\mapsto V\cap E_0$. The signature supports the current target set and its exact update after every finite evidence sequence. Any deterministic retained state supporting the same readouts and updates on all candidate subsets must distinguish every two distinct signatures. Thus the image of $\Sigma$ has the least possible cardinality for this contract.
223 \end{theorem}
224 \begin{proof}
225 If $\Sigma(V)=\Sigma(W)$, then for each $E$,
226 \[
227 t((V\cap E_0)\cap E)=t(V\cap(E_0\cap E))=t(W\cap(E_0\cap E)).
228 \]
229 Intersection closure supplies the coordinate $E_0\cap E$, so the updated signatures agree. The $\Omega$ coordinate is the present target set. Induction gives every finite sequence.
230 
231 If signatures differ, one admitted event produces distinct target sets. A memory that merged those candidates would update identically and return the same answer on that event, contradicting exactness. Hence each signature needs its own state. The signature construction attains the lower bound.
232 \end{proof}
233 \source{[GA], Theorem 5.2. This is a behavioral quotient of the correction process, not a claim that all candidate sets must be stored literally.}
234 
235 \section{An exact count for partition evidence}
236 Suppose $C_1,\ldots,C_m$ partition $\Omega$ into nonempty cells and the admitted events are \emph{exactly} their unions. Let
237 \[
238 D_t=\{(i,y): C_i\cap t^{-1}(y)\ne\varnothing\},\qquad r=|D_t|.
239 \]
240 The occupancy memory retains whether a candidate exists in each attainable cell--target pair.
241 
242 \begin{corollary}[The size of partition correction memory]\label{r:occupancy}
243 On all subsets of $\Omega$, correction signatures are exactly distinguished by these occupancy records. There are $2^r$ signatures, and $r$ fixed binary bits are necessary and sufficient to encode them.
244 \end{corollary}
245 \begin{proof}
246 An individual-cell filter reveals the target values occupied in that cell, so the signature determines occupancy. Conversely, occupancy determines the target values left by any union of cells. Every subset of $D_t$ occurs: select one world from each included nonempty cell--target intersection and none from excluded intersections. Those intersections are disjoint. Thus there are precisely $2^r$ possible records. The preceding theorem and binary counting give necessity, while the occupancy vector supplies sufficiency.
247 \end{proof}
248 \source{[GA], Corollary 5.3. The word ``exactly'' in the evidence premise is essential.}
249 
250 For this sensor contract, the four cells are fixed pairs $(b,s)$ with either nuisance value. We admit the entire Boolean algebra generated by calibration and display events, including every union of its cells. This is a choice of evidence language, not a claim that a single calibration physically implements every union event. The target is $b$, so there are four attainable cell--target pairs. Candidate membership uses eight bits for eight worlds. Correction memory uses four bits for sixteen possible occupancies. The current target set alone has four possibilities and needs only two bits, but is not sufficient for later calibration.
251 
252 For example,
253 \[
254 V=\{(0,0,0),(1,1,0)\},\qquad W=\{(0,1,0),(1,0,0)\}
255 \]
256 have the same possible target set $\{0,1\}$. After the event $s=0$, one leaves target zero and the other target one. Their different associations are operationally relevant.
257 
258 \begin{counterexample}[A new evidence event changes the required memory]\label{ce:split}
259 Take one cell $\Omega=\{u,v\}$ and a constant target. The singleton candidate sets have the same old occupancy. If the event $\{u\}$ is added, filtering one singleton gives a target value while filtering the other gives contradiction. A record sufficient for the old event algebra is insufficient for the larger one.
260 \end{counterexample}
261 
262 \section{Noisy correction is not elimination}
263 A likelihood can be small without being zero. Deleting a candidate because an observation was surprising can invalidate a correct noise model. We therefore specify a separate probability contract.
264 
265 Let $\mathcal M$ be a finite nonempty model set with prior $p(m)$. The sampled model remains fixed during the experiment. For each $m$, let $L_m$ be a probability distribution on a finite nonempty observation alphabet $\mathcal O$. Let $\mathcal Z$ be a finite nonempty report alphabet. A stochastic reporting channel $B(o,z)$, conditionally independent of the model given $o$, creates a retained report $Z\in\mathcal Z$. The joint law is
266 \[
267 \Pr(m,o,z)=p(m)L_m(o)B(o,z),\qquad Q_m(z)=\sum_oL_m(o)B(o,z).
268 \]
269 Posterior distributions are defined only on positive-probability events.
270 
271 \begin{theorem}[When a report preserves every Bayesian correction]\label{r:bayes}
272 The following are equivalent:
273 \begin{enumerate}
274 \item For every prior, the posterior after $o$ equals that after $z$ on every positive-probability pair $(o,z)$.
275 \item The equality holds for one prior positive on every model.
276 \item There is a stochastic kernel $\rho(o\mid z)$ such that
277 \[
278 L_m(o)B(o,z)=Q_m(z)\rho(o\mid z)\quad\text{for all }m,o,z.
279 \]
280 \end{enumerate}
281 The reconstruction in the last condition refers to the actual joint experiment, not an unrelated simulation with matching marginals.
282 \end{theorem}
283 \begin{proof}
284 The first condition implies the second. Under a positive prior, define $\rho(o\mid z)=\Pr(o\mid z)$ whenever $z$ has positive probability. For a positive pair, posterior equality yields
285 \[
286 p(m)L_m(o)B(o,z)=\Pr(o,z)p(m\mid o)
287 =\rho(o\mid z)\Pr(z)p(m\mid z).
288 \]
289 Substituting Bayes' formula and cancelling positive $p(m)$ gives the factorization. A zero-probability pair under a positive prior has $L_m(o)B(o,z)=0$ for all $m$. Its conditional weight is zero. If $z$ is impossible for every model, assign any probability row to $\rho(\cdot\mid z)$ because both sides vanish.
290 
291 Conversely, the factorization makes the likelihood of $(o,z)$ a model-independent multiple of the likelihood of $z$. Normalization under any prior therefore gives $p(m\mid o,z)=p(m\mid z)$. Since the common channel only reads $o$, the same positive-pair posterior equals $p(m\mid o)$. This proves the first condition.
292 \end{proof}
293 \source{[MU], Theorem 12.1. The full-support and zero-probability cases are included in the proof.}
294 
295 The theorem permits removal of an independent nuisance flag. It does not permit removal of every association. Consider two priors on $(b,s)$, with rows indexed by $b$ and columns by $s$:
296 \[
297 P=\begin{pmatrix}1/2&0\\0&1/2\end{pmatrix},\qquad
298 P'=\begin{pmatrix}0&1/2\\1/2&0\end{pmatrix}.
299 \]
300 Both individual marginals are uniform. A noisy calibration reports $s$ correctly with probability $3/4$, independently conditional on the fixed world. The probability of report one is $1/2$ under both priors. After that report, however, the target posteriors are $3/4$ and $1/4$. Separate target and sensor marginals cannot support this correction. Their association matters even though neither marginal changed.
301 
302 These examples do not identify a universally optimal memory. They identify the least information required by a specified correction contract. A new likelihood, a newly admitted model, or a different target can change that requirement.
303 
304 
305 \section{A record must close under prediction as well as correction}
306 The preceding Bayesian theorem preserves the posterior over a fixed model family after one experiment. A continuing reasoner also predicts what happens between observations. The same compressed record must support both operations. Otherwise a valid posterior can become an inadequate input to the very next prediction.
307 
308 First consider a known finite state set $X$ with row-stochastic transition matrices $K_a(x,x')$. We retain column-vector probability distributions. A partition $\pi$ has aggregation $C_\pi(z,x)=1_{\{\pi(x)=z\}}$, so prediction is $p\mapsto K_a^\top p$. For each permitted observation symbol $o$, let $\ell_o(x)>0$ be its specified likelihood. When these are a complete report alphabet, assume also $\sum_o\ell_o(x)=1$.
309 
310 A mandatory partition $\pi_0$ with at least two blocks protects the target distinctions. We seek a refinement that supports every prediction and each separate Bayesian update for every prior. The observation is an operation available in its own right. This is stronger than inspecting only a chosen combined transition-and-report schedule.
311 
312 \begin{theorem}[Least refinement closed under prediction and correction]\label{r:joint-refinement}
313 First split $\pi_0$ by the complete vectors $(\ell_o(x))_o$, obtaining $\pi_{\rm init}$. Then repeatedly split current blocks by
314 \[
315  \left(\sum_{x'\in B}K_a(x,x')\right)_{a,B},
316 \]
317 where $B$ runs over the current blocks. The process stops after at most $|X|-|\pi_{\rm init}|$ strict refinement rounds. Its final partition is the unique coarsest refinement of $\pi_0$ for which all specified predictions admit stochastic coarse transitions and all separate Bayesian updates admit fixed strictly positive coarse likelihoods for every prior.
318 \end{theorem}
319 \begin{proof}
320 At a stable partition the probability of reaching each coarse block depends only on the current block. These sums define a stochastic coarse transition and yield $C_\pi K_a^\top=\bar K_a^\top C_\pi$, first on point masses and then by linearity. Likelihoods are constant within final blocks. Grouping the numerator and normalizer by those blocks therefore commutes with every Bayesian update.
321 
322 For minimality, take any admissible refinement $\eta$ of $\pi_0$. It has at least two blocks. Fix a strictly positive fine likelihood $\ell$ and a strictly positive coarse likelihood $\bar\ell$ inducing its assumed update. For states $x,y$ in one block and $z$ in a different block, compare priors assigning half their mass to $x,z$ and to $y,z$. Their coarse priors agree. Equality of the posterior odds gives
323 \[
324  \ell(x)/\ell(z)=\bar\ell(\eta(x))/\bar\ell(\eta(z))=\ell(y)/\ell(z).
325 \]
326 Thus $\ell(x)=\ell(y)$, and $\eta$ refines the first likelihood split. Coarse likelihoods may differ by a positive scale for each observation without changing this conclusion.
327 
328 If $\eta$ refines a current partition, each current block is a union of $\eta$ blocks. Exact prediction under $\eta$ makes the probability of reaching each such union constant inside every $\eta$ block. Hence $\eta$ refines the next split too. Induction proves that every admissible refinement refines the terminal one. Each strict round increases the block count, proving the bound. Coarseness determines the partition uniquely, up to naming its blocks.
329 \end{proof}
330 \source{[LSM], Proposition 9 and Proposition 12, physical pages 11--14. Bayesian necessity also appears in PRIQ [PRIQ], Theorem 5.6. The proof includes the two-block and strict-positivity premises rather than importing them by a cross-reference.}
331 
332 For the sensor, the mandatory display partition has two blocks. A noisy calibration that reports $s$ correctly with probability $3/4$ splits it into the four $(b,s)$ blocks. The nuisance bit remains merged. The physical flip maps these four blocks among themselves, so the transition stage introduces no further split. The representation is now closed for both prediction and correction, not merely for today's display.
333 
334 Refinement can also propagate backward through dynamics. In a separate four-state example, the mandatory partition is $\{0,1,2\}\mid\{3\}$ and the deterministic successors are $(0,2,3,3)$. A constant likelihood adds no information. Transition signatures first isolate state 2, then separate 0 from 1. The final partition is discrete. The reason for the second split is a future observable difference, not a newly sampled measurement.
335 
336 The construction uses complete tables. It does not acquire those tables, certify their physical accuracy, or guarantee a finite encoding of every posterior coordinate. Its least-state statement concerns the specified separate operations and all priors. Different admissible schedules or reachable-prior restrictions can justify another quotient.
337 
338 \section{Retain the joint law of the report and the next state}
339 A general experiment can change the state and report correlated information about the change. Describing its transition and report marginals separately is then insufficient. Let
340 \[
341  K_{a,o}(x',x)=\Pr(X_{t+1}=x',O_{t+1}=o\mid X_t=x,A_t=a)
342 \]
343 be a nonnegative finite instrument with $\sum_{o,x'}K_{a,o}(x',x)=1$ for every $a,x$. This notation is column-oriented: $K_{a,o}p$ is an unnormalized post-experiment distribution. It specifies an experiment's physical change and its observation in one object.
344 
345 For a surjection $\pi:X\to Z$, let $C$ sum probabilities over its fibres. Write
346 \[
347  z_{a,o}(p)=\mathbf1^\top K_{a,o}p,\qquad
348  \Psi_{a,o}(p)=K_{a,o}p/z_{a,o}(p)
349 \]
350 when the denominator is positive. Zero mass means an impossible report under that prior, not an arbitrarily assigned posterior.
351 
352 \begin{theorem}[One quotient for reports, posteriors, and feedback]\label{r:instrument}
353 A nonnegative normalized coarse instrument $\bar K_{a,o}$ satisfies
354 \[
355  CK_{a,o}=\bar K_{a,o}C\quad\text{for every }a,o
356 \]
357 if and only if, for all $a,o,z'$,
358 \[
359  \sum_{x':\pi(x')=z'}K_{a,o}(x',x)
360 \]
361 is constant as $x$ varies within any one input fibre. Such a coarse instrument is unique. Equivalently, it preserves for every prior both the report probabilities and the aggregated positive-probability posteriors:
362 \[
363  z_{a,o}(p)=\bar z_{a,o}(Cp),\qquad C\Psi_{a,o}(p)=\bar\Psi_{a,o}(Cp).
364 \]
365 Starting from $Cp_0$, these identities preserve every finite joint action/report law and every corresponding coarse posterior under one common policy that uses only the previously observed action/report history. This includes randomized policies with the same history-conditional action probabilities.
366 \end{theorem}
367 \begin{proof}
368 Applying the matrix identity to a point mass proves necessity of the fibre condition. Conversely, use the common sums to define each column of $\bar K_{a,o}$. They are nonnegative. Summing across $z',o$ partitions the fine successor set and gives column mass one. The definition proves the matrix equality on point masses, hence on every vector. Surjectivity gives uniqueness.
369 
370 Because $\mathbf1_Z^\top C=\mathbf1_X^\top$, the matrix equality gives equal report masses. Dividing it by a common positive mass gives equal aggregated posteriors. Conversely, equality of masses and positive-mass posteriors gives the unnormalized matrix equality on every prior. If the common mass is zero, both unnormalized vectors are zero by nonnegativity. Point masses finish that direction.
371 
372 For a history $h$, keep unnormalized states $u_h,\bar u_h$. Initially $\bar u_\varnothing=Cu_\varnothing$. After choosing action $a$ with common probability $\gamma(a\mid h)$ and receiving $o$, the next states are $\gamma(a\mid h)K_{a,o}u_h$ and $\gamma(a\mid h)\bar K_{a,o}\bar u_h$. The intertwining identity preserves their aggregation. Induction gives equal mass for every history, including zero-mass histories. Normalization on positive histories gives the posterior statement. Stopping decisions based on the same history can be included as matching terminal choices.
373 \end{proof}
374 \source{Selected synthesis of the positive-transfer and filtering arguments in [PRIQ], Theorems 5.2, 6.1 and 6.3, and the projected-law construction in AVOC [AVOC], Theorem 4.5. The joint instrument and feedback formulation is proved here. No entire nonlinear source theorem or Lean implementation is imported.}
375 
376 \begin{counterexample}[Correct marginals with an incorrect correction]\label{ce:joint-marginals}
377 Two fine current states have the same retained label. From the first, the next retained state and report are $(0,0)$ or $(1,1)$, each with probability $1/2$. From the second they are $(0,1)$ or $(1,0)$, again equally likely. In both cases the next-state marginal is uniform and the report marginal is uniform. After report one, however, the next retained state is certainly one in the first case and certainly zero in the second. No common filter based only on the old label can realize both. The joint fibre condition detects exactly the lost association.
378 \end{counterexample}
379 
380 Preserving only normalized posteriors is weaker still. A report coin independent of the hidden state leaves every prior unchanged whether its success probability is $1/4$ or $3/4$. Those two instruments have identical posterior maps but different report laws. A planner that prices later branches needs those probabilities. In the exact instrument theorem the evidence scale is fixed, rather than silently discarded during normalization.
381 
382 \section{Small law error and a rare conditional history}
383 Approximate models must be compared before declaring their posteriors close. Let $\widetilde K$ be a normalized instrument on the same coarse state and report alphabets. Suppose, at step $t$, every relevant action and fine state satisfy
384 \[
385  \TV\left(\left(\sum_{x':\pi(x')=z'}K_{a,o}(x',x)\right)_{o,z'},
386              (\widetilde K_{a,o}(z',\pi(x)))_{o,z'}\right)\le\epsilon_t.
387 \]
388 This is a bound on a complete report/next-state distribution, not on an isolated matrix entry. Assume $\TV(Cp_0,\widetilde p_0)\le\delta_0$ with nonnegative $\delta_0,\epsilon_t$. Both models run the same history-based policy. Coarse states recorded in the comparison below are analytical coordinates, not extra observations supplied to that policy.
389 
390 \begin{proposition}[A whole-history bound with an explicit conditioning cost]\label{r:history-bound}
391 At horizon $H$, the distributions $P_H,\widetilde P_H$ of the full coarse-state and action/report histories satisfy
392 \[
393  \TV(P_H,\widetilde P_H)\le d_H:=\min\left\{1,\delta_0+\sum_{t=0}^{H-1}\epsilon_t\right\}.
394 \]
395 The same bound holds after forgetting any of those history coordinates. For an observed history event $E$ with probabilities $p_E,\widetilde p_E>0$, the conditional final coarse-state distributions obey
396 \[
397  \TV\bigl(P_H(Z_H\in\cdot\mid E),\widetilde P_H(Z_H\in\cdot\mid E)\bigr)
398  \le\min\left\{1,\frac{d_H}{\max(p_E,\widetilde p_E)}\right\}.
399 \]
400 If either event probability exceeds $d_H$, the other is necessarily positive.
401 \end{proposition}
402 \begin{proof}
403 Condition on a complete coarse history with positive fine probability. Its hidden current-state distribution is a mixture of states in the last coarse fibre. Convexity of total variation makes the true next report/coarse-state row differ from the declared row by at most $\epsilon_t$. Mixing over a common action kernel preserves this bound. Extend the two old history laws first through the same declared row. Total variation cannot increase under a common stochastic kernel, by the triangle inequality and row sums. Replacing those rows with the true conditional rows adds at most $\epsilon_t$, weighted by a total history mass of one. Hence the history distance at the next step is at most the old distance plus $\epsilon_t$. Induction and the cap one prove the first claim. Summing over forgotten coordinates is also a stochastic map, proving the second.
404 
405 For conditioning, let $u,v$ be the restrictions of the two history laws to $E$, with masses $p_E,\widetilde p_E$. The difference on the complement has $\ell^1$ norm at least $|p_E-\widetilde p_E|$. Thus
406 \[
407  \|u-v\|_1+|p_E-\widetilde p_E|\le2d_H.
408 \]
409 Adding and subtracting $v/p_E$ bounds the conditional distance by $d_H/p_E$. Interchanging the laws gives $d_H/\widetilde p_E$, so the smaller of these bounds has the displayed maximum denominator. Projection to the final state cannot increase the distance. Finally, the probability of any event changes by at most total variation, which proves positivity when one mass exceeds $d_H$.
410 \end{proof}
411 \source{Finite probability-instrument specialization of [LSM], Propositions 43--44, with the joint retained-state record made explicit. The symmetric conditioning form follows by applying the same elementary bound in both directions. [PRIQ], Section 9 supplies the complementary stepwise posterior-error perspective.}
412 
413 \begin{counterexample}[A rare report carries the entire discrepancy]\label{ce:rare-history}
414 Two joint laws place mass $1-\delta$ on the same ordinary outcome. On a report event $E$ of mass $\delta>0$, one puts all mass on retained state zero and the other on retained state one. Their whole-law distance is $\delta$, while their conditional distance after $E$ is one. The factor involving event probability is therefore essential. This is a finite-law statement, not an empirical estimate of a sensor error.
415 \end{counterexample}
416 
417 \begin{figure}[ht]
418 \centering\includegraphics[width=.92\linewidth]{figures/rare_history.pdf}
419 \caption{In Counterexample~\ref{ce:rare-history}, shrinking the rare-event mass reduces whole-law error but leaves conditional error maximal. The points are exact specified probability laws, not sampled observations.}
420 \end{figure}
421 
422 The bound compares one policy across two models, not independently optimized controllers. Chapter~\ref{ch:inquiry} supplies the uniform comparison needed for re-optimization. First, the next chapter asks what decisions and explanations the corrected record can justify.
423 
424 \chapter{From corrected records to decisions and explanations}\label{ch:decision}
425 \question{The same record, model, and continuation must support the decision being certified.}
426 Correctness of a probability calculation is not a guarantee that a real process follows its likelihood model. Within the declared model, however, a small error in the retained distribution can support a precise decision bound. We state that bridge before introducing communication, so that an explanation has a definite object to preserve.
427 
428 \section{One quantitative decision contract}
429 Let $p$ and $\widehat p$ be distributions on the same finite world set. For each world let $v_\omega$ be a response and $\widehat v_\omega$ its approximation in one metric space. Assume
430 \[
431 \TV(p,\widehat p)\le e,\qquad
432 \sup_\omega d(v_\omega,\widehat v_\omega)\le d_0.
433 \]
434 For each action $a$ in a finite nonempty set, let the loss $\ell(a,v)$ lie in $[0,1]$ and be $K$-Lipschitz in $v$. Define the model risks
435 \[
436 R(a)=\sum_\omega p(\omega)\ell(a,v_\omega),\qquad
437 \widehat R(a)=\sum_\omega\widehat p(\omega)\ell(a,\widehat v_\omega).
438 \]
439 
440 \begin{theorem}[A decision bound for one actual approximation chain]\label{r:risk}
441 Put $\xi=\min\{1,e+Kd_0\}$. For every action, $|R(a)-\widehat R(a)|\le\xi$. If $\widehat a$ minimizes the approximate risk, then
442 \[
443 R(\widehat a)-\min_a R(a)\le\min\{1,2\xi\}.
444 \]
445 If the approximate gap between its unique minimizer and every alternative exceeds $2\xi$, that action is also the unique true model-risk minimizer.
446 \end{theorem}
447 \begin{proof}
448 Add and subtract $\sum_\omega p(\omega)\ell(a,\widehat v_\omega)$. The response term has absolute value at most $Kd_0$. The expectation of a function in $[0,1]$ changes by at most total variation, giving the other term at most $e$. Risks lie in $[0,1]$, so their difference is also at most one.
449 
450 For a true minimizer $a_*$,
451 \[
452 R(\widehat a)\le\widehat R(\widehat a)+\xi
453 \le\widehat R(a_*)+\xi\le R(a_*)+2\xi.
454 \]
455 The loss range supplies the cap one. Finally, for any other $a$, subtract the two error bounds to obtain
456 $R(a)-R(\widehat a)\ge\widehat R(a)-\widehat R(\widehat a)-2\xi>0$.
457 \end{proof}
458 \source{[GA], ``A common quantitative grounding certificate'' and [MU], ``A joint posterior and recipient decision certificate.'' This is a specialization to a common finite candidate set and bounded loss.}
459 
460 The phrase ``model risk'' matters. The theorem cannot repair an omitted candidate, a false sensor convention, or an action outside the stated loss function. It also cannot combine a posterior bound from one history with a response bound from another. The record must bind the actual calculation and its premises.
461 
462 For the noisy calibration example, use zero-one loss for selecting the target bit. Under $P$ and report one, choosing one has risk $1/4$, while choosing zero has risk $3/4$. An approximation with total variation at most $1/10$ and no response error preserves the unique decision because the gap $1/2$ exceeds $2/10$. Under $P'$ the correct decision reverses. A valid error bound around the wrong prior is not a substitute for retaining the correct association.
463 
464 \section{An explanation belongs to a recipient}
465 An artifact is not an explanation merely because its producer can interpret it. Fix a finite case set $X$, a sender-access map $\alpha:X\to H$, and a finite artifact catalogue $\mathcal C$. Recipient $i$ has a background record $\beta_i(x)$, a demanded output $t_i(x)$, and a fixed bounded procedure $L_i$. A timeout, malformed artifact, wrong output, or budget overrun counts as failure.
466 
467 Let $\mathcal C(x)$ be the artifacts that succeed for every recipient in case $x$. For an attained sender value $h$, put
468 \[
469 \mathcal C_h=\bigcap_{x:\alpha(x)=h}\mathcal C(x).
470 \]
471 
472 \begin{theorem}[A common artifact for fixed recipients]\label{r:recipient}
473 A sender restricted to $\alpha(x)$ can provide one exact artifact for all recipients if and only if every $\mathcal C_h$ is nonempty. When feasible, the smallest possible number of distinct transmitted artifacts is
474 \[
475 \min\{|C|:C\subseteq\mathcal C,\ C\cap\mathcal C_h\ne\varnothing
476 \text{ for every attained }h\}.
477 \]
478 \end{theorem}
479 \begin{proof}
480 A sender seeing $h$ must choose the same artifact for all cases in that fibre. It must therefore select a member of $\mathcal C_h$, proving necessity. Choosing one member of each nonempty finite intersection gives a valid encoder. The image of any encoder intersects every $\mathcal C_h$. Conversely, any catalogue meeting all those sets supplies such an encoder by choosing from the intersections. Finite minimization gives the formula.
481 \end{proof}
482 \source{[MU], ``The fixed-recipient covering criterion.'' The earlier designed-decoder coloring criterion is not substituted for the installed-recipient problem.}
483 
484 \begin{counterexample}[Individual acceptability is not a common message]\label{ce:message}
485 Two cases have the same sender record. In one, the sole acceptable artifact is $c_0$. In the other it is $c_1\ne c_0$. Each case has a valid explanation if its hidden identity is known. Their intersection is empty, so the sender cannot select a valid common explanation from its actual information.
486 \end{counterexample}
487 
488 In the sensor, a sender observing $y$ can transmit one bit to a recipient holding $s$. The recipient's fixed XOR procedure returns $b=y\oplus s$. The sender need not know $b$: its message combines with the recipient's background.
489 
490 A decoder that ignores this message fails where background alone cannot distinguish the target. More strings do not fix that procedure. Installed information, interpreter work, and message size are separate resources.
491 
492 \chapter{One investigation, one resource budget}\label{ch:inquiry}
493 \question{A possible answer, an affordable observation, and a small program must belong to the same workflow.}
494 Let $X$ be a finite nonempty state space. It includes every origin tag, permission, background record, and history variable that affects the stated behavior. An experiment $e$ is allowed on a domain $D_e\subseteq X$, has a deterministic successor $f_e:D_e\to X$, a report $o_e:D_e\to O_e$, and a fixed nonnegative integer resource vector $c_e$.
495 
496 A current support $V\ne\varnothing$ records possible states. The experiment is permitted only if $V\subseteq D_e$. After report $o$, the possible \emph{post-experiment} states are
497 \[
498 V_{e,o}=\{f_e(x):x\in V,\ o_e(x)=o\}.
499 \]
500 Only nonempty report branches are retained. If the target concerns a past value, that value must survive as an immutable tag. Resetting the current state is not recovering its history.
501 
502 The experiment catalogue and the terminal-artifact catalogue are finite, and the resource vector has a fixed finite dimension. A terminal artifact $a$ is acceptable only if every fixed recipient succeeds in every state of $V$. Its worst-case terminal cost is $g_a(V)$, computed componentwise. A controller is a literal finite tree with one record per experiment or terminal node. Stored memory counts all branches, including those not visited in one execution.
503 
504 \section{The complete finite frontier}
505 Let $\mathcal P_h(V)$ be the nondominated pairs $(v,m)$ of worst-case online resource vectors and stored-record counts attainable by successful trees with at most $h$ experiment steps. At depth zero the available pairs are
506 \[
507 \operatorname{Pareto}\{(g_a(V),1):a\text{ succeeds throughout }V\}.
508 \]
509 At greater depth retain those stops and, for each uniformly permitted experiment and one feasible child pair $(v_o,m_o)$ for every nonempty branch, form
510 \[
511 \left(c_e+\max_o v_o,\quad1+\sum_o m_o\right).
512 \]
513 A profile dominates another when it is no larger in every resource coordinate and strictly smaller in at least one. The maximum is componentwise. An impossible child contributes no tree. It is not a zero-cost branch.
514 
515 \begin{theorem}[Exact joint feasibility for explicit controllers]\label{r:inquiry}
516 This recurrence gives exactly the nondominated resource profiles of successful depth-bounded controllers. Every retained pair has a concrete tree witness. A common online and storage budget is feasible if and only if it bounds one retained pair. Removing dominated child profiles does not change feasibility under any componentwise budget.
517 \end{theorem}
518 \begin{proof}
519 At zero depth the only possibilities are acceptable terminals, whose profiles are exactly the stated stops. At positive depth a successful tree either stops or begins with one uniformly allowed experiment. Every possible report needs a successful child on precisely $V_{e,o}$. By induction those children have profiles in the lower-depth attainable set. Worst-case online cost is the root cost plus their componentwise maximum. Complete tree storage is one plus the sum of all child records.
520 
521 Conversely, combining any allowed root with a successful child for every report constructs a successful tree with that profile. This proves exact enumeration before pruning. Replacing a dominated child by a dominating one cannot increase either a coordinatewise maximum or a sum of record counts, and does not change its supported initial set. Thus Pareto pruning preserves every feasible budget and every retained profile has a witness.
522 \end{proof}
523 \source{[MU], ``A joint resource certificate for fixed recipients,'' and [SII], Theorem 6.2. The scalar-cost repair case is a specialization, not a different composition theorem.}
524 
525 The recurrence can be expensive. It is a finite mathematical characterization, not an efficient general learner. It assumes its transition and acceptance tables. Their discovery and checking are preparation costs, not free consequences of the existence theorem.
526 
527 \begin{counterexample}[Two separate optima do not form one controller]\label{ce:pareto}
528 There are four immutable cases, each requiring its own terminal answer. A direct observation of the case costs four units and gives a five-record tree including four terminals. Unit-cost equality tests can identify the case in at most three tests with seven records. Terminal answers have zero online cost in this particular example. The frontier is $(4,5)$ and $(3,7)$. The mixed budget $(3,5)$ is infeasible: an all-equality successful tree needs four leaves and at least seven records. Any tree using the direct observation on a reachable path costs at least four.
529 \end{counterexample}
530 
531 \begin{figure}[ht]
532 \centering\includegraphics[width=.88\linewidth]{figures/joint_frontier.pdf}
533 \caption{The four-origin example has two nondominated profiles. Combining the lowest coordinate from each does not construct a feasible controller. Terminal answers have zero online cost in this example.}
534 \end{figure}
535 
536 \section{When a checked candidate can end the search}
537 Consider $n\ge1$ immutable cases with total nondestructive binary unit-cost queries. Every unit-cost repair succeeds in exactly one case, and every case has a repair. A controller must succeed certainly in every case.
538 
539 \begin{theorem}[A candidate attaining both lower bounds is optimal]\label{r:lowerbound}
540 Every successful controller has worst-case work at least $1+\lceil\log_2n\rceil$ and literal storage at least $2n-1$. A checked controller attaining both bounds and the requested horizon realizes the entire nondominated work/storage frontier.
541 \end{theorem}
542 \begin{proof}
543 Distinct cases cannot end at the same successful repair leaf, so at least $n$ leaves are reachable. A binary tree of query depth $d$ has at most $2^d$ leaves, giving $d\ge\lceil\log_2n\rceil$. The terminal repair adds one unit.
544 
545 Let $l$ be the number of leaves and $i_1,i_2$ the counts of unary and binary internal nodes. Counting tree edges gives $i_1+2i_2=i_1+i_2+l-1$, hence $i_2=l-1$. Total records are $2l-1+i_1\ge2n-1$. A successful candidate at both coordinatewise lower bounds dominates every other attainable cost profile. Its validity and horizon check make it an actual member of the frontier, leaving that pair as the whole nondominated frontier.
546 \end{proof}
547 \source{[SII], Theorem 11.1. The assumptions exclude destructive resets and repairs that succeed on several cases.}
548 
549 For eight possible defective cells, equality-first diagnosis requires seven queries in the worst case, while three coordinate-bit queries identify the cell. Including repair gives costs eight and four, respectively. Both literal trees have fifteen records. Faster execution has not eliminated the cost of storing the procedure.
550 
551 This eight-cell example is separate from the eight-world sensor. The sensor has only four action-relevant $(b,s)$ pairs and an irrelevant nuisance coordinate. Confusing hidden-world cardinality with the number of required repair distinctions would import a false lower bound.
552 
553 
554 \section{Expected-cost inquiry uses the report probabilities}
555 The preceding frontier certifies worst-case execution and complete tree storage for deterministic observations. A noisy report requires a different optimization. Expected cost weights each future branch by its probability. A low expectation is not a hard execution budget, and neither replaces the cost of storing the whole controller.
556 
557 Use the finite instrument of Theorem~\ref{r:instrument}, with fine belief $p$ and coarse belief $q=Cp$. At $q$, a finite set of experiments $A(q)$ is permitted, and a nonempty finite set of terminal decisions $D(q)$ is available. These catalogues must be identical for every fine belief with the same $q$. Stopping with decision $d$ has loss $\ell_d(\pi(x))$ in fine state $x$, so its conditional risk is $\langle q,\ell_d\rangle$. An experiment has a finite nonnegative charge $c_a(q)$, identical on the fine and coarse side. All history variables affecting permissions, charges, or targets must be included in the declared state.
558 
559 Let $J_h(p)$ be the least expected charge plus terminal loss attainable using at most $h$ further experiments, with terminal decisions permitted at any step. It is defined by finite observation trees, not by a hidden-state controller. Its coarse recurrence is
560 \begin{align*}
561  \bar J_0(q)&=\min_{d\in D(q)}\langle q,\ell_d\rangle,\\
562  \mathcal Q_h(q,a)&=c_a(q)+\sum_{o:\bar z_{a,o}(q)>0}
563        \bar z_{a,o}(q)\bar J_{h-1}\bigl(\bar\Psi_{a,o}(q)\bigr),\\
564  \bar J_h(q)&=\min\left\{\bar J_0(q),\ \min_{a\in A(q)}\mathcal Q_h(q,a)\right\}.
565 \end{align*}
566 An empty experiment catalogue leaves only stopping. Impossible reports do not receive invented posteriors.
567 
568 \begin{theorem}[The same compressed belief supports the same inquiry]\label{r:belief-planning}
569 Under the exact instrument quotient and the common loss, charge, and catalogue assumptions above,
570 \[
571  J_h(p)=\bar J_h(Cp)\quad\text{for every prior and every finite }h.
572 \]
573 Every first-action value and optimal first-action set agrees. A minimizing coarse-belief policy produces a fine-model optimal history-based policy, including its stopping decision. Finite minimizing trees exist. The result supplies neither an efficient synthesis algorithm nor a worst-case storage or resource guarantee.
574 \end{theorem}
575 \begin{proof}
576 At zero horizon the terminal risks agree by fibrewise summation. Suppose the equality holds at $h-1$. For any permitted first experiment, Theorem~\ref{r:instrument} gives the same probability of each report and the same coarse posterior on every positive branch. The induction hypothesis gives equal optimal continuation costs on each such branch. The first charge agrees, so the entire action value agrees. Stopping has the same value as well. Taking the minimum over the identical catalogues proves both value equality and equality of minimizing first choices.
577 
578 Choose one minimizing first choice and attach minimizing lower-horizon trees to its finitely many positive branches. If the choice is terminal, no child is required. Induction constructs a finite tree attaining the value. The same induction bounds every other admissible tree below by that minimum. An observed history initializes the same coarse belief in the fine execution, so selecting from that belief realizes the coarse policy without observing the fine hidden state.
579 \end{proof}
580 \source{The finite backup and projected-law proof mechanisms of [AVOC], Theorems 4.5 and 9.2, applied here to the belief transition supplied by Theorem~\ref{r:instrument}. The source-facing Machine Theory correspondence covers this selected result. That correspondence is separate from any claim that the complete AVOC implementation is verified. The established partially observed planning context is [KLC].}
581 
582 \begin{counterexample}[A correct probability quotient can hide a forbidden action]\label{ce:permission-loss}
583 Two fine states share all report and transition probabilities and are given the same coarse label. A terminal repair is permitted in one state but forbidden in the other. The instrument quotient is valid, but a coarse interface that offers the repair in both states is not. Exact belief and value formulas do not repair a missing permission distinction. The catalogues must factor through the retained state, or the state must be refined.
584 \end{counterexample}
585 
586 \section{The sensor chooses when another calibration is worth its cost}
587 Return to the sensor after display $y=0$. Conditional on that display, assign equal probability to $(b,s)=(0,0)$ and $(1,1)$, with any nuisance distribution inside each pair. Only noisy calibration and terminal bit selection are offered in this example. A calibration reports $s$ correctly with probability $3/4$, with fresh conditionally independent noise and no change to the hidden world. It costs $1/20$ in the same stated loss units as a wrong terminal choice, whose loss is one. A correct terminal choice has loss zero.
588 
589 The retained belief on the four $(b,s)$ pairs is an exact quotient of the eight-world belief. Its two diagonal masses initially equal $1/2$. After one calibration the favored target has probability $3/4$. A second matching report raises that probability to $9/10$, while conflicting reports restore $1/2$.
590 
591 \begin{center}\begin{tabular}{@{}>{\raggedright\arraybackslash}p{.16\linewidth}>{\raggedright\arraybackslash}p{.24\linewidth}>{\raggedright\arraybackslash}p{.54\linewidth}@{}}\toprule
592 Report limit & Optimal expected cost & An optimal initial choice\\\midrule
593 0 & $1/2$ & Stop and select either bit.\\
594 1 & $3/10$ & Calibrate once, then select.\\
595 2 & $3/10$ & Calibrate once, then stop.\\
596 3 & $11/40$ & Calibrate, then use an adaptive continuation.\\\bottomrule\end{tabular}\end{center}
597 
598 \begin{figure}[H]
599 \centering\includegraphics[width=.94\linewidth]{figures/calibration_policy.pdf}
600 \caption{An optimal three-report policy in the unchanged eight-world sensor with the explicitly added noisy calibration channel. All masses and costs are exact. The diagram groups sign-symmetric report histories, not distinct hidden states supplied to the agent.}
601 \end{figure}
602 
603 With three reports available, the optimal policy takes a second report after the first. If the first two agree, it stops. If they disagree, it takes the third. The disagreement probability is $3/8$. Thus the expected report count is $2+3/8=19/8$, the expected charge is $19/160$, and the error probability is $5/32$. The total is $19/160+5/32=11/40$.
604 
605 A second report alone does not reduce expected classification error enough to pay for itself. A third-report allowance makes it worthwhile to investigate only the unresolved branch. This gain is achieved by one contingent policy, without access to the hidden bit.
606 
607 
608 
609 The two-valued display state is too coarse for this inquiry. The four-pair probability record supports calibration and decisions while still discarding the nuisance bit.
610 
611 \section{An approximate model supports a different, quantitative claim}
612 Exact policy transport and approximate planning must not share one unqualified guarantee. Fix a finite horizon $H$ and one nonempty finite class $\mathfrak P$ of admitted action/report trees, shared by the true and approximate models. The complete loss of a tree is the same function of its coarse-state and action/report path in both models, taking values in $[0,B]$. For example, a terminal loss in $[0,1]$ and at most $H$ charges bounded by $c_{\max}$ give $B=1+Hc_{\max}$.
613 
614 Assume Theorem~\ref{r:history-bound}'s bound $d_H$ holds uniformly over every tree in that class. An early stop is padded by a common absorbing terminal step for the history comparison. State-dependent charges are permitted when included in the same coarse-path loss. A model-dependent posterior score used as an uncharged surrogate loss would be a different problem.
615 
616 \begin{proposition}[Uniform model error controls a changed policy]\label{r:policy-error}
617 Let $J(\pi)$ and $\widetilde J(\pi)$ be a tree's expected losses in the true and approximate models. Then
618 \[
619  |J(\pi)-\widetilde J(\pi)|\le Bd_H\quad(\pi\in\mathfrak P).
620 \]
621 If $\widetilde\pi$ minimizes the approximate loss and $\pi_*$ minimizes the true loss over this same class, then
622 \[
623  J(\widetilde\pi)-J(\pi_*)\le\min\{B,2Bd_H\}.
624 \]
625 These conclusions do not certify a zero-risk constraint or preservation of admissibility outside the common class.
626 \end{proposition}
627 \begin{proof}
628 The expectation of a function in $[0,B]$ changes by at most $B$ times total variation. Apply the common-policy history bound separately to each fixed tree, proving the first assertion uniformly. Now
629 \[
630  J(\widetilde\pi)\le\widetilde J(\widetilde\pi)+Bd_H
631  \le\widetilde J(\pi_*)+Bd_H\le J(\pi_*)+2Bd_H.
632 \]
633 The loss range gives the cap $B$. Each tree is first compared with itself across models, before applying optimality to different controllers. A zero-probability bad event in one model can have positive probability in the other, so the average bound does not certify sure feasibility.
634 \end{proof}
635 \source{Direct combination of the whole-history bound with the selection argument already used in Theorem~\ref{r:risk}. [AVOC], Sections 8--10, provide the source context for guarded planning and model-error value bounds. This finite fixed-policy-class formulation is stated and proved in full here.}
636 
637 With true calibration accuracy $37/50$ and planning accuracy $3/4$, the one-step defect is $1/100$. Taking $H=3$ and $B=23/20$ gives the uniform regret bound $69/1000$. A computed performance value does not replace that guarantee. Expected-risk and hard-budget claims remain distinct.
638 
639 \chapter{Improving discovery without changing its meaning}\label{ch:discovery}
640 \question{Removing redundant work is an improvement only when the removed work could not change the justified result.}
641 Let $\mathcal G=(p_0,\ldots,p_{N-1})$ be a finite ordered grammar of pure, total candidate programs. Let $D$ be a finite context set and $t:D\to Y$ a fixed labeling. A teacher either accepts a candidate that agrees everywhere or returns a context where it disagrees. The teacher's work is part of the development account.
642 
643 \section{Finite counterexample-guided acquisition}
644 The learner retains every returned counterexample. It proposes the earliest candidate consistent with all retained examples, or reports exhaustion of the grammar when none remains.
645 
646 \begin{proposition}[What finite counterexamples establish]\label{r:cegis}
647 The learner never submits the same rejected candidate twice. Within at most $N$ teacher calls, it returns the earliest globally correct candidate in the declared grammar or exhausts that grammar. A timeout before this process finishes is neither acceptance nor exhaustion.
648 \end{proposition}
649 \begin{proof}
650 Each counterexample refutes the submitted program and remains a constraint forever. That program cannot be submitted again. A globally correct candidate never violates a truthful counterexample. With only $N$ candidates, either an accepted one is found or all are ruled out. If the accepted candidate were preceded by a globally correct candidate, that earlier candidate would still be consistent and would have been selected first. This proves the ordering claim. Interruption changes none of these logical implications and cannot supply a completed search result.
651 \end{proof}
652 \source{[SII], Theorem 15.1. This is finite exact synthesis in a supplied language, not a statistical generalization guarantee.}
653 
654 Agreement on $D$ is not validity outside $D$. That distinction is especially important when a candidate is used to prune future searches. A wrong proposal can be rejected by a final checker. A wrong pruning rule may remove the only candidate the checker ought to see.
655 
656 \section{A learned search representation can preserve the exact investigation}
657 Suppose a deterministic normalizing map $n$ is sound in the following direction:
658 \[
659 n(p)=n(q)\ \Longrightarrow\ p(z)=q(z)\quad\text{for every admitted context }z.
660 \]
661 The map need not detect every semantic equivalence or produce a mathematically canonical normal form. Each successful contextual rewrite must be justified under the actual pure, total semantics. Keep the earliest original AST for every attained normal form, not a replacement AST with an uncharged new interpreter.
662 
663 \begin{theorem}[Ordered semantic compression preserves the teacher trace]\label{r:ordered}
664 Assume all counterexamples are retained, candidate and example orders are fixed, and the teacher is deterministic and extensional, returning the first disagreement in a fixed context order. Searching only the earliest representatives yields exactly the same submitted ASTs, counterexamples, and final acceptance or grammar exhaustion as the original learner. With the same AST interpreter it uses no more retained-example evaluations. Preparation, dispatch, and stored-index costs are separate.
665 \end{theorem}
666 \begin{proof}
667 A removed expression has an earlier representative with the same values on every admitted context. If that representative was accepted, the original search ended before reaching the removed expression. Otherwise an already retained example refuted the representative, either during a consistency test or from the teacher. Persistence of examples means that the same example refutes the later equivalent expression. The original learner therefore never submits that removed expression to the teacher.
668 
669 Deleting only those unsuccessful consistency tests preserves the next submitted AST. A deterministic teacher then returns the same counterexample or acceptance. Induction over submissions proves equality of the complete trace, including exhaustion. Every deleted evaluation has nonnegative cost in the named evaluation count. The argument makes no claim that constructing or consulting the representative index is free.
670 \end{proof}
671 \source{[SII], Theorems 21.1 and 21.2. Sound equational replacement is the premise. Empirical agreement on a few probe points does not supply it.}
672 
673 \begin{counterexample}[A probe-equivalent equation is not a general identity]\label{ce:probe}
674 The expressions $\max(x,1)$ and $x$ agree for probes $x\in\{1,2,3\}$. At zero they differ. Grouping them by those probe values alone can remove a needed candidate. The identity $\max(x,0)=x$ is valid over nonnegative integers, but not over all integers. The semantic domain is part of the equation's certificate.
675 \end{counterexample}
676 
677 The retained object may therefore improve later search without containing its answers. This is the precise process-level role of a checked equation library. The grammar, primitive semantics, teacher, and proof rules can still be supplied. Their presence must remain visible instead of being redescribed as discoveries.
678 
679 \section{A reusable rule for stopping an unpromising read}
680 A diagnostic compiler inspects a binary query on $m$ immutable cases. In the prefix already read, $a$ cases give zero and $b$ give one. Each child is allowed at most $C$ cases because the remaining binary depth has that leaf capacity. Assume integers
681 \[
682 C\ge1,\quad 2\le m\le2C,\quad a,b\ge0,\quad a+b\le m.
683 \]
684 
685 \begin{proposition}[A sound prefix exclusion]\label{r:prefix}
686 The unread reports can be completed with both final branch counts at most $C$ if and only if $\max(a,b)\le C$. A scan may therefore stop when one count first exceeds $C$. In a fixed ordered depth-first compiler with identical scope, terminal, and fallback rules, replacing full root scans by this early rejection preserves the first returned tree or the completed depth-bounded failure result.
687 \end{proposition}
688 \begin{proof}
689 Counts only increase, so an overfull child cannot be rescued. Otherwise the two remaining capacities are $C-a$ and $C-b$, both nonnegative. Their sum $2C-a-b$ is at least the number $m-a-b$ of unread rows. Distributing the unread cases between those capacities gives a feasible completion.
690 
691 Every root rejected early would also be rejected after its full scan. A root not rejected early is read completely and produces the same ordered child supports. Induction on the finite remaining depth therefore yields identical recursive searches, backtracking, and first completion. The same failure condition invokes the same fallback. The skipped rows are only suffixes whose contents could not change rejection. A resource timeout is excluded from the completed-failure claim.
692 \end{proof}
693 \source{[SII], Proposition 16.1 and Theorem 16.3. The conclusion concerns capacity feasibility, not the existence of a completing query in the installed language.}
694 
695 For $C=4$, a fifth zero already closes a root. Reading more rows cannot reduce that branch. By contrast, a four-versus-four split merely survives this necessary test. If no remaining query distinguishes either child, the root still fails.
696 
697 \begin{counterexample}[A changed repair defeats the old premise]\label{ce:universal}
698 Four cases previously required four different repairs. Admit one new repair successful in all four. No identifying query is now needed. The old singleton-leaf lower bound and its pruning interpretation are not applicable. The correct response is to recheck the repair scope, not to preserve an obsolete optimization because it once passed.
699 \end{counterexample}
700 
701 \section*{What is now available}
702 The resulting method is semantically justified only under its premises. We must still determine whether it saves total resources, and which proof records remain usable when a later revision changes those premises. Both questions belong to the next chapter rather than being inferred from a successful synthesis.
703 
704 \chapter{What remains valid after a revision}\label{ch:revision}
705 \question{A mathematical proof can remain true while no longer applying to the installed system.}
706 A certificate for ordinary integer addition is not a certificate for an operation with the same printed name and a different implementation. A grammar quotient depends on the grammar order. A comparison depends on the actual controller and the prices used to value its events. These are distinct dependencies.
707 
708 \section{Reuse follows semantic dependencies}
709 Let an artifact state be $a=(a_1,\ldots,a_d)$. A finite directed acyclic graph represents claimed guarantees. For vertex $v$, let $D_v$ be its direct artifact dependencies and let $\operatorname{pa}(v)$ be its parent guarantees. The declaration is semantically complete if the meaning of its claim and local verification rule is determined by those components and parent claims. External assumptions are included explicitly as premises.
710 
711 After changing $a$ to $a'$, mark a vertex stale when a direct input changes and propagate staleness to all descendants. Call the resulting set $\Delta$.
712 
713 \begin{theorem}[Selective reuse with complete dependencies]\label{r:dependencies}
714 Assume the graph is finite and acyclic, direct dependencies are semantically complete, local rules are sound, and the applicable external premises hold. Assume also that every old witness established its old claim before the revision. Old witnesses still establish every claim outside $\Delta$. Re-establishing affected claims in topological order, using revised values and established parents, restores the corresponding revised claims. Without an affected parent's re-establishment, this reuse rule supplies no justification for its dependent claim.
715 \end{theorem}
716 \begin{proof}
717 A vertex outside $\Delta$ has unchanged direct values and no stale parent. In topological order, induction shows that every parent retains its meaning and proof. Completeness of the dependency declaration leaves the local argument applicable. For a stale vertex, once its revised parents are established, soundness of the newly checked local rule gives the revised conclusion. A second topological induction proves restoration. An unchecked parent leaves a missing premise, so the rule alone cannot justify a dependent conclusion. This is not a proof that the conclusion is false.
718 \end{proof}
719 \source{[SII], Theorem 24.1. It is a theorem about a declared complete dependency graph, not a method that infers complete dependencies from arbitrary programs.}
720 
721 \begin{counterexample}[A missing dependency defeats a perfect replay]\label{ce:dependency}
722 A stored claim is $u=v$, initially with both values zero. Its registry records only $u$. Change $v$ to one. A flawless comparison with the recorded $u$ still passes, while the claim is false. A hash or replay cannot recover the premise the registry omitted.
723 \end{counterexample}
724 
725 Adding the universal repair from the preceding chapter changes a successful-repair set. It invalidates a cardinality certificate and any dependent performance statement. It need not invalidate an arithmetic equation used elsewhere. A new valid repair also does not inherit the old controller's speed comparison. Rechecking can legitimately conclude that the new route is slower, cheaper, or incomparable under the stated resources.
726 
727 \begin{figure}[ht]
728 \centering\includegraphics[width=\linewidth]{figures/revision_scope.pdf}
729 \caption{A change to the repair language affects the diagnostic justification but need not change arithmetic semantics. The depicted graph is a declared example, not an automatically discovered dependency registry.}
730 \end{figure}
731 
732 \section{Semantic improvement and resource improvement are separate}
733 Fix named additive event types. Let $K\ge0$ be an extra preparation vector, let $s_i$ be the old-minus-new per-use vector for workload type $i$, and let $n_i$ count its uses. The net event difference is
734 \[
735 \Delta=\sum_i n_i s_i-K.
736 \]
737 A nonnegative price vector $w$ converts these events into one declared additive measure. Storage capacity, peak memory, and elapsed time need their own models unless a justified conversion is specified.
738 
739 \begin{proposition}[Which gains survive every admitted price?]\label{r:prices}
740 The saving $w\cdot\Delta$ is nonnegative for every nonnegative price vector if and only if every coordinate of $\Delta$ is nonnegative. If prices lie in the convex hull of a finite nonempty set $W$, their minimum saving equals $\min_{w\in W}w\cdot\Delta$.
741 \end{proposition}
742 \begin{proof}
743 A componentwise nonnegative vector has nonnegative inner product with every nonnegative vector. If coordinate $j$ is negative, assigning price one only to that coordinate gives a negative result. This proves the first assertion. A point in the stated convex hull is a convex combination of its listed prices, so its saving is the same convex combination of their savings. It cannot be smaller than the minimum listed value, and a listed minimizer attains that value.
744 \end{proof}
745 \source{[SII], Proposition 25.1. No hardware performance law follows from this additive accounting identity.}
746 
747 For the source's checked weighted-search comparison, the event difference is $(1552,1552,-1868)$ in reads, rational additions, and comparisons. Equal prices give $1236$ saved units. Prices $(1,0,1)$ give a loss of $316$. Both conclusions concern the same valid controller. The main text uses this as a transparently rechecked source calculation, not as a new measured timing result.
748 
749 \section{Evidence across an adaptive sequence}
750 A procedure that searches many candidates can select a favorable error in its evaluator. The right statement must therefore condition on the information that produced the candidate, not merely repeat a marginal error bound for a candidate fixed in advance.
751 
752 \begin{proposition}[A conditional error budget for a lineage]\label{r:lineage}
753 Let $\mathcal H_{j-1}$ contain the information available before attempt $j$. Suppose the event $A_j$ of accepting a false claim satisfies
754 \[
755 \Pr(A_j\mid\mathcal H_{j-1})\le\delta_j\quad\text{almost surely},
756 \qquad\sum_{j\ge1}\delta_j\le\delta,
757 \]
758 for deterministic nonnegative $\delta_j$. Then the probability of ever accepting any false claim is at most $\delta$, even when candidates and the stopping time depend on earlier history.
759 \end{proposition}
760 \begin{proof}
761 Taking expectations gives $\Pr(A_j)\le\delta_j$. A union bound gives the result for every finite set of attempts. The finite unions increase to the event of any false acceptance, so continuity of probability gives the infinite statement. Stopping removes attempted events and cannot enlarge their union.
762 \end{proof}
763 \source{[SII], Proposition 26.1. The mathematical input is conditional validity of each actual attempt. A numerical error schedule alone does not establish that premise.}
764 
765 This proposition is not an empirical result about a population of agents. It explains what evidence would need to remain valid when an evaluator is used adaptively. Deterministic exact checks in this book are not treated as statistical samples and are not assigned confidence intervals through this formula.
766 
767 \section*{What is now available}
768 A revision can preserve its meaning, identify stale obligations, and state its resource advantage under explicit prices. None of this yet determines what several participants can know together or which authority they should exercise. The next chapter keeps information sharing and institutional permissions separate while applying the same preservation discipline.
769 
770 \chapter{Shared work and maintained obligations}\label{ch:shared}
771 \question{Joint information can support a task without creating a single decision maker.}
772 One agent may have a display record and another a calibration record. Neither need know the physical target bit alone. Together their records can determine it. This is an informational relation before it is any claim about collective agency.
773 
774 \section{What several accessible records can reconstruct}
775 Let $V$ be a finite-dimensional vector space over a field. Participant $i$ has a linear record $A_i v$. Stack the records into $Av=(A_1v,\ldots,A_mv)$, and let $Qv$ be the protected linear target.
776 
777 \begin{proposition}[Target-relative joint reconstruction]\label{r:reconstruction}
778 There is a linear decoder $D$ with $Q=DA$ if and only if $\ker A\subseteq\ker Q$. Full-state reconstruction is possible exactly when $A$ is injective. The intersection identity $\ker A=\bigcap_i\ker A_i$ determines which ambiguities sharing removes.
779 \end{proposition}
780 \begin{proof}
781 If $Q=DA$, a vector annihilated by $A$ is also annihilated by $Q$. Conversely, define $D(Av)=Qv$ on $\im A$. If $Av=Aw$, then $v-w\in\ker A\subseteq\ker Q$, so this definition is independent of the representative. It is linear and extends to the full record space by extending a basis. For $Q=I_V$ the kernel condition is injectivity. A stacked record vanishes exactly when each component record vanishes, giving the intersection identity.
782 \end{proof}
783 \source{Target-relative specialization of the reconstruction and factorization machinery in Sufficient Resolution [SR] and Stratified Relational Workspace Theory [SRWT]. The proof here does not import their complete noise, dynamics, or identity theories.}
784 
785 Over $\mathbb F_2$, Agent A observes $A_A(b,s)=b+s$ and Agent B observes $A_B(b,s)=s$. The joint matrix is invertible. Either agent alone lacks a direction needed to recover $b$. The nuisance bit may remain unknown because the target map ignores it.
786 
787 The theorem concerns accessible records. It does not send them. A communication protocol, truthful interpretation, permitted disclosure, and the recipient's executable decoder remain separate requirements. Chapter~\ref{ch:decision} states the corresponding fixed-recipient criterion.
788 
789 \section{Permissions are part of an operational state}
790 Now let a finite institutional state $x$ have a protected label $\ell(x)$, an enabled-action set $D(x)$ within a fixed finite alphabet, and a deterministic successor $F(x,a)$ for enabled actions. Labels may include resource balances, outstanding obligations, and offices, but need not retain every historical byte.
791 
792 \begin{theorem}[A quotient that preserves legal operations]\label{r:governance}
793 For a surjection $\pi:X\to Z$, quotient labels, enabled sets, and successors satisfying
794 \[
795 \ell=\bar\ell\pi,\qquad D=\bar D\pi,\qquad
796 \pi F(x,a)=\bar F(\pi x,a)
797 \]
798 exist exactly when equal fibres have equal labels, equal enabled sets, and equal projected successors for every enabled action. The quotient labels, enabled sets, and successors on enabled actions are unique. They preserve every legal finite action and label sequence. Values assigned by a totalized implementation to disabled actions are outside this uniqueness statement.
799 \end{theorem}
800 \begin{proof}
801 Factoring each quantity proves necessity. For sufficiency choose a representative of each fibre to define its label, enabled set, and successor. The three equalities make those definitions independent of the representative. Surjectivity gives uniqueness. Equal enabled sets admit the same first action, and successor equality preserves membership in one fibre. Induction on the sequence length preserves legality and all labels.
802 \end{proof}
803 \source{[MS], ``Exact governance quotient.'' This extends the deterministic behavioral construction by explicitly protecting action availability. It does not derive moral or external legal authority from the state description.}
804 
805 A summary that preserves only the next sensor response can merge states in which a repair is authorized with states in which it is forbidden. It may remain a good predictor while becoming an invalid action interface. The necessary correction is to preserve the enabled-set distinction, not merely to attach a reassuring name to the old code.
806 
807 \section{Continuing should not erase the ability to finish}
808 Use a finite \emph{observed} configuration space $Z$. Under partial observation, the configurations would instead have to be justified public possibility states. At $z$ there are finite catalogues of running actions and ending actions, each with a nonempty successor set. A declared safe set is $S$, and an ending target is $G\subseteq S$. A safe hold action is available at $G$.
809 
810 A stop command is assumed authentic and observable before the next action is selected. Its delivery and authentication are premises, not consequences of the following fixed-point calculation. Define
811 \begin{align*}
812 T_0&=G,\\
813 T_{k+1}&=T_k\cup\{z\in S:\exists a\in A_{\rm end}(z),\ \operatorname{Post}(z,a)\subseteq T_k\}.
814 \end{align*}
815 Let $T_*$ be the stable set. Then define
816 \[
817 L_0=T_*,\qquad
818 L_{k+1}=\{z\in L_k:\exists a\in A_{\rm run}(z),\ \operatorname{Post}(z,a)\subseteq L_k\},
819 \]
820 and let $L_*$ be its stable value. Both sequences stabilize because $Z$ is finite.
821 
822 \begin{theorem}[Safe continuation that retains an ending strategy]\label{r:ending}
823 A starting configuration belongs to $L_*$ exactly when one policy can run safely indefinitely without a stop command and, after a stop command at any decision epoch, reach $G$ on every possible successor path using only the admitted ending actions. Before the command a policy preserving $L_*$ suffices. After the command it can reach $G$ within the first-entry rank of the current state in the $T_k$ sequence.
824 \end{theorem}
825 \begin{proof}
826 Induction shows that membership in $T_k$ is equivalent to an ending-only policy reaching $G$ within $k$ transitions while staying safe. The chosen action moves every successor to a smaller rank. Outside $T_*$, every ending action has a successor outside $T_*$ or outside safety. Choosing such a successor at every step defeats any purported surely safe ending. Thus $T_*$ is exactly the sure-ending region.
827 
828 At $L_*$ a running action keeps every successor inside $L_*$. Repeatedly using such actions is safe and retains membership in $T_*$. A command can therefore switch to the decreasing-rank ending policy at any epoch.
829 
830 Conversely, if a policy has the stated guarantee, every pre-command reachable configuration must admit an ending immediately and hence lie in $T_*$. For any finite number of further running steps, it must keep all paths in that set. Induction in the decreasing construction places the initial state in every $L_k$, hence in $L_*$. No action is chosen after secretly observing its successor.
831 \end{proof}
832 \source{Fully observed finite specialization of [MS], ``Continued operation with an available authorized ending.'' The more general public-possibility construction is not silently assumed in this version.}
833 
834 \begin{counterexample}[Safe inactivity without an ending]\label{ce:ending}
835 A state $z$ has a safe idle self-loop and no ending action reaching $G$. It is safe forever but outside $T_*$. In a second state $u$, an ending is available, while the only running action spends its reserved resource and moves to $z$. Then $u$ belongs to $T_*$ but not $L_*$. Being able to stop now does not establish that ordinary operation preserves that ability.
836 \end{counterexample}
837 
838 These results do not establish society formation, strategic compliance, or a just constitution. They establish information, action, and continuation properties of a specified finite institution. Their place in this finite reasoning chain follows from the preceding account of accessible evidence, common artifacts, feasible controllers, and dependency-preserving revision.
839 
840 \chapter{One continuous chain, with no hidden promotion}\label{ch:close}
841 The sensor story can now be followed without changing the meaning of a record midway through the argument.
842 
843 Begin with eight candidate worlds $(b,s,n)$. The agent's initial display $y$ determines its two-state predictive class under flips, but not the physical target bit. The first chapter proves both claims. The second gives the operator on the retained class and the coordinate map that becomes usable after calibration. Neither requires the nuisance bit.
844 
845 When display and calibration observations arrive, candidate sets are filtered. The third chapter proves why the joint association must be retained, and why sixteen occupancy states suffice for the exact partition-evidence contract. Under a separately declared noisy calibration, four probability masses replace the occupancy bits. The same numerical posterior cannot be inferred from separate marginals. The correction argument requires a joint report/next-state law, not only correct separate marginals. Its finite refinement makes the required distinctions explicit, and its history bound states the separate price of conditioning on a rare report.
846 
847 The fourth chapter places that posterior and any response approximation under one loss function. It also specifies what a recipient can decode from a message and its prior record. The fifth asks whether the sender can acquire the missing observation and transmit a successful artifact within a single online and stored-controller budget. The complete tree is counted even if an execution visits only one path. A separate noisy-calibration calculation then uses the exact same retained belief to select a finite expected-cost inquiry. Uniform whole-history error supports a quantitative policy comparison, but not an automatic hard-budget or zero-risk guarantee.
848 
849 The sixth chapter then changes the discovery procedure rather than the hidden world. Checked equations can remove equivalent candidates while preserving every teacher proposal and counterexample. A separately justified capacity rule can stop reading an impossible diagnostic root. Neither step invents the primitive grammar, the teacher, or the theorem used to authorize pruning.
850 
851 The seventh chapter binds those uses to their premises. Adding a universal repair changes the required diagnostic distinctions. The old lower bound becomes inapplicable. Arithmetic identities can remain applicable. A fresh cost comparison may find a saving or a loss. The eighth chapter finally combines different participants' records and asks what actions they are entitled to perform under their declared institutional state. Safe indefinite operation and preservation of an authorized ending are checked separately.
852 
853 \section{A worked end-to-end record}
854 Take the actual illustrative world $(b,s,n)=(0,1,1)$. The complete protocol begins with all eight worlds possible:
855 \begin{center}\begin{tabular}{p{0.25\linewidth}p{0.27\linewidth}p{0.35\linewidth}}\toprule
856 Event & Remaining worlds & What is justified\\\midrule
857 Before observation & All eight & No physical target identified.\\
858 Display $y=1$ & Four worlds & Predict every later display flip.\\
859 Calibration $s=1$ & Two worlds differing only in $n$ & Physical target $b=0$.\\
860 Send $y$ to a recipient holding $s$ & Same two worlds & Recipient computes $b=0$ through its fixed XOR decoder.\\
861 Commit the authorized target action & As declared by its effect & One action justified across the current support.\\
862 Record the fulfilled obligation & Includes the action's receipt & Continuation or ending can refer to the actual completed act.\\\bottomrule\end{tabular}\end{center}
863 
864 The witness does not claim to have discovered its sensor semantics. Its exact checking confirms the stated scenario. Another physical process requires its own evidence. A failed receipt, an untrusted calibration, or an altered action effect changes the guarantee rather than being averaged away as a small numerical error.
865 
866 \section{Why the core is narrower than the archive}
867 This book does not append the old Neuralese experimental history, proposed PRISM architecture, full SRIC lineage, or every formal guide. Their presence would make the reader repeatedly switch between a proved conditional statement, a proposed mechanism, a historical execution, and an implementation plan. Those are useful source objects, but they are not one continuous proof.
868 
869 Selected source results are restated and proved where they carry the argument. Selected stochastic-value arguments from AVOC enter through complete proofs and explicitly matched finite models. Several resulting statements have source-facing counterparts in the archived Machine Theory development. The full AVOC implementation and the specialist Certified Bayesian Inference construction remain outside this selection. The correspondence appendix records the difference between those archived counterparts and the present editorial work.
870 
871 Nor is a source excluded merely because it contains open questions. Its proved results can be considered individually. A claim enters when its exact form, dependencies, and evidence have been reviewed at the level promised for this edition. This is a stricter and more useful rule than treating every page of a final-named document as equally checked.
872 
873 \section{The result of the compilation}
874 The core establishes a connected conditional account of accessible state, meaningful operations, corrective memory, usable explanations, bounded investigations, justified search changes, and maintained obligations. The arguments share several elementary constructions, but each use preserves its distinct type and hypotheses.
875 
876 No theorem here turns a semantic interface into a trained neural model, a finite investigation into general intelligence, a shared record into a collective subject, or an invariant into legitimate external authority. The mathematical contribution is the explicit chain and the failures that break it. Those failures can be investigated without changing the standard of proof or requiring a large implementation campaign.
877 

Back to source controls

Back to Machine Native Reasoning: wider continuation