Certified Task-Conditioned Active Observability
Abstract
Before an autonomous agent can act upon an unobservable physical system, it must resolve a fundamental operational dilemma: which latent distinctions actually govern the downstream task, how many active interventions are necessary to certify them, and when must the system abstain rather than risk catastrophic misclassification? In classical control and physical estimation, observability is posed as an unconditioned binary predicate: either the microscopic state can be uniquely reconstructed, or it is unobservable. In deployed environments, however, passive observations cannot break latent degeneracies without active perturbation, full microscopic inversion is prohibitively expensive, and attempting to distinguish task-irrelevant degrees of freedom squanders bounded interaction budgets. We formulate task-conditioned active observability complexity, determining the minimum worst-case expected interaction cost required to identify the task-relevant current state under explicit error and safe abstention guarantees. We prove that task-predictive equivalence induces the unique minimal sufficient quotient , leaving active observability complexity strictly invariant while eliminating superfluous physical distinctions. In deterministic regimes, this complexity is characterized exactly by an optimal adaptive distinguishing tree and a Bellman recursion; in noisy regimes, it obeys a stopped-transcript relative-entropy lower bound alongside adaptive martingale certificates that compose without independence assumptions. We instantiate the theory in a prospective certified observer that operationalizes staged recovery: a nominal verifier defers candidate compilation, triggering active probing only upon evidence, while a history-measurable score shell prunes hypotheses without sacrificing risk bounds. Stress audits across high-dimensional physical systems and thousands of operational trials demonstrate that the observer reliably recovers states while slashing sensor reads and model steps, achieving zero false acceptances and safely abstaining under ambiguity. The framework bridges discovered physical ontologies and certified real-time control, transforming active state recovery from unconditioned microscopic inversion into provably minimal physical inquiry.
Keywords:
Active Observability, State Estimation, Sequential Decision Making, Representation Learning1 Introduction
In classical control and physical estimation, observability is posed as an all-or-nothing predicate: either the microscopic state can be uniquely reconstructed, or it is unobservable. In practical deployment, however, this classical formulation overlooks critical operational constraints. Passive observations often cannot break latent degeneracies without physical perturbation; fully inverting microscopic state spaces is computationally and energetically prohibitive; and downstream tasks typically require distinguishing task-relevant operational regimes rather than resolving superfluous physical degrees of freedom. Conversely, an observer that prematurely discards candidate hypotheses risks catastrophic misclassification. Bridging this gap demands an operational theory of observability that explicitly balances active interaction costs, hypothesis memory, and certified decision risk.
We address this challenge by formalizing task-conditioned active observability: given a physical system with candidate hypotheses, how much active physical interaction is necessary and sufficient to identify the task-relevant state under certified error and safe abstention guarantees? In this setting, an autonomous observer adaptively selects probe actions, updates belief over candidate hypotheses, and terminates either with a certified task decision or with a provably safe abstention when ambiguity cannot be resolved within budget.
Our first contribution formalizes task-conditioned active observability complexity, separating representation complexity (which candidate distinctions govern downstream task outcomes) from interaction complexity (the minimal cost of adaptive experiments required to separate them). We prove that task-predictive equivalence induces the unique minimal sufficient quotient , eliminating task-irrelevant distinctions while leaving active observability complexity strictly invariant. In deterministic settings, this complexity is characterized exactly by an optimal adaptive distinguishing tree via a Bellman recursion; in stochastic regimes, it satisfies a stopped-transcript relative-entropy lower bound alongside adaptive martingale certificates that compose constructively under arbitrary filtration histories.
Our second contribution is an operational observer architecture that realizes this theoretical separation in practice. The observer decouples tracking from recovery by verifying a lightweight nominal state first, compiling the broader fallback bank only when accumulated evidence warrants, and certifying state transitions on independent forward measurements. To scale recovery, a history-measurable score-shell rule compresses the candidate bank while provably preserving conditional safety guarantees, ensuring unresolvable ambiguities map to certified abstention rather than misclassification. Furthermore, conformal calibration of the shell rank controls marginal coverage, while an admissible lower-bound certificate enables direct, closed-form candidate compilation.
Our third contribution establishes an optimality principle for physical resource scheduling. We prove that when candidate compilation produces no useful intermediate outputs during sensing, any interleaved scheduling between sensor reads and partial compilation is pathwise weakly dominated by an atomic fallback policy. This result establishes that compilation progress does not act as an intrinsic state variable of the active observability problem, providing a formal justification for executing fallback compilation atomically upon certified trigger.
We validate the theoretical framework across high-dimensional physical systems and extensive operational trials. The experiments demonstrate that the staged observer reliably recovers task-relevant states while substantially reducing sensor queries and model computation, achieving zero false acceptances and safely abstaining under ambiguity. Together, these results provide an end-to-end framework for certified active state recovery, transforming classical observability from unconditioned microscopic inversion into provably minimal physical inquiry.
2 Problem formulation
2.1 Finite controlled hypothesis model
A completed operation history produces a finite candidate set . A hypothesis contains a candidate operation endpoint and its known future controlled transition and observation model. At future time , the observer selects , receives , and updates the propagated state of each candidate. The action rule, stopping time , and output are nonanticipating. Policies are deterministic measurable maps of the observed history; there is no exogenous randomization, and all probability comes from the observation process. The output is either a label or abstention .
A fixed task map
| (1) |
specifies which distinctions matter. It can request the exact operation endpoint, an active/inactive label, or any other fixed task-relevant quotient. When the desired report is a current state, the operation-end label can be propagated through the executed confirmation actions before output.
Let be the physical interaction cost of action . A policy is -valid if, uniformly for all ,
| (2) | ||||
| (3) |
The worst-case task-conditioned active observability complexity is
| (4) |
The value is if no valid policy exists. Computation is recorded separately in the empirical study; it can also be folded into a generalized cost when it is serial and action-independent.
2.2 Task-predictive equivalence
Let be the family of finite deterministic nonanticipating experimental policies. For , write for the induced finite transcript law.
Definition 2.1 (Task-predictive equivalence).
Two hypotheses are equivalent, written , when
| (5) |
For standard controlled Markov kernels, equality can equivalently be checked on all finite open-loop action words; adaptive transcript equality then follows by conditioning on the common history and induction.
Theorem 2.2 (Minimal predictive quotient).
Let . Then:
- 1.
every representation from which both and all future experimental laws can be recovered must refine ;
- 2.
is sufficient;
- 3.
for every ,
(6)
Thus is the unique minimal sufficient representation up to relabeling.
The theorem isolates the only candidate distinctions that can affect either the answer or any future evidence. It also justifies quotienting before optimizing an active observer.
Corollary 2.3 (Identifiability obstruction).
Suppose two hypotheses have different task labels but identical transcript laws under every policy. If , then no -valid observer exists.
3 Active observability theory
3.1 Exact deterministic characterization
Assume deterministic transitions and observations. An information configuration is a finite set of pairs , where is the fixed task label of an initial hypothesis and is its current propagated state. Duplicate pairs are removed. A configuration is pure if all pairs have the same label. For action and observation , let be the propagated subset that produces .
A task-separating experiment tree places actions at internal nodes, observations on edges, and label-pure configurations at leaves. Define its minimax cost by
| (7) |
with when no finite separating tree exists.
Theorem 3.1 (Deterministic closure).
For a deterministic noiseless controlled system,
| (8) |
Equivalently, is the least extended nonnegative solution of
| (9) |
and otherwise
| (10) |
The equality is exact, not asymptotic: every exact policy unfolds into a separating tree, and every such tree is an executable exact policy. Combined with theorem 2.2, it gives a two-step characterization: first quotient the representation, then solve the minimum distinguishing-tree problem.
3.2 Noisy information lower bound
Let denote the stopped transcript law, including the decision, under policy . Define binary relative entropy
| (11) |
Theorem 3.2 (Pairwise stopped-transcript necessity).
Assume . For every -valid policy and every pair with ,
| (12) |
For controlled Markov observations with kernel , the adaptive chain rule yields
| (13) | ||||
Let be the largest one-step directed KL per unit cost over paired states reachable under a common action history. Then
| (14) | ||||
A zero information rate for any task-inequivalent pair makes the complexity infinite.
3.3 Certified-tree upper bound
A node-level certified test may itself be sequential. At node with candidate configuration , it has a correct branch map and, conditional on every possible entry history, obeys
| (15) | ||||
| (16) |
with conditional expected cost at most . A certified distinguishing tree has task-pure leaves and stops globally if any node abstains.
Theorem 3.3 (Adaptive certified composition).
Executing a certified distinguishing tree gives
| (17) | ||||
| (18) |
and worst-case expected cost at most
| (19) |
No independence between node tests is required.
Corollary 3.4 (Active-observability sandwich).
Let denote the pairwise information lower bound in equation 14, and let be the least path cost of a certified tree satisfying the pathwise risk budgets. Then
| (20) |
In the deterministic noiseless specialization, the certified-tree optimum reduces to the exact quantity in
crefthm:deterministic.
4 Certified observer construction
4.1 Nominal-first staged confirmation
Rather than compiling the full hypothesis space upfront, the observer maintains a nominal candidate for expected tracking while deferring compilation of the generic fallback candidate bank , where the unified candidate set is . The observer first interrogates on a fresh observation stream under risk budget . If confirmed, is accepted immediately at minimal query and compute cost; otherwise, atomic fallback compiles and verifies on subsequent independent measurements under risk budget . Partitioning the overall risk budget as guarantees conditional safety via theorem 3.3, with candidate set instantiation statistically decoupled from certification.
4.2 Readwise evidence-triggered fallback
In latency-sensitive deployments, waiting for exhaustive nominal rejection can incur unnecessary physical query cost. The observer incorporates an evidence-triggered sequential rule that monitors the running verification transcript readwise. When intermediate observations yield strong discordant evidence against , the system preemptively triggers atomic fallback without exhausting the nominal testing budget. Because the trigger functions as an adaptive stopping rule while fallback certification operates on disjoint subsequent data, this early switching modulates interaction cost without compromising conditional safety guarantees. The parameter governs the interaction-versus-compilation tradeoff in algorithm 1, evaluated across frozen values alongside eager and staged baselines.
4.3 Score-shell compression and exact compilation
Each endpoint candidate receives the lexicographic score
| (21) |
Candidates with the same score form a shell. The compressed representation keeps the first distinct shells after endpoint-wise minimization, plus the nominal endpoint.
Theorem 4.1 (History-measurable sub-bank safety).
Let be the completed operation history and let be any finite history-measurable candidate bank fixed before a fresh confirmation stream. If the verifier has conditional family-wise false-accept probability at most for every fixed bank, then
| (22) |
Candidate omission can reduce coverage, but it cannot increase the allocated false-accept bound.
Calibration is performed in exchangeable blocks that each contain all 20 active strata. If is the maximum true-shell rank in block and , then
| (23) |
The inequality follows because failure requires the final block to be a unique strict maximum. With , the frozen choice has next-block marginal coverage at least .
Exact direct compilation.
To avoid enumerating the full bank before discarding later shells, every partial search node is assigned an admissible lexicographic lower bound on the score of all of its completions. Once eight distinct endpoint-best shells have been found with eighth threshold , the search terminates directly when
| (24) |
When this certificate fails, the compiler falls back to exact exhaustive enumeration. Hence the hybrid compiler returns the identical endpoint-score candidate map as exhaustive filtering on every input while bypassing unviable branches.
Theorem 4.2 (Atomic fallback dominance).
Assume the compilation target is fixed before confirmation, compilation has no usable intermediate output, compute produces no plant observation, read and compute costs add serially, and there is no deadline, discount, or reward for early completion. Every policy that interleaves reads and partial compilation is pathwise weakly dominated by a policy that performs no compilation until an observation stopping time and then either never compiles or completes the entire fallback atomically.
The proof moves all useful compile microsteps to the first point at which the completed bank is used and deletes all unused work. The read sequence, decision, and useful computation are unchanged; therefore, compilation progress need not appear as an additional state variable in the active-observability formulation.
5 Empirical evaluation
5.1 Experimental setup and evaluation metrics
We evaluate the certified active observability framework across three complementary benchmark domains:
Benchmark domains.
First, a prospective closed-loop control testbed evaluates sequential tracking and fallback policies across two 24-bit controlled Boolean models with 96 public commands. Each operational episode executes 192 commanded actions under hidden command substitutions and sensor flips. The benchmark spans 72 prospective tasks across six families, consisting of 20 active and 52 inactive operations. To ensure strict paired comparisons without multiplying physical risk, every policy replays identical prospective observation streams of length at most 600. Second, a large-scale confirmatory benchmark evaluates candidate compression and compiler exactness over 100 calibration blocks and 100 independent evaluation blocks, comprising 2,000 total operations across the 20 active strata. All hyperparameters are frozen prior to evaluation, with , a probe target of 16 shells, and an evaluation budget of 95,000 queries. Third, a synthetic control suite evaluates theoretical invariants across 600 random deterministic Mealy automata and 5,000 adaptive stochastic policies.
Evaluation dimensions.
Performance is audited across four operational axes: (i) physical interaction cost, measured by future sensor reads and commanded actions; (ii) computational complexity, quantified by candidate-compilation evaluations and verifier model steps; (iii) certification reliability, tracked via correct confirmations, safe abstentions, and empirical false acceptances; and (iv) compiler exactness, verified by state-by-state equality of pruned versus full candidate maps. Candidate coverage and conditional false-accept safety are audited and reported separately.
5.2 Closed-loop interaction and computation trade-offs
All six evaluated controller policies correctly confirm all 72 prospective tasks without producing unknown outcomes. Table 1 and Figure 1 summarize the aggregate interaction and computational trade-offs. Eager compilation incurs severe computational waste by executing 8.62 million model steps to compile candidates unconditionally across all 52 inactive tasks. In contrast, nominal-first staging exploits expected physical regularity, reducing model computation more than five-fold to 1.65 million steps while lowering mean future reads from 104.25 to 88.76.
| Policy | Mean reads | Model steps (M) | Compilations | Correct |
|---|---|---|---|---|
| Eager | 104.250 | 8.6213 | 72 | 72/72 |
| Staged | 88.764 | 1.6532 | 20 | 72/72 |
| Readwise | 86.375 | 1.9802 | 47 | 72/72 |
| Readwise | 86.222 | 1.6862 | 36 | 72/72 |
| Readwise | 87.431 | 1.6527 | 21 | 72/72 |
| Readwise | 87.708 | 1.6505 | 20 | 72/72 |
Readwise evidence-triggered switching further optimizes this Pareto frontier. Rather than waiting to exhaust the nominal testing budget, the readwise rule monitors accumulated discordance and triggers fallback early. Conservative switching with compiles the exact same 20 active tasks as formal staging while trimming mean future reads from 88.76 to 87.71. More aggressive switching with achieves the lowest physical interaction at 86.22 reads, though incurring 16 unnecessary compilations on inactive tasks.
| Outcome | Policy | Episodes | Mean reads | Compilations |
|---|---|---|---|---|
| Active | Staged | 20 | 104.600 | 20 |
| Active | Readwise | 20 | 100.800 | 20 |
| Inactive | Staged | 52 | 82.673 | 0 |
| Inactive | Readwise | 52 | 82.673 | 0 |
Table 2 reveals the mechanistic origin of these savings by stratifying tasks across operational outcomes. The domain naturally bifurcates into two regimes: (i) inactive operations, comprising 52 tasks or 72.2% of the domain, where the nominal hypothesis is confirmed immediately using only 82.67 future reads and zero candidate compilations; and (ii) active operations, comprising 20 tasks or 27.8% of the domain, where conservative readwise triggering with reduces average reads from 104.60 to 100.80. Crucially, the median fallback trigger shifts from 9 reads under formal rejection down to 4 reads under readwise monitoring. Evidence-triggered switching thus protects nominal-path throughput without compromising worst-case safety auditing.
5.3 Representation compression and exact compilation
Candidate compression and coverage calibration.
Restricting the fallback bank to the top- score shells eliminates 85.51% of candidate states, dropping from 7,520,508 to 1,090,024, and 85.57% of verifier model steps, dropping from 140,052,481 to 20,210,639, while reducing physical reads by 2.19% through earlier verification (Table 3, Figure 2). Across 2,000 independent operations, the true endpoint is certified in 1,999 instances, with the single omission resulting in a safe abstention, thereby achieving zero false acceptances and zero unknown outcomes. This confirms theorem 4.1: representation pruning governs empirical coverage as a calibrated availability property while strictly preserving conditional safety.
| Metric | Full bank | Top-8 shells | Change |
| Candidate states | 7,520,508 | 1,090,024 | |
| Verifier model steps | 140,052,481 | 20,210,639 | |
| Physical reads | 203,135 | 198,683 | |
| Correct confirmations | 2,000 | 1,999 | |
| Safe rejections | 0 | 1 | |
| Wrong acceptances | 0 | 0 | 0 |
Compiler exactness and search truncation.
Direct score-shell compilation reproduces the candidate-score map of full exhaustive enumeration with 100% state-by-state identity across all 2,000 operations. When the lexicographic bound in (24) certifies that unexpanded branches cannot reach the eighth score shell, search terminates early. Direct certificates are established in 38 operations, reducing compilation evaluations by 28.19% on those instances. Over the full 2,000-operation benchmark, total evaluations fall from 10,033,791,134 to 9,929,092,066, representing a net reduction of 104,699,068 evaluations (1.04%) that fully absorbs the 91,390,153 evaluations expended on uncertified exploratory probes in the remaining 962 operations. Exact fallback boundaries ensure that branch pruning introduces zero approximation error into state verification.
Theoretical invariants on synthetic systems.
Across 600 random Mealy automata and 5,000 adaptive noisy policies, the structural predictions of section 3 hold uniformly. Task-predictive quotienting preserves exact distinguishing depth in all 600 deterministic systems while reducing state representations in 75. In stochastic regimes, stopped-transcript relative entropy strictly dominates the divergence of every induced binary decision event, and the explicit information lower bound holds across all 461 nonvacuous risk-constrained instances.
6 Related work
Classical linear and nonlinear observability characterize whether internal state can be reconstructed from input-output behavior (Kalman, 1960; Hermann and Krener, 1977). Active state-estimation work chooses inputs to improve estimation quality (Hu and Ersson, 2004). Our formulation differs by making task equivalence, finite candidate representations, interaction cost, error, and abstention explicit, and by seeking an exact finite-system characterization rather than a rank condition or estimator design.
Sequential experimental design and controlled sensing study how actions should be chosen to discriminate hypotheses under sample or decision-risk constraints (Chernoff, 1959; Wald, 1947; Naghshvar and Javidi, 2013; Nitinawarat et al., 2013). The KL lower bound in theorem 3.2 follows this information-theoretic lineage. Our emphasis is the interface between evolving controlled states, task-conditioned quotients, certified node tests, candidate compilation, and safe abstention.
Finite-state-machine testing studies state identification, distinguishing sequences, and conformance experiments (Moore, 1956; Chow, 1978; Lee and Yannakakis, 1994; van den Bos and Vaandrager, 2019). The deterministic tree in theorem 3.1 is closely related to adaptive distinguishing experiments, but here it is embedded in a risk-controlled noisy observer and coupled to history-dependent candidate representations.
While automata learning reconstructs unknown state machines from query responses (Angluin, 1987; Vaandrager, 2017), our setting optimizes state recovery within a known dynamical representation.
Interface with physical coordinate discovery and ontology learning.
The active observability framework developed here addresses a complementary operational challenge to the physical representation learning program established in Papers 1–3 of this series (Zhang and Xu, 2026b; Zhang and Xu, 2026a; Zhang and Xu, 2026c). In physical representation learning, an autonomous agent seeks to discover the continuous coordinate geometry, Lie group gauge symmetries, and thermodynamic contact structures of an unknown physical system through experimental scaling, contact, and reservoir interventions. Once this continuous physical ontology is discovered and frozen, practical execution in autonomous facilities, such as self-driving synthesis laboratories or battery management platforms, requires monitoring the operational regime in real time.
In such deployed environments, full continuous state deconvolution is often unobservable or prohibitively expensive under bounded instrumentation. Task-conditioned active observability bridges this divide: by quotienting the state space modulo the target control task into , the agent avoids wasting physical resources to resolve task-irrelevant physical fluctuations, while retaining certified mathematical guarantees against erroneous state assertions.
7 Limitations
The theoretical guarantees apply to finite controlled models with known representations under deterministic policies. The formulation focuses on certified tracking within verified dynamics and does not address unanchored cold-start identification or unmodeled process faults. Extending the guarantees from marginal next-block coverage to distribution-free conditional coverage across arbitrary covariates remains an open theoretical direction.
Our atomicity analysis considers sequential evaluation; extending the framework to parallel execution, execution deadlines, or incremental candidate generation presents a practical direction for deployment.
8 Conclusion
Task-conditioned active observability separates a system’s minimal predictive representation from the interaction needed to identify its current task-relevant state. The predictive quotient is uniquely minimal and leaves the complexity unchanged. Deterministic systems admit an exact adaptive-tree characterization; noisy systems admit complementary information lower bounds and certified-tree upper bounds. The prospective observer demonstrates how these ideas organize practical choices: defer expensive candidates, trigger fallback from evidence, use fresh confirmation data after selection, compress representations without conflating safety and coverage, and stop expanding the controller when partial computation has no decision value.
Within a fixed representation, tightening the gap between the noisy information lower bound and executable certified trees remains the primary open direction.
References
- Learning regular sets from queries and counterexamples. Information and Computation 75 (2), pp. 87–106. External Links: Document Cited by: §6.
- Sequential design of experiments. The Annals of Mathematical Statistics 30 (3), pp. 755–770. External Links: Document Cited by: §6.
- Testing software design modeled by finite-state machines. IEEE Transactions on Software Engineering SE-4 (3), pp. 178–187. External Links: Document Cited by: §6.
- Nonlinear controllability and observability. IEEE Transactions on Automatic Control 22 (5), pp. 728–740. External Links: Document Cited by: §6.
- Active state estimation of nonlinear systems. Automatica 40 (12), pp. 2075–2082. External Links: Document Cited by: §6.
- A new approach to linear filtering and prediction problems. Journal of Basic Engineering 82 (1), pp. 35–45. External Links: Document Cited by: §6.
- Testing finite-state machines: state identification and verification. IEEE Transactions on Computers 43 (3), pp. 306–320. External Links: Document Cited by: §6.
- Gedanken-experiments on sequential machines. In Automata Studies, C. E. Shannon and J. McCarthy (Eds.), Annals of Mathematics Studies, Vol. 34, pp. 129–153. Cited by: §6.
- Active sequential hypothesis testing. The Annals of Statistics 41 (6), pp. 2703–2738. External Links: Document Cited by: §6.
- Controlled sensing for multihypothesis testing. IEEE Transactions on Automatic Control 58 (10), pp. 2451–2464. External Links: Document Cited by: §6.
- Model learning. Communications of the ACM 60 (2), pp. 86–95. External Links: Document Cited by: §6.
- State identification for labeled transition systems with inputs and outputs. arXiv preprint arXiv:1907.11034. External Links: 1907.11034 Cited by: §6.
- Sequential analysis. John Wiley and Sons, New York. Cited by: §6.
- Blind thermodynamic ontology discovery from anonymous experiments. arXiv preprint. Cited by: §6.
- Discovering physical representation languages: metric-free axiomatics and topological ontology identification. arXiv preprint. Cited by: §6.
- Parasitic-free three-frequency laws for positive relaxation ports. arXiv preprint. Cited by: §6.
Appendix A Proofs
A.1 Proof of the minimal predictive quotient theorem
Suppose a representation is sufficient to recover both and the transcript law of every future experiment. If , every decoded quantity agrees, hence and for every . Therefore and every sufficient representation refines .
Conversely, one task label and one family of future experimental laws are well-defined on every equivalence class, so is sufficient. Any policy on induces identical transcript, cost, error, and abstention laws for all members of a class and therefore descends to . Every policy on lifts to . Taking the same infimum and supremum proves complexity invariance.
For corollary 2.3, let be the event that the observer outputs . Under , validity requires . Under , the same output is wrong, so . Identical transcript laws imply identical output laws, contradicting .
A.2 Proof of the deterministic closure theorem
Fix any exact policy. By the policy convention in section 2, its decisions are deterministic functions of the observation history, so unfolding them gives an action-observation tree. At every reachable stopping leaf, all remaining candidate pairs must have the same task label; otherwise the common output would be wrong for at least one candidate. Hence the policy induces a finite task-separating tree with the same worst-case cost and cannot beat .
Conversely, execute any task-separating tree and output the unique label at the reached leaf. The policy is exact and has the tree’s worst-case path cost. Taking infima proves . Decomposing a nonterminal tree at its root gives the Bellman lower bound in equation 10; adjoining optimal child trees gives the reverse bound. Because all action costs are positive, the least extended solution assigns exactly to configurations with no finite separating tree.
A.3 Proof of the KL lower bound
Let . Under , ; under , . Data processing through the indicator gives
| (25) |
Since , binary relative entropy is increasing in its first argument and decreasing in its second over the relevant rectangle. This proves equation 12.
For the cost bound, the action-selection kernels are the same functions of the observed history under both hypotheses and cancel in the likelihood ratio. The chain rule gives equation 13. Each term is at most , hence
| (26) |
Repeat in the reverse direction and use the worst-case objective.
A.4 Proof of certified adaptive composition
A wrong terminal label implies that at least one visited node misrouted the true hypothesis. Condition on each node’s entry sigma-field. Its misrouting probability is at most for every possible entry history. The tower property and a union bound over the realized root-to-leaf path give the path sum. Maximizing over paths gives the first bound. The abstention proof is identical. Conditional expected costs add by iterated expectation, and the sum along every realized path is bounded by the largest path sum. No cross-node independence is used.
A.5 Proof of history-measurable sub-bank safety
Condition on the completed operation history . Then is a fixed finite bank. By the fixed-bank verifier guarantee,
| (27) |
Because is measurable with respect to , conditioning on both is the same as conditioning on . Candidate omission does not alter this inequality; it only removes the completeness premise needed to guarantee an acceptance.
For equation 23, exchangeability makes every block equally likely to be the unique strict maximum among block maxima. Failure occurs only when the last block is that unique maximum, whose probability is at most . Ties can only improve coverage.
A.6 Proof of atomic fallback dominance
Fix a realized read/outcome path of an arbitrary policy. If no completed bank is used, delete every compile microstep. If a completed bank is first used at some observation stopping history, move every useful compile microstep to one contiguous block immediately before that use. Compilation emits no observation, does not change the plant, and has a fixed target, so all read-dependent decisions and the completed bank remain unchanged. Additive serial cost remains the same; unused work is deleted. Applying this exchange pathwise yields a policy that never maintains partial progress and is weakly cheaper on every path.
Appendix B Additional protocol details
B.1 Staged risk accounting
The eager verifier uses false-accept budget . The staged method uses . Let be a wrong nominal acceptance and a wrong fallback acceptance. Conditional on the entire stage-1 history and on entering stage 2, the propagated bank is fixed before the fresh stage-2 stream. Therefore
| (28) |
This argument does not assume that the full or compressed bank contains truth.
B.2 Why stage-1 reads are not rescored
The decision to materialize the generic bank is a function of stage-1 data. Rescoring the newly selected bank on those same observations would use the data both for model selection and confirmation, invalidating the fixed-bank conditional guarantee unless a selective-inference correction were supplied. The protocol instead propagates the bank through the executed actions and starts a new verifier on fresh data.
B.3 Exact direct-shell certificate
At a partial compiler node, let the current score components be , and let be the remaining opportunities to reduce the two window scores. The lower bound
| (29) | ||||
is admissible and lexicographically nondecreasing along every search path. If the current endpoint-best map contains eight distinct shells and every open node has lower bound strictly larger than the eighth shell, no unseen completion can change any retained endpoint score. An arbitrary probe may propose an achievable threshold, but only the exhaustive bounded search below that threshold supplies the certificate. Failure invokes exact full enumeration.
Appendix C Additional empirical results
C.1 Parallel speculation sensitivity
A separate-worker sensitivity study compares deferred compilation, full background compilation, evidence-gated background compilation, and actual readwise switching on 72 new prospective streams. Evidence-gated background compilation uses the same trigger as readwise switching but continues the nominal verifier, spending 85 additional reads in aggregate. Full speculation provides a 0.258% wall-clock advantage at 1 ms/read and 0.085% at 10 ms/read while using 1.95 and 5.36 times as much compilation CPU, respectively; at 100 ms/read, readwise switching is faster. The measured aggregate crossing is 12.78 ms/read. This is a deployment sensitivity for the frozen compiler and traces, not a hardware-independent theorem.
C.2 Development replay
Before the independent 2,000-operation shell confirmation, the same representation is replayed on the inherited 72 controller tasks. It remains correct on 72/72, reduces fallback candidates by 62.20%, reduces model steps by 62.02%, and saves 98 physical reads. This replay is developmental; the frozen independent split is the primary evidence.