Paper deep dive
Auditing Emergent LLM-Agent Collaboration through Cooperation-Obligation Coupling
Zuyuan Zhang, Hanqing Yang, Carlee Joe-Wong, Tian Lan
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 8/1/2026, 1:03:53 AM
Summary
The paper introduces iCORE (Integrated Cooperation-Obligation REpresentation), a framework for auditing emergent LLM-agent collaboration. It addresses the 'auditability gap' by coupling observable agent interactions (cooperation graph G) with evolving work assignments (obligation graph Q) via an audit map (Π). This allows auditors to certify 'Work soundness' (justification of work assertions) and 'Agent-assignment stability' (optimal agent allocation). The authors propose iCORE-Audit, an instrumentation layer that improves trajectory quality and terminal performance in controlled and real-LLM executions.
Entities (8)
Relation Signals (8)
iCORE → comprises → Cooperation Graph
confidence 95% · It creates a unified encoding X=(G,Q,Π) integrating observable interactions as a cooperation graph G
iCORE → comprises → Obligation Graph
confidence 95% · integrating observable interactions as a cooperation graph G, evolving work and assignments as an obligation graph Q
iCORE → comprises → Audit Map
confidence 95% · and the audit map Π linking them with verifiable properties and evidence
iCORE → certifies → Work Soundness
confidence 92% · This iCORE representation enables the auditor to certify two complementary properties: Work soundness
iCORE → certifies → Agent-assignment Stability
confidence 92% · and Agent-assignment stability, which requires that no feasible alternative agent improve the declared contribution value
iCORE-Audit → isinstanceof → iCORE
confidence 90% · We operationalize iCORE through iCORE-Audit, an event-triggered layer around the host policy.
iCORE-Audit → improves → Trajectory Quality
confidence 85% · iCORE-Audit yields absolute trajectory-quality improvements of 11.5% and 26.4%
iCORE-Audit → improves → terminal-performance
confidence 85% · with corresponding absolute terminal-performance improvements of 15.1% and 31.0%
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:LLM-agent systems can solve complex tasks through dynamic self-organization and emergent cooperation. Auditing this process is essential because plausible intermediate or final outputs can conceal incomplete or unsupported work and poorly allocated responsibility, ultimately compromising response quality. While existing approaches may record messages, tool calls, provenance, or task dependencies, an auditability gap exists as they do not jointly represent what work remains, who is responsible for it, and what evidence justifies each work-state transition. We address this auditability gap by proposing \emph{Integrated Cooperation-Obligation REpresentation} (iCORE). It creates a unified encoding $X=(G,Q,\Pi)$ integrating observable interactions as a cooperation graph $G$, evolving work and assignments as an obligation graph $Q$, and the audit map $\Pi$ linking them with verifiable properties and evidence. This iCORE representation enables the auditor to certify two complementary properties: {Work soundness}, where every active decision-relevant work assertion must have a finite justification through $G$ and $\Pi$; and {Agent-assignment stability}, which requires that no feasible alternative agent improve the declared contribution value for an evaluated obligation by more than $\epsilon$. We establish local-to-global soundness and assignment-regret guarantees and a performance bound under stated conditions. iCORE is an instrumentation layer over workflows. Numerical results show that the full coupled state exactly reconstructs soundness and assignment defects in two execution modes and that, relative to passive full-state observation, iCORE-Audit yields absolute trajectory-quality improvements of $11.5\%$ and $26.4\%$ in controlled and real-LLM execution, respectively, with corresponding absolute terminal-performance improvements of $15.1\%$ and $31.0\%$.
Tags
Links
- Source: https://arxiv.org/abs/2607.27429v1
- Canonical: https://arxiv.org/abs/2607.27429v1
Trouble viewing inline? Open PDF directly →
Full Text
184,628 characters extracted from source content.
Expand or collapse full text
Auditing Emergent LLM-Agent Collaboration through Cooperation–Obligation Coupling Zuyuan Zhang1 , Hanqing Yang2 , Carlee Joe-Wong2, Tian Lan1 Abstract LLM-agent systems can solve complex tasks through dynamic self-organization and emergent cooperation. Auditing this process is essential because plausible intermediate or final outputs can conceal incomplete or unsupported work and poorly allocated responsibility, ultimately compromising response quality. While existing approaches may record messages, tool calls, provenance, or task dependencies, an auditability gap exists as they do not jointly represent what work remains, who is responsible for it, and what evidence justifies each work-state transition. We address this auditability gap by proposing Integrated Cooperation-Obligation REpresentation (iCORE). It creates a unified encoding X=(G,Q,Π)X=(G,Q, ) integrating observable interactions as a cooperation graph G, evolving work and assignments as an obligation graph Q, and the audit map Π linking them with verifiable properties and evidence. This iCORE representation enables the auditor to certify two complementary properties: Work soundness, where every active decision-relevant work assertion must have a finite justification through G and Π ; and Agent-assignment stability, which requires that no feasible alternative agent improve the declared contribution value for an evaluated obligation by more than ϵε. We establish local-to-global soundness and assignment-regret guarantees and a performance bound under stated conditions. iCORE is an instrumentation layer over workflows. Numerical results show that the full coupled state exactly reconstructs soundness and assignment defects in two execution modes and that, relative to passive full-state observation, iCORE-Audit yields absolute trajectory-quality improvements of 11.5%11.5\% and 26.4%26.4\% in controlled and real-LLM execution, respectively, with corresponding absolute terminal-performance improvements of 15.1%15.1\% and 31.0%31.0\%. 1 Introduction Large language models are increasingly deployed as cooperative systems rather than isolated agents (Wang et al. 2024; Guo et al. 2024). Conversation-oriented frameworks support dynamic role coordination and intermediate-work exchange (Wu et al. 2023; Li et al. 2023; Yang et al. 2026), while software-oriented systems organize agents around shared artifacts and staged responsibilities (Hong et al. 2024; Qian et al. 2024). Tool-using agents adapt later actions to external observations (Yao et al. 2022; Schick et al. 2023; Shen et al. 2023). Planning methods revise execution structure (Wang et al. 2023; Yao et al. 2023), and self-refinement methods revise outputs from intermediate feedback (Madaan et al. 2023; Shinn et al. 2023). Generative-agent simulations also show how local interactions can produce collective behavior (Park et al. 2023). These capabilities allow cooperation to emerge without fixing every role or work transition in advance. We focus on an auditability gap in emergent LLM-agent collaboration–where existing approaches may record messages, tool calls, provenance, or task dependencies, but they do not jointly represent what work remains, who is responsible for it, and what evidence justifies each work-state transition. A work obligation is a basic unit of progress, whether introduced by the task or created as agents organize the work. We call a cooperation state auditable when every active work assertion that can affect a later update, diagnostic, or terminal output can be traced to observable actions or artifacts, the operation that changed the work, and currently valid evidence, e.g., from environment observations. Auditability is essential for reasoning, certifying, and improving emergent collective behavior, as a plausible output can often conceal unsupported intermediate claims, incomplete work, poor task allocation, or failures that propagated through the workflow. Existing approaches provide important but partial views. LLM-agent frameworks record workflow traces, but do not define the obligations or evidence governing work-state transitions (Wu et al. 2023; Li et al. 2023; Hong et al. 2024; Qian et al. 2024). Distributed-event and provenance models represent ordering, causality, and derivation, but not evolving task obligations and their settlement (Lamport 2019; Belhajjame et al. 2013; Groth and Moreau 2013). Planning and workflow models represent decomposition and dependencies while often abstracting away the event-level support for committed updates (Erol et al. 1994; Torreno et al. 2017; van Der Aalst et al. 2003; Van der Aalst 1998; Murata 1989). Runtime verification and LLM judges assess traces or outputs, but lack the event–work correspondence needed to locate unsupported obligations or justify capability-based reassignment (Havelund and Roşu 2001; Leucker and Schallhart 2009; Zheng et al. 2023). The limitation is representational: interaction without work semantics is ambiguous, whereas work state without observable provenance is unauditable. We introduce the Integrated Cooperation-Obligation REpresentation (iCORE), with a unified state representation X=(G,Q,Π)X=(G,Q, ). The cooperation graph G encodes observable agent execution and artifacts, the obligation graph Q encodes evolving work and assignments, and the audit map Π certifies the correspondence between them with verifiable properties and evidence for reasoning on collective emergent behavior. iCORE is an instrumentation layer over workflows. The application specifies the environment- or task-specific observable and validation interfaces in a declaration package D, while the host framework retains control of execution. This iCORE representation enables the auditor to certify two complementary properties: Work soundness, where every active decision-relevant work assertion from Q must have a finite justification through G and Π ; and Agent-assignment stability, which requires that no feasible alternative agent improve the declared contribution value for an evaluated obligation by more than a threshold ϵε. The weighted satisfaction rates of these properties define iCORE-state quality cqD,ϵcq_D,ε. We use the iCORE framework to prove local-to-global soundness and assignment-regret guarantees. Specifically, legal local updates preserve global work soundness and that componentwise stability bounds aggregate reassignment gain. Under explicit decomposability, validator-adequacy, and value-calibration conditions, iCORE-state quality also lower-bounds expected task performance; otherwise, it remains a process diagnostic. We operationalize iCORE through iCORE-Audit, an event-triggered layer around the host policy. It audits each proposal’s intended state effects and can diagnose unsupported work, beneficial reassignment, or stalled progress before a terminal result is produced. Proposed repairs are themselves audited, to prevent the system from appearing to improve simply by deleting or excluding difficult work. Relative to passive full-state observation, iCORE-Audit yields absolute trajectory-quality (as quantified by the iCORE state quality) improvements of 11.5%11.5\% and 26.4%26.4\% in controlled and real-LLM execution, respectively, with corresponding absolute terminal-performance improvements of 15.1%15.1\% and 31.0%31.0\%. This paper makes three main contributions. 1. We define auditability for emergent LLM-agent cooperation and introduce iCORE to couple observable interaction with evolving work and responsibility. 2. We formalize work soundness, agent-assignment stability, their local-to-global guarantees, and the conditions relating iCORE-state quality to task performance. 3. We develop iCORE-Audit and evaluate representation sufficiency, matched quality improvement, task performance, and cost in controlled and real-LLM settings. 2 Cooperation-Obligation Representation We study fully cooperative, non-strategic agents with heterogeneous capabilities that jointly produce solve a single application-assigned task. The application supplies a quantitative outcome metric PerfPerf, and iCORE audits the process that produced the result, aiming to detect and forestall cooperation failures like execution errors, unsupported updates, incompatible partial results, or poor work assignments. Before execution, the application fixes a declaration package D=(D,ℳD,Ω,V,ℐD)D=(O_D,M_D, ,V,I_D), where DO_D specifies observable action and artifact types and semantic fields and ℐDI_D collects the capability-value, work-weighting, local-view, equivalence, and terminal interfaces; ℳDM_D, Ω , and V are the finite observable agent set, work-operation vocabulary, and validation specification (e.g., on work correctness). The Integrated Cooperation-Obligation REpresentation (iCORE) represents emergent cooperation through observable interaction in G, evolving work and responsibility in Q, and their certified correspondence in Π , as we formally define below. A work-level assertion is any semantic fact encoded in Q, including for example a node, relation, work status, result signature, coverage or compatibility claim, assignment, or terminal marker. It is active if currently asserted and not superseded, and decision-relevant if changing it can affect a declared update, an unresolved work obligation, a iCORE diagnostic, or a terminal predicate. A state is auditable when every active, decision-relevant assertion traces through Π to finitely many observable actions or artifacts in G, its declared work operation, and active evidence valid under V. An asserted work update is justified when it instantiates an operation declared by D, its recorded preconditions are current, and its certificates pass V. Auditability thus requires more than a message log: it checks each decision-relevant update, assignment, and terminal decision up to the observational equivalence declared by D. This equivalence may ignore fresh identifiers and inessential timestamps, but must preserve assignees, statuses, coverage, and terminal evidence. Definition 1 (iCORE state). A iCORE state is X=(G,Q,Π),X=(G,Q, ), where G is a cooperation graph, Q is an obligation graph, and Π is an audit map between them. 2.1 Cooperation Graph: Observable Agent Interactions Definition 2 (Cooperation graph). A cooperation graph is a finite typed directed acyclic graph G=(VG,EG,sG,tG,θG,λG,τG,μG),G=(V_G,E_G,s_G,t_G, _G, _G, _G, _G), where sG,tG:EG→VGs_G,t_G:E_G→ V_G are the source and target maps, and θG _G and λG _G assign application-declared types and observable labels to vertices and edges. The logical-time map τG:VG→ℕ _G:V_G satisfies u→Gv⟹τG(u)<τG(v).u _Gv _G(u)< _G(v). The vertex types distinguish action nodes Act(G)⊆VGAct(G) V_G and artifact nodes Art(G)⊆VG.Art(G) V_G. An artifact is a recorded, referenceable output of execution—for example, a message, plan, code patch, tool result, partial answer, or verification report—that may be consumed or checked by later actions. The metadata map μG _G stores observable information such as the acting agent, recipient, tool, verifier, capability evidence, or monitor decision. G therefore records observable actions, artifacts, and typed production, consumption, routing, or verification dependencies. This directed acyclic graph (DAG) records interaction events over time rather than an agent interaction topology: repeated agent interactions create distinct nodes in VGV_G. Thus, G identifies observable provenance but not the required work or its current assignee. 2.2 Obligation Graph: Evolving Work A work obligation is a unit of work that must be addressed as part of completing the assigned task. It may stem from the initial request or emerge as agents organize, assign, and perform work. Q tracks relationships between work obligations. Definition 3 (Obligation graph). An obligation graph is a finite typed directed graph Q=(VQ,EQ,sQ,tQ,θQ,λQ,ρQ,statQ,σQ,αQ).Q=(V_Q,E_Q,s_Q,t_Q, _Q, _Q, _Q,stat_Q, _Q, _Q). Here sQ,tQ:EQ→VQs_Q,t_Q:E_Q→ V_Q are the source and target maps; θQ _Q and λQ _Q assign declared types and observable labels; ρQ _Q assigns declared semantic roles to edges; statQ:VQ→Qstat_Q:V_Q _Q records one of the eight statuses listed below for each work obligation v∈VQv∈ V_Q; σQ _Q stores observable result signatures used for compatibility; and αQ:VQ→ℳD∪⊥ _Q:V_Q _D∪\ \ stores the current assignee of unresolved work or the last assignee of settled work, with ⊥ denoting no assignment. The typed relations represented in EQE_Q encode dependency, refinement, support, aggregation, or contradiction. The work obligation statuses mean: open, identified but not enabled; ready, enabled; blocked, waiting on a recorded condition; closed, execution complete; submitted, awaiting validation or aggregation; accepted, validated and eligible to discharge work; rejected, failed acceptance; and invalid, unusable under V. We define Unres(Q)Unres(Q) to comprise open, ready, blocked, and submitted obligations; we refer to all other obligations as settled work. A required root is an obligation with no predecessor under the obligation relation. To complete the task, it must be discharged unless active valid evidence marks it as excluded, duplicated, irrelevant, or superseded. Formally, the required root set ReqRoot(Q)⊆q∈VQ:∄p∈VQ with p≺QoblqReqRoot(Q) \q∈ V_Q: p∈ V_Q with p _Q^oblq\. Let EffRoot(X)EffRoot(X) be the roots not so removed and CovQ(q)Cov_Q(q) the roots that q may discharge. These semantics allow work to emerge without a complete decomposition in advance; Appendix A.2 gives the full definitions. Definition 4 (Relative obligation and evaluation set). For a component q, let Dis−q(X)Dis_-q(X) be the effective roots discharged by accepted work whose active support does not depend on q. Its relative obligation is ObX(q)=CovQ(q)∩(EffRoot(X)∖Dis−q(X)).Ob_X(q)=Cov_Q(q)∩ (EffRoot(X) _-q(X) ). The evaluation set (X)W(X) contains every unresolved q with ObX(q)≠∅Ob_X(q)≠ and every component carrying an active decision-relevant assertion for a iCORE diagnostic or terminal predicate. Thus, unresolved obligations remain evaluated while nonempty, and settled, excluded, or superseded components remain only while they affect a diagnostic or terminal decision. This preserves terminal support and prevents terminal iCORE-state scores from becoming vacuous. Unlike G, Q represents work semantics and assignment but does not identify the interactions or capability evidence justifying them. 2.3 Audit Map: Connecting Interaction and Work The audit map connects the interactions recorded in G with the work evolution recorded in Q using the application-declared vocabulary Ω of operations that create, assign, reassign, transform, verify, or resolve work. Definition 5 (Audit map). Given G and Q, an audit map is Π=(π,ω,κ),π:VG⇀2VQ,ω:ℒπ⇀Ω, =(π,ω,κ), π:V_G 2^V_Q, ω:L_π , where ℒπ=(a,q)∈Act(G)×VQ:q∈π(a)L_π=\(a,q) (G)× V_Q:q∈π(a)\, π links observable actions and artifacts to the work components they affect, ω records the declared work operation for each linked action–component pair, and κ stores the certificates supporting the correspondence and resulting work update. For a∈Act(G)a (G) and q∈π(a)q∈π(a), ω(a,q)ω(a,q) records how an agent action a changes or maintains the work obligation q, so one action may implement different declared operations on different components. A linked artifact z∈Art(G)z (G) may be a certificate premise but needs no operation label. A certificate c∈κc∈κ stores an identifier, internal and external premises, a claim, and an issuer; its claim must instantiate a schema declared by D. Internal premises refer to the current iCORE state, whereas external premises enter through declared environment-input nodes in G. The certificate is valid when active, current, authorized in issuer and scope, and accepted by V; it remains active until validly revoked or superseded. The complete record is given in Appendix A.3. Certificate validity alone is insufficient: the certificate and its premises must connect through Π to the affected assertion in Q and the responsible observable nodes in G. In particular, an assignment is auditable only when the responsible action, affected work and assignee, assignment operation, and capability evidence agree across G, Q, ω, and κ. Together, G, Q, and Π determine whether work is justified, responsibility is suitably assigned, and both assessments evolve. Appendix A.8 shows why unlabeled interaction topology alone cannot determine these properties. 3 iCORE for Work Soundness iCORE uses work soundness in the proof-theoretic sense: every active decision-relevant work-level assertion must have a finite valid derivation from recorded interaction, its declared operation, and active evidence under V. The preservation, reconstruction, and terminal-report results below are specification invariants induced by the update legality, recording, and terminal contracts; required-root completeness is enforced separately by Section 3.3, and semantic task correctness still depends on validator adequacy. 3.1 Legal Cooperation Processes Using the declaration package from Section 2, a iCORE system is =(D,D,ℛ^,X0,Acc,Rej)S=(D,X_D, R,X_0,Acc,Rej), where DX_D is the feasible-state space, ℛ R is the family of candidate local-update schemas, X0∈DX_0 _D is the initial state, and Acc,Rej:D→0,1Acc,Rej:X_D→\0,1\ are the terminal predicates. The relation X≡XYX _XY identifies states differing only in fields declared inessential by D while preserving, under transported typed-graph isomorphisms, every field affecting update enablement, obligations, assignments, evidence, or terminal decisions; it is a congruence for legal updates, as detailed in Appendix A.5. Membership in DX_D constrains represented states, not the physical actions agents may attempt: an unsupported effect may be recorded in G but cannot be committed in Q except as an explicit blocked, rejected, invalid, superseded, or repair-pending record. Feasibility anchors work to observable input, keeps unresolved work accountable, supports assignments with observable assignment and capability evidence, and certifies aggregate coverage and compatibility; Appendix A.4 gives the complete conditions. A candidate local update, induced by an observable agent action, tool result, validator decision, or monitor intervention, may change G, Q, and Π . Its finite declared local view contains the events read, their linked work, and the active evidence required by the operation; enablement uses neither future events nor unrecorded global information. Definition 6 (Legal iCORE update). A candidate local update X→X′X→ X is legal if it (i) accesses only declared finite interfaces and depends only on its declared local view and D; (i) applies an operation permitted by D; (i) provides active V-valid evidence for every assertion it creates, activates, makes decision-relevant, or semantically modifies, and leaves no active assertion supported only by evidence that the update revokes or supersedes; and (iv) yields X′∈DX _D while respecting ≡X _X. An admissible process is any finite or infinite sequence X0→X1→X2→⋯X_0→ X_1→ X_2→·s of legal updates; different interaction orders, agent outputs, and monitor interventions may induce different admissible processes. 3.2 Work Soundness Using the correspondence established by Π , work soundness determines whether the evolving state of work in Q is justified by observable interaction in G. Definition 7 (Work soundness). For q∈(X)q (X), let D(q;X) A_D(q;X) be its active decision-relevant work-level assertions and set D(X)=⋃q∈(X)D(q;X) A_D(X)= _q (X) A_D(q;X). A iCORE state X is work-sound when every a∈D(X)a∈ A_D(X) has a finite justification through observable initial-input or interaction nodes in G, the declared operation for each non-initial assertion, the corresponding links in Π , and evidence active and valid under V. A process is work-sound when every state it reaches is work-sound. Soundness therefore applies to every decision-relevant creation, assignment, transformation, resolution, and terminal-support assertion, not only the final report. For the evaluation set (X)W(X) in Definition 4, D predeclares positive weights wqw_q based on declared information such as work type or covered-root importance; uniform weights are allowed. Let JD(q;X)=1J_D(q;X)=1 exactly when all assertions in D(q;X) A_D(q;X) are justified. Define sndD(X)=1,(X)=∅,∑q∈(X)wqJD(q;X)∑q∈(X)wq,otherwise.snd_D(X)= cases1,&W(X)= ,\\[5.69054pt] _q (X)w_qJ_D(q;X) _q (X)w_q,&otherwise. cases Then X is work-sound if and only if sndD(X)=1snd_D(X)=1. Proposition 1 (Local-to-global preservation of work soundness). If X0X_0 is work-sound, every state reachable by an admissible process is work-sound. The proof is given in Appendix D.2; thus, legality checked from finite local views yields a global guarantee over all active decision-relevant assertions in each reachable state. Work soundness also makes the recorded work process reconstructable. Proposition 2 (Audit reconstruction). If every legal update and its effects on G, Q, and Π are recorded, the ordered record reconstructs every iCORE state up to ≡X _X. For any finite accepted process, it also gives each component in the terminal cover a finite explanation from the initial input through linked interactions in G, work transformations in Q, and their correspondence in Π . The proof is given in Appendix D.3. 3.3 Sound Terminal Outcomes For A⊆Accepted(Q)A (Q) and R⊆ReqRoot(Q)R (Q), A covers R when R⊆⋃a∈ACovQ(a)R _a∈ ACov_Q(a), and is a terminal cover when it also has the joint compatibility evidence required by V. The relevant root set EffRoot(X)EffRoot(X) omits roots excluded, duplicated, rendered irrelevant, or superseded by active valid evidence. Let EffUnres(X)EffUnres(X) contain the non-excluded unresolved components whose coverage intersects EffRoot(X)EffRoot(X), and let FailRoot(X)FailRoot(X) contain effective roots with active valid failure evidence not neutralized by an active valid repair. Then Acc(X)Acc(X) requires feasibility, no effective unresolved work, accepted work forming a certified terminal cover of all effective roots, no failed effective root or accepted component with unresolved or invalid support, and no live action or artifact that can change any effective root’s discharge, failure, exclusion, or compatibility. Conversely, Rej(X)Rej(X) requires feasibility, no effective unresolved work, a nonempty effective-root set entirely contained in FailRoot(X)FailRoot(X) with no effective root discharged, and no live action or artifact that can repair, discharge, or reopen an effective root. Appendix A.6 gives the exact predicates. A finite process is terminally complete when its final state satisfies Acc(X)Acc(X) or Rej(X)Rej(X), or active valid evidence certifies that it is externally stuck. Definition 8 (Terminal-report soundness). A work-sound process is terminal-report sound when every Accept report emitted at a state X satisfies Acc(X)Acc(X) and every Reject report emitted at a state X satisfies Rej(X)Rej(X). Work soundness justifies individual work updates, while terminal-report soundness additionally requires the reported outcome to account for all required work. Corollary 1 (Terminal-report soundness). If X0X_0 is work-sound, every committed update is legal, and Accept and Reject are emitted only when Acc(X)Acc(X) and Rej(X)Rej(X) hold, respectively, then the process is terminal-report sound. When process guarantees imply task correctness. These process guarantees imply semantic task correctness only when V is adequate for the declared task class. An emitted decision is semantically correct when its Accept output or Reject report satisfies the class’s declared acceptance or rejection semantics. A V-certified failed-root set F⊆EffRoot(X)F (X) contains roots with active valid failure evidence not neutralized by active valid repair. We call V task-adequate when every V-certified accepted terminal cover yields a semantically correct accepted output, every V-certified failed-root set satisfying the declared rejection rule yields a semantically correct rejection, and every process-relevant fault in coverage, compatibility, evidence, or terminal settlement is detectable under V. Proposition 3 (Task-level implication under validator adequacy). If V is task-adequate and a process is work-sound, terminal-report sound, and terminally complete, then every emitted Accept or Reject decision is semantically correct for the declared task class; an externally stuck report certifies only process status. The proof is given in Appendix D.5. For open-ended tasks whose quality is not fully captured by V, iCORE exposes unsupported process states but does not certify the remaining semantic quality of the agents’ outputs. 4 iCORE for Agent-Assignment Suitability Work soundness determines whether evaluated work is justified, not whether it is assigned suitably. We formalize agent-assignment stability as the absence of a feasible alternative whose declared contribution advantage exceeds a fixed tolerance; here, “stability” means resistance to beneficial reassignment, not temporal invariance. 4.1 Capability Values and Beneficial Reassignment For each q∈(X)q (X), D defines a feasible-agent set ℱD(q,X)⊆ℳDF_D(q,X) _D using declared observable constraints such as tool access, modality, availability, authorization, or resource limits; feasibility does not predict success. The rule is evaluated from registered metadata and capability evidence in G. If no hard filter is available, it may conservatively set ℱD(q,X)=ℳDF_D(q,X)=M_D; by convention, a maximum over an empty feasible set is zero, indicating that no reassignment candidate is currently available. The map αQ(q)∈ℳD∪⊥ _Q(q) _D∪\ \ records the current assignee for unresolved work and the last assignee for settled work, using the statuses defined after Definition 3; ⊥ denotes a blocked or unassigned component. Feasibility of DX_D requires every non-⊥ assignee to belong to the feasible set in the applicable evaluation context. To prevent retrospective evaluation, let XDeval(q)X_D^eval(q) be X for unresolved work and the reconstructible snapshot immediately before the assignment or reassignment establishing αQ(q) _Q(q) for settled work, and abbreviate ℱD(q,X):=ℱD(q,XDeval(q)),vD(m,q∣X):=vD(m,q∣XDeval(q)).F_D(q,X):=F_D (q,X_D^eval(q) ), v_D(m,q X):=v_D (m,q X_D^eval(q) ). Thus, later availability changes and post-outcome oracle information cannot alter settled-work assessment. For m∈ℳDm _D, D declares a normalized net contribution value vD(m,q∣X)∈[0,1]v_D(m,q X)∈[0,1]. It may be a scalarization, fixed before evaluation, of auditable criteria such as validated success estimates, latency, cost, or risk; it need not be an oracle estimate. If no defensible scalarization exists, report the criteria separately and do not invoke the scalar regret guarantee. Set vD(⊥,q∣X)=0v_D( ,q X)=0. Every capability observation used by feasibility or contribution values must be recorded in G and linked through Π to the corresponding assignment in Q; unsupported self-reports and post-outcome oracle information are excluded. For m∈ℱD(q,X)m _D(q,X), define the counterfactual assignment gain ΔD(m←αQ(q);q,X)=vD(m,q∣X)−vD(αQ(q),q∣X). _D(m← _Q(q);q,X)=v_D(m,q X)-v_D( _Q(q),q X). A gain above a declared tolerance ϵ≥0ε≥ 0 is an actionable ϵε-beneficial reassignment for unresolved work. For settled work retained in (X)W(X), it is a historical assignment-regret diagnostic computed in the assignment-time context and excludes later evidence. Definition 9 (Agent-assignment stability). A component q∈(X)q (X) is ϵε-stable at X when maxm∈ℱD(q,X)ΔD(m←αQ(q);q,X)≤ϵ. _m _D(q,X) _D(m← _Q(q);q,X)≤ε. Using the same predeclared weights wqw_q as work soundness, define astabD,ϵ(X)=1,(X)=∅,∑q∈(X)wq[q is ϵ-stable at X]∑q∈(X)wq,otherwise.astab_D,ε(X)= cases1,&\\ (X)= ,\\[5.69054pt] _q (X)w_q1[q is $ε$-stable at X] _q (X)w_q,&\\ . cases The state is agent-assignment stable when astabD,ϵ(X)=1astab_D,ε(X)=1. The definition couples all three iCORE components: Q supplies the component and assignee, G the agents and observable capability evidence, and Π the certified assignment correspondence. Theorem 1 (From Local Stability to Global Assignment-Regret Bound). Assume (X)≠∅W(X)≠ and normalize its weights so that ∑q∈(X)wq=1 _q (X)w_q=1. Let UD(α∣X)=∑q∈(X)wqvD(α(q),q∣X).U_D(α X)= _q (X)w_qv_D(α(q),q X). For any componentwise feasible alternative assignment β, meaning β(q)∈ℱD(q,X)∪⊥β(q) _D(q,X)∪\ \ for every q, UD(β∣X)−UD(αQ∣X)≤1−(1−ϵ)astabD,ϵ(X).U_D(β X)-U_D( _Q X)≤ 1-(1-ε)astab_D,ε(X). In particular, if X is agent-assignment stable, no feasible joint reassignment can improve the declared aggregate value by more than ϵε. The proof is given in Appendix D.6. The left-hand side is the declared global assignment regret of replacing the recorded assignment αQ _Q by β. The theorem is local-to-global because componentwise stability bounds this regret for every feasible reassignment of the full evaluated work set; it does not require strategic agents or an equilibrium interpretation. 4.2 iCORE-State Quality and Task Performance Definition 10 (iCORE-state quality). The normalized iCORE-state quality is cqD,ϵ(X)=12(sndD(X)+astabD,ϵ(X))∈[0,1].cq_D,ε(X)= 12 (snd_D(X)+astab_D,ε(X) )∈[0,1]. We report 100cqD,ϵ(X)100cq_D,ε(X) together with both component scores; equal weighting is fixed before evaluation. Because both components are weight-normalized satisfaction rates, cqD,ϵcq_D,ε is invariant to common weight rescaling and supports comparison across work-set sizes; reporting the components separately prevents the average from hiding a severe soundness or assignment defect. Proposition 4 (Performance implication of iCORE-state quality). Let =(X)≠∅W=W(X)≠ . Assume (i) Perf=∑q∈wqYqPerf= _q w_qY_q with Yq≥0Y_q≥ 0 and ∑q∈wq=1 _q w_q=1; (i) V is task-adequate; (i) every justified q∈q satisfies [Yq∣X]≥vD(αQ(q),q∣X)E[Y_q X]≥ v_D( _Q(q),q X); and (iv) every q∈q has a feasible agent with value at least pmin>ϵp_ >ε. Then [Perf∣X]≥2(pmin−ϵ)[cqD,ϵ(X)−12]+.E[Perf X]≥ 2(p_ -ε) [cq_D,ε(X)- 12 ]_+. The proof is given in Appendix D.7. Assumption (i) restricts the bound, not the definition of cqD,ϵcq_D,ε, to metrics decomposable over required roots or verifier-certified components. Without such a decomposition, adequate validators, lower calibration, or the feasible-agent floor, cqD,ϵcq_D,ε remains a process diagnostic rather than a performance certificate. 5 iCORE-Audit iCORE-Audit is an event-triggered intervention layer around an existing multi-agent execution policy. It neither defines the task nor generates or selects ordinary work; ScheduleDSchedule_D in Algorithm 1 is only the host-policy interface. Each proposal is labeled by its intended effects on G, Q, and Π and audited under Definition 6. Unsupported work is detected from certificate or event–work correspondence defects, assignment instability from Definition 9, and stalling from a progress predicate fixed in D, so no trigger relies on unrecorded monitor judgment. After each ordinary attempt, iCORE-Audit recomputes sndD(X)snd_D(X), astabD,ϵ(X)astab_D,ε(X), and cqD,ϵ(X)cq_D,ε(X) from (X)W(X), active certificates, assignments, and capability evidence. A hard flag records a repair-requiring defect, such as an unsupported attempted assertion, a revocation that makes dependent work repair-pending, or a validator inconsistency; the unsupported semantic effect is not committed. Let h count consecutive iterations since the last committed transition satisfying the predeclared ProgressDProgress_D predicate. It resets only on such a transition and otherwise increases after a legal nonproductive step, a rejected proposal, or no enabled productive work. An intervention fires when the current state has no enabled productive ordinary update, h≥Hh≥ H, a hard flag, an ϵε-beneficial reassignment, or cqD,ϵ(X)<τcq_D,ε(X)<τ; H and τ are fixed before execution. A diagnosis F identifies the affected obligations, missing or invalid evidence, current assignees, feasible alternatives, and relevant interaction history. The deterministic routing rule ResponsibleAgentD(X,F)ResponsibleAgent_D(X,F) selects the agent authorized to propose the repair; “responsible” denotes repair authority rather than blame. For a work or evidence defect, this is the current assignee or the proposer whose attempted update produced the flag, according to a priority rule fixed in D. For an assignment defect, it is the recorded agent designated by D as authorized to revise assignments, which may be the original assigner and need not be the currently assigned worker. The selected agent proposes a repair, verification, decomposition, or reassignment, but iCORE-Audit still labels and audits the candidate recovery. The recovery is committed only if it is legal and work-sound, satisfies the matched-set conditions below, and resolves every diagnosed hard flag whose resolution is required for continuation or acceptance; otherwise, only a legal failure-and-feedback record is added to the iCORE state. To compare intervention quality without rewarding the silent deletion of difficult work, let X−X^- denote the state at which F is issued, let XfX_f be the candidate repaired state, and let X+=CommitD(Xf)X^+=Commit_D(X_f) when the recovery is accepted. Before feedback is sent, F freezes a matched audit set FW_F containing the affected obligations and every active support component whose assertions or assignments may be changed by the recovery. The comparison is therefore between the problematic pre-intervention state and its proposed repair on the same frozen cohort: cqD,ϵ(Xf;F)≥cqD,ϵ(X−;F).cq_D,ε(X_f;W_F) _D,ε(X^-;W_F). After commitment, the left-hand side is equivalently evaluated at X+X^+. A valid discharge, replacement, or supersession counts as satisfied, whereas removal without valid transport or settlement evidence remains in the frozen cohort and counts as unsound. The complete matched-set semantics are given in Appendix A.9. Algorithm 1, given in Appendix A.10, formalizes this loop. It checks the terminal predicates, requests an ordinary proposal through the host execution policy when productive work is enabled, audits the proposal, updates the patience counter h, and recomputes the iCORE diagnostics. When a trigger fires, it constructs F and FW_F, routes the diagnosis to the declared repair authority, and commits the proposed recovery only after AuditRecoveryDAuditRecovery_D returns no violation. Because rejected proposals, diagnoses, feedback, and accepted recoveries are represented by legal iCORE updates, a later auditor can reconstruct what information was supplied, which agent responded, and how the response changed the work and assignment state. Proposition 5 (Soundness and intervention quality). Assume that X0X_0 is work-sound, every committed update in Algorithm 1 is legal, and AuditRecoveryDAuditRecovery_D enforces the matched-set conditions above. Then every committed state is work-sound. Moreover, for every committed intervention from X−X^- to X+X^+ with diagnosis F, cqD,ϵ(X+;F)≥cqD,ϵ(X−;F).cq_D,ε(X^+;W_F) _D,ε(X^-;W_F). The proof is given in the Appendix.If Proposition 4’s assumptions hold for both matched states on normalized FW_F with the same pminp_ and ϵε, its certified lower bound cannot decrease and increases strictly when post-intervention matched quality exceeds both its pre-intervention value and 1/21/2. This is a conditional guarantee, not a claim that every intervention improves every open-ended outcome. 6 Experiments We test three claims: whether the coupled state X=(G,Q,Π)X=(G,Q, ) is necessary to reconstruct both work-soundness and assignment defects; whether state-grounded auditing improves passive observation of the same full state; and whether iCORE quality follows the conditional performance relation in Proposition 4. Realized terminal performance is reported separately from process quality. 6.1 Protocol Applications and systems. We use six structured collaborative task (SCT) applications with obligation graphs that evolve during execution: Binary Coverage (BC), Decompose and Solve (DS), Compatible Merge (CM), Dependency Ladder (DL), Repair Verification (RV), and Capability Assignment (CA), with terminal performance defined as the weighted correctness of required roots. Each uses three agents, ϵ=0.05ε=0.05, and pmin=0.65p_ =0.65. The controlled suite evaluates all six under five cooperation failure conditions, allowing us to observe iCORE’s ability to detect distinct classes of faults; the real-LLM suite evaluates BC, DS, and CA under clean and mixed faults with Qwen2.5-0.5B-Instruct. The main suites contain 540540 controlled and 108108 real-LLM episodes, while ablation and boundary tests bring the total to 882882 artifacts. Appendix C gives the full matrix, replication settings, and runtime specifications. We compare two variants of iCORE to several baselines. In MAS-Only, agents receive no monitor state; agents under Interaction-only (INT), Task-only (TASK), and LLM-Judge (JUDGE) observe G, Q, and the execution trace, respectively. iCORE-Observe (iCORE-O) and iCORE-Audit (iCORE-A) both observe X=(G,Q,Π)X=(G,Q, ), but only iCORE-A returns structured diagnoses and applies the frozen-set preview guard. A shared proposal backend within each mode makes iCORE-A versus iCORE-O isolate intervention. Metrics and inference. We report iCORE quality cqD,ϵcq_D,ε, the conditional performance from Proposition 4, and terminal performance on required roots. Proposal-probe detection is measured before feedback. Comparisons use matched episode keys, one-sided paired Wilcoxon tests with Holm correction, and paired-bootstrap 95%95\% confidence intervals. 6.2 Reconstruction and Auditing Effects (a) Representation validity (b) Paired auditing effect Figure 1: Coupled-state reconstruction and auditing. (a) Representation validity across observation settings and execution modes. Markers distinguish controlled and real-LLM execution. iCORE (O/A) overlaps because both use FULL. (b) Paired iCORE-A minus iCORE-O gains. Error bars are paired-bootstrap 95%95\% confidence intervals over 9090 controlled and 1818 real-LLM episode keys. Figure 1(b) compares iCORE-A with iCORE-O on identical episode keys. Auditing improves trajectory quality, conditional performance, and terminal performance by 0.115/0.214/0.1510.115/0.214/0.151 in controlled execution and 0.264/0.480/0.3100.264/0.480/0.310 in real-LLM execution. Moreover, every recorded intervention is nondecreasing in matched iCORE quality (512512 controlled and 108108 real-LLM records). This monotonicity is enforced by the preview guard, while the paired episode gains measure its downstream effect. 6.3 Aggregate Results Controlled Real LLM System CQ Cond. Term. CQ Cond. Term. Best partial 0.738 0.592 0.671 0.683 0.511 0.495 iCORE-O 0.684 0.570 0.638 0.586 0.392 0.356 iCORE-A 0.799 0.785 0.789 0.850 0.872 0.667 Table 1: Main-suite results under controlled and real-LLM execution. “Best partial” is the columnwise best result among MAS-Only, INT, TASK, and JUDGE. Cond. and Term. denote conditional and terminal performance. Complete system-wise results appear in Appendix C.2. Table 1 compares iCORE-A with passive full-state observation and the strongest partial-state baseline. iCORE-A is best on all six mode–metric combinations, with particularly large gains in conditional performance under real-LLM execution. Its improvements over all five baselines remain significant after Holm correction (largest adjusted p=8.71×10−3p=8.71× 10^-3 controlled and 3.41×10−23.41× 10^-2 real LLM). For every controlled quality bin with a positive certified bound, even the lower bootstrap endpoint of conditional performance remains above the bound in Proposition 4. The boundary suite shows why this conclusion requires adequate validators, calibrated capability values, and feasible agents, and the real-LLM suite is a finite candidate-selection stress test rather than an open-ended autonomous benchmark. Full results, boundary tests, and prompts appear in Appendix C. 7 Conclusion This paper introduced iCORE, a coupled representation X=(G,Q,Π)X=(G,Q, ) for observable cooperation, evolving work obligations and assignments, and their certificate-backed correspondence. iCORE separates two complementary process properties: work soundness, which requires each decision-relevant work assertion to be justified, and agent-assignment stability, which requires active work to be assigned within a declared tolerance of the best feasible heterogeneous agent. Their quantitative satisfaction rates define iCORE-state quality, making it possible to compare states, interventions, and complete executions. Under decomposable tasks, adequate validators, and calibrated capability values, this score provides a lower bound on expected task performance; outside these assumptions, it remains a process-quality diagnostic rather than a certificate of open-ended answer quality. iCORE-Audit operationalizes the representation by allowing the ordinary agent process to run and returning state-grounded feedback when the process stalls or exposes a quality defect. Every diagnosis and recovery remains part of the auditable state, so quality improvement does not come at the cost of losing process accountability. References K. Belhajjame, R. B’Far, J. Cheney, S. Coppens, S. Cresswell, Y. Gil, P. Groth, G. Klyne, T. Lebo, J. McCusker, et al. (2013) Prov-dm: the prov data model. W3C Recommendation 14, p. 15–16. Cited by: §1. K. Erol, J. Hendler, and D. S. Nau (1994) HTN planning: complexity and expressivity. In AAAI, Vol. 94, p. 1123–1128. Cited by: §1. P. Groth and L. Moreau (2013) PROV-overview. an overview of the prov family of documents. Cited by: §1. T. Guo, X. Chen, Y. Wang, R. Chang, S. Pei, N. V. Chawla, O. Wiest, and X. Zhang (2024) Large language model based multi-agents: a survey of progress and challenges. arXiv preprint arXiv:2402.01680. Cited by: §1. K. Havelund and G. Roşu (2001) Monitoring java programs with java pathexplorer. Electronic Notes in Theoretical Computer Science 55 (2), p. 200–217. Cited by: §1. S. Hong, M. Zhuge, J. Chen, X. Zheng, Y. Cheng, J. Wang, C. Zhang, S. Yau, Z. Lin, L. Zhou, et al. (2024) MetaGPT: meta programming for a multi-agent collaborative framework. In International Conference on Learning Representations, Vol. 2024, p. 23247–23275. Cited by: §1, §1. L. Lamport (2019) Time, clocks, and the ordering of events in a distributed system. In Concurrency: the Works of Leslie Lamport, p. 179–196. Cited by: §1. M. Leucker and C. Schallhart (2009) A brief account of runtime verification. The journal of logic and algebraic programming 78 (5), p. 293–303. Cited by: §1. G. Li, H. Hammoud, H. Itani, D. Khizbullin, and B. Ghanem (2023) Camel: communicative agents for" mind" exploration of large language model society. Advances in neural information processing systems 36, p. 51991–52008. Cited by: §1, §1. A. Madaan, N. Tandon, P. Gupta, S. Hallinan, L. Gao, S. Wiegreffe, U. Alon, N. Dziri, S. Prabhumoye, Y. Yang, et al. (2023) Self-refine: iterative refinement with self-feedback. Advances in neural information processing systems 36, p. 46534–46594. Cited by: §1. T. Murata (1989) Petri nets: properties, analysis and applications. Proceedings of the IEEE 77 (4), p. 541–580. Cited by: §1. J. S. Park, J. O’Brien, C. J. Cai, M. R. Morris, P. Liang, and M. S. Bernstein (2023) Generative agents: interactive simulacra of human behavior. In Proceedings of the 36th annual acm symposium on user interface software and technology, p. 1–22. Cited by: §1. C. Qian, W. Liu, H. Liu, N. Chen, Y. Dang, J. Li, C. Yang, W. Chen, Y. Su, X. Cong, et al. (2024) Chatdev: communicative agents for software development. In Proceedings of the 62nd annual meeting of the association for computational linguistics (volume 1: Long papers), p. 15174–15186. Cited by: §1, §1. T. Schick, J. Dwivedi-Yu, R. Dessì, R. Raileanu, M. Lomeli, E. Hambro, L. Zettlemoyer, N. Cancedda, and T. Scialom (2023) Toolformer: language models can teach themselves to use tools. Advances in neural information processing systems 36, p. 68539–68551. Cited by: §1. Y. Shen, K. Song, X. Tan, D. Li, W. Lu, and Y. Zhuang (2023) Hugginggpt: solving ai tasks with chatgpt and its friends in hugging face. Advances in Neural Information Processing Systems 36, p. 38154–38180. Cited by: §1. N. Shinn, F. Cassano, A. Gopinath, K. Narasimhan, and S. Yao (2023) Reflexion: language agents with verbal reinforcement learning. Advances in neural information processing systems 36, p. 8634–8652. Cited by: §1. A. Torreno, E. Onaindia, A. Komenda, and M. Štolba (2017) Cooperative multi-agent planning: a survey. ACM Computing Surveys (CSUR) 50 (6), p. 1–32. Cited by: §1. W. M. van Der Aalst, A. H. Ter Hofstede, B. Kiepuszewski, and A. P. Barros (2003) Workflow patterns. Distributed and parallel databases 14 (1), p. 5–51. Cited by: §1. W. M. Van der Aalst (1998) The application of petri nets to workflow management. Journal of circuits, systems, and computers 8 (01), p. 21–66. Cited by: §1. L. Wang, C. Ma, X. Feng, Z. Zhang, H. Yang, J. Zhang, Z. Chen, J. Tang, X. Chen, Y. Lin, et al. (2024) A survey on large language model based autonomous agents. Frontiers of Computer Science 18 (6), p. 186345. Cited by: §1. L. Wang, W. Xu, Y. Lan, Z. Hu, Y. Lan, R. K. Lee, and E. Lim (2023) Plan-and-solve prompting: improving zero-shot chain-of-thought reasoning by large language models. In Proceedings of the 61st annual meeting of the association for computational linguistics (volume 1: long papers), p. 2609–2634. Cited by: §1. Q. Wu, G. Bansal, J. Zhang, Y. Wu, B. Li, E. Zhu, L. Jiang, X. Zhang, S. Zhang, J. Liu, et al. (2023) Autogen: enabling next-gen llm applications via multi-agent conversation. arXiv preprint arXiv:2308.08155. Cited by: §1, §1. H. Yang, H. Lee, Y. Yao, Z. Liu, K. Liu, J. Chen, and C. Joe-Wong (2026) DIG to heal: scaling general-purpose agent collaboration via explainable dynamic decision paths. arXiv preprint arXiv:2603.00309. Cited by: §1. S. Yao, D. Yu, J. Zhao, I. Shafran, T. Griffiths, Y. Cao, and K. Narasimhan (2023) Tree of thoughts: deliberate problem solving with large language models. Advances in neural information processing systems 36, p. 11809–11822. Cited by: §1. S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao (2022) React: synergizing reasoning and acting in language models. arXiv preprint arXiv:2210.03629. Cited by: §1. L. Zheng, W. Chiang, Y. Sheng, S. Zhuang, Z. Wu, Y. Zhuang, Z. Lin, Z. Li, D. Li, E. Xing, et al. (2023) Judging llm-as-a-judge with mt-bench and chatbot arena. Advances in neural information processing systems 36, p. 46595–46623. Cited by: §1. Appendix A Formal iCORE Semantics This appendix provides the detailed semantics and proofs underlying Sections 2–5. It retains the complete execution model while the main text presents only the definitions needed to state the central results. A.1 Typed Observable Graphs A typed observable graph is H=(VH,EH,sH,tH,θH,λH),H=(V_H,E_H,s_H,t_H, _H, _H), where VHV_H and EHE_H are finite node and edge sets, sH,tH:EH→VHs_H,t_H:E_H→ V_H are source and target maps, and θH _H and λH _H assign declared types and observable labels. We write u→Hvu _Hv when an edge connects u to v and u↝Hvu _Hv when there is a directed path from u to v. A field is semantic when it may affect update enablement, feasibility, coverage, compatibility, or a terminal decision. Two typed graphs are observationally equivalent when a type-preserving graph isomorphism preserves every semantic field declared by D. Only representational fields, such as fresh identifiers, formatting, or inessential timestamps, may differ. iCORE imposes an observational boundary. Private prompts, hidden chain-of-thought, and internal tool-selection heuristics may influence an agent, but they cannot support a work assertion or terminal decision unless their relevant effect is emitted as an observable action, artifact, label, or certificate premise represented in G, Q, or Π . Thus auditability concerns declared observables rather than access to an agent’s hidden internal reasoning. For S⊆VGS V_G, define PastG(S)=u∈VG:u↝Gs for some s∈S.Past_G(S)=\u∈ V_G:u _Gs for some s∈ S\. The live frontier Live(G)Live(G) contains the actions and artifacts whose effects may still influence unresolved work or a terminal decision. A node leaves the live frontier only when its use, resolution, rejection, discard, invalidation, or supersession is observably recorded. A.2 Work Semantics The application declares how each relation in ℛQR_Q contributes to obligation, coverage, and support. We write p≺Qoblqp _Q^oblq when p must be resolved before q, p≺Qcovqp _Q^covq when q may contribute to discharging p, and p≺Qsupqp _Q^supq when p supports the existence or state of q. The exact status vocabulary is Q=open,ready,blocked,closed,submitted,accepted,rejected,invalid.S_Q=\ open, ready, blocked, closed,\\ submitted, accepted, rejected, invalid\. The required roots satisfy ReqRoot(Q)⊆q∈VQ:∄p∈VQ with p≺Qoblq.ReqRoot(Q) \q∈ V_Q: p∈ V_Q with p _Q^oblq\. The unresolved and accepted work sets are Unres(Q)=q∈VQ:statQ(q)∈open,ready,blocked,submitted,Unres(Q)=\q∈ V_Q:stat_Q(q)∈\ open, ready, blocked, submitted\\, and Accepted(Q)=q∈VQ:statQ(q)=accepted.Accepted(Q)=\q∈ V_Q:stat_Q(q)= accepted\. For a work component q, its root coverage is CovQ(q)=r∈ReqRoot(Q):r⪯Qcovq.Cov_Q(q)=\r (Q):r _Q^covq\. A set A⊆Accepted(Q)A (Q) is a terminal cover of R⊆ReqRoot(Q)R (Q) when R⊆⋃a∈ACovQ(a)R _a∈ ACov_Q(a) and the joint compatibility evidence required by V exists. A required root is discharged when a terminal cover exists for it. We write Dis(Q)=r∈ReqRoot(Q):r is discharged.Dis(Q)=\r (Q):r is discharged\. The declaration package fixes a finite observable agent set ℳDM_D. The map αQ _Q records the current assignee of unresolved work and retains the last recorded assignee of settled work. For a component q, let Dis−q(X)Dis_-q(X) contain the effective roots discharged by active accepted work whose support chain does not depend on q, and define ObX(q)=CovQ(q)∩(EffRoot(X)∖Dis−q(X)).Ob_X(q)=Cov_Q(q)∩ (EffRoot(X) _-q(X) ). The evaluation set (X)W(X) contains every unresolved component q with ObX(q)≠∅Ob_X(q)≠ , together with every component carrying an active decision-relevant assertion for a iCORE diagnostic or terminal predicate. Consequently, settled support components remain auditable rather than disappearing from terminal quality scores. If (X)=∅W(X)= , the task has no remaining or terminal-support work and both component scores are defined as one by convention. For each q∈(X)q (X), D specifies a feasible-agent set ℱD(q,X)F_D(q,X) and a normalized net contribution value vD(m,q∣X)∈[0,1]v_D(m,q X)∈[0,1]. The formula and permissible evidence are fixed before evaluation. For settled work, vDv_D may use only capability evidence observable no later than the relevant assignment or settlement event; post-outcome oracle information is excluded. Any capability observation used by vDv_D must be represented in G, and any assignment or reassignment in Q must be connected through Π to the corresponding observable event and active valid evidence. A.3 Certificates and Correspondence A certificate is a finite record c=(id(c),premint(c),premext(c),claim(c),issuer(c)).c= (id(c),prem_int(c),prem_ext(c),claim(c),issuer(c) ). Internal premises reference information already represented in X. External premises reference sources whose authority and scope are declared by V. An external premise enters a work-support chain only through a declared environment-input node in G and an active valid certificate linking that node, through Π , to the affected work assertion. External evidence therefore does not bypass the observable support requirement. A certificate is active when no active valid revocation or supersession certificate targets it. The predicate ValidCertV(c;X)=1ValidCert_V(c;X)=1 holds when c∈κc∈κ, c is active, its internal premises are present and current, its external premises satisfy V, and its claim passes the declared validation procedure. The active certificate-dependency graph must be acyclic. A work-level assertion includes any asserted node, relation, status, signature, coverage fact, compatibility fact, or terminal marker in Q. Every non-initial decision-relevant assertion must be connected through Π to observable execution and active valid evidence. A.4 Feasibility A well-typed state X=(G,Q,(π,ω,κ))X=(G,Q,(π,ω,κ)) is feasible when: 1. every required root is connected to an observable initial input and supporting certificate; 2. every non-initial work assertion is backed by responsible nodes in G, corresponding operation labels, and active valid certificates; 3. every non-root work node has a finite support chain ending at a required root or declared external input; 4. every unresolved work component remains connected to live execution or has an explicitly certified blocked, delegated, waiting, submitted, superseded, or repair-pending condition; 5. coverage uses only eligible work, and every aggregate has the joint compatibility evidence required by V; 6. every active assignment in Q names a feasible agent or carries valid blocked/unassigned evidence, and every assignment or reassignment is supported by an observable event and capability evidence through Π ; 7. every terminal event in G corresponds to the appropriate work state in Q, and every terminal work state has an observable witness; 8. revoked or superseded evidence cannot continue supporting an active assertion without re-certification, repair, invalidation, rejection, or supersession; and 9. no active assertion simultaneously depends on a certificate and an active valid revocation of that certificate. A.5 iCORE Systems, Local Views, and Admissible Processes Definition 11 (iCORE system). A iCORE system is =(D,D,ℛ^,X0,Acc,Rej),S=(D,X_D, R,X_0,Acc,Rej), where D fixes the observable semantics, agent set ℳDM_D, operation vocabulary, validation specification V, capability-value interface, local-view interface, and declared equivalence; DX_D is the set of feasible iCORE states satisfying the preceding conditions; ℛ R is the family of candidate local-update schemas; X0∈DX_0 _D is the initial state; and Acc,Rej:D→0,1Acc,Rej:X_D→\0,1\ are the declared terminal predicates. The declared state equivalence X≡X′X _XX holds when X and X′X differ only in fields declared inessential by D while agreeing, under transported graph isomorphisms, on every field that may affect update enablement, obligations, assignments, capability evidence, or terminal decisions. The relation is required to be a congruence for legal updates. A rewrite occurrence ρ at X=(G,Q,Π)X=(G,Q, ) has finite declared interfaces ReadG(ρ;X),Read_G(ρ;X), WriteG(ρ;X),Write_G(ρ;X), ReadQ(ρ;X),Read_Q(ρ;X), WriteQ(ρ;X),Write_Q(ρ;X), ReadΠ(ρ;X),Read_ (ρ;X), WriteΠ(ρ;X).Write_ (ρ;X). Its local cooperation view is LocG(ρ;X)=ReadG(ρ;X)∪AncGD(ReadG(ρ;X)),Loc_G(ρ;X)=Read_G(ρ;X) ^D_G(Read_G(ρ;X)), where the permitted ancestry rule and finite depth bound are fixed by D. Its mapped work view is ViewQ(ρ;Π,X)= _Q(ρ; ,X)= ReadQ(ρ;X) _Q(ρ;X) ∪⋃g∈LocG(ρ;X)∩VGπ(g), ∪ _g _G(ρ;X)∩ V_Gπ(g), together with the incident semantic relations, current statuses and signatures, and active certificates required by the declared operation. The complete local view is L(ρ;X)=(LocG(ρ;X),ViewQ(ρ;Π,X),ReadΠ(ρ;X)).L(ρ;X)=(Loc_G(ρ;X),View_Q(ρ; ,X),Read_ (ρ;X)). Definition 12 (Legal local update). A candidate update schema induces a partial function R^ρ:D⇀D,R^ρ(X)=X′. R_ρ:X_D _D, R_ρ(X)=X . An occurrence is enabled when every declared object and certificate premise is present and current in L(ρ;X)L(ρ;X) and D permits the proposed operation. The enabled update is legal when it (i) reads and writes only through its declared interfaces, (i) depends only on L(ρ;X)L(ρ;X) and the fixed declarations, (i) supports every new semantic assertion with active valid evidence under V, (iv) produces X′∈DX _D, and (v) respects declared state equivalence. Definition 13 (Admissible process and reachability). An admissible process is a finite or infinite sequence X0→X1→X2→⋯X_0→ X_1→ X_2→·s in which every transition is a legal local update. A state Y is reachable when X0→∗YX_0→^*Y along a finite admissible prefix. Anchoring, obligation settlement, certificate consistency, and event–work correspondence are state-space conditions encoded by feasibility rather than separate dynamic axioms. The remaining dynamic contract is online locality plus preservation: a legal update may use only its current declared view and must preserve feasibility and equivalence congruence. An incorrect proposal must therefore become an observable blocked, rejected, invalid, superseded, excluded, or repair-pending fact rather than silently breaking the model. A.6 Terminal Predicates Let OffX(Q)Off_X(Q) contain work components marked by active valid evidence as duplicated, excluded, irrelevant, or superseded. Define EffRoot(X)=ReqRoot(Q)∖OffX(Q)EffRoot(X)=ReqRoot(Q) _X(Q) and EffUnres(X)=q∈Unres(Q)∖OffX(Q):CovQ(q)∩EffRoot(X)≠∅.EffUnres(X)= \q (Q) _X(Q):Cov_Q(q) (X)≠ \. The failed roots FailRoot(X)FailRoot(X) are the effective roots with active valid rejection, invalidity, impossibility, or unreachability evidence and no valid repair neutralizing that failure. A state satisfies Acc(X)Acc(X) when: 1. X is feasible and EffUnres(X)=∅EffUnres(X)= ; 2. accepted work forms a certified terminal cover of EffRoot(X)EffRoot(X); 3. no effective root belongs to FailRoot(X)FailRoot(X); 4. no accepted component depends on unresolved, invalid, rejected, contradictory, or unrepaired work; and 5. no live productive artifact can change the discharge, failure, exclusion, or compatibility of an effective root. A state satisfies Rej(X)Rej(X) when: 1. X is feasible, EffUnres(X)=∅EffUnres(X)= , and EffRoot(X)≠∅EffRoot(X)≠ ; 2. every effective root belongs to FailRoot(X)FailRoot(X); 3. EffRoot(X)∩Dis(Q)=∅;EffRoot(X) (Q)= ; and 4. no live productive artifact can repair, accept, discharge, or reopen an effective root. A.7 Productivity and Fairness A transition X→YX→ Y is productive when X≢XYX _XY. The productive quotient is defined by [X]≡X→p[Y]≡X[X]_ _X _p[Y]_ _X when there exist X′≡X _XX and Y′≡XYY _XY such that X′→Y′X → Y is productive. We write →p∗ _p^* for its reflexive-transitive closure. The system is productively terminating when no reachable state begins an infinite productive path. It is productively normalizing when every reachable state has a finite productive continuation to a productive normal form. An occurrence is continuously enabled when, from some point onward, its declared objects and premises remain available. A productive execution is fair when it does not permanently starve a continuously enabled productive occurrence. The occurrence must eventually execute, or another recorded productive update must invalidate one of its premises by resolving, blocking, delegating, excluding, superseding, or repairing the relevant work. A.8 Why the Coupling Is Necessary Theorem 2 (Projection insufficiency). Consider any class of iCORE states containing two states with identical unlabeled cooperation-graph topology but different obligation, assignment, certificate, or event–work correspondence information, such that one state is work-sound or agent-assignment stable and the other is not. No monitor restricted to the unlabeled topology of G can be both sound and complete for the differing property on that class. A.9 Matched Intervention Quality Let F be a diagnosis produced at state X. The matched audit set FW_F is the finite weighted set containing every diagnosed component, every active component whose support or assignment is changed by the proposed recovery, and the active support ancestors required to evaluate those assertions. The set and weights are frozen before the agent receives feedback. For a successor state Y, the declaration package transports each q∈Fq _F through recorded identity, refinement, replacement, supersession, or settlement links. Define JDF(q;Y)=1J_D^F(q;Y)=1 when the transported component remains fully justified or has been validly discharged, rejected, replaced, or superseded with all required evidence; deletion without a valid transport or settlement record gives JDF(q;Y)=0J_D^F(q;Y)=0. Define AD,ϵF(q;Y)=1A_D,ε^F(q;Y)=1 when the transported unresolved component is ϵε-stable, or when a settled component was completed under an assignment that was ϵε-stable according to capability evidence available no later than settlement. The matched scores are sndD(Y;F)=∑q∈FwqJDF(q;Y)∑q∈Fwq,astabD,ϵ(Y;F)=∑q∈FwqAD,ϵF(q;Y)∑q∈Fwq,snd_D(Y;W_F)= _q _Fw_qJ_D^F(q;Y) _q _Fw_q, _D,ε(Y;W_F)= _q _Fw_qA_D,ε^F(q;Y) _q _Fw_q, with value one when F=∅W_F= , and cqD,ϵ(Y;F)=12(sndD(Y;F)+astabD,ϵ(Y;F)).cq_D,ε(Y;W_F)= 12 (snd_D(Y;W_F)+astab_D,ε(Y;W_F) ). Freezing the cohort prevents an intervention from increasing its score merely by deleting, renaming, or excluding a difficult obligation without valid evidence. A.10 iCORE-Audit Procedure Algorithm 1 gives the complete state-maintenance loop. The routine AuditOrdinaryDAuditOrdinary_D returns the set of legality or work-soundness violations in an ordinary proposal. If that set is nonempty, RecordFailureDRecordFailure_D records the attempted proposal and its audit result without committing the unsupported effects on Q or Π . Similarly, AuditRecoveryDAuditRecovery_D returns the violations of legality, work soundness, diagnosed-flag resolution, or matched-set quality. All recording operations below are themselves legal iCORE updates. Here h counts consecutive iterations without a committed transition satisfying ProgressDProgress_D. The recovery audit accepts XfX_f only when the candidate update is legal and work-sound, does not silently remove any obligation in FW_F, resolves each diagnosed hard flag required for continuation or acceptance, and satisfies cqD,ϵ(Xf;F)≥cqD,ϵ(X−;F).cq_D,ε(X_f;W_F) _D,ε(X^-;W_F). A successful but nonproductive recovery therefore does not reset h. Algorithm 1 iCORE-Audit with State-Grounded Agent Feedback 0: Initial request u0u_0, declarations D, tolerance ϵε, quality threshold τ, patience H, budget B 1: X←InitD(u0)X _D(u_0); h←0h← 0 2: for t=0,1,…,B−1t=0,1,…,B-1 do 3: if Acc(X)Acc(X) then 4: return Accept 5: else if Rej(X)Rej(X) then 6: return Reject 7: end if 8: U←EnabledProdD(X)U _D(X) 9: if U≠∅U≠ then 10: (m,ρ)←ScheduleD(X,U)(m,ρ) _D(X,U) 11: L←LocalViewD(X,ρ)L _D(X,ρ) 12: (o,C)←AgentStepD(m,L)(o,C) _D(m,L) 13: X~←LabelUpdateD(X,ρ,m,o,C) X _D(X,ρ,m,o,C) 14: E←AuditOrdinaryD(X,X~)E _D(X, X) 15: if E=∅E= then 16: X+←CommitD(X~)X^+ _D( X) 17: h←0h← 0 if ProgressD(X,X+)Progress_D(X,X^+); otherwise h←h+1h← h+1 18: X←X+X← X^+ 19: else 20: X←RecordFailureD(X,X~,E)X _D(X, X,E); h←h+1h← h+1 21: end if 22: else 23: h←h+1h← h+1 24: end if 25: q←cqD,ϵ(X)q _D,ε(X) 26: if U=∅∨h≥H∨HardFlagD(X)∨BeneficialReassignD,ϵ(X)∨q<τU= h≥ H _D(X) _D,ε(X) q<τ then 27: X−←X^-← X; F←DiagnoseD(X−)F _D(X^-); F←MatchedSetD(X−,F)W_F _D(X^-,F) 28: mf←ResponsibleAgentD(X−,F)m_f _D(X^-,F) 29: Lf←FeedbackViewD(X−,F)L_f _D(X^-,F) 30: (of,Cf)←AgentReviseD(mf,Lf,F)(o_f,C_f) _D(m_f,L_f,F) 31: Xf←LabelInterventionD(X−,mf,of,Cf,F)X_f _D(X^-,m_f,o_f,C_f,F) 32: Ef←AuditRecoveryD(X−,Xf,F,F)E_f _D(X^-,X_f,F,W_F) 33: if Ef=∅E_f= then 34: X+←CommitD(Xf)X^+ _D(X_f) 35: h←0h← 0 if ProgressD(X−,X+)Progress_D(X^-,X^+); otherwise h←h+1h← h+1 36: X←X+X← X^+ 37: else 38: X←RecordFeedbackD(X−,Xf,F,Ef)X _D(X^-,X_f,F,E_f); h←h+1h← h+1 39: if CertifiedStuckD(X)CertifiedStuck_D(X) then 40: return Stuck 41: end if 42: end if 43: end if 44: end for 45: return CertifyBudgetD(X)CertifyBudget_D(X) if valid; otherwise Incomplete Appendix B Supplementary Execution-Order Stability This section retains the earlier task-process notion of stability as a supplementary property. It is intentionally excluded from the main text, where stability refers only to heterogeneous-agent assignment. Here the question is whether different legal orders of productive updates reach equivalent semantic outcomes. A legal update X→YX→ Y is productive when X≢XYX _XY and stuttering otherwise. A reachable state is a productive normal form when no productive legal update remains enabled. Suppose two productive updates ρ and η are enabled at X. They are residual-sound independent when both residual executions ρ;ηρ; _ρ and η;ρη; _η are defined and reach equivalent states. Otherwise the one-step fork is a productive local critical pair. Two states Y and Z are productively joinable modulo ≡X _X, written Y↓p,≡XZY _p, _XZ, when they have productive descendants Y′Y and Z′Z with Y′≡XZ′Y _XZ . Definition 14 (Execution-order stability). A iCORE system is globally execution-order stable when any two productive continuations from the same reachable state to productive normal forms terminate in equivalent iCORE states. Theorem 3 (Local-to-global execution-order stability). Assume that the reachable productive quotient terminates and every reachable one-step productive fork is either residual-sound independent or a productive local critical pair. Then the system is globally execution-order stable if and only if every reachable productive local critical pair is productively joinable modulo ≡X _X. Joinability requires agreement across the full state: the branches must reconcile their cooperation events in G, work and assignment states in Q, and event–work/certificate correspondence in Π . Therefore an unlabeled cooperation topology alone cannot characterize execution-order stability. This supplementary property may be useful when reproducible ordering is itself an application requirement, but it is not used to define agent-assignment stability or iCORE-state quality in the main text. Appendix C Additional Experimental Details This appendix documents the exact experiment matrix materialized in the supplied artifact. All 882882 scheduled keys listed below produced episode JSON files; “completed” elsewhere in the tables is a task-success indicator rather than a file-completion indicator. C.1 Experiment Matrix Mode Suite Environments Systems/variants Conditions or boundaries Episodes Controlled Main BC, DS, CM, DL, RV, CA six systems clean, missing evidence, misassignment, verifier delay, stall 540 Real LLM Main BC, DS, CA six systems clean, mixed 108 Controlled Ablation BC, DS, CM, DL, RV, CA Full, SO, AO, −Π- , NC mixed 90 Controlled Boundary BC, DS, CM, DL, RV, CA iCORE-O, iCORE-A standard, DV, SC, WP 144 Total materialized episode artifacts 882 Table 2: Executed matrix. DV, SC, and WP denote degraded validator, shuffled declared capabilities, and weak agent pool. The controlled main, real-LLM main, ablation, and boundary suites contain 540540, 108108, 9090, and 144144 materialized episode artifacts, respectively. C.2 Full Aggregate Results Controlled (540 episodes) Real LLM (108 episodes) System CQ Cond. Perf. Term. Perf. CQ Cond. Perf. Term. Perf. MAS-Only 0.684 0.570 0.638 0.586 0.392 0.356 Interaction-only 0.680 0.579 0.662 0.586 0.392 0.356 Task-only 0.738 0.592 0.654 0.683 0.511 0.495 LLM-Judge 0.686 0.581 0.671 0.586 0.392 0.356 iCORE-Observe 0.684 0.570 0.638 0.586 0.392 0.356 iCORE-Audit 0.799 0.785 0.789 0.850 0.872 0.667 Table 3: Complete aggregate main-suite means. CQ is trajectory iCORE quality; Cond. Perf. is the calibrated conditional expectation used in Proposition 4; Term. Perf. is realized performance on required roots. Bold and underlined entries denote the best and second-best distinct means in each column. C.3 Structured Collaborative Task Environments All environments use agents agent_1, agent_2, and agent_3, with ϵ=0.05ε=0.05 and pmin=0.65p_ =0.65. Every action becomes an event in G; work status, assignee, prerequisites, values, and weights reside in Q; assignment, result, merge, verification, and repair certificates are appended to Π . The implementation is a self-contained graph runtime. It does not import an external DIG runtime package. Env. Obligation structure Targets/validator Required roots Max rounds Primary mechanism BC six independent atomic items each value 11, exact six, weight 11 each 7 complete each item exactly once with active evidence DS aggregate root plus four latent children children 1,2,3,41,2,3,4; root sum 1010 root, weight 22 9 decompose, solve, certify, and merge CM three source items supporting one aggregate 0.2,0.3,0.5→1.00.2,0.3,0.5→ 1.0 aggregate, weight 22 8 retain all compatible support sources DL chain d0→d1→d2→d3d_0→ d_1→ d_2→ d_3 values 1,2,3,41,2,3,4, exact d3d_3, weight 1.51.5 8 respect certified prerequisites RV draft, check, repair, final chain 7,7,8,87,7,8,8; versioned evidence final, weight 22 9 invalidate stale version-1 evidence and certify repair CA four independent heterogeneous items 11,13,17,1911,13,17,19, exact four, weight 11 each 7 assign math/search/code/review to capable agents Table 4: Environment specifications Binary Coverage (BC). The six work points p0,…,p5p_0,…,p_5 are independent required roots. A valid terminal state requires every point to be closed with a valid result certificate. Duplicate completion is permitted by the runtime but consumes an agent action and can be detected from recent events in G. Decompose and Solve (DS). The root begins open while children s1,…,s4s_1,…,s_4 are latent. A legal decomposition activates the children. Their exact values must sum to 1010, and the aggregate certificate must retain the child identifiers. Direct root completion before decomposition lacks the required support relation. Compatible Merge (CM). Three independent components with values 0.20.2, 0.30.3, and 0.50.5 support an aggregate root of 1.01.0. The merge is justified only if all support components are current and certified. Dependency Ladder (DL). Only d0d_0 is initially open. The remaining nodes are blocked until all predecessors close. Completing a blocked node still creates an observable event, but its work assertion is unsupported. Repair Verification (RV). The graph requires a value-77 draft and check, followed by a value-88 repair and final result. Check and repair items use versioned validators. Evidence with version 11 is stale after the required version becomes 22. Capability Assignment (CA). Four independent roots encode math, search, code, and review. Ground-truth capability tables are fixed before evaluation. For example, the best agents for math, search, and code have probabilities 0.940.94, 0.950.95, and 0.960.96; review is best assigned to agent_2 with probability 0.880.88. A work item is stable when no declared feasible agent improves expected contribution by more than ϵ=0.05ε=0.05. C.4 Systems and Observable Projections System Projection Intervention Operational distinction MAS-Only none no shared worker policy without monitoring Interaction-only G yes detects duplicate actions and stalls from event history Task-only Q yes detects dependencies, incomplete submission, and beneficial reassignment LLM-Judge trace yes free-form trace judge; no direct Q or Π access iCORE-Observe (G,Q,Π)(G,Q, ) no exact passive measurement of both iCORE components iCORE-Audit (G,Q,Π)(G,Q, ) yes structured diagnosis, recommended repair, and frozen-set preview guard Table 5: Evaluated systems. iCORE-Observe and iCORE-Audit intentionally share the same measurement projection. For every proposed action, the evaluator first creates an unreviewed proposal state and records measurement predictions on that same state. Only then does the selected system review or modify the action. This proposal-probe protocol prevents iCORE-Audit from receiving artificially easy labels after it repairs a defect. iCORE-Audit diagnoses duplicate work, assignments more than ϵε below the best declared agent, blocked dependencies, missing evidence, incomplete submission, and unsupported closed work. It evaluates the recommended successor on the same frozen work set. A candidate that reduces frozen-set soundness or iCORE quality is replaced with wait; the diagnosis remains visible to the next decision. This explains why nondecreasing matched intervention quality is an enforced guard property rather than an unconstrained empirical coincidence. C.5 Controlled Proposal Backend Every controlled system uses the same SharedPolicyMLP: a 12→32→32→112→ 32→ 32→ 1 network with ReLU activations. Its twelve candidate features are enabled status, assigned-to-self, unassigned, prerequisites ready, aggregate ready, evidence available, current-agent capability, best capability, already complete, duplicate risk, audit recommendation, and terminal-submit readiness. The checkpoint is trained on 8,0008,000 synthetic feature vectors for 2020 epochs with batch size 256256, AdamW learning rate 2×10−32× 10^-3, weight decay 10−410^-4, and binary cross entropy. A deterministic keyed Gaussian jitter with standard deviation 0.0250.025 breaks exact score ties. If the checkpoint is absent, the implementation falls back to the fixed linear score recorded in models.py; the supplied run used the trained checkpoint. The controlled JUDGE condition cannot call a language model. Its review surrogate selects the first diagnosed alternative with probability 0.700.70 and otherwise selects a keyed random alternative. The real-LLM JUDGE condition instead uses the separate judge prompt below. C.6 Real-LLM Backend and Prompts Reporting prompt templates is standard and useful for reproducibility in LLM-agent experiments. We therefore include the exact system strings and the JSON payload schemas used by the artifact. The LLM does not generate arbitrary tools or free-form work products. It selects one candidate from the finite list constructed by the environment. Consequently, this suite tests orchestration and monitor feedback under an LLM decision policy; it is not an open-ended natural-language problem-solving benchmark. Worker system prompt. ⬇ You are one cooperative worker in a multi-agent graph task. Choose exactly one listed action. Return JSON only as "candidate_index": <integer>, "reasoning": "brief". <environment description from the YAML specification> Worker user payload. ⬇ "observation": "agent": <agent id>, "round": <integer>, "max_rounds": <integer>, "own_assignments": <list>, "messages": <last five messages>, "feedback": <monitor message or null> , "candidate_actions": [ "index": <integer>, "action": <structured action>, "description": <candidate description>, ... ] Trace-judge system prompt. ⬇ You are a process judge. Select the safest action index using only the provided observable trace summary. Return JSON only as "candidate_index": <integer>. Trace-judge user payload. ⬇ "trace_summary": "round": <integer>, "events": <last 12 events>, "proposed_action": <structured action>, "alternatives": <up to eight structured actions> The local model is Qwen/Qwen2.5-0.5B-Instruct, accessed through the OpenAI-compatible vLLM endpoint. Decoding uses temperature 0, at most 160160 completion tokens, and JSON-object response format. The server log records vLLM 0.26.00.26.0, bfloat16 weights, maximum sequence length 40964096, tensor parallel size 11, asynchronous scheduling, prefix caching, chunked prefill, and GPU-memory utilization 0.850.85. It records one CUDA rank with 47.3747.37 GiB visible memory, but not the GPU product name; we therefore do not infer a hardware SKU from the log. The checkpoint occupies approximately 0.930.93 GiB. The default endpoint is http://127.0.0.1:8000/v1. C.7 Fault Injection and Theory-Boundary Conditions The controlled main suite uses the following conditions. • Clean: no explicit action fault. • Missing evidence: completion, merge, repair, or verification loses its evidence with probability 0.650.65. • Misassignment: assignment or reassignment is redirected to the least capable declared agent with probability 0.750.75. • Verifier delay: relevant certificates become available two rounds later. • Stall: a proposed action becomes wait with probability 0.300.30. The real-LLM mixed condition combines missing evidence, misassignment, and stall with a common probability scale of 0.550.55, yielding probabilities 0.65×0.550.65× 0.55, 0.75×0.550.75× 0.55, and 0.30×0.550.30× 0.55. Fault draws use stable keyed randomness, so system-specific calls do not shift the perturbation schedule. The boundary suite changes assumptions rather than merely increasing random noise. DV accepts a wrong result with probability 0.650.65, breaking validator adequacy. SC cyclically permutes declared capability values while retaining the original ground-truth success probabilities, breaking calibration. WP scales both true and declared capabilities by 0.550.55, weakening the feasible-agent floor. These variants are used to delimit Proposition 4, not to claim robustness under arbitrary assumption violations. C.8 Metrics For an active or frozen work set, the implementation computes weighted fractions sndD(X) _D(X) =∑wωw 1[w is justified]∑wωw, = _w _w\,1[w is justified] _w _w, astabD,ϵ(X) _D,ε(X) =∑wωw 1[gain(w)≤ϵ]∑wωw. = _w _w\,1[gain(w)≤ε] _w _w. and cqD,ϵ(X)=(sndD(X)+astabD,ϵ(X))/2cq_D,ε(X)=(snd_D(X)+astab_D,ε(X))/2. The paper macros define the same quantities; the displayed indicator notation here is only an implementation-level restatement. Trajectory metrics average state scores over all recorded rounds. Conditional performance sums the ground-truth success probability of each currently assigned, justified component and normalizes by active work weight. It is the empirical conditional expectation corresponding to the proposition. Terminal performance is the realized weighted correctness of required roots. Terminal violation indicates a submitted but invalid terminal state. Completion indicates that all required roots were closed before the round limit. The certified bound is 2max(pmin−ϵ,0)[cqD,ϵ(X)−1/2]+.2 (p_ -ε,0)\,[cq_D,ε(X)-1/2]_+. A single terminal realization below this expectation bound is not a theorem violation; the appropriate empirical comparison is between conditional-performance means and the bound within quality bins. C.9 Measurement Reconstruction Controlled Real LLM System Sound. F1 Reassign. F1 |CQ^−CQ|| CQ-CQ| Sound. F1 Reassign. F1 |CQ^−CQ|| CQ-CQ| MAS-Only 0.000 0.000 0.291 0.000 0.000 0.412 Interaction-only 0.810 0.000 0.234 0.952 0.000 0.337 Task-only 0.000 1.000 0.071 0.000 1.000 0.052 LLM-Judge 0.592 0.047 0.196 0.640 0.031 0.298 iCORE-Observe 1.000 1.000 0.000 1.000 1.000 0.000 iCORE-Audit 1.000 1.000 0.000 1.000 1.000 0.000 Table 6: Proposal-probe reconstruction results across controlled and real-LLM execution. Table 6 gives all proposal-probe results. FULL-state reconstruction is exact in both modes. TASK reconstructs assignment defects but cannot validate certificate-backed work assertions. INT detects many event-visible soundness failures but has no access to capability comparisons. JUDGE is noisy on both components. MAS predicts no defects and is included as a zero-information reference. C.10 Quality–Performance Relationship Figure 2: Controlled conditional performance by iCORE-quality bin. Shaded regions are bootstrap 95%95\% confidence intervals; the dashed curve is the mean certified lower bound. The controlled figure uses trajectory states from TASK, iCORE-O, and iCORE-A. At the zero-bound quality bin, both the performance estimate and bound are zero for iCORE-A. For every reported bin with positive certified bound, the lower endpoint of the performance interval remains above that bound. This is the assumption-aligned empirical check of Proposition 4; terminal performance is analyzed separately. C.11 Environment-Level Paired Gains Figure 3: Paired trajectory-CQ gain of iCORE-Audit over iCORE-Observe by environment. Error bars are bootstrap 95%95\% confidence intervals. Real-LLM bars exist only for BC, DS, and CA. The mean controlled gain is positive in all six environments: 0.1140.114 (BC), 0.0870.087 (DS), 0.1200.120 (CM), 0.0970.097 (DL), 0.1030.103 (RV), and 0.1670.167 (CA). Real-LLM gains are 0.2280.228 (BC), 0.3710.371 (DS), and 0.1940.194 (CA). These are paired process-quality effects and do not imply that every environment reaches a valid terminal submission. C.12 Ablations Variant Sound. Assign. CQ Term. Perf. Full 1.000 0.637 0.818 1.000 Sound.-only 1.000 0.350 0.675 0.944 Assign.-only 0.840 0.621 0.730 0.694 No Π 0.840 0.621 0.730 0.694 No cert. val. 0.847 0.622 0.735 0.657 Table 7: Controlled mixed-condition ablations over six environments (90 episodes total). Figure 4: Controlled mixed-condition ablations. SO retains only soundness diagnoses, AO retains only beneficial-reassignment diagnoses, −Π- removes ledger visibility, and NC disables certificate validation in review. Full iCORE-A achieves soundness 1.0001.000, assignment stability 0.6370.637, CQ 0.8180.818, conditional performance 0.8650.865, and terminal performance 1.0001.000. SO preserves soundness but reduces assignment stability to 0.3500.350. AO preserves more assignment stability (0.6210.621) but allows soundness to fall to 0.8400.840. The −Π- and NC variants reduce CQ to 0.7300.730 and 0.7350.735 and terminal performance to 0.6940.694 and 0.6570.657. AO and −Π- have identical aggregate scores in this matrix; this tie should not be presented as evidence that the two mechanisms are equivalent beyond the current generator. C.13 Boundary of the Performance Claim Boundary CQ Cond. Perf. Term. Perf. Completed Standard 0.818 0.865 1.000 1.000 Degraded val. 0.812 0.865 0.704 0.944 Shuffled cap. 0.825 0.723 0.833 0.778 Weak pool 0.807 0.442 0.519 0.333 Table 8: iCORE-Audit in the controlled theory-boundary suite (144 episodes across iCORE-Observe and iCORE-Audit). Figure 5: iCORE-Audit quality and realized terminal performance under standard and theory-boundary conditions. DV, SC, and WP denote degraded validator, shuffled declared capabilities, and weak pool. The boundary suite illustrates why iCORE quality requires the proposition’s external adequacy assumptions. DV leaves CQ near the standard value (0.8120.812 versus 0.8180.818) while terminal performance falls from 1.0001.000 to 0.7040.704, because invalid evidence can be accepted. WP similarly retains CQ 0.8070.807 while terminal performance falls to 0.5190.519, because all available agents are weak. SC produces CQ 0.8250.825 and terminal performance 0.8330.833 by decoupling declared and true capabilities. These are expected boundary failures, not counterexamples to a claim made without those assumptions. C.14 Execution Cost Mode System Wall (s) Model calls Prompt tok. Completion tok. Verifier calls Certificates Controlled MAS-Only 0.016 16.30 0.0 0.0 4.26 8.81 Interaction-only 0.018 16.62 0.0 0.0 4.52 9.16 Task-only 0.017 15.96 0.0 0.0 4.39 9.02 LLM-Judge 0.020 16.52 0.0 0.0 4.71 9.37 iCORE-Observe 0.018 16.30 0.0 0.0 4.26 8.81 iCORE-Audit 0.026 17.47 0.0 0.0 3.59 7.87 Real LLM MAS-Only 2.608 14.67 5776.4 764.8 8.22 12.11 Interaction-only 2.763 14.72 5799.9 762.6 8.28 12.17 Task-only 2.658 15.28 5981.6 731.6 7.22 11.33 LLM-Judge 3.010 14.78 5858.3 762.4 8.22 12.11 iCORE-Observe 2.672 14.67 5776.4 758.9 8.22 12.11 iCORE-Audit 3.131 18.17 6543.3 877.2 4.33 9.67 Table 9: Per-episode execution-cost means. Controlled token counts are zero because the shared MLP does not tokenize prompts. Wall time is implementation- and hardware-specific and is not used as a quality metric. Figure 6: Mean real-LLM wall time per episode. The shared local server, model, and decoding configuration are fixed across systems. iCORE-A requires 0.0260.026 seconds per controlled episode versus 0.0180.018 for iCORE-O, an approximately 49%49\% relative increase but only 0.0090.009 seconds absolute. In the local real-LLM run, the corresponding values are 3.1313.131 and 2.6722.672 seconds, an approximately 17%17\% increase. iCORE-A makes more model decisions because recovery can extend a trace, but successful structured repair reduces mean verifier calls from 8.228.22 to 4.334.33 and certificates from 12.1112.11 to 9.679.67 relative to iCORE-O. Wall time depends on the local server, compilation cache, and hardware and is therefore reported as an implementation cost rather than a general latency claim. C.15 Statistical Tests Mode Metric Pairs Min. gain Max. pHp_H Controlled CQ 90 0.060 1.13e-09 Controlled Cond. Perf. 90 0.193 2.73e-07 Controlled Term. Perf. 90 0.118 8.71e-03 Real LLM CQ 18 0.168 7.30e-03 Real LLM Cond. Perf. 18 0.361 2.30e-03 Real LLM Term. Perf. 18 0.171 3.41e-02 Table 10: One-sided paired Wilcoxon tests for iCORE-Audit against each of the five baselines. Holm correction is applied jointly over 15 comparisons within each execution mode. The table reports the least favorable adjusted result. Each target–baseline comparison uses the same materialized episode keys across systems and is paired on environment, condition, and boundary. Controlled tests have 9090 pairs; real-LLM tests have 1818. We use the one-sided alternative that iCORE-A is greater and Holm-adjust all 1515 comparisons within each mode. The compact table reports the smallest mean gain and largest adjusted p-value across the five baselines for each metric. The full baseline-specific CSV is included with the generated package. C.16 Reproducibility and Limitations The artifact stores complete per-episode JSON objects containing G, Q, Π , trajectories, proposal probes, predictions, interventions, metrics, and costs. Figure source CSVs and table source CSVs are included. The plotting and table scripts supplied with the artifact write to new output directories and never overwrite the original experiment code or results. Two limitations constrain interpretation. First, the real-LLM test covers only BC, DS, and CA with a 0.50.5B model, so its scope across task families and model scales remains limited. Second, the LLM selects from environment-generated candidate actions whose structured fields include task values and evidence templates; it does not independently solve the underlying numerical or semantic task. These limitations are compatible with the paper’s narrower claim: a coupled representation makes the target process properties measurable, and state-grounded auditing can use that measurement to guard and repair graph-structured cooperation. Appendix D Proofs D.1 Proof of Theorem 2 Lemma 1 (Indistinguishability on a projection fiber). Let C be a class of states, let ϱ:→ :C be an observation map, and let :→0,1 P:C→\0,1\ be a Boolean property. Suppose that there exist X+,X−∈X^+,X^- such that ϱ(X+)=ϱ(X−),(X+)=1,(X−)=0. (X^+)= (X^-), P(X^+)=1, P(X^-)=0. Then no monitor whose decision depends only on ϱ(X) (X) can be both sound and complete for P on C. Proof. A monitor restricted to the observation ϱ(X) (X) is a map M:→0,1M:C→\0,1\ for which there exists a decision rule M^:→0,1 M:Y→\0,1\ satisfying M(X)=M^(ϱ(X))M(X)= M ( (X) ) for every X∈X . We use the convention that M(X)=1M(X)=1 means that the monitor declares that P holds at X. Soundness therefore requires M(X)=1⟹(X)=1M(X)=1 P(X)=1 for every X∈X , whereas completeness requires (X)=1⟹M(X)=1 P(X)=1 M(X)=1 for every X∈X . Assume, for contradiction, that such a monitor is both sound and complete. Since ϱ(X+)=ϱ(X−), (X^+)= (X^-), the restriction of M to ϱ gives M(X+) M(X^+) =M^(ϱ(X+)) = M ( (X^+) ) =M^(ϱ(X−)) = M ( (X^-) ) =M(X−). =M(X^-). Thus the monitor must return the same Boolean value on X+X^+ and X−X^-. Denote this common value by b∈0,1b∈\0,1\. If b=1b=1, then M(X−)=1.M(X^-)=1. Soundness would imply (X−)=1, P(X^-)=1, contradicting the assumption (X−)=0. P(X^-)=0. If instead b=0b=0, then M(X+)=0.M(X^+)=0. However, since (X+)=1, P(X^+)=1, completeness requires M(X+)=1,M(X^+)=1, which is again a contradiction. Since the common output must be either zero or one and both possibilities contradict one of the two required guarantees, no monitor depending only on ϱ(X) (X) can be both sound and complete for P. ∎ Proof of Theorem 2. Let C be the class of iCORE states appearing in the theorem. For a iCORE state X=(G,Q,Π),X=(G,Q, ), with G=(VG,EG,sG,tG,θG,λG,τG,μG),G=(V_G,E_G,s_G,t_G, _G, _G, _G, _G), define its unlabeled cooperation-graph topology by Top(X)=[(VG,EG,sG,tG)]≅,Top(X)= [(V_G,E_G,s_G,t_G) ]_ , where [⋅]≅[·]_ denotes the directed-graph isomorphism class obtained after discarding vertex and edge identifiers together with all types, observable labels, logical times, metadata, agent identities, capability evidence, verifier information, and monitor annotations. In particular, Top(X)Top(X) retains only the incidence structure of the cooperation graph and contains no information from the obligation graph Q or the audit map Π . By assumption, C contains two states with identical unlabeled cooperation-graph topology for which one of the properties named in the theorem has different truth values. Choose such states and denote them by X+=(G+,Q+,Π+)andX−=(G−,Q−,Π−),X^+=(G^+,Q^+, ^+) X^-=(G^-,Q^-, ^-), where X+X^+ satisfies the differing property and X−X^- does not. The assumed identity of their unlabeled topologies means Top(X+)=Top(X−).Top(X^+)=Top(X^-). If the differing property is work soundness, define ws(X)=[X is work-sound]. P_ws(X)=1 [X is work-sound ]. By Definition 7, this is equivalently ws(X)=[sndD(X)=1]. P_ws(X)=1 [snd_D(X)=1 ]. The choice of X+X^+ and X−X^- then gives ws(X+)=1andws(X−)=0. P_ws(X^+)=1 P_ws(X^-)=0. Consequently, the property ws P_ws is not constant on the fiber Top−1(Top(X+)).Top^-1 (Top(X^+) ). This difference cannot be recovered from the unlabeled topology. Indeed, work soundness requires that, for every decision-relevant component q∈(X)q (X), every active decision-relevant assertion associated with q be justified by observable interaction, a declared work operation, and evidence valid under V. In terms of the state representation, evaluating the indicator JD(q;X)J_D(q;X) requires the semantic status, obligation, coverage, and support information stored in Q, together with the event–work correspondence π, operation label ω, and certificate information κ stored in Π=(π,ω,κ). =(π,ω,κ). Accordingly, sndD(X)=∑q∈(X)wqJD(q;X)∑q∈(X)wqsnd_D(X)= _q (X)w_qJ_D(q;X) _q (X)w_q when (X)≠∅W(X)≠ depends on information that is absent from Top(X)Top(X). Two states can therefore have the same directed incidence pattern in G while differing in whether a work assertion is linked to the correct event, whether the corresponding operation is declared, whether the required certificate exists, whether that certificate is valid and active, or whether the asserted work is an actual decision-relevant obligation. The hypothesis of the theorem selects precisely such a pair for which these erased distinctions change the truth value of work soundness. If the differing property is instead agent-assignment stability, define as(X)=[X is agent-assignment stable]. P_as(X)=1 [X is agent-assignment stable ]. By Definition 9, this is equivalently as(X)=[astabD,ϵ(X)=1]. P_as(X)=1 [astab_D,ε(X)=1 ]. The selected states satisfy as(X+)=1andas(X−)=0. P_as(X^+)=1 P_as(X^-)=0. Hence as P_as is likewise not constant on a fiber of TopTop. More explicitly, for each q∈(X)q (X), assignment stability requires evaluation of maxm∈ℱD(q,X)ΔD(m←αQ(q);q,X)≤ϵ, _m _D(q,X) _D (m← _Q(q);q,X )≤ε, where ΔD(m←αQ(q);q,X) _D (m← _Q(q);q,X ) =vD(m,q∣X)−vD(αQ(q),q∣X). =v_D(m,q X)-v_D( _Q(q),q X). Determining the left-hand side requires the work component q, its current or recorded assignee αQ(q) _Q(q), the feasible-agent set ℱD(q,X)F_D(q,X), the declared contribution values vD(m,q∣X)v_D(m,q X), and the observable capability evidence and assignment correspondence validating those quantities. The assignee is stored in Q, while the agreement among the responsible event in G, the affected work in Q, the assignment operation, and its supporting evidence is represented through Π . None of these quantities is determined by the unlabeled incidence structure of G. Thus identical unlabeled cooperation topology is compatible with different values of maxm∈ℱD(q,X)[vD(m,q∣X)−vD(αQ(q),q∣X)] _m _D(q,X) [v_D(m,q X)-v_D( _Q(q),q X) ] and therefore with different truth values of agent-assignment stability, exactly as assumed by the theorem. Now let M be any monitor restricted to the unlabeled topology of G. By the meaning of this restriction, there must exist a function M M such that M(X)=M^(Top(X))M(X)= M (Top(X) ) for every X∈X . Therefore, M(X+) M(X^+) =M^(Top(X+)) = M (Top(X^+) ) =M^(Top(X−)) = M (Top(X^-) ) =M(X−). =M(X^-). For whichever property differs between X+X^+ and X−X^-, take =wsor=as, P= P_ws P= P_as, respectively. We then have Top(X+)=Top(X−),(X+)=1,(X−)=0.Top(X^+)=Top(X^-), P(X^+)=1, P(X^-)=0. Applying Lemma 1 with ϱ=Top =Top shows that no such monitor can be both sound and complete for P on C. The same conclusion also holds for a randomized topology-restricted monitor under zero-error soundness and completeness. If a(T)=Pr[M declares that holds|Top(X)=T],a(T)= \! [M declares that P holds\, |\,Top(X)=T ], then the common topology T=Top(X+)=Top(X−)T=Top(X^+)=Top(X^-) forces the same acceptance probability on both states. Completeness at X+X^+ requires a(T)=1a(T)=1, while soundness at X−X^- requires a(T)=0a(T)=0, which is impossible. Hence neither deterministic nor zero-error randomized access to the unlabeled cooperation-graph topology suffices to obtain both guarantees. This proves the theorem. ∎ D.2 Proof of Proposition 1 For a iCORE state X=(G,Q,Π)X=(G,Q, ), denote by D(X) A_D(X) the set of active decision-relevant work-level assertions in Q. For a∈D(X)a∈ A_D(X), write JustD(a;X)=1Just_D(a;X)=1 when there exists a finite justification for a consisting of observable interaction recorded in G, the corresponding operation labels from the declared vocabulary Ω , the event–work correspondence recorded by Π , and certificates that are active and valid under V in state X. With this notation, Definition 7 is equivalently X is work-sound⟺ X is work-sound JustD(a;X)=1 _D(a;X)=1 for every a∈D(X). every a∈ A_D(X). Lemma 2 (One-step preservation of work soundness). If X is work-sound and X→X′X→ X is a legal iCORE update, then X′X is work-sound. Proof. Fix an arbitrary assertion a∈D(X′).a∈ A_D(X ). We prove that JustD(a;X′)=1.Just_D(a;X )=1. First suppose that a was already active and decision-relevant in X and that the update changes neither the semantic content of a, its active status, its decision relevance, nor any semantic object used by one of its valid justification witnesses. Since X is work-sound, Definition 7 gives JustD(a;X)=1.Just_D(a;X)=1. Consequently, there exist a finite set of observable actions or artifacts Ha⊆VG,H_a V_G, a finite set of declared operation labels Oa⊆Ω,O_a , the corresponding event–work links represented in Π , and a finite set of certificates Ca⊆κC_a κ such that these objects jointly justify a in X. More explicitly, the nodes in HaH_a record the observable actions or artifacts responsible for the assertion, the labels in OaO_a identify the declared work operations by which those observable events affect the relevant work components, the corresponding entries of Π connect those events and operations to a, and every certificate c∈Cac∈ C_a satisfies ValidCertV(c;X)=1.ValidCert_V(c;X)=1. A legal update reads and writes only through its declared interfaces. By the present case assumption, none of the semantic objects belonging to this justification is changed by the update. Therefore every node in HaH_a, every operation label in OaO_a, every relevant event–work correspondence in Π , and every certificate in CaC_a remains present in X′X with the same semantic meaning. Moreover, every c∈Cac∈ C_a remains active, its internal premises remain present and current, its external premises continue to satisfy V, and its claim continues to pass the declared validation procedure. If any of these activity, currentness, or validation conditions changed, then the support of a would be affected and the assertion would belong to the complementary case considered below. Hence ValidCertV(c;X′)=1for every c∈Ca.ValidCert_V(c;X )=1 every c∈ C_a. The same finite collection (Ha,Oa,Ca)(H_a,O_a,C_a) together with the unchanged correspondence entries in Π is therefore a valid justification witness for a in X′X . It follows that JustD(a;X′)=1.Just_D(a;X )=1. It remains to consider the complementary case, in which a is newly created, newly activated, newly decision-relevant, semantically modified, or affected because some part of its former justification is written, revoked, superseded, invalidated, or replaced by the update. Suppose first that a is newly created, newly activated, newly decision-relevant, or semantically modified. A work-level assertion includes an asserted node, relation, status, signature, coverage fact, compatibility fact, or terminal marker. Thus creating such an assertion, changing its semantic value, or making it newly active and decision-relevant produces a new decision-relevant assertion in the successor state. By Definition 6, legality requires the update to support every such assertion using an operation permitted by D and evidence valid under V. Therefore the update must provide valid supporting evidence for a. Legality additionally requires X′∈D.X _D. By the feasibility conditions defining DX_D, every non-initial work assertion must be backed by responsible observable nodes in G, corresponding operation labels, and active valid certificates through Π , while every required initial root must remain connected to observable initial input and supporting evidence. Consequently, the support required by legality cannot consist only of an unrecorded or external assertion. It must be represented in the successor state by observable interaction in G, an operation from Ω , the corresponding event–work links in Π , and certificates valid under V. Hence JustD(a;X′)=1.Just_D(a;X )=1. Now suppose that a existed before the update but a certificate, correspondence entry, operation label, premise, or other semantic object in its former justification is revoked, superseded, invalidated, replaced, or otherwise made noncurrent. The former witness can no longer be used automatically, because the definition of certificate validity requires all certificates and premises in the witness to remain active and current. Nevertheless, legality still requires X′∈D.X _D. The feasibility conditions defining DX_D require that revoked or superseded evidence cannot continue to support an active assertion without re-certification, repair, invalidation, rejection, or supersession. They also prohibit an active assertion from depending simultaneously on a certificate and an active valid revocation of that certificate. Therefore, after the update, precisely one of the following must occur: the old assertion is made observably inactive by a valid invalidation, rejection, or supersession record, or the assertion remains active and is supplied with replacement, repaired, or re-certified support that is active and valid in X′X . The first alternative is impossible for the fixed assertion a, because a∈D(X′)a∈ A_D(X ) means that a is active and decision-relevant in the successor state. Hence the second alternative must hold. There therefore exist responsible observable nodes in G′G , corresponding declared operation labels, event–work links in Π′ , and active certificates valid under V that jointly support a in X′X . Thus JustD(a;X′)=1.Just_D(a;X )=1. The assertion a∈D(X′)a∈ A_D(X ) was arbitrary. We have proved ∀a∈D(X′),JustD(a;X′)=1.∀ a∈ A_D(X ), _D(a;X )=1. Definition 7 therefore implies that X′X is work-sound. ∎ Proof of Proposition 1. Let X0→X1→X2→⋯X_0→ X_1→ X_2→·s be an arbitrary admissible process. By the definition of admissibility, every transition Xn→Xn+1X_n→ X_n+1 is a legal iCORE update. We prove by induction on n∈ℕn that every state XnX_n is work-sound. The base case is immediate from the hypothesis: X0 is work-sound.X_0 is work-sound. Now let n≥0n≥ 0 and assume that Xn is work-sound.X_n is work-sound. Since the process is admissible, the transition Xn→Xn+1X_n→ X_n+1 is legal. Applying Lemma 2 with X=XnandX′=Xn+1X=X_n X =X_n+1 gives Xn+1 is work-sound.X_n+1 is work-sound. The induction therefore yields ∀n∈ℕ,Xn is work-sound.∀ n , X_n is work-sound. Equivalently, for every n and every component q∈(Xn),q (X_n), all active decision-relevant assertions associated with q are justified. Hence JD(q;Xn)=1for every q∈(Xn).J_D(q;X_n)=1 every q (X_n). When (Xn)=∅,W(X_n)= , the definition of the work-soundness score directly gives sndD(Xn)=1.snd_D(X_n)=1. When (Xn)≠∅,W(X_n)≠ , we obtain sndD(Xn) _D(X_n) =∑q∈(Xn)wqJD(q;Xn)∑q∈(Xn)wq = _q (X_n)w_qJ_D(q;X_n) _q (X_n)w_q =∑q∈(Xn)wq⋅1∑q∈(Xn)wq = _q (X_n)w_q· 1 _q (X_n)w_q =∑q∈(Xn)wq∑q∈(Xn)wq = _q (X_n)w_q _q (X_n)w_q =1. =1. The denominator is strictly positive because the index set is nonempty and every predeclared importance weight satisfies wq>0.w_q>0. Thus every state occurring in the admissible process is work-sound. Finally, let Y be any state reached from X0X_0 by an admissible process. By the definition of reachability, there exists a finite admissible prefix X0→X1→⋯→Xn=YX_0→ X_1→·s→ X_n=Y for some n∈ℕn . The induction result gives that XnX_n is work-sound, and therefore Y is work-sound.Y is work-sound. The same reasoning applies when the complete admissible process is infinite, because every state reached along an infinite process occurs at some finite index. Hence every state reached by an admissible process from X0X_0 is work-sound. ∎ D.3 Proof of Proposition 2 For an admissible process X0→ρ0X1→ρ1X2→ρ2⋯,Xi=(Gi,Qi,Πi),X_0 _0X_1 _1X_2 _2·s, X_i=(G_i,Q_i, _i), write the ordered audit entry of the transition Xi→ρiXi+1X_i _iX_i+1 as i=(ρi,ΔiG,ΔiQ,ΔiΠ), r_i= ( _i, _i^G, _i^Q, _i ), where ρi _i identifies the legal update occurrence and ΔiG _i^G, ΔiQ _i^Q, and ΔiΠ _i record all of its semantic effects on the three components of the iCORE state. Thus these effects include every created or removed node and edge, every changed semantic label, status, signature, or assignment, every created, revoked, or superseded certificate, and every changed event–work or operation correspondence. Fields declared inessential by D, such as a choice of fresh identifiers or an inessential timestamp, need not be reproduced literally. The order of the entries is the commit order of the process, equivalently the order in which the corresponding state transitions occur. Lemma 3 (Replay uniqueness modulo declared equivalence). Let ℜ=(0,1,…) R=( r_0, r_1,…) be the ordered audit record of an admissible process from the fixed initial state X0X_0. Any replay of ℜ R from a representative X^0≡X0 X_0 _XX_0 produces states X^i X_i satisfying X^i≡XXi X_i _XX_i for every recorded index i. Consequently, any two state sequences consistent with the same record are pointwise equivalent under ≡X _X. Proof. We argue by induction on the number of replayed entries. At index zero, the replay is initialized with a representative satisfying X^0≡X0, X_0 _XX_0, so the claim holds before any update is replayed. Suppose that, for some i≥0i≥ 0, the replay has already produced a state X^i X_i for which X^i≡XXi. X_i _XX_i. By the definition of the declared state equivalence, there are transported type-preserving graph isomorphisms between the G- and Q-components of these states, together with the induced transport of Π , and these transports preserve every field that may affect update enablement, feasibility, obligations, assignments, capability evidence, certificate validity, or terminal decisions. Transport the recorded occurrence ρi _i along these isomorphisms and denote the transported occurrence by ρ^i ρ_i. Because the semantic read objects, statuses, signatures, operation labels, correspondence entries, and certificate premises are preserved, the complete local views agree up to the same transport: L(ρ^i;X^i)≅L(ρi;Xi).L( ρ_i; X_i) L( _i;X_i). The occurrence ρi _i is legal at XiX_i, because the original process is admissible. Hence every object and certificate premise required by ρi _i is present and current in L(ρi;Xi)L( _i;X_i), the operation is permitted by D, every new semantic assertion has active valid support, and the recorded successor is Xi+1=R^ρi(Xi)∈D.X_i+1= R_ _i(X_i) _D. The transported equality of local views implies that the same enablement and validation tests hold for ρ^i ρ_i at X^i X_i. Moreover, declared state equivalence is required to be a congruence for legal updates. Therefore the transported occurrence is legal and its successor satisfies X^i+1=R^ρ^i(X^i)≡XR^ρi(Xi)=Xi+1. X_i+1= R_ ρ_i( X_i) _X R_ _i(X_i)=X_i+1. The recorded effects ΔiG _i^G, ΔiQ _i^Q, and ΔiΠ _i determine all semantic writes of this occurrence. Since an update occurrence induces a partial function on DX_D, a replay consistent with the entry cannot choose a different semantic successor; it may differ only in fields that D declares inessential. This proves the induction step, and thus X^i≡XXi X_i _XX_i for every finite index i. The argument applies without change to an infinite record, because every state at a finite index is determined by a finite prefix. Finally, if (X^i)i( X_i)_i and (X~i)i( X_i)_i are two replays of the same record, then X^i≡XXiandX~i≡XXi, X_i _XX_i X_i _XX_i, and symmetry and transitivity of ≡X _X give X^i≡X~i X_i _X X_i for every i. ∎ Lemma 4 (Finite backward explanation of terminal-cover work). Let X0→ρ0X1→ρ1⋯→ρN−1XNX_0 _0X_1 _1·s _N-1X_N be a finite admissible process with Acc(XN)=1Acc(X_N)=1, and let A⊆Accepted(QN)A (Q_N) be the certified terminal cover used by the acceptance predicate. For every component a∈Aa∈ A, there exists a finite explanation substructure consisting of recorded interaction objects from the cooperation graphs, recorded work objects and transformations from the obligation graphs, and the corresponding restriction of the audit maps, such that the explanation contains the accepted status and terminal-cover role of a, connects every non-initial work assertion in the explanation to responsible observable interaction and active valid evidence, and reaches an observable initial input through the required-root coverage and support structure. Proof. Fix a∈Aa∈ A. Since Acc(XN)=1Acc(X_N)=1, the terminal-state conditions in Appendix A.6 imply that XNX_N is feasible, that a has status accepted, that the accepted components in A jointly cover every effective required root with the compatibility evidence required by V, and that no accepted component depends on unresolved, invalid, rejected, contradictory, or unrepaired work. Let N(a) S_N(a) be the finite set containing the assertion statQN(a)=accepted,stat_Q_N(a)= accepted, the active result and signature assertions of a used by the terminal decision, the coverage assertions by which a participates in the certified terminal cover, and the compatibility assertions involving a that are used by the joint terminal-cover certificate. This set is finite because QNQ_N, ΠN _N, and every certificate record are finite. We first expose the work-side connection to the input. Because a belongs to the certified terminal cover, its terminal-cover evidence identifies the effective required root or roots whose discharge uses a. For each such root r, the coverage semantics provide a finite coverage path in QNQ_N from r to a; schematically, r=q0⪯QNcovq1⪯QNcov⋯⪯QNcovqℓ=a.r=q_0 _Q_N^covq_1 _Q_N^cov·s _Q_N^covq_ =a. If an intermediate work component occurring in the selected terminal support is not itself a required root, feasibility supplies a finite support chain ending at a required root or a declared input node. We add the nodes, semantic relations, statuses, signatures, coverage facts, and support facts on these finitely many selected chains to N(a) S_N(a). Every required root reached in this way is connected, by feasibility, to an observable initial-input node and a supporting certificate. Any auxiliary external premise is not treated as hidden support: by Appendix A.3, it enters only through a declared environment-input node in G and an active valid certificate. Thus the work-side support of a is anchored at the declared observable input boundary and, through the required-root branch of the terminal cover, at the initial input. It remains to show that every assertion on these work chains can be expanded into a finite recorded cross-layer explanation. We construct a backward audit slice. At a generic transition Xi→ρiXi+1,X_i _iX_i+1, consider a finite set i+1 S_i+1 of semantic objects and assertions in Xi+1X_i+1 that are currently required by the explanation. Partition it as i+1=i∪i, S_i+1= U_i∪ W_i, where i U_i contains the objects that were already present in XiX_i with the same semantic value and remained unchanged by ρi _i, while i W_i contains the objects created, activated, semantically modified, re-certified, repaired, or otherwise supplied with their current support by the transition. Objects in i U_i can simply be carried to the preceding state. For an object or assertion z∈iz∈ W_i, the update is legal, so the current semantic value of z cannot have been introduced without the support required by D and V. In particular, the relevant part of the recorded update contains observable action or artifact nodes g∈VGi+1g∈ V_G_i+1, a declared operation label ωi+1(g)∈Ω _i+1(g)∈ , an event–work correspondence q∈πi+1(g),q∈ _i+1(g), and certificates in κi+1 _i+1 that are active and valid for the claim being introduced or maintained. For every such certificate c, ValidCertV(c;Xi+1)=1.ValidCert_V(c;X_i+1)=1. We add these recorded G-objects, Q-effects, operation labels, correspondence entries, and certificates to the explanation. We then place into i S_i the objects and premises from the pre-update local view L(ρi;Xi)L( _i;X_i) that are needed to enable and validate this relevant part of the update. Formally, it is sufficient to set i=i∪⋃z∈iPremi(z), S_i= U_i∪ _z∈ W_iPrem_i(z), where Premi(z)Prem_i(z) denotes the subset of L(ρi;Xi)L( _i;X_i) used by the declared operation and validators to support z. If the implementation does not separately mark the minimal subset, we may take Premi(z)=L(ρi;Xi),Prem_i(z)=L( _i;X_i), which is still finite by the finite-interface and finite-ancestry requirements. This construction also covers changes of evidence. If support formerly used by a required assertion is revoked, superseded, or made noncurrent, feasibility prohibits that assertion from remaining active unless it is re-certified, repaired, invalidated, rejected, or superseded. Since the assertions in the selected terminal explanation remain active and support an accepted component, the invalidation or rejection alternative cannot be the terminal support used for a. The backward slice therefore follows the recorded replacement, repair, re-certification, or valid supersession chain. Internal certificate premises are added to the slice; external premises terminate at their declared environment-input nodes. The active certificate-dependency graph is acyclic, so expanding the certificates occurring within one state or one update cannot create an infinite regress. Likewise, the cooperation graph is a finite directed acyclic graph, so adding the causal ancestors of a responsible event adds only finitely many observable actions and artifacts. Starting with the finite seed N(a) S_N(a) and applying the preceding construction successively for i=N−1,N−2,…,0i=N-1,N-2,…,0 produces finite sets i S_i at every stage. The update index strictly decreases whenever the construction asks for pre-update premises, so after exactly N backward transitions no further process history remains to be traversed. The remaining objects lie in the fixed initial state X0X_0. Feasibility of X0X_0 connects every required root to an observable initial input and gives every non-root initial work object a finite support chain ending at such a root or at a declared input node. Adding these initial anchors closes the explanation. Let Ia⊆0,1,…,N−1I_a \0,1,…,N-1\ be the set of update indices whose entries were included by the backward slice, and let ℰaE_a be the union of the selected initial objects, selected local-view premises, selected update effects, selected causal ancestors in G, selected work chains in Q, and selected restrictions of Π and κ. Its size is bounded by |ℰa|≤|X0|+∑i∈Ia(|L(ρi;Xi)|+|ΔiG|+|ΔiQ|+|ΔiΠ|),|E_a|≤|X_0|+ _i∈ I_a (|L( _i;X_i)|+| _i^G|+| _i^Q|+| _i | ), and the right-hand side is finite because IaI_a is finite and every state, local interface, update effect, and certificate record is finite. By construction, every selected work transformation is paired through the selected audit-map entries with the observable event and declared operation that justified it, every selected certificate premise is represented and validated, the explanation begins at the observable input anchors, and it ends at the accepted terminal assertions of a. Thus ℰaE_a is the required finite explanation. ∎ Proof of Proposition 2. Let X0→ρ0X1→ρ1X2→ρ2⋯X_0 _0X_1 _1X_2 _2·s be the legal process represented by the record. The declaration package fixes X0X_0, and the hypothesis supplies the ordered entry i r_i for every committed transition. Lemma 3 therefore shows, by replaying the entries from X0X_0, that the record determines every state XiX_i up to ≡X _X. It also shows uniqueness: any other state sequence compatible with the same initial state and the same recorded updates and effects is pointwise equivalent to the original sequence. Hence the record reconstructs the complete sequence of iCORE states up to the declared observational equivalence. For an infinite process, this statement is understood pointwise, since every finite-index state is reconstructed from a finite record prefix. Now suppose that the process is finite and accepted, so that for some N<∞N<∞ its final state satisfies Acc(XN)=1.Acc(X_N)=1. Let A be the certified terminal cover used by the acceptance predicate and fix an arbitrary a∈Aa∈ A. Lemma 4 constructs a finite explanation ℰaE_a whose G-part contains the responsible observable interaction events and artifacts, whose Q-part contains the relevant work components and transformations, and whose Π -part records the operation, event–work, and certificate correspondence connecting those two parts. The explanation is anchored at the observable initial input and terminates at the accepted status, coverage role, and compatibility support of a. Since a was arbitrary, every accepted component in the terminal cover has such a finite explanation. This proves both claims. ∎ D.4 Proof of Corollary 1 Proof. Consider the sequence of states produced by the committed updates of the execution. This sequence has the form X0→ρ0X1→ρ1X2→ρ2⋯,X_0 _0X_1 _1X_2 _2·s, where the index set of states is either ℐ=0,1,…,NI=\0,1,…,N\ for some finite execution, or ℐ=ℕI=N for an infinite execution. For every index n∈ℐn such that n+1∈ℐn+1 , the transition Xn→ρnXn+1X_n _nX_n+1 is a committed update. By hypothesis, every committed update is legal. Hence Xn→Xn+1is a legal iCORE updateX_n→ X_n+1 a legal iCORE update for every such n. It follows directly from the definition of an admissible process that the committed-state sequence is an admissible process beginning at X0X_0. Candidate updates that are rejected, blocked, aborted, or otherwise not committed do not occur as transitions in this sequence and therefore do not change any state reached by the process. The initial state is work-sound by hypothesis. Proposition 1 states that every state reached from a work-sound initial state by an admissible process is work-sound. Applying that proposition to the committed-state sequence gives Xn is work-soundfor every n∈ℐ.X_n is work-sound every n . Equivalently, for every n∈ℐn and every active decision-relevant work-level assertion a∈D(Xn),a∈ A_D(X_n), there exists a justification consisting of observable interaction recorded in GnG_n, declared operation labels from Ω , the corresponding event–work relations recorded by Πn _n, and certificates that are active and valid under V in XnX_n. In the notation used in Appendix D.2, JustD(a;Xn)=1for every a∈D(Xn).Just_D(a;X_n)=1 every a∈ A_D(X_n). Thus every state reached by the execution is work-sound, and Definition 7 therefore implies that the entire committed process is work-sound. It remains to verify the conditions governing the emitted terminal reports. Let e be an arbitrary terminal-report occurrence in the execution, and let Xn(e)X_n(e) denote the current committed state when e is emitted. Such a state exists even when no update has yet been committed, in which case n(e)=0n(e)=0 and the current state is X0X_0. Because Xn(e)X_n(e) belongs to the committed-state sequence, the preceding argument gives Xn(e) is work-sound.X_n(e) is work-sound. Suppose first that the report occurrence e emits Accept. The reporting hypothesis states that the execution emits Accept only when the acceptance predicate holds at the current state. Therefore, e=Accept⟹Acc(Xn(e)).e= Accept (X_n(e) ). In particular, the execution cannot emit Accept at a state for which Acc(Xn(e))Acc (X_n(e) ) is false. Notice that this conclusion is not inferred merely from work soundness: work soundness justifies the active decision-relevant assertions, whereas AccAcc additionally requires complete settlement of the effective required roots, a certified compatible terminal cover, the absence of unresolved relevant work and supported failures, and the absence of a live productive artifact that can change the outcome. These additional terminal conditions are supplied precisely by the assumed acceptance guard. Suppose instead that e emits Reject. The corresponding reporting hypothesis states that the execution emits Reject only when the rejection predicate holds at the current state. Hence, e=Reject⟹Rej(Xn(e)).e= Reject (X_n(e) ). Consequently, the execution cannot emit Reject at a state for which Rej(Xn(e))Rej (X_n(e) ) is false. As in the acceptance case, this implication is imposed by the terminal-report guard rather than by work soundness alone. The report occurrence e was arbitrary. We have therefore established that every terminal-report occurrence satisfies e=Accept⟹Acc(Xn(e))e= Accept (X_n(e) ) and e=Reject⟹Rej(Xn(e)).e= Reject (X_n(e) ). Together with the fact that every state in the committed process is work-sound, these are exactly the conditions in Definition 8. Hence the process is terminal-report sound. The argument applies equally to finite and infinite executions, because every report in an infinite execution occurs after a finite committed prefix and is therefore associated with some state XnX_n covered by the preceding reasoning. ∎ D.5 Proof of Proposition 3 Proof. Let :X0→X1→⋯→XN p:X_0→ X_1→·s→ X_N be the process under consideration. The process is finite because terminal completeness is defined for a finite process. Write Xi=(Gi,Qi,Πi)(0≤i≤N).X_i=(G_i,Q_i, _i) (0≤ i≤ N). Since the process is work-sound, Definition 7 gives Xi is work-soundfor every i∈0,1,…,N.X_i is work-sound every i∈\0,1,…,N\. Equivalently, using the notation introduced in Appendix D.2, for every active decision-relevant assertion b∈D(Xi)b∈ A_D(X_i) we have JustD(b;Xi)=1.Just_D(b;X_i)=1. Thus every accepted or rejected status, every coverage or compatibility claim, every failure claim, every exclusion, duplication, irrelevance, or supersession claim used to determine the effective required roots, and every terminal-support assertion that is active and decision-relevant at any reported state is connected through Πi _i to observable interaction in GiG_i, a declared operation, and evidence active and valid under V. In particular, the terminal predicates cannot be supported by an unrecorded work assertion or by evidence that is inactive, revoked, superseded, noncurrent, or invalid under V. Let e be an arbitrary emitted Accept or Reject report, and let Xn(e)X_n(e) be the current committed state when e is emitted. Because e occurs after a finite prefix of p, its index satisfies n(e)∈0,1,…,N.n(e)∈\0,1,…,N\. For readability, set Xe=Xn(e),Qe=Qn(e).X^e=X_n(e), Q^e=Q_n(e). The preceding work-soundness conclusion applies to XeX^e. Suppose first that e=Accept.e= Accept. Terminal-report soundness implies that an Accept report may be emitted only at a state satisfying the declared acceptance predicate. Hence e=Accept⟹Acc(Xe).e= Accept (X^e). Unfolding Acc(Xe)Acc(X^e) from Appendix A.6, there exists a set Ae⊆Accepted(Qe)A_e (Q^e) that forms a certified terminal cover of EffRoot(Xe)EffRoot(X^e). Therefore EffRoot(Xe)⊆⋃a∈AeCovQe(a),EffRoot(X^e) _a∈ A_eCov_Q^e(a), and the joint compatibility evidence required by V exists for the components in AeA_e. The other clauses of the acceptance predicate give EffUnres(Xe)=∅EffUnres(X^e)= and EffRoot(Xe)∩FailRoot(Xe)=∅.EffRoot(X^e) (X^e)= . They also ensure that no accepted component depends on unresolved, invalid, rejected, contradictory, or unrepaired work, and ensure that no live productive artifact can change the discharge, failure, exclusion, or compatibility of an effective root. Consequently, the cover is terminal rather than merely provisional: every effective required root is discharged by accepted work, no effective required root simultaneously carries an unneutralized supported failure, no unresolved relevant work remains, and no still-live productive artifact can alter the reported outcome. It remains to verify that the terminal cover just described is genuinely certified under V, rather than merely having the correct set-theoretic shape. Every assertion that a component belongs to Accepted(Qe)Accepted(Q^e), every active coverage assertion used in CovQe(a)Cov_Q^e(a), every compatibility assertion used to combine the members of AeA_e, and every active assertion used to remove a root from EffRoot(Xe)=ReqRoot(Qe)∖OffXe(Qe)EffRoot(X^e)=ReqRoot(Q^e) _X^e(Q^e) is decision-relevant to the Accept report. Since XeX^e is work-sound, each such assertion has a justification through observable interaction, a declared operation, the correspondence recorded by Πn(e) _n(e), and active evidence valid under V. Hence no required root is silently omitted: a root is absent from EffRoot(Xe)EffRoot(X^e) only when its duplicated, excluded, irrelevant, or superseded status is supported by active valid evidence. It follows that AeA_e is a V-certified accepted terminal cover in precisely the sense used by task adequacy. By the first clause of task adequacy, every V-certified accepted terminal cover yields a semantically correct accepted output for the declared task class. Applying that clause to AeA_e shows that the output certified by AeA_e is semantically correct. Therefore the emitted decision e=Accepte= Accept is semantically correct for the declared task class. Notice that validator adequacy is essential here: work soundness proves that the acceptance evidence is valid according to V, while task adequacy is what permits the further inference from validity under V to correctness under the task semantics. Suppose instead that e=Reject.e= Reject. Terminal-report soundness now gives e=Reject⟹Rej(Xe).e= Reject (X^e). Define Fe=EffRoot(Xe).F_e=EffRoot(X^e). Unfolding the rejection predicate yields Fe≠∅,EffUnres(Xe)=∅,F_e≠ , (X^e)= , and Fe⊆FailRoot(Xe).F_e (X^e). Because Fe=EffRoot(Xe)F_e=EffRoot(X^e), the last inclusion states that every effective required root has active valid rejection, invalidity, impossibility, or unreachability evidence and has no valid repair neutralizing that failure. The rejection predicate also gives Fe∩Dis(Qe)=∅F_e (Q^e)= and states that no live productive artifact can repair, accept, discharge, or reopen any root in FeF_e. Thus the reported failure is complete over the effective requirement set, is not contradicted by a valid discharge of any of those roots, and cannot still be changed by remaining productive work. Each active failure assertion used to place a root in FailRoot(Xe)FailRoot(X^e), together with each exclusion or supersession assertion used to determine FeF_e, is decision-relevant to the Reject report. Work soundness of XeX^e therefore supplies, for every r∈Fer∈ F_e, observable interaction in Gn(e)G_n(e), a declared work operation, the corresponding entries in Πn(e) _n(e), and active evidence valid under V supporting the asserted failure of r. Moreover, the definition of FailRoot(Xe)FailRoot(X^e) excludes any root whose failure has been neutralized by a valid repair. Hence FeF_e is a V-certified failed-root set, not merely a set of roots carrying unsupported failure labels. By the second clause of task adequacy, every V-certified failed-root set of this kind justifies rejection for the declared task class. Applying that clause to FeF_e proves that the decision e=Rejecte= Reject is semantically correct. The detectability clause in task adequacy is consistent with both cases above: any process-relevant defect in required-root coverage, compatibility, evidence, or terminal settlement must be detectable under V, and therefore cannot be hidden behind a purportedly certified terminal cover or failed-root set. Without this clause, a process could be internally sound relative to an incomplete validator while still missing a task-relevant defect. The report occurrence e was arbitrary. Let SemCorrectD(e)SemCorrect_D(e) denote that the report e is semantically correct for the task class declared by D. We have proved e=Accept⟹SemCorrectD(e)e= Accept _D(e) and e=Reject⟹SemCorrectD(e)e= Reject _D(e) for every emitted Accept or Reject report. It remains to identify what terminal completeness permits when neither semantic decision is reported. Since p is terminally complete, its final state XNX_N satisfies Acc(XN)∨Rej(XN)∨CertStuckV(,XN),Acc(X_N)\; \;Rej(X_N)\; \;CertStuck_V( p,X_N), where CertStuckV(,XN)CertStuck_V( p,X_N) abbreviates the existence of valid evidence certifying that the process is externally stuck at XNX_N. The acceptance and rejection predicates cannot both hold. Indeed, Rej(XN)Rej(X_N) would imply EffRoot(XN)≠∅EffRoot(X_N)≠ and EffRoot(XN)⊆FailRoot(XN),EffRoot(X_N) (X_N), whereas Acc(XN)Acc(X_N) would imply EffRoot(XN)∩FailRoot(XN)=∅.EffRoot(X_N) (X_N)= . These relations would force EffRoot(XN)=∅,EffRoot(X_N)= , contradicting the nonemptiness required by Rej(XN)Rej(X_N). Thus an accepted terminal decision and a rejected terminal decision are mutually exclusive. If terminal completeness is witnessed instead by external stuckness, then by definition there exists valid evidence certifying that the cooperation process cannot presently continue because of an external process condition. Denote one such certificate by cstuckc_stuck. Its validity means ValidCertV(cstuck;XN)=1,ValidCert_V(c_stuck;X_N)=1, and its claim is that the process is externally stuck at XNX_N. Because the process is work-sound, any active decision-relevant terminal-status assertion supported by this certificate is also connected through ΠN _N to the relevant observable events and declared operation. This validates the reported process status. It does not, however, provide either a V-certified accepted terminal cover or a V-certified failed-root set. The definition of task adequacy licenses semantic acceptance only from the former and semantic rejection only from the latter. External stuckness may arise from unavailable tools, permissions, resources, communication, or other process conditions without establishing that the task output is correct or that the task itself is semantically impossible. Therefore no Accept or Reject conclusion follows from external stuckness alone, and an externally stuck report is valid only as the certified status of the cooperation process. This proves the proposition. ∎ D.6 Proof of Theorem 1 Proof. Let :=(X).W:=W(X). By assumption, ≠∅W≠ , and the component weights are normalized so that ∑q∈wq=1. _q w_q=1. Define the set of ϵε-stable components by ϵ(X):=q∈:maxm∈ℱD(q,X)ΔD(m←αQ(q);q,X)≤ϵ,S_ε(X):= \q : _m _D(q,X) _D (m← _Q(q);q,X )≤ε \, and define its complement in W by ℛϵ(X):=∖ϵ(X).R_ε(X):=W _ε(X). Hence, =ϵ(X)∪˙ℛϵ(X).W=S_ε(X)\, ∪\,R_ε(X). By the definition of the assignment-stability score and the normalization ∑q∈wq=1 _q w_q=1, we have astabD,ϵ(X) _D,ε(X) =∑q∈wq[q∈ϵ(X)]∑q∈wq = _q w_q1 [q _ε(X) ] _q w_q =∑q∈wq[q∈ϵ(X)] = _q w_q1 [q _ε(X) ] =∑q∈ϵ(X)wq. = _q _ε(X)w_q. It follows that ∑q∈ℛϵ(X)wq _q _ε(X)w_q =∑q∈wq−∑q∈ϵ(X)wq = _q w_q- _q _ε(X)w_q =1−astabD,ϵ(X). =1-astab_D,ε(X). Now fix an arbitrary componentwise feasible alternative assignment β, so that β(q)∈ℱD(q,X)∪⊥for every q∈.β(q) _D(q,X)∪\ \ every q . For each q∈q , define the componentwise utility gain gq:=vD(β(q),q∣X)−vD(αQ(q),q∣X).g_q:=v_D(β(q),q X)-v_D( _Q(q),q X). Using the definition of UDU_D, the aggregate gain produced by β can be written exactly as UD(β∣X)−UD(αQ∣X) U_D(β X)-U_D( _Q X) =∑q∈wqvD(β(q),q∣X)−∑q∈wqvD(αQ(q),q∣X) = _q w_qv_D(β(q),q X)- _q w_qv_D( _Q(q),q X) =∑q∈wq(vD(β(q),q∣X)−vD(αQ(q),q∣X)) = _q w_q (v_D(β(q),q X)-v_D( _Q(q),q X) ) =∑q∈wqgq = _q w_qg_q =∑q∈ϵ(X)wqgq+∑q∈ℛϵ(X)wqgq. = _q _ε(X)w_qg_q+ _q _ε(X)w_qg_q. Consider any component q∈ϵ(X).q _ε(X). If β(q)∈ℱD(q,X),β(q) _D(q,X), then, by the definition of the counterfactual assignment gain, gq g_q =vD(β(q),q∣X)−vD(αQ(q),q∣X) =v_D(β(q),q X)-v_D( _Q(q),q X) =ΔD(β(q)←αQ(q);q,X). = _D (β(q)← _Q(q);q,X ). Because β(q)β(q) is an element of ℱD(q,X)F_D(q,X), its gain cannot exceed the maximum gain over that feasible set. Therefore, gq g_q =ΔD(β(q)←αQ(q);q,X) = _D (β(q)← _Q(q);q,X ) ≤maxm∈ℱD(q,X)ΔD(m←αQ(q);q,X). ≤ _m _D(q,X) _D (m← _Q(q);q,X ). Since q∈ϵ(X)q _ε(X), the defining inequality of ϵε-stability gives maxm∈ℱD(q,X)ΔD(m←αQ(q);q,X)≤ϵ. _m _D(q,X) _D (m← _Q(q);q,X )≤ε. Combining the preceding two inequalities yields gq≤ϵ.g_q≤ε. If instead β(q)=⊥,β(q)= , then the convention vD(⊥,q∣X)=0v_D( ,q X)=0 gives gq g_q =vD(⊥,q∣X)−vD(αQ(q),q∣X) =v_D( ,q X)-v_D( _Q(q),q X) =−vD(αQ(q),q∣X). =-v_D( _Q(q),q X). Since declared component values are nonnegative, vD(αQ(q),q∣X)≥0,v_D( _Q(q),q X)≥ 0, and hence gq≤0.g_q≤ 0. Because ϵ≥0ε≥ 0, it follows that gq≤0≤ϵ.g_q≤ 0≤ε. Thus, regardless of whether β(q)β(q) is a feasible agent or ⊥ , gq≤ϵfor every q∈ϵ(X).g_q≤ε every q _ε(X). Now consider any component q∈ℛϵ(X).q _ε(X). Although no ϵε-stability guarantee is available for such a component, the normalization of the declared values implies 0≤vD(β(q),q∣X)≤1.0≤ v_D(β(q),q X)≤ 1. Indeed, this follows directly from the range of vDv_D when β(q)∈ℱD(q,X)β(q) _D(q,X), while for β(q)=⊥β(q)= it follows from vD(⊥,q∣X)=0v_D( ,q X)=0. Similarly, 0≤vD(αQ(q),q∣X)≤1.0≤ v_D( _Q(q),q X)≤ 1. Therefore, gq g_q =vD(β(q),q∣X)−vD(αQ(q),q∣X) =v_D(β(q),q X)-v_D( _Q(q),q X) ≤1−0 ≤ 1-0 =1. =1. Hence, gq≤1for every q∈ℛϵ(X).g_q≤ 1 every q _ε(X). Substituting the two componentwise bounds into the decomposition of the aggregate gain, and using wq>0w_q>0, gives UD(β∣X)−UD(αQ∣X) U_D(β X)-U_D( _Q X) =∑q∈ϵ(X)wqgq+∑q∈ℛϵ(X)wqgq = _q _ε(X)w_qg_q+ _q _ε(X)w_qg_q ≤∑q∈ϵ(X)wqϵ+∑q∈ℛϵ(X)wq ≤ _q _ε(X)w_qε+ _q _ε(X)w_q =ϵ∑q∈ϵ(X)wq+∑q∈ℛϵ(X)wq. =ε _q _ε(X)w_q+ _q _ε(X)w_q. Using ∑q∈ϵ(X)wq=astabD,ϵ(X) _q _ε(X)w_q=astab_D,ε(X) and ∑q∈ℛϵ(X)wq=1−astabD,ϵ(X), _q _ε(X)w_q=1-astab_D,ε(X), we obtain UD(β∣X)−UD(αQ∣X) U_D(β X)-U_D( _Q X) ≤ϵastabD,ϵ(X)+1−astabD,ϵ(X) ≤ _D,ε(X)+1-astab_D,ε(X) =1−astabD,ϵ(X)+ϵastabD,ϵ(X) =1-astab_D,ε(X)+ _D,ε(X) =1−(1−ϵ)astabD,ϵ(X). =1-(1-ε)astab_D,ε(X). This proves the first claim. Finally, suppose that X is agent-assignment stable. By definition, astabD,ϵ(X)=1.astab_D,ε(X)=1. Substituting this identity into the established bound gives UD(β∣X)−UD(αQ∣X) U_D(β X)-U_D( _Q X) ≤1−(1−ϵ)⋅1 ≤ 1-(1-ε)· 1 =ϵ. =ε. Since β was an arbitrary componentwise feasible joint reassignment, no feasible joint reassignment can improve the declared aggregate value by more than ϵε. ∎ D.7 Proof of Proposition 4 Proof. Fix a iCORE state X satisfying the assumptions of the proposition, and write =(X).W=W(X). Because assumption (i) requires normalized weights over W, the evaluated work set is nonempty and the weights satisfy wq>0for every q∈,∑q∈wq=1.w_q>0 every q , _q w_q=1. By the weighted decomposition of task performance in assumption (i), there exist nonnegative random component contributions Yq≥0Y_q≥ 0, indexed by q∈q , such that Perf=∑q∈wqYq.Perf= _q w_qY_q. For every q∈q , define Jq=JD(q;X)∈0,1J_q=J_D(q;X)∈\0,1\ and Sq=[q is ϵ-stable at X]∈0,1.S_q=1\! [q is $ε$-stable at X ]∈\0,1\. Equivalently, by Definition 9, Sq=[maxm∈ℱD(q,X)ΔD(m←αQ(q);q,X)≤ϵ].S_q=1\! [ _m _D(q,X) _D(m← _Q(q);q,X)≤ε ]. Since the state X is fixed, the quantities JqJ_q, SqS_q, αQ(q) _Q(q), ℱD(q,X)F_D(q,X), and vD(m,q∣X)v_D(m,q X) are deterministic under the conditional expectation given X. We first relate the expected task contribution of each component to the declared contribution value of its current or recorded assignee. Suppose that Jq=1J_q=1. Then every active decision-relevant assertion associated with q is justified under the declared validator. Since V is task-adequate, such a justified component is semantically valid for the task-performance decomposition. If αQ(q)≠⊥ _Q(q)≠ , the calibration assumption therefore gives [Yq∣X]≥vD(αQ(q),q∣X).E[Y_q X]≥ v_D( _Q(q),q X). If αQ(q)=⊥ _Q(q)= , then the convention vD(⊥,q∣X)=0v_D( ,q X)=0 and the nonnegativity of YqY_q give [Yq∣X]≥0=vD(αQ(q),q∣X).E[Y_q X]≥ 0=v_D( _Q(q),q X). Thus, whenever Jq=1J_q=1, [Yq∣X]≥vD(αQ(q),q∣X).E[Y_q X]≥ v_D( _Q(q),q X). When Jq=0J_q=0, the nonnegativity of YqY_q implies [Yq∣X]≥0,E[Y_q X]≥ 0, while JqvD(αQ(q),q∣X)=0.J_qv_D( _Q(q),q X)=0. Consequently, for every q∈q , regardless of whether q is justified, [Yq∣X]≥JqvD(αQ(q),q∣X).E[Y_q X]≥ J_qv_D( _Q(q),q X). Using the weighted decomposition of PerfPerf and linearity of conditional expectation, we obtain [Perf∣X] [Perf X] =[∑q∈wqYq|X] =E\! [ _q w_qY_q\, |\,X ] =∑q∈wq[Yq∣X] = _q w_qE[Y_q X] ≥∑q∈wqJqvD(αQ(q),q∣X). ≥ _q w_qJ_qv_D( _Q(q),q X). We next derive a uniform lower bound on the declared value of every ϵε-stable component. Fix an arbitrary q∈q for which Sq=1S_q=1. Assumption (iv) states that q has at least one feasible agent whose declared value is at least pminp_ . Hence, there exists an agent mq⋆∈ℱD(q,X)m_q _D(q,X) such that vD(mq⋆,q∣X)≥pmin.v_D(m_q ,q X)≥ p_ . Since Sq=1S_q=1, component q is ϵε-stable, and therefore maxm∈ℱD(q,X)ΔD(m←αQ(q);q,X)≤ϵ. _m _D(q,X) _D(m← _Q(q);q,X)≤ε. By the definition of the reassignment gain, ΔD(m←αQ(q);q,X)=vD(m,q∣X)−vD(αQ(q),q∣X). _D(m← _Q(q);q,X)=v_D(m,q X)-v_D( _Q(q),q X). Substituting this definition into the stability condition yields maxm∈ℱD(q,X)vD(m,q∣X)−vD(αQ(q),q∣X)≤ϵ. _m _D(q,X) \v_D(m,q X)-v_D( _Q(q),q X) \≤ε. Because mq⋆∈ℱD(q,X)m_q _D(q,X), its reassignment gain cannot exceed the maximum over the feasible-agent set. Thus, vD(mq⋆,q∣X)−vD(αQ(q),q∣X) v_D(m_q ,q X)-v_D( _Q(q),q X) ≤maxm∈ℱD(q,X)vD(m,q∣X)−vD(αQ(q),q∣X) ≤ _m _D(q,X) \v_D(m,q X)-v_D( _Q(q),q X) \ ≤ϵ. ≤ε. Rearranging this inequality gives vD(αQ(q),q∣X)≥vD(mq⋆,q∣X)−ϵ.v_D( _Q(q),q X)≥ v_D(m_q ,q X)-ε. Using the lower bound vD(mq⋆,q∣X)≥pmin,v_D(m_q ,q X)≥ p_ , we conclude that vD(αQ(q),q∣X)≥pmin−ϵ.v_D( _Q(q),q X)≥ p_ -ε. In particular, an ϵε-stable component cannot be unassigned under the assumptions of the proposition. Indeed, if αQ(q)=⊥ _Q(q)= , then vD(αQ(q),q∣X)=vD(⊥,q∣X)=0,v_D( _Q(q),q X)=v_D( ,q X)=0, and hence ΔD(mq⋆←⊥;q,X) _D(m_q ← ;q,X) =vD(mq⋆,q∣X)−vD(⊥,q∣X) =v_D(m_q ,q X)-v_D( ,q X) =vD(mq⋆,q∣X) =v_D(m_q ,q X) ≥pmin ≥ p_ >ϵ, >ε, which would contradict the ϵε-stability of q. We have therefore shown that Sq=1⟹vD(αQ(q),q∣X)≥pmin−ϵ.S_q=1 v_D( _Q(q),q X)≥ p_ -ε. If Sq=0S_q=0, then (pmin−ϵ)Sq=0,(p_ -ε)S_q=0, and the range condition vD(αQ(q),q∣X)∈[0,1]v_D( _Q(q),q X)∈[0,1] again gives vD(αQ(q),q∣X)≥(pmin−ϵ)Sq.v_D( _Q(q),q X)≥(p_ -ε)S_q. Consequently, the inequality vD(αQ(q),q∣X)≥(pmin−ϵ)Sqv_D( _Q(q),q X)≥(p_ -ε)S_q holds for every q∈q . Multiplying both sides by the nonnegative indicator JqJ_q gives JqvD(αQ(q),q∣X)≥(pmin−ϵ)JqSq.J_qv_D( _Q(q),q X)≥(p_ -ε)J_qS_q. Substituting this componentwise bound into the preceding lower bound on conditional task performance yields [Perf∣X] [Perf X] ≥∑q∈wqJqvD(αQ(q),q∣X) ≥ _q w_qJ_qv_D( _Q(q),q X) ≥(pmin−ϵ)∑q∈wqJqSq. ≥(p_ -ε) _q w_qJ_qS_q. It remains to lower-bound the total normalized weight of the components that are simultaneously justified and ϵε-stable. Since Jq,Sq∈0,1J_q,S_q∈\0,1\, one has (1−Jq)(1−Sq)≥0.(1-J_q)(1-S_q)≥ 0. Expanding the left-hand side gives 1−Jq−Sq+JqSq≥0,1-J_q-S_q+J_qS_q≥ 0, and therefore JqSq≥Jq+Sq−1.J_qS_q≥ J_q+S_q-1. Multiplying by wq>0w_q>0 and summing over q∈q gives ∑q∈wqJqSq _q w_qJ_qS_q ≥∑q∈wq(Jq+Sq−1) ≥ _q w_q(J_q+S_q-1) =∑q∈wqJq+∑q∈wqSq−∑q∈wq. = _q w_qJ_q+ _q w_qS_q- _q w_q. Since the weights are normalized, ∑q∈wq=1. _q w_q=1. Moreover, by the definition of work soundness and the fact that ≠∅W≠ , sndD(X)=∑q∈wqJD(q;X)∑q∈wq=∑q∈wqJq.snd_D(X)= _q w_qJ_D(q;X) _q w_q= _q w_qJ_q. Similarly, by the definition of agent-assignment stability, astabD,ϵ(X)=∑q∈wq[q is ϵ-stable at X]∑q∈wq=∑q∈wqSq.astab_D,ε(X)= _q w_q1[q is $ε$-stable at X] _q w_q= _q w_qS_q. Hence, ∑q∈wqJqSq≥sndD(X)+astabD,ϵ(X)−1. _q w_qJ_qS_q _D(X)+astab_D,ε(X)-1. On the other hand, every term wqJqSqw_qJ_qS_q is nonnegative, so ∑q∈wqJqSq≥0. _q w_qJ_qS_q≥ 0. Combining these two inequalities gives ∑q∈wqJqSq≥max0,sndD(X)+astabD,ϵ(X)−1. _q w_qJ_qS_q≥ \0,\,snd_D(X)+astab_D,ε(X)-1 \. Equivalently, ∑q∈wqJqSq≥[sndD(X)+astabD,ϵ(X)−1]+. _q w_qJ_qS_q≥ [snd_D(X)+astab_D,ε(X)-1 ]_+. Therefore, [Perf∣X] [Perf X] ≥(pmin−ϵ)∑q∈wqJqSq ≥(p_ -ε) _q w_qJ_qS_q ≥(pmin−ϵ)[sndD(X)+astabD,ϵ(X)−1]+. ≥(p_ -ε) [snd_D(X)+astab_D,ε(X)-1 ]_+. By Definition 10, cqD,ϵ(X)=12(sndD(X)+astabD,ϵ(X)),cq_D,ε(X)= 12 (snd_D(X)+astab_D,ε(X) ), and therefore sndD(X)+astabD,ϵ(X)=2cqD,ϵ(X).snd_D(X)+astab_D,ε(X)=2cq_D,ε(X). Substituting this identity into the preceding bound gives [Perf∣X] [Perf X] ≥(pmin−ϵ)[2cqD,ϵ(X)−1]+ ≥(p_ -ε) [2cq_D,ε(X)-1 ]_+ =(pmin−ϵ)[2(cqD,ϵ(X)−12)]+. =(p_ -ε) [2 (cq_D,ε(X)- 12 ) ]_+. Since 2>02>0, the positive-part operator satisfies [2z]+=2[z]+[2z]_+=2[z]_+ for every z∈ℝz . Applying this identity with z=cqD,ϵ(X)−12z=cq_D,ε(X)- 12 finally yields [Perf∣X]≥2(pmin−ϵ)[cqD,ϵ(X)−12]+.E[Perf X]≥ 2(p_ -ε) [cq_D,ε(X)- 12 ]_+. This is the claimed performance implication. ∎ D.8 Proof of Proposition 5 Proof. Let X(0),X(1),X(2),…X^(0),X^(1),X^(2),… denote the actual sequence of states retained by Algorithm 1, with X(0)=X0.X^(0)=X_0. Tentative states such as X~ X and intervention proposals such as XfX_f that fail their corresponding audits are not members of this sequence, because they are never committed. The failure and feedback records retained by the algorithm are themselves represented as legal iCORE updates and do not install the rejected candidate assertions. Hence every transition X(k)⟶X(k+1)X^(k) X^(k+1) in the retained sequence is a legal iCORE update under the hypotheses of the proposition. We first prove that every retained state is work-sound. We proceed by induction on k. The initial state is work-sound by assumption, and therefore X(0)=X0X^(0)=X_0 is work-sound. Now fix an arbitrary k≥0k≥ 0 and suppose that X(k)X^(k) is work-sound. Since X(k)⟶X(k+1)X^(k) X^(k+1) is a legal iCORE update, Lemma 2 applies with X=X(k)andX′=X(k+1).X=X^(k) X =X^(k+1). It follows that X(k+1)X^(k+1) is work-sound. The induction therefore gives X(k) is work-sound for every retained index k.X^(k) is work-sound for every retained index k. In particular, the conclusion holds after both an ordinary commitment and an intervention commitment. For a committed intervention, the same conclusion is also certified directly by AuditRecoveryDAuditRecovery_D, because the recovery audit accepts an intervention candidate only when the candidate is legal and work-sound. Thus every committed state produced by Algorithm 1 is work-sound. It remains to establish that quality is nondecreasing on the matched audit set whenever an intervention is committed. Consider an arbitrary committed intervention. Let X−X^- denote the state immediately before the diagnosis, and write F=DiagnoseD(X−),F=MatchedSetD(X−,F).F=Diagnose_D(X^-), _F=MatchedSet_D(X^-,F). Let XfX_f be the labeled intervention state proposed in response to F. Since this intervention is committed, its recovery audit returns no violation: AuditRecoveryD(X−,Xf,F,F)=∅.AuditRecovery_D (X^-,X_f,F,W_F )= . Let X+=CommitD(Xf)X^+=Commit_D(X_f) denote the state retained after the successful intervention. Commitment changes the audited proposal from tentative to retained but does not alter the semantic contents of G, Q, or Π on which the matched-set indicators depend. Hence, for every q∈Fq _F, JDF(q;X+)=JDF(q;Xf)J_D^F(q;X^+)=J_D^F(q;X_f) and AD,ϵF(q;X+)=AD,ϵF(q;Xf).A_D,ε^F(q;X^+)=A_D,ε^F(q;X_f). Consequently, cqD,ϵ(X+;F)=cqD,ϵ(Xf;F).cq_D,ε(X^+;W_F)=cq_D,ε(X_f;W_F). By construction, the set FW_F and all of its weights are frozen before the diagnosis is supplied to the responsible agent. Therefore the intervention cannot alter the cohort or the weights on which the pre-intervention and post-intervention scores are evaluated. Moreover, every q∈Fq _F is transported from X−X^- to X+X^+ through the identity, refinement, replacement, supersession, or settlement relations declared by D. For brevity, define Jq− J_q^- =JDF(q;X−), =J_D^F(q;X^-), Jq+ J_q^+ =JDF(q;X+), =J_D^F(q;X^+), Aq− A_q^- =AD,ϵF(q;X−), =A_D,ε^F(q;X^-), Aq+ A_q^+ =AD,ϵF(q;X+). =A_D,ε^F(q;X^+). Suppose first that F=∅.W_F= . By the empty-set convention in the matched-set definitions, sndD(X−;F)=1snd_D(X^-;W_F)=1 and astabD,ϵ(X−;F)=1.astab_D,ε(X^-;W_F)=1. The same convention gives sndD(X+;F)=1snd_D(X^+;W_F)=1 and astabD,ϵ(X+;F)=1.astab_D,ε(X^+;W_F)=1. It follows that cqD,ϵ(X−;F) _D,ε(X^-;W_F) =12(sndD(X−;F)+astabD,ϵ(X−;F)) = 12 (snd_D(X^-;W_F)+astab_D,ε(X^-;W_F) ) =12(1+1) = 12(1+1) =1 =1 and, similarly, cqD,ϵ(X+;F) _D,ε(X^+;W_F) =12(sndD(X+;F)+astabD,ϵ(X+;F)) = 12 (snd_D(X^+;W_F)+astab_D,ε(X^+;W_F) ) =12(1+1) = 12(1+1) =1. =1. Therefore cqD,ϵ(X+;F)=cqD,ϵ(X−;F),cq_D,ε(X^+;W_F)=cq_D,ε(X^-;W_F), so the required nondecrease holds with equality when the matched audit set is empty. Now suppose that F≠∅.W_F≠ . Define the frozen total matched weight by WF=∑q∈Fwq.W_F= _q _Fw_q. Every predeclared importance weight satisfies wq>0.w_q>0. Since FW_F is nonempty, it follows that WF>0.W_F>0. Using the matched-set definitions, the pre-intervention soundness score is sndD(X−;F)=∑q∈FwqJq−WF,snd_D(X^-;W_F)= _q _Fw_qJ_q^-W_F, and the corresponding assignment-stability score is astabD,ϵ(X−;F)=∑q∈FwqAq−WF.astab_D,ε(X^-;W_F)= _q _Fw_qA_q^-W_F. Therefore cqD,ϵ(X−;F) _D,ε(X^-;W_F) =12(sndD(X−;F)+astabD,ϵ(X−;F)) = 12 (snd_D(X^-;W_F)+astab_D,ε(X^-;W_F) ) =12(∑q∈FwqJq−WF+∑q∈FwqAq−WF) = 12 ( _q _Fw_qJ_q^-W_F+ _q _Fw_qA_q^-W_F ) =12WF(∑q∈FwqJq−+∑q∈FwqAq−) = 12W_F ( _q _Fw_qJ_q^-+ _q _Fw_qA_q^- ) =12WF∑q∈Fwq(Jq−+Aq−). = 12W_F _q _Fw_q (J_q^-+A_q^- ). The same expansion for the committed successor gives cqD,ϵ(X+;F) _D,ε(X^+;W_F) =12(sndD(X+;F)+astabD,ϵ(X+;F)) = 12 (snd_D(X^+;W_F)+astab_D,ε(X^+;W_F) ) =12(∑q∈FwqJq+WF+∑q∈FwqAq+WF) = 12 ( _q _Fw_qJ_q^+W_F+ _q _Fw_qA_q^+W_F ) =12WF∑q∈Fwq(Jq++Aq+). = 12W_F _q _Fw_q (J_q^++A_q^+ ). Because AuditRecoveryD(X−,Xf,F,F)=∅AuditRecovery_D (X^-,X_f,F,W_F )= and because the recovery audit enforces the matched-set conditions of Algorithm 1, the accepted intervention satisfies cqD,ϵ(Xf;F)≥cqD,ϵ(X−;F).cq_D,ε(X_f;W_F) _D,ε(X^-;W_F). Since the matched semantic indicators of XfX_f and X+X^+ are identical, this inequality is equivalent to cqD,ϵ(X+;F)≥cqD,ϵ(X−;F).cq_D,ε(X^+;W_F) _D,ε(X^-;W_F). Substituting the two expanded expressions yields 12WF∑q∈Fwq(Jq++Aq+)≥12WF∑q∈Fwq(Jq−+Aq−). 12W_F _q _Fw_q (J_q^++A_q^+ )≥ 12W_F _q _Fw_q (J_q^-+A_q^- ). Since 2WF>0,2W_F>0, multiplication by 2WF2W_F preserves the direction of the inequality and gives ∑q∈Fwq(Jq++Aq+)≥∑q∈Fwq(Jq−+Aq−). _q _Fw_q (J_q^++A_q^+ )≥ _q _Fw_q (J_q^-+A_q^- ). Subtracting the right-hand side from the left-hand side gives ∑q∈Fwq[(Jq+−Jq−)+(Aq+−Aq−)]≥0. _q _Fw_q [ (J_q^+-J_q^- )+ (A_q^+-A_q^- ) ]≥ 0. Dividing by the positive quantity 2WF2W_F now yields cqD,ϵ(X+;F)−cqD,ϵ(X−;F) _D,ε(X^+;W_F)-cq_D,ε(X^-;W_F) =12WF∑q∈Fwq[(Jq+−Jq−)+(Aq+−Aq−)] = 12W_F _q _Fw_q [ (J_q^+-J_q^- )+ (A_q^+-A_q^- ) ] ≥0. ≥ 0. Hence cqD,ϵ(X+;F)≥cqD,ϵ(X−;F).cq_D,ε(X^+;W_F) _D,ε(X^-;W_F). The transport and no-silent-removal conditions ensure that this inequality represents an actual quality comparison rather than a change of evaluation cohort. In particular, if some q∈Fq _F is deleted without a valid identity, refinement, replacement, supersession, or settlement record, then the matched-set definition assigns JDF(q;X+)=0J_D^F(q;X^+)=0 instead of removing q and its weight from the score. A component that is discharged, rejected, replaced, or superseded receives JDF(q;X+)=1J_D^F(q;X^+)=1 only when the corresponding transport or settlement operation is supported by all evidence required by D. Likewise, a settled component receives AD,ϵF(q;X+)=1A_D,ε^F(q;X^+)=1 only when it was completed under an ϵε-stable assignment according to capability evidence available no later than settlement. Thus the intervention cannot obtain the preceding inequality merely by deleting, renaming, hiding, or retrospectively relabeling difficult work. The committed intervention was arbitrary. Therefore every committed intervention satisfies cqD,ϵ(X+;F)≥cqD,ϵ(X−;F).cq_D,ε(X^+;W_F) _D,ε(X^-;W_F). Hence iCORE-Audit is quality-nondecreasing on the matched audit set at every committed intervention. Together with the work-soundness induction, this proves both conclusions of the proposition. ∎ D.9 Proof of Theorem 3 Lemma 5 (Termination and local joinability imply global joinability). Let (,⇒)(A, ) be an abstract rewrite system such that ⇒ terminates. Then every element of A has a ⇒ -normal descendant. If, in addition, every one-step fork is joinable, in the sense that whenever A⇒B,A⇒C,A B, A C, there exists D∈D satisfying B⇒∗D,C⇒∗D.B ^*D, C ^*D. Then every pair of descendants of a common source is joinable: for all A,B,C∈A,B,C such that A⇒∗B,A⇒∗C,A ^*B, A ^*C, there exists H∈H such that B⇒∗H,C⇒∗H.B ^*H, C ^*H. Under this additional local-joinability assumption, any two normal descendants of the same element are equal. Proof. We first verify existence of normal descendants. Fix A∈A . If no normal element were reachable from A, then A itself would not be normal, so there would exist A1A_1 with A⇒A1.A A_1. The element A1A_1 would likewise have no normal descendant, because any normal descendant of A1A_1 would also be a normal descendant of A. Hence there would exist A2A_2 with A1⇒A2.A_1 A_2. Repeating the same argument would produce an infinite sequence A⇒A1⇒A2⇒A3⇒⋯,A A_1 A_2 A_3 ·s, contradicting termination. Therefore every A∈A has at least one normal descendant. We now prove global joinability by well-founded induction. Define a strict descendant relation ≺ on A by B≺A⟺A⇒+B,B A A ^+B, where ⇒+ ^+ is the transitive closure of ⇒ . Since ⇒ terminates, there is no infinite chain A0⇒+A1⇒+A2⇒+⋯,A_0 ^+A_1 ^+A_2 ^+·s, and consequently ≺ is well founded. For A∈A , let (A) P(A) denote the assertion that every two descendants of A are joinable. Assume inductively that (A′) P(A ) holds for every A′≺A A, and consider arbitrary reductions A⇒∗B,A⇒∗C.A ^*B, A ^*C. If the first reduction has length zero, then B=AB=A, and choosing H=CH=C gives B=A⇒∗C=H,C⇒∗C=H.B=A ^*C=H, C ^*C=H. The same argument applies if the second reduction has length zero. We may therefore assume that both reductions are nonempty and write their first steps as A⇒A1⇒∗B,A⇒A2⇒∗C.A A_1 ^*B, A A_2 ^*C. By the assumed joinability of every one-step fork, there exists D such that A1⇒∗D,A2⇒∗D.A_1 ^*D, A_2 ^*D. Because A⇒A1A A_1, we have A1≺A_1 A. Both B and D are descendants of A1A_1, so the induction hypothesis (A1) P(A_1) yields an element E satisfying B⇒∗E,D⇒∗E.B ^*E, D ^*E. Similarly, A2≺A_2 A, and both C and D are descendants of A2A_2. The induction hypothesis (A2) P(A_2) therefore yields an element F satisfying C⇒∗F,D⇒∗F.C ^*F, D ^*F. The element D is itself a strict descendant of A, because A⇒A1⇒∗D.A A_1 ^*D. Thus D≺AD A. Since E and F are both descendants of D, the induction hypothesis (D) P(D) gives an element H for which E⇒∗H,F⇒∗H.E ^*H, F ^*H. Combining the reductions gives B⇒∗E⇒∗HandC⇒∗F⇒∗H,B ^*E ^*H C ^*F ^*H, so B and C are joinable. This proves (A) P(A). Well-founded induction now implies (A) P(A) for every A∈A . Finally, suppose that N1N_1 and N2N_2 are normal descendants of the same element A. Global joinability provides H such that N1⇒∗H,N2⇒∗H.N_1 ^*H, N_2 ^*H. Because N1N_1 is normal, the first reduction must have length zero, and hence H=N1H=N_1. Because N2N_2 is normal, the second reduction must also have length zero, and hence H=N2H=N_2. Therefore N1=N2,N_1=N_2, which proves uniqueness of the normal descendant. ∎ Proof of Theorem 3. Let preach=[X]≡X:X is reachableX_p^reach= \[X]_ _X:X is reachable \ be the set of reachable equivalence classes, and abbreviate the productive quotient relation by A⇒B⟺A→pB,A,B∈preach.A B A _pB, A,B _p^reach. The theorem assumes that this relation terminates. We first record how the quotient relation is connected to actual legal updates. Suppose [S]≡X⇒[T]≡X.[S]_ _X [T]_ _X. By the definition of the productive quotient, there exist representatives S′S and T′T such that S′≡XS,T′≡XT,S′→T′,S′≢XT′.S _XS, T _XT, S → T , S _XT . Let ρ be the legal update occurrence realizing S′→T′S → T . Since declared state equivalence is a congruence for legal updates, ρ can be transported from S′S to any equivalent representative S^≡XS′ S _XS . The transported occurrence is enabled and legal at S S, and it produces a successor T T satisfying S^→T^,T^≡XT′. S→ T, T _XT . This transported update remains productive. Indeed, if S^≡XT S _X T, then S′≡XS^≡XT^≡XT′,S _X S _X T _XT , which would imply S′≡XT′S _XT by transitivity and contradict the productivity of S′→T′S → T . Consequently, every quotient edge can be realized by a productive legal update from any representative of its source class. Applying this observation successively gives the following path-lifting property. For every finite quotient path A0⇒A1⇒⋯⇒AkA_0 A_1 ·s A_k and every state X0′X_0 satisfying [X0′]≡X=A0,[X_0 ]_ _X=A_0, there exists a sequence of productive legal updates X0′→X1′→⋯→Xk′X_0 → X_1 →·s→ X_k such that [Xi′]≡X=Aifor every i∈0,1,…,k.[X_i ]_ _X=A_i every i∈\0,1,…,k\. This follows by induction on i: once Xi′X_i has been constructed in the class AiA_i, the next quotient edge can be transported to Xi′X_i by the preceding congruence argument, producing Xi+1′X_i+1 in the class Ai+1A_i+1. The quotient normal forms are exactly the equivalence classes of productive normal forms. To see one direction, suppose that N is a productive normal form but that [N]≡X[N]_ _X has an outgoing quotient edge. A witness for that edge would be a productive update from some state N′≡XNN _XN, and congruence would transport that update to a productive update enabled at N, contradicting normality. Conversely, if [N]≡X[N]_ _X is quotient-normal but a productive legal update N→N′N→ N is enabled, then [N]≡X⇒[N′]≡X[N]_ _X [N ]_ _X would be an outgoing quotient edge, again a contradiction. Hence N is a productive normal form⟺[N]≡X is ⇒-normal.N is a productive normal form [N]_ _X is $ $-normal. Assume first that the system is globally execution-order stable. Let X→Y,X→ZX ρY, X ηZ be an arbitrary reachable productive local critical pair. Since the quotient relation terminates, the normal-form-existence conclusion of Lemma 5 guarantees that both [Y]≡X[Y]_ _X and [Z]≡X[Z]_ _X have quotient-normal descendants. Thus there exist quotient-normal classes AYA_Y and AZA_Z such that [Y]≡X⇒∗AY,[Z]≡X⇒∗AZ.[Y]_ _X ^*A_Y, [Z]_ _X ^*A_Z. By the path-lifting property, these quotient reductions can be realized by productive legal continuations Y→∗NY,Z→∗NZ,Y→^*N_Y, Z→^*N_Z, with [NY]≡X=AY,[NZ]≡X=AZ.[N_Y]_ _X=A_Y, [N_Z]_ _X=A_Z. Because AYA_Y and AZA_Z are quotient-normal, the established normal-form correspondence implies that NYN_Y and NZN_Z are productive normal forms. Concatenating the two first updates with these continuations gives two productive continuations from the same reachable state X: X→Y→∗NY,X→Z→∗NZ.X ρY→^*N_Y, X ηZ→^*N_Z. Global execution-order stability therefore gives NY≡XNZ.N_Y _XN_Z. Equivalently, [Y]≡X⇒∗[NY]≡X,[Z]≡X⇒∗[NZ]≡X,[NY]≡X=[NZ]≡X.[Y]_ _X ^*[N_Y]_ _X, [Z]_ _X ^*[N_Z]_ _X, [N_Y]_ _X=[N_Z]_ _X. This is exactly Y↓p,≡XZ.Y _p, _XZ. Since the reachable productive local critical pair was arbitrary, every reachable productive local critical pair is productively joinable modulo ≡X _X. For the converse, assume that every reachable productive local critical pair is productively joinable modulo ≡X _X. We show that every one-step fork of the reachable productive quotient is joinable. Consider arbitrary quotient edges A⇒B,A⇒C,A B, A C, where A∈preachA _p^reach. Choose a reachable state X with A=[X]≡X.A=[X]_ _X. By the definition of the two quotient edges, each edge has a productive legal-update witness whose source is equivalent to X. Transporting both witnesses to the common representative X by congruence yields productive legal updates X→Y,X→ZX ρY, X ηZ such that B=[Y]≡X,C=[Z]≡X.B=[Y]_ _X, C=[Z]_ _X. If B=CB=C, then the quotient fork is trivially joinable by taking its common descendant to be B=CB=C. Suppose therefore that B≠CB≠ C. By the fork-classification assumption of the theorem, the reachable one-step productive fork at X is either residual-sound independent or a productive local critical pair. If the two updates are residual-sound independent, then both residual executions are defined. Hence there exist states U and V such that X→Y→ηρU,X→Z→ρηV,U≡XV.X ρY _ρU, X ηZ _ηV, U _XV. A residual update may itself be productive or stuttering. If Y→UY→ U is productive, then [Y]≡X⇒[U]≡X;[Y]_ _X [U]_ _X; if it is stuttering, then Y≡XUY _XU, so [Y]≡X=[U]≡X,[Y]_ _X=[U]_ _X, so a zero-step quotient reduction connects the same two classes. In either case, [Y]≡X⇒∗[U]≡X.[Y]_ _X ^*[U]_ _X. The identical argument gives [Z]≡X⇒∗[V]≡X.[Z]_ _X ^*[V]_ _X. Since U≡XVU _XV, we have [U]≡X=[V]≡X.[U]_ _X=[V]_ _X. Thus B=[Y]≡XB=[Y]_ _X and C=[Z]≡XC=[Z]_ _X are joinable. If instead the fork is a productive local critical pair, the present assumption gives Y↓p,≡XZ.Y _p, _XZ. By definition, there exist productive descendants Y′Y and Z′Z satisfying [Y]≡X⇒∗[Y′]≡X,[Z]≡X⇒∗[Z′]≡X,Y′≡XZ′.[Y]_ _X ^*[Y ]_ _X, [Z]_ _X ^*[Z ]_ _X, Y _XZ . Therefore [Y′]≡X=[Z′]≡X,[Y ]_ _X=[Z ]_ _X, so the quotient branches are again joinable. We have proved that every one-step fork of (preach,⇒)(X_p^reach, ) is joinable. The quotient relation terminates by hypothesis. Lemma 5 therefore applies and shows that any two quotient descendants of a common reachable class are joinable. Let X be any reachable state, and consider arbitrary productive continuations X→∗N1,X→∗N2X→^*N_1, X→^*N_2 to productive normal forms. Passing to equivalence classes gives [X]≡X⇒∗[N1]≡X,[X]≡X⇒∗[N2]≡X.[X]_ _X ^*[N_1]_ _X, [X]_ _X ^*[N_2]_ _X. The normal-form correspondence shows that both [N1]≡X[N_1]_ _X and [N2]≡X[N_2]_ _X are quotient-normal. The uniqueness conclusion of Lemma 5 therefore gives [N1]≡X=[N2]≡X.[N_1]_ _X=[N_2]_ _X. Equality of the quotient classes is equivalent to N1≡XN2.N_1 _XN_2. Since X and the two productive continuations were arbitrary, the system is globally execution-order stable. This proves the converse implication and completes the equivalence. ∎