Paper deep dive
Beyond Memory: A Transactional Continuity Kernel for Long-Lived AI Agents
Jun He, Deying Yu
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Persistent AI agents accumulate versioned state across long horizons, but storage retention alone does not identify authoritative state. Without an explicit control plane, unmediated updates by models, tools, and background workers risk stale overwrites, un-audited exposures, and self-authorizing privilege escalation. We argue that agent state governance is an infrastructural activation problem, defining continuity as an unbroken, authorized lineage of accepted branch heads. We present the Continuity Kernel (CK), an activation contract that decouples off-commit candidate evaluation from atomic state activation. Untrusted components propose typed changes against an exact predecessor head or typed absence. A short activation transaction revalidates ownership, pre-state authority, freshness, and effect uniqueness, recording one stable disposition (Commit, Reject, Quarantine, or Defer). Only Commit atomically advances the branch head and installs the complete accepted unit (state, authority, lineage, effects, outcome, and receipt). A bounded executable model verifies the protocol across 2,808,230 reachable states and 5,526,474 state-changing transitions with zero invariant violations.
Tags
Links
- Source: https://arxiv.org/abs/2608.11632v1
- Canonical: https://arxiv.org/abs/2608.11632v1
Trouble viewing inline? Open PDF directly →
Full Text
89,138 characters extracted from source content.
Expand or collapse full text
Beyond Memory: A Transactional Continuity Kernel for Long-Lived AI Agents Jun He Affiliation: OpenKedge.io Deying Yu Affiliation: OpenKedge.io Abstract Persistent AI agents accumulate versioned state across long horizons, but storage retention alone does not identify authoritative state. Without an explicit control plane, unmediated updates by models, tools, and background workers risk stale overwrites, un-audited exposures, and self-authorizing privilege escalation. We argue that agent state governance is an infrastructural activation problem, defining continuity as an unbroken, authorized lineage of accepted branch heads. We present the Continuity Kernel (CK), an activation contract that decouples off-commit candidate evaluation from atomic state activation. Untrusted components propose typed changes against an exact predecessor head or typed absence. A short activation transaction revalidates ownership, pre-state authority, freshness, and effect uniqueness, recording one stable disposition (Commit, Reject, Quarantine, or Defer). Only Commit atomically advances the branch head and installs the complete accepted unit (state, authority, lineage, effects, outcome, and receipt). A bounded executable model verifies the protocol across 2,808,230 reachable states and 5,526,474 state-changing transitions with zero invariant violations. Models, tools, operators untrusted proposers Authenticate proposal and identifier Acquire evidence and seal candidate Revalidate and decide atomically Authoritative state and branch head Outcome, receipt, and effect index Figure 1: Probabilistic proposal generation and remote evaluation precede the short activation transaction. Only activation advances an authoritative head. 1 Introduction Long-lived AI agents increasingly retain memories, profiles, plans, tool state, and policies beyond a single context window [15, 14]. However, high retrieval quality does not determine which state version is authoritative when models, tools, compactors, and background recovery workers submit concurrent or conflicting updates. Without a strict mutation boundary, a storage layer may preserve every version yet accept a stale retry, expose uncommitted state without audit trails, or allow a proposal to authorize itself by injecting the required privileges into its own proposed state. We define continuity as an unbroken, authorized lineage of accepted heads on one branch. This is infrastructural continuity—a guarantee about state activation and lineal provenance—not a philosophical claim about agent consciousness or behavioral identity. Continuity fundamentally differs from retention: rejected and quarantined objects may remain stored for diagnostic or policy reasons, but they remain unreachable from the authoritative branch head. Cryptographic commitments can enforce this reachability boundary; they cannot make an inferred memory factually true or a policy normatively legitimate. The core thesis of this paper is that agent state governance is an infrastructural activation contract problem. To operationalize this principle, we define the Continuity Kernel (CK) as an activation contract that separates off-commit candidate proposal from atomic activation. Models, tools, and operators act as untrusted proposers. They may perform probabilistic reasoning, remote network fetches, and candidate state construction, but only the deterministic CK control plane may advance an authoritative branch head. Each proposal targets an exact predecessor head or typed target absence. Slow evaluation and evidence acquisition precede activation; a short transaction then revalidates all mutable facts governing admission and records exactly one durable disposition. Figure 1 illustrates this activation boundary. CK introduces no new low-level transaction engine. Instead, standard substrates—such as relational database transactions, conditional object manifests, or consensus state-machine logs—execute its atomic step. The primary contribution is the agent-state activation contract enforced within that step: it atomically binds proposal identity, exact predecessor state, pre-state authority, acquired evidence, lifecycle status, effect manifests, lineage, and outcome receipts. Specifically, this paper makes three contributions: 1. System Model and Contract: A formal model separating stored retention from authoritative reachability, defining the boundary between untrusted proposers and trusted activation (Section 2); 2. Activation Protocol: An owner-bound, exact-head activation protocol with pre-state authorization, four terminal dispositions (Commit, Reject, Quarantine, Defer), at-most-once effect execution, and explicit receipt evidence levels (Section 3); and 3. Lifecycle Rules and Model Verification: Typed lifecycle semantics for branch creation, writer handoff, schema migration, and forward restoration, verified through bounded state-space exploration (Sections 4–5). Sections 2–5 develop the core architecture and evaluation; Appendices A–D detail normative specifications, lineage proofs, and model parameters. 2 System Model and Contract 2.1 Authority Is Reachability As illustrated in Figure 1, CK establishes a strict boundary between candidate object preparation and authoritative state activation. Agent state is partitioned into isolated branches identified by a subject/system identifier sidsid and a branch identifier bidbid, denoted k=(sid,bid)k=(sid,bid). The branch-indexed state X[k]X[k] holds the complete collection of typed agent components for branch k, including memory records, user profiles, tool configurations, and policy-bearing objects. As summarized in Table 1, the storage layer maintains multiple functional namespaces. Candidate proposals, execution attempt logs, quarantined candidates, and read-only runtime projections coexist in storage alongside accepted state. However, storage presence alone does not confer authority: an object is authoritative if and only if it is reachable from the current branch head committed by CK. Table 1: Storage does not by itself confer authority. Namespace Purpose In head? Accepted Current typed state Yes Candidate Prepared successor No Attempt Outcome and diagnostics No Quarantine Isolated candidate No Projection Read-only runtime view No For branch k=(sid,bid)k=(sid,bid), the branch directory maintains the complete-head type h and branch-row type B[k]B[k]: h h =⟨sid,bid,seq,root,,parentRef,lineageRef⟩, = sid,bid,seq,root, v,parentRef,lineageRef , (1) B[k] B[k] =⟨h,status,writer,epoch,dirSeq,handoff,createdFrom⟩. = h,status,writer,epoch,dirSeq,handoff,createdFrom . Here rootroot commits the typed component state; =(schemaV,policyV,evalV,authV) v=(schemaV,policyV,evalV,authV) names the pinned versions; parentRefparentRef is the parent head reference; lineageReflineageRef binds the causal lineage; dirSeqdirSeq is directory sequence; handoffhandoff is the open revision pointer; and createdFromcreatedFrom records genesis provenance. Heads are equal only when every canonically encoded field agrees. The abstract kernel configuration is C=⟨X,B,Γ,,t⟩.C= X,B, ,S,t . (2) Γ is the pre-state authority context; S represents persistent metadata stores (outcomes, receipts, lineage, effects, and quarantine); and t is trusted transaction time. An activation serializes the branch row and every admission, allocation, and effect row that its proposal names. 2.2 Proposals and Typed Transitions Models, tools, memory services, and operators are untrusted proposers. Evaluators and approvers issue signed evidence but cannot advance a head. A trusted gateway authenticates proposal ownership; a preparation service acquires the required evidence and derives a candidate; the activation engine alone changes authority. A signed proposal is summarized by τ=⟨pid,target,expected,ops,a,req⟩.τ= pid,target,expected,ops,a,req . (3) Here pidpid is the unique proposal identifier; targettarget is the target branch key k=(sid,bid)k=(sid,bid); expectedexpected is the expected predecessor head; opsops is an ordered sequence of state operations; a is a sequence of authority changes; and reqreq declares the evidence required for admission. Candidate derivation occurs off-commit, producing candidate state X′=F(X,ops,W)X =F(X,ops,W) using evidence W. Crucially, authorization evaluates against the pre-state context A: X′=F(X,ops,W),A=Γ,existing branch,ξk,branch creation.X =F(X,ops,W), 20.00003ptA= cases ,&existing branch,\\ _k,&branch creation. cases (4) AuthorizeA(τ,W)Authorize_A(τ,W) runs before computing the authority update Γ′=FA(A,a) =F_A(A,a); a proposal cannot authorize itself. The candidate seal binds the proposal, evidence, interpreter, and component roots. Activation recomputes these bindings against the serialized branch state. Schema evolution is an explicit Migration transition with a pinned, deterministic migrator. Deletion creates a typed tombstone; physical erasure remains subject to retention policy. Hashes establish cryptographic integrity, not confidentiality, semantic truth, or policy legitimacy. 2.3 Threat Model and Conditional Contract Proposers may be buggy or adversarial: they may replay requests, reuse identifiers, reorder operations, bind a stale head, omit evidence, forge scope, or request self-authorizing changes. Infrastructure may crash, lose replies, duplicate messages, expose stale replicas, or partition. Evaluators may be wrong; their outputs are policy inputs rather than semantic oracles. The safety claims depend on nine explicit assumptions (A1–A9, stated individually in Appendix D): (1) Boundary & Cryptography (A1–A3): all authoritative writes cross an authenticated kernel boundary, typed cryptography is sound, and signing keys are protected; (2) Atomic Serialization (A4): the storage substrate atomically serializes the complete activation key set; (3) Complete Context & Time (A5–A6): policy, authority, revocation, lifecycle, dependency, and trusted-time values are available for commit-time validation; (4) Lifecycle Order & Non-Recycled Scopes (A7–A8): lifecycle operations share one order and proposal/effect scopes and writer epochs are not recycled; and (5) Verification Objects (A9): stronger receipt claims are made only when their required verification objects are available. Under those assumptions, the contract has four consequences: 1. Exact succession. One complete predecessor has at most one accepted successor; one serialized absence has at most one genesis. Each is installed with state, lineage, effects, outcome, and receipt. 2. Pre-state admission. Authorization and freshness are checked against the serialized predecessor or creation context, never the proposed context. 3. Stable execution identity. A proposal identifier has one terminal disposition and an effect identifier has at most one accepted binding, including after safe reclamation. 4. Lifecycle isolation. Branch creation, fencing, handoff, migration, and restoration preserve branch scope and current authority. These are safety properties, not availability guarantees. The kernel may be unavailable or may return Defer when evidence cannot be obtained. It governs only state behind its mutation boundary; prompts, caches, model weights, tool-local data, prior disclosures, and remote side effects remain outside unless separately mediated. 3 Activation Protocol The protocol separates slow, fallible preparation from one short serialized decision. Preparation authenticates the proposer, acquires exactly the evidence declared by the proposal, runs the pinned transition function, and seals the candidate. Activation admits that sealed package only if the relevant state is still current. Appendix A fixes the complete stage order and receipt variants; this section states the activation rule. 3.1 One activation predicate Let P=⟨τ,W,X′,ME,s⟩P= τ,W,X ,M_E,s be a prepared package containing the signed proposal, exact evidence set, candidate state, ordered effect manifest, and trusted candidate seal. Inside the activation transaction, the kernel evaluates the ordered vector kind(C,P)=⟨Gakind(C,P)⟩a∈.G_kind(C,P)= G^kind_a(C,P) _a∈ ActCheck. (5) The kernel evaluates this vector strictly in the Appendix A order and accepts only an all-Pass vector. Table 2 gives one predicate per stage; no aggregate guard can move a failure across stages. Table 2: One commit-time predicate per activation stage; read down the left pair, then down the right pair. Stage Predicate Stage Predicate TargetLookup Existing kind: B[k]B[k] exists. BranchCreate: B[k]B[k] is absent and serialized Ξ[k] [k] exists. CandidateBinding Seal binds proposal, evidence, interpreter, candidate root, and applicable creation-context or open-revision digest. Allocation Owner allocation is current; pid/eidpid/eid names are live, unused, and unretired. EffectBinding Operations and manifest are bijective; effect scopes are live and unused. ExpectedHead Existing kind: (dh) Present(d_h) is exact; BranchCreate: expectation is Absent. FreshnessInitial Revalidate time and the kind-indexed snapshot: head/epoch/dirSeqdirSeq/authority, or absence/dξd_ξ/genesis inputs. Lifecycle Status, writer, epoch, and kind-specific lifecycle row are admissible. Authorization AχA_χ—predecessor Γ or serialized creation context ξk _k—authorizes the operations. HandoffRevision Applicable target, open SourceFenced revision, reserved epoch, and dirSeqdirSeq are exact. Decision Policy records Proceed, Reject, or Quarantine independently of authorization. AcquisitionAuth Acquisition result set and signer are authentic. AuthorityTransition A declared authority change is valid under the authorized kind context AχA_χ. RequirementCoverage Signed requirements and results form an exact ordered cover. FreshnessFinal Repeat the complete kind-indexed snapshot immediately before prospective construction. VersionBinding Policy, evaluator, authority, revocation, issuer/allocation, dependency, and processing versions are current. WellFormedness Receipt-independent prospective unit PχP_χ is complete, deterministic, and well typed. WitnessBinding Every required witness or authenticated Missing is bound exactly. The trusted acquisition service returns an exact one-to-one mapping for the declared requirements: no declared requirement is omitted, and no unrequested evidence is included. Any unavailable evidence is returned as an explicit, authenticated Missing status, preventing callers from manufacturing Defer by suppressing inconvenient facts or injecting extraneous context. Mutable requirements specify explicit serialization keys and versions, which VersionBinding revalidates at commit time. Freshness is validated prior to policy evaluation and re-checked immediately before prospective state construction. Ordinary transitions revalidate the exact branch head snapshot, while BranchCreate revalidates target absence, creation context ξk _k, allocator versions, and genesis inputs. The candidate seal certifies that the candidate state was derived by the pinned deterministic interpreter from the signed inputs and acquired evidence. Authorization is a separate commit-time predicate evaluated over the pre-state authority context AχA_χ. The subsequent Decision stage records the policy result, and an authority transition Γ′ is computed only after both authorization and decision stages succeed. 3.2 Four stable dispositions As illustrated in the proposal transition lifecycle (Figure 2), for an authenticated, owner-bound identifier, the kernel records exactly one of four dispositions: q∈,(r),(r),(r).q∈\ Commit, Reject(r), Quarantine(r), Defer(r)\. (6) Preparation Off-commit Defer Missing data Activation Atomic check Reject Terminal fail Commit Advances head Quarantine Retain unlinked SealedMissingNew pidpidPassFailPolicy Figure 2: Proposal transition lifecycle and four terminal dispositions, expanding chronologically left-to-right. Table 3: Only Commit changes authoritative state. Result Meaning Commit Install the exact successor and all acceptance metadata atomically. Reject A permanent validation or policy failure; retain no successor. Quarantine Retain sealed material outside the authoritative head. Defer Trusted acquisition reports required evidence unavailable. Every disposition is terminal for its proposal identifier. Resubmission after Defer or Quarantine uses a new identifier linked to the old attempt; a lost response is resolved by looking up the original identifier. Malformed outer framing, failed outer authentication, or an invalid allocation capability are protocol errors rather than dispositions and must not consume the identifier. After ownership succeeds, a fixed stage order chooses the result: any permanent failure that can already be evaluated precedes a trusted Missing; later predicates remain unevaluated. This prevents a missing witness from masking a known invalid proposal. Algorithm 1 Prepare and activate a proposal (abstract) 1: signed proposal τ and authenticated allocation 2: authenticate the principal and ownership of pidpid 3: return a prior outcome or identifier conflict, if present 4: run PrepStage to Ready; acquire and derive only at named stages 5: on terminal preparation Fail/Missing, durably return q(rP)q(r_P) 6: begin a transaction over the branch and every named mutable key 7: return the prior outcome if another retry installed it 8: read every row named by ActCheck 9: for a in the normative ActCheck order do 10: if a=a= WellFormedness then 11: P^χ←χ(P,C) P_χ← BuildProspective_χ(P,C) 12: end if 13: evaluate only GakindG^kind_a and append its stage result 14: if a=a= Decision and result is Quarantine then 15: durably return (rQ) Quarantine(r_Q) 16: else if result is Fail or Missing then 17: durably return q(rA)q(r_A) 18: end if 19: end for 20: rC←rbC(P^χ)r_C← rb_C( P_χ); compute drCd_r_C 21: accept(χ)←χ(P^χ,drC)U_accept(χ)← Finalize_χ( P_χ,d_r_C) 22: atomically install the complete unit; return (rC) Commit(r_C) Algorithm 1 abstracts concrete wire encodings and storage driver APIs. After all validation stages pass, the kernel constructs the receipt-independent prospective unit P P: P^=(X′,h,B[k]). P= BuildProspective(X ,h,B[k]). (7) Construction follows a strictly cycle-free order: P^⟶WellFormedness(P^)⟶rC⟶h′⟶accept. P WellFormedness( P) r_C h _accept. (8) First, the Commit receipt rCr_C is derived directly over P P, binding candidate state X′X , evidence, and pinned versions without circular dependency on the receipt itself. Second, the complete head h′h is finalized by binding rCr_C and lineage. Finally, the kernel installs the complete accepted unit acceptU_accept: accept=X′,Γ′,h′,B′[k],rC,O[pid].U_accept=\X , ,h ,B [k],r_C,O[pid]\. (9) The set acceptU_accept denotes one all-or-nothing atomic transaction, installing candidate state X′X , updated authority context Γ′ , finalized branch row B′[k]B [k] pointing to head h′h , execution outcome O[pid]O[pid], and receipt record rCr_C. Any non-Commit disposition leaves X, B, and Γ unchanged. Proposal and effect records need not remain online forever. Reclamation first advances a durable, monotonically increasing watermark for a non-recycled allocation scope and only then removes covered rows. An identifier below that watermark returns RetiredIdentifier rather than re-entering execution. This preserves stable identity while allowing bounded online metadata. 3.3 Receipts state what they prove A receipt binds the proposal, disposition, reached protocol stage, decisive reason, and the evidence available at that stage. Commit receipts additionally bind the applicable typed parent and context, successor core, lineage, authority versions, and effect manifest. Preparation failures need not pretend that a canonical proposal or candidate existed. Receipt verification has four increasing evidence levels: Table 4: A signature is not evidence that its transaction committed. Level Established claim Structural The receipt has canonical syntax, typed bindings, and a valid signature under its declared key. Attested A trusted kernel key attests the first terminal stage and reason; this does not independently establish correct evaluation. Replay Retained inputs and pinned versions reproduce the stated decision or transition. Inclusion A certified snapshot or log proof places the receipt and outcome, and for Commit the head and lineage, in durable state. The distinction matters because a kernel may sign a receipt before its storage transaction aborts. Replay strength also depends on retained objects: deleting an old proposal may preserve replay exclusion through its watermark while removing the evidence needed to reproduce its original decision. Appendix A specifies these verification obligations. 3.4 Safety properties under the stated assumptions Under the conditional assumptions A1–A9 introduced in Section 2 and detailed in Appendix D, the protocol satisfies three primary safety properties: Proposition 1 (Owner-bound stable outcome). Under A1–A4 and A8, only the principal named by an active allocation may create O[pid]O[pid], and at most one disposition becomes durable for that identifier. Proposition 2 (Single exact continuation). Under A1–A4, at most one proposal commits from one complete predecessor or serialized target absence, and the installed state is its sealed candidate. Proposition 3 (At-most-once accepted effect). Under A1, A4, and A8, each effect identifier has at most one accepted binding, including after online effect records are reclaimed. The proofs are short serialization arguments and appear in Appendix B. The propositions do not claim semantic correctness: a policy may approve a false memory, and an idempotent intent may still cause a non-idempotent remote action if its connector is faulty. 3.5 Realization boundary The transaction contains no model call, network fetch, or human interaction; those finish during preparation. A relational database may lock the branch and named context rows. An object store may conditionally install one immutable commit manifest, and a replicated service may serialize one activation command. In every case readers reject a head whose accepted unit is incomplete. CK atomicity ends at its state boundary. External actions should be committed as intents and delivered through an idempotent outbox when possible. No local protocol can make an irreversible action atomic with an unrelated remote system. Similarly, strict revocation requires the revocation row to share the activation serialization order; a remote revocation service provides only a declared bounded-staleness guarantee. 4 Branch Lifecycle and Restoration Copying state, transferring write authority, and restoring old content are different operations. Treating all three as “load checkpoint” can silently fork a branch or revive an obsolete credential. CK gives each operation a typed forward transition. 4.1 Branch creation A new branch has no predecessor. Its genesis record binds the authenticated creation request, dξd_ξ, fresh identifier, initial roots/writer, and absence proof. Candidate derivation uses declared genesis inputs; authorization uses serialized ξk _k, never nonexistent predecessor state or authority. Both freshness checks protect continued absence, ξk _k versions/dirSeqdirSeq, and all bound genesis inputs. An optional source head is provenance, not a parent. Branch creation runs Algorithm 1 with kind BranchCreate and records the ordinary Commit disposition. One atomic unique insert installs the initial state, admission context, genesis lineage, receipt, complete head, and branch-directory row. Two concurrent creators cannot both win the absent-key comparison. Every later transition has an ordinary accepted parent. Reconciliation between branches is a later typed proposal over exact source and target heads; the kernel does not choose a semantic merge policy. 4.2 Writer handoff A handoff uses a monotonically versioned directory record. Figure 3 shows the small state machine; Table 5 explains its actions. Every step compares the exact current directory revision and appends a signed lifecycle result, yielding maintenance receipts distinct from proposal dispositions. Preparedpointer openSourceFencedpointer openTargetActivepointer ⊥ ⊥ activefenceactivateretargetabort Figure 3: Handoff first removes the source writer, then activates the target. Retargeting advances the epoch while the branch remains fenced. Table 5: Directory-serialized handoff actions. Action Atomic directory effect Prepare Append Prepared and open its pointer; source may still advance. Abort Append Aborted, clear the pointer, and keep the source active. Fence Append SourceFenced, advance the open pointer, clear writer, advance epoch. Retarget Append SourceFenced and advance the open pointer, target, and epoch. Activate Run Algorithm 1 against the fenced revision and append TargetActive, clear the pointer, and make the target writer active. The gap between Fence and Activate is intentional. After fencing, no writer is authorized; therefore a crash cannot expose two active writers. A retry either uses the same handoff revision or fails after retargeting. Target activation is the intentional exception to writer-bearing admission: it requires the exact Frozen row, writer ⊥ , open SourceFenced revision, target, canonical epoch, separately reserved successor epoch, and current admission context. Its ordinary Commit receipt is indexed by both O and HRH_R, so there is one authoritative activation receipt. Prepared recovery may retry, fence, or abort. SourceFenced recovery may retry target activation or append a retarget, but it never returns to Prepared. If directory and branch storage cannot share atomic ordering, a consensus or coupled protocol is required; polling alone cannot establish writer isolation. 4.3 Migration and forward restoration Migration names source and target schemas plus a pinned deterministic migrator. The migrator must be allowed by current policy, terminate with a well-formed target, and obey an explicit loss policy. A rollback is another forward migration, never a rewrite of an accepted head. Restoration also creates a new successor. Let XcX_c be current state, XkX_k an authenticated historical checkpoint, MμM_μ an optional migration, and M a typed path mask. The restored candidate is X′=RestoreM(Xc,Mμ(Xk)),Γ′=Γc.X =Restore_M(X_c,M_μ(X_k)), 20.00003pt = _c. (10) Paths in M take checkpoint values after migration; all other paths take current values. Authority, revocation, writer epoch, and lifecycle fields are protected and therefore remain current. The successor’s parent is the current head, while the checkpoint is an auxiliary provenance reference. Restoration cannot truncate lineage, revive an old writer or credential, or undo an external action already performed. Appendix C gives the total postconditions and stale-request behavior for every lifecycle action. 5 Evaluation We evaluate the Continuity Kernel (CK) design by addressing four key research questions: • RQ1 (Activation Integrity & Succession): Does the 17-stage activation predicate enforce exact predecessor succession, pre-state authorization, and non-self-authorizing state transitions across all five transition kinds? • RQ2 (Concurrency & Replay Isolation): Does the protocol maintain at-most-once execution identity, prevent replay attacks, and safely reclaim online proposal/effect records under concurrent races and watermark advances? • RQ3 (Lifecycle Isolation & Writer Fencing): Do lifecycle rules for branch creation, writer handoff, retargeting, aborts, and forward restoration prevent split-brain access and stale writer state transitions? • RQ4 (Self-Critical Scope & Realization Limits): What are the exact bounds of the formal state-space exploration, and what system-level guarantees require physical storage-engine verification beyond the abstract model? 5.1 Formal State-Space Exploration (RQ1–RQ3) To evaluate the protocol’s state-transition logic, we construct an executable bounded model in Python (artifacts/bounded_model.py). The model performs exhaustive breadth-first search (BFS) state exploration over a finite abstraction of the kernel specification using only the Python standard library. The model state space incorporates: (1) one active branch directory B[k]B[k] and state store X[k]X[k]; (2) a shared admission context Γ and creation context Ξ[k] [k]; (3) an honest proposal owner and an adversarial principal; (4) proposal identifiers pid∈0…12pid∈\0… 12\ (13 IDs) and effect identifiers eid∈0…3eid∈\0… 3\ (4 IDs); (5) source writer w0w_0 and target writers w1,w2w_1,w_2; and (6) integer versioning for schema, policy, and authority contexts. Transitions simulate all five closed transition kinds (Ordinary, Migration, Restoration, HandoffActivate, BranchCreate), exact-head concurrency races, pre-state authority changes, missing/malformed evidence, two-stage freshness expiration, resubmissions, watermark reclamation, writer fencing, retargeting, and masked restoration. Table 6: State-space expansion and BFS exploration metrics by search depth d. Depth Unique States Cum. States Cum. Attempts Time (s) 0 1 1 0 <0.01 1 15 16 17 <0.01 2 160 176 270 0.04 3 1,455 1,631 2,959 0.33 4 11,309 12,940 27,353 2.69 5 76,028 88,968 216,413 18.88 6 445,649 534,617 1,483,284 124.62 7 2,273,613 2,808,230 8,880,248 27.45 Table 7: Distribution of transition outcomes across full state space (8.88M8.88M transition attempts). Transition Outcome Full Count Share (%) IdReuseConflict 1,673,300 18.84% Commit (Head Advance) 916,956 10.33% ReclaimedEffects 842,195 9.48% RejectStaleHead 770,555 8.68% PrefixNotFinal 731,466 8.24% Defer (Missing Evidence) 418,375 4.71% RejectDuplicateInProposal 418,375 4.71% RejectUnauthorized 395,905 4.46% RejectExpiredAtActivation 395,905 4.46% RejectCandidateBinding 395,905 4.46% RejectPolicy 395,905 4.46% Prepared (Handoff) 306,121 3.45% Other Dispositions (1111 kinds) 1,219,285 13.73% Total Attempts 8,880,248 100.00% Under CPython 3.13.9, the depth-seven search evaluates 8,880,248 total transition attempts (including idempotency checks and retries). Of these, exactly Nstates=2,808,230,Ntransitions=5,526,474N_states=2,808,230, 20.00003ptN_transitions=5,526,474 (11) are unique state-changing transitions where the successor state differs from the predecessor state. As shown in Table 6, state space exploration scales exponentially up to depth 7. Depth 6 timing (124.62s) includes evaluating all 7.4M outgoing transition attempts to generate depth 7 states, whereas depth 7 timing (27.45s) reflects terminal invariant validation on the 2.27M2.27M boundary states without further successor expansion. On a standard single-threaded execution harness, kernel transition evaluation achieves a throughput of 31,132 transitions/sec with an average evaluation latency of 32.12 μ per transition. Table 7 details the empirical distribution of transition dispositions across all 8.88M evaluated transition attempts. Successful state transitions (Commit) represent 916,956 committed heads (10.33%), while concurrency and identifier reuse protections (RejectStaleHead, IdReuseConflict, ReclaimedEffects) account for 37.00% (3.28M transitions), proving that the protocol actively isolates concurrent races and stale proposals. Table 8: Reached coverage witnesses and invariant assertions (2,808,2302,808,230 reachable states, depth 7). Target Category Evaluated Invariant / Witness Status Dispositions Reached Commit, Reject, Quarantine, and Defer Pass Activation Guard 17 stages evaluated in normative sequential order Pass Authorization Self-authorizing proposal (τ.aτ.a) rejected at pre-state Pass Freshness Revalidated initially and immediately prior to commit Pass Reclamation Safe watermark advances for pidpid and eideid scopes Pass Exact Succession At-most-one accepted successor per complete head Pass Writer Fencing Stale/abandoned writer blocked from branch mutation Pass Handoff Lifecycle SourceFenced, TargetActive, Retarget, and Abort Pass Restoration Masked restored root with protected current fields Pass As summarized in Table 8, the exploration finds zero encoded invariant violations across all 2.8 million reachable states and reaches 100% of the named protocol coverage witnesses. 5.2 Invariant & Safety Analysis The model validates three core structural properties across every reachable state: 1. Pre-State Authorization Safety (RQ1). For every committed transition, authorization is checked against the predecessor authority context Γ (or genesis context ξk _k for BranchCreate). In the model, when an adversarial proposer submits a self-authorizing proposal that attempts to inject its own required permissions into a, the Authorization stage evaluates AuthorizeΓ(τ,W)Authorize_ (τ,W) and rejects 395,905 invalid proposals (4.46% of transitions) with RejectUnauthorized. 2. Execution Identity & Replay Safety (RQ2). Each proposal identifier pidpid has at most one durable disposition O[pid]O[pid], and each effect identifier eideid is bound at most once in E[eid]E[eid]. Watermark advances correctly transition covered online identifiers to RetiredIdentifier, preventing re-execution or identifier recycling attacks after online metadata is pruned. 3. Writer Fencing & Lifecycle Isolation (RQ3). During writer handoff, once the source writer is fenced (SourceFenced), any subsequent write attempt by the old writer w0w_0 fails with StaleRevision or WriterEpoch. Retargeting to a new target writer w2w_2 advances the writer epoch, ensuring that an abandoned target writer w1w_1 cannot activate the branch. 5.3 Self-Critical Thesis Analysis & Realization Limits (RQ4) While bounded model exploration provides strong evidence for the logical consistency of the finite protocol, a self-critical assessment highlights critical gaps between the formal model and physical system implementations: 1. Abstraction vs. Physical Storage Realization. The model treats preparation and atomic activation as single logical state steps. In a production system, atomic activation relies on the underlying storage engine (e.g., PostgreSQL conditional updates, FoundationDB OCC, or Raft consensus). Physical storage crashes during write-ahead logging (WAL), network partitions, or storage-engine bugs fall outside the model’s abstract state space. 2. Signature vs. Durable Inclusion. As established in Section 3.3, a signed candidate seal or preparation receipt proves cryptographic origin (Attested level) but not transactional durability (Inclusion level). If a kernel gateway signs a receipt in memory but the backing transaction fails to commit, the signed receipt is uncommitted. Production deployments must issue Level 4 inclusion proofs backed by durable log anchors. 3. External Side-Effect Atomicity. As discussed in Section 3, CK atomicity governs state transitions inside its mutation boundary. It cannot make irreversible remote side effects (e.g., external API calls or physical robot actuation) atomic with internal state updates. Remote actions must be staged as idempotent outbox intents. 4. Performance & Latency Trade-offs. The protocol adds overhead during commit: 17 sequential stage checks, double freshness validation, and prospective unit construction (32.12 μ in single-threaded Python). In high-throughput environments, this overhead requires storage-level optimizations, such as single-pass SQL transaction procedures or batched multi-key compare-and-swap operations. 6 Related Work Agent memory. Generative Agents and MemGPT organize reflection, retrieval, and long-term context [15, 14]; LoCoMo, A-MEM, Mem0, and MemOS study long-horizon evaluation, consolidation, scalable memory, and versioned management [11, 20, 2, 9]. These systems motivate governed memory. As part of the broader Persistent Cognitive Identity (PCI) framework [5], CK addresses the narrower question of how any typed component version becomes the authoritative branch head. MemTX is the closest agent-memory transaction system: it stages evidence-bearing beliefs under a snapshot, gates actions, and propagates repairs after retraction [8]. CK applies an activation boundary to typed persistent state and specifies pre-state authority, complete-head equality, stable four-way outcomes, writer epochs, and forward restoration. MemTxn supplies source-supported memory admission, visible-version selection, snapshots, and journal-based recovery [3]. MemTX’s unit is a belief commit and MemTxn’s is a source-supported memory update; CK specifies a typed branch-head transition and its pre-state authority boundary. Transactions and retries. Optimistic concurrency control validates read assumptions at commit, database transactions provide atomic durability, and replicated terms fence stale leaders [6, 4, 13]. For linearizable retries, RIFL (Reusable Infrastructure for Linearizability) combines unique request identifiers, atomic completion records, and safe reclamation [7]. CK composes these mechanisms into an agent-state contract: the accepted unit also binds typed state, authority, evidence, lineage, effects, and a calibrated receipt. Commit-time authorization for LLM agents similarly exposes the gap between temporary authority and durable effects [16]; CK places that check inside a persistent-state transition. Effects and evidence. Cordon defines task-level semantic transactions with staged effects, delegated authorization, compensation, and audit evidence [1]. Its task boundary complements CK’s branch-head boundary: an outbox intent may be a CK component, but CK cannot make an unrelated remote action atomic. PROV-DM, JSON-LD, RDFC-1.0, and Data Integrity provide provenance, canonicalization, and cryptographic proof formats [12, 18, 10, 19]. Those standards can show derivation and integrity; the activation protocol is still needed to determine which validly encoded proposal became authoritative. 7 Conclusion For persistent agents, state retention is not authority. Infrastructural continuity requires an authorized lineage of accepted branch heads. CK makes the transition to authority explicit: untrusted components propose typed candidates off-commit; a deterministic control plane validates an exact predecessor head and pre-state authority (or typed absence and genesis context); a short activation transaction records one stable disposition; and only Commit advances the branch head. The protocol contract addresses linearizable retries, effect uniqueness, writer epoch fencing, schema migration, and forward restoration without expanding the kernel’s trusted semantic scope. Our safety propositions are conditional on explicit serialization, access-control, cryptographic, and durability assumptions. In a depth-seven finite abstraction, an executable bounded model explores 2,808,230 reachable states and 5,526,474 state-changing transitions, finding zero encoded invariant violations and reaching 100% of named coverage witnesses. The model validates logical protocol consistency within its finite bounds; it does not establish unbounded mathematical correctness, physical storage driver conformance, or throughput performance under hardware faults. The core contribution of this work is the activation contract itself—providing a principled systems foundation that separates stored retention from authoritative reachability and distinguishes cryptographic receipt signatures from durable transactional inclusion. References [1] Z. Chen, H. Liu, D. Xu, D. Dong, J. Li, B. Pu, and J. Zhai (2026) Cordon: semantic transactions for tool-using LLM agents. Note: Preprint, arXiv:2606.17573v1, version 1, 16 June 2026. https://arxiv.org/abs/2606.17573v1 External Links: 2606.17573v1, Document, Link Cited by: §6. [2] P. Chhikara, D. Khant, S. Aryan, T. Singh, and D. Yadav (2025) Mem0: building production-ready AI agents with scalable long-term memory. arXiv preprint arXiv:2504.19413. External Links: Document Cited by: §6. [3] H. Cui, Z. Tang, Z. Yao, F. Meng, Q. Ma, and W. Jia (2026) MemTxn: a transaction boundary for source-supported updates and complete-state recovery in agent memory. arXiv preprint arXiv:2607.27834. Note: Version 1, submitted July 30, 2026 External Links: Link Cited by: §6. [4] J. Gray and A. Reuter (1992) Transaction processing: concepts and techniques. Morgan Kaufmann. Cited by: §6. [5] J. He and D. Yu (2026) Persistent cognitive identity: a systems architecture for continuity across AI substrates and embodiments. Note: Position and architecture manuscript, OpenKedge.io Cited by: §6. [6] H. Kung and J. T. Robinson (1981) On optimistic methods for concurrency control. ACM Transactions on Database Systems (TODS) 6 (2), p. 213–226. External Links: Document Cited by: §6. [7] C. Lee, S. J. Park, A. Kejriwal, S. Matsushita, and J. Ousterhout (2015) Implementing linearizability at large scale and low latency. In Proceedings of the 25th Symposium on Operating Systems Principles, p. 71–86. External Links: Document Cited by: §6. [8] X. Li, Y. Wang, H. Lu, Z. Chen, M. Li, P. Song, M. Zheng, and T. Cai (2026) MemTX: transactional belief commit for stateful agent memory. Note: Preprint, arXiv:2607.23929v2, version 2, 28 July 2026. https://arxiv.org/abs/2607.23929v2 External Links: 2607.23929v2, Document, Link Cited by: §6. [9] Z. Li, C. Xi, C. Li, D. Chen, B. Chen, S. Song, S. Niu, H. Wang, J. Yang, C. Tang, Q. Yu, J. Zhao, Y. Wang, P. Liu, Z. Lin, P. Wang, J. Huo, T. Chen, K. Chen, K. Li, Z. Tao, H. Lai, H. Wu, B. Tang, Z. Wang, Z. Fan, N. Zhang, L. Zhang, J. Yan, M. Yang, T. Xu, W. Xu, H. Chen, H. Wang, H. Yang, W. Zhang, Z. J. Xu, S. Chen, and F. Xiong (2025) MemOS: a memory OS for AI system. Note: Preprint, arXiv:2507.03724v4, version 4, 3 December 2025. https://arxiv.org/abs/2507.03724v4 External Links: 2507.03724v4, Document, Link Cited by: §6. [10] D. Longley, G. Kellogg, and D. Yamamoto (2024) RDF dataset canonicalization. Note: W3C Recommendation21 May 2024, Sections 4.4.3 and 7.1 External Links: Link Cited by: §D.1, §D.1, §6. [11] A. Maharana, D. Lee, S. Tulyakov, M. Bansal, F. Barbieri, and Y. Fang (2024) Evaluating very long-term conversational memory of LLM agents. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), p. 13851–13870. External Links: Document Cited by: §6. [12] L. Moreau and P. Missier (2013) PROV-DM: the PROV data model. Note: W3C Recommendation External Links: Link Cited by: §6. [13] D. Ongaro and J. Ousterhout (2014) In search of an understandable consensus algorithm. In 2014 USENIX Annual Technical Conference (USENIX ATC 14), p. 305–319. Cited by: §6. [14] C. Packer, S. Wooders, K. Lin, V. Fang, S. G. Patil, I. Stoica, and J. E. Gonzalez (2023) MemGPT: towards LLMs as operating systems. arXiv preprint arXiv:2310.08560. External Links: Document Cited by: §1, §6. [15] J. S. Park, J. C. 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. External Links: Document Cited by: §1, §6. [16] I. Santos-Grueiro (2026) Temporary authority, permanent effects: commit-time authorization for LLM agents. Note: Preprint, arXiv:2607.10487v1, version 1, 11 July 2026. https://arxiv.org/abs/2607.10487v1 External Links: 2607.10487v1, Document, Link Cited by: §6. [17] W3C JSON-LD Working Group (2020) JSON-LD 1.1 processing algorithms and API. Note: W3C Recommendation16 July 2020 External Links: Link Cited by: §D.1. [18] W3C JSON-LD Working Group (2020) JSON-LD 1.1: a JSON-based serialization for linked data. Note: W3C Recommendation16 July 2020 External Links: Link Cited by: §D.1, §6. [19] W3C Verifiable Credentials Working Group (2025) Verifiable credential data integrity 1.0: securing the integrity of verifiable credential data. Note: W3C Recommendation15 May 2025 External Links: Link Cited by: §6. [20] W. Xu, Z. Liang, K. Mei, H. Gao, J. Tan, and Y. Zhang (2025) A-MEM: agentic memory for LLM agents. In Advances in Neural Information Processing Systems 38, p. 17577–17604. External Links: Link Cited by: §6. Appendix A Normative Receipt Semantics A.1 Stage Sequences and Disposition Mapping This appendix fixes the stage order and minimum contents left implicit in the main-text receipt abstractions. Preparation and activation checks evaluate two strictly ordered, closed sequences: Preparation Stage Order (PrepStage): RawScreen RawScreen ≺Decode≺Canonicalize Decode Canonicalize ≺ProposalAuth≺StaticValidation ProposalAuth StaticValidation ≺TargetLookup≺AcquisitionAuth TargetLookup AcquisitionAuth ≺RequirementCoverage≺WitnessAuth RequirementCoverage WitnessAuth ≺AcquisitionTime≺CandidateDerivation AcquisitionTime CandidateDerivation ≺PolicyAuthorization≺Ready. PolicyAuthorization Ready. Activation Check Order (ActCheck): TargetLookup≺Allocation≺ExpectedHead TargetLookup Allocation ExpectedHead ≺Lifecycle≺HandoffRevision Lifecycle HandoffRevision ≺AcquisitionAuth≺RequirementCoverage AcquisitionAuth RequirementCoverage ≺VersionBinding≺WitnessBinding VersionBinding WitnessBinding ≺CandidateBinding≺EffectBinding CandidateBinding EffectBinding ≺FreshnessInitial≺Authorization FreshnessInitial Authorization ≺Decision≺AuthorityTransition Decision AuthorityTransition ≺FreshnessFinal≺WellFormedness. FreshnessFinal WellFormedness. In both pipelines, TargetLookup requires existence for existing-branch kinds and absence plus serialized ξk _k for BranchCreate. The latter’s preparation derives from genesis inputs and runs PolicyAuthorization against ξk _k; activation ExpectedHead accepts only Absent. Existing kinds use the current predecessor X,ΓX, and (dh) Present(d_h). An outcome-eligible failure at position j records vi=,i<j,(r) or (r),i=j,,i>j,v_i= cases Pass,&i<j,\\ Fail(r) or Missing(r),&i=j,\\ NE,&i>j, cases (12) where NE means not evaluated. A verifier never asks a failing predicate to pass. Known permanent failures precede a trusted Missing, so unavailability cannot mask a rejection. Malformed outer framing, failed outer authentication, and invalid allocation are protocol errors: they create neither O[pkey]O[pkey] nor a receipt. Table 9: The four proposal-receipt variants and their terminal semantics. Tag Terminal location Stage/reason rule Builder Durable effect rPr_P Preparation First failed or trusted-Missing preparation stage; later stages are NE rbPrb_P Insert one owner-bound O[pkey]O[pkey] and ℛ[drP]=rPR[d_r_P]=r_P; no candidate becomes authoritative. rAr_A Serialized activation First failed activation check; earlier checks pass and later checks are NE rbArb_A Insert one O[pkey]O[pkey] and ℛ[drA]=rAR[d_r_A]=r_A; X,B,Γ,EX,B, ,E are unchanged. rQr_Q = Decision= Quarantine Earlier checks pass, Decision records Quarantine, later checks are NE rbQrb_Q Insert O[pkey]O[pkey], ℛ[drQ]=rQR[d_r_Q]=r_Q, and unreachable Q[pkey]Q[pkey] only. rCr_C All activation checks Pass PχP_χ passes WellFormedness; the terminal result is Commit rbCrb_C Store ℛ[drC]=rCR[d_r_C]=r_C and install the complete accepted unit of Equation 9. For T∈P,A,Q,CT∈\P,A,Q,C\, rbTrb_T canonically encodes and signs exactly rTr_T, computes drTd_r_T, and uses the sole receipt-store rule ℛ[drT]=rTR[d_r_T]=r_T. No other proposal-receipt builder or receipt key exists. Table 10 is the closed stage–reason map. Table 10: Closed V1 stage–reason map. “Limit” abbreviates CanonicalizationLimit; a stage vector disambiguates repeated reasons. Preparation stage ↦ allowed reason Activation check ↦ allowed reason RawScreen↦ \Limit\; Decode↦ \DecodeFailure, Limit\; Canonicalize↦ \CanonicalizationFailure, Limit\; ProposalAuth↦ \ProposalAuthentication\; StaticValidation↦ \MalformedProposal, EffectManifest, DuplicateEffectInProposal\; TargetLookup↦ \UnknownTargetAtPreparation, CreationContextMissing, BranchAlreadyExists\; AcquisitionAuth↦ \UntrustedRequirementResult, AcquisitionAuthentication\; RequirementCoverage↦ \RequirementCoverage\; WitnessAuth↦ \WitnessAuthentication\; AcquisitionTime↦ \ExpiredAtPreparation, EvidenceUnavailable\; CandidateDerivation↦ \CandidateDerivation\; PolicyAuthorization↦ \PreparationUnauthorized\. TargetLookup↦ \TargetMissingAtActivation, TargetAlreadyExistsAtActivation, CreationContextMissingAtActivation\; Allocation↦ \AllocationRevoked\; ExpectedHead↦ \StaleHead\; Lifecycle↦ \OrdinaryLifecycle, HandoffLifecycle\; HandoffRevision↦ \StaleHandoffRevision, StaleDirSeq, TargetWriter, StaleEpoch\; AcquisitionAuth↦ \AcquisitionAuthentication\; RequirementCoverage↦ \RequirementCoverage\; VersionBinding↦ \StaleVersion\; WitnessBinding↦ \WitnessBinding\; CandidateBinding↦ \CandidateBinding\; EffectBinding↦ \EffectManifest, EffectScope, RetiredEffect, DuplicateEffect\; FreshnessInitial, FreshnessFinal↦ \ExpiredAtActivation, StaleHead, StaleEpoch, StaleDirSeq, StaleAuthority, StaleVersion, StaleCreationContext, TargetAppearedAtActivation\; Authorization↦ \Unauthorized\; Decision↦ \PolicyReject, PolicyQuarantine\; AuthorityTransition↦ \InvalidAuthorityTransition\; WellFormedness↦ \InvalidSuccessor\. At activation TargetLookup, BranchCreate evaluates target presence before creation context: B[k]≠B[k]≠ Absent yields TargetAlreadyExistsAtActivation; B[k]=∧Ξ[k] missingB[k]= Absent [k] missing yields CreationContextMissingAtActivation. Freshness checks evaluate in deterministic intra-stage order. For existing branches: (1) t>deadlinet>deadline yields ExpiredAtActivation; (2) head mismatch yields StaleHead; (3) epoch mismatch yields StaleEpoch; (4) dirSeqdirSeq mismatch yields StaleDirSeq; (5) authority/revocation/policy mismatch yields StaleAuthority; (6) pinned version mismatch yields StaleVersion. For BranchCreate: (1) t>deadlinet>deadline yields ExpiredAtActivation; (2) post-lookup target appearance (B[k]≠B[k]≠ Absent) yields TargetAppearedAtActivation; (3) creation context (Ξ[k] [k] missing/altered) yields StaleCreationContext; (4) genesis profile/allocator version mismatch yields StaleVersion. Every reason selects Reject (rbArb_A), requires preparation and prefix Πj−1 _j-1, forbids later fields, and leaves X,B,Γ,Ξ,EX,B, , ,E unchanged. Earlier stages dominate later stages. At preparation, a Fail selects Reject/rbPrb_P and only EvidenceUnavailable is Missing, selecting Defer/rbPrb_P. At activation, every reason selects Reject/rbArb_A except PolicyQuarantine, which selects Quarantine/rbQrb_Q; all-pass through WellFormedness selects Commit/rbCrb_C. Thus Algorithm 1 has no other terminal path. Adding a stage or reason requires a new receipt schema version. An exact retry returns the indexed result; any changed attempt under the same pidpid conflicts. Lifecycle maintenance is typed separately. Its closed actions are Prepare, Fence, Retarget, and Abort. Its closed results are Applied, StaleHead, StaleRevision, StaleDirSeq, WriterEpoch, TargetConflict, InvalidState, and Unauthorized. rbL=()rb_L= Build( LifecycleReceiptV1) binds the action identifier, pre/post directory tuples, optional input/output revision digests, result, trusted time, and signature. It is stored in ℛR and indexed by the typed HRH_R key defined in Appendix C; it never creates O[pkey]O[pkey] and is not a fifth proposal disposition. Its digest is drL=d(rL)d_r_L=d_ LifecycleReceiptV1(r_L) under Equation 14. Replay recomputes the action and its pre/post tuples; inclusion requires a certified state containing ℛR, HRH_R, and, for Applied, the assigned F and B records. Lifecycle field presence is action-indexed. Every rLr_L binds its common fields, authenticated request, requested pre-directory tuple, result, and exact post tuple. For Applied, the input/output revision states are Prepare ⊥→ \!→ Prepared, Fence Prepared→ , Retarget SourceFenced→ , and Abort Prepared→ . For an allowed non-Applied result, post equals pre, output is forbidden, and neither F nor B changes; Prepare forbids input, while the other actions require the requested input. Let S= S=\ StaleRevision,StaleDirSeq,WriterEpoch, StaleRevision, StaleDirSeq, WriterEpoch, InvalidState,Unauthorized. InvalidState, Unauthorized\. The exact failure sets are S∖StaleRevision∪StaleHead,TargetConflictS \ StaleRevision\∪\ StaleHead, TargetConflict\ for Prepare, S∪StaleHeadS∪\ StaleHead\ for Fence, S∪TargetConflictS∪\ TargetConflict\ for Retarget, and S for Abort. No other action/result pair is schema-valid. A.2 Field presence and early input binding After owner authentication, the gateway computes draw=d(rawBytes).d_raw=d_ WireInputV1(rawBytes). (13) An early RawScreen, Decode, or Canonicalize receipt binds drawd_raw but omits dτd_τ; there is not yet a canonical proposal to hash. Let j be the terminal stage. A receipt requires the common fields, the terminal Fail/Missing observation, and exactly the fields whose producing stages successfully completed before j. It forbids fields first produced at j or later. Thus later NE stages impose no field obligation. The only profile choice is raw retention: drawd_raw is required when rawRetention=true and forbidden otherwise. Absence is encoded by the typed variant, never a zero digest. Table 11: Stage-indexed field production. A field is required exactly after its producer passes and forbidden beforehand. Field group Producer that must Pass Contents Common Outcome-eligible owner authentication Type/version, subject/branch, principal, allocation scope, pidpid, tag, disposition, stage vector, reason, issue time, kernel key and signature Raw input Request capture under the signed profile drawd_raw; profile makes it required or forbidden, never optional Canonical proposal Canonicalize dτd_τ, typed (dh) Present(d_h)/ Absent expectation, kind reference, and unverified signature/credential bytes Authenticated proposal ProposalAuth Verified signer, owner, principal, allocation scope, and proposal-authentication result Acquisition RequirementCoverage (preparation) Ordered requirements/results, witness and dependency-version commitments Candidate package CandidateDerivation Candidate root, pinned interpreter, candidate-seal key/signature, effect manifest, and direct applicable dξd_ξ or open SourceFenced-revision digest Activation prefix Πj _j Corresponding ActCheck stage Existing row or absence plus dξd_ξ; allocation; exact Present/Absent expectation; lifecycle; open revision; acquisition signer; exact cover; versions; witness binding; candidate binding; effect binding; initial freshness; authorization; Decision; authority-after; final freshness—each introduced only by its same-named successful stage Prospective unit BuildProspective after FreshnessFinal Produced successor/core/lineage inputs, receipt-independent branch-row plan (B^χ B_χ), receipt-independent assignment plan (Δ^χ _χ), and deterministic parameters for receipt-dependent finalization Finalized Commit WellFormedness Pass Commit receipt/digest, complete head, outcome, HRH_R, effects, receipt store, and directory binding Consequently, a CandidateDerivation failure forbids candidate fields. Every activation receipt requires the completed preparation package, but an early TargetLookup or ExpectedHead failure contains only its successful activation prefix and terminal observation—never later freshness, authorization, Decision, authority-after, or successor fields. A Decision Reject or Quarantine binds that terminal policy result; it does not manufacture an AuthorityTransition prefix. A BranchCreate prefix binds absence and dξd_ξ, never a predecessor head, state, or authority. An InvalidSuccessor receipt may bind the produced prospective fields but forbids every finalized Commit field. Exact evidence coverage is a bijection between the signed ordered requirement sequence and acquired results: no omission, duplicate, substitution, injection, or forbidden reordering is accepted. Each result is either a signed witness or an authenticated Missing. A candidate seal authenticates these bindings; it is neither pre-state authorization nor proof of durable commit. A.3 Verification levels Verification is monotone but not automatic: 1. Structural authenticity checks the receipt variant, canonical syntax, typed digests, signature, key scope, and internal bindings. 2. Kernel-attested reason additionally establishes that the authenticated kernel reported the declared first terminal stage. It does not independently establish that the predicate was evaluated correctly. 3. Independent replay recomputes each predicate through the terminal stage from retained inputs and pinned versions. For Commit it also recomputes candidate derivation, the authority transition, manifest, successor core, and lineage. Replay is unavailable when any required object or interpreter is absent. 4. Durable inclusion verifies a certified snapshot, commit manifest, or replicated-log proof containing O[pkey]O[pkey] and the receipt; Commit also requires the installed head and lineage. An archive proof terminates at a retirement root in such a certified state. A signature or locator alone is not inclusion. A conforming verifier first completes level 1, reports level 2 only for a trusted kernel key, attempts level 3 only with a complete replay package, and reports level 4 only with an inclusion proof. Thus a signed receipt from an aborted storage transaction cannot be upgraded to a committed fact. Appendix B Typed Lineage and Cycle-Free Construction B.1 Acyclic Hash Graph and Construction Order Table 12: Exact typed construction dependencies. Every input appears earlier. Object and domain Immediate inputs Downstream references 1 dξd_ξ / CreationContextV1; Ξ[k] [k] Namespace, allocator and policy versions, dirSeqdirSeq, authority root, genesis profile BranchCreate proposal, seal, authorization, freshness 2 dfjSourceFenced_f_j^SourceFenced / existing HandoffRevisionV1; F[hid,j]F[hid,j] Prior digest, SourceFenced state, branch/head, target, epochs, directory tuple, context versions HandoffActivate proposal, seal, admission 3 dτd_τ / TransitionV1 pkey,kpkey,k, Present/Absent expectation, χ, operations, authority changes, dependencies, requirements, validity, kind reference, and direct applicable dξd_ξ or dfjSourceFenced_f_j^SourceFenced Acquisition and candidate derivation 4 dWd_W / AcquisitionV1 dτd_τ, ordered requirements/results, signer/key identifiers and pinned versions; detached authentication is verified Candidate seal 5 dX′,dΓ′,dMEd_X ,d_ ,d_M_E / StateRootV1, AuthorityStateV1, EffectManifestV1 Ordered typed successor component digests; ordered authority entries; ordered (opIndex,eid,opDigest)(opIndex,eid,opDigest), derived from initial inputs with dτ,dWd_τ,d_W and the interpreter Seal, head core 6 g,dgg,d_g / BranchGenesisV1 dτ,dξd_τ,d_ξ, absence proof, initial roots/writer/zero counters, optional source provenance Genesis parent 7 dseald_seal / CandidateSealV1 dτ,dWd_τ,d_W, interpreter, component/effect roots, and direct applicable dξd_ξ or open-revision digest Receipt 8 hc,dhch_c,d_h_c / HeadCoreV1 Exact Equation 1 fields: root, typed parent, versions, counters, time, kind, and closed auxRefauxRef Output revision, lineage 9 dfj+1TargetActived_f_j+1^TargetActive / new HandoffRevisionV1 dfjSourceFenced,dhcd_f_j^SourceFenced,d_h_c, exact target, epochs, directory tuple and context versions Lineage, receipt, HResult 10 ℓ,dℓ ,d_ / LineageEdgeV1; L[λ]L[λ] Parent, dhc,dτ,pkeyd_h_c,d_τ,pkey, versions, and applicable input/output handoff digests Commit receipt 11 rC,drCr_C,d_r_C / CommitReceiptV1; ℛ[drC]R[d_r_C] pkey,dτ,dW,dsealpkey,d_τ,d_W,d_seal, parent, dhc,dℓd_h_c,d_ , all-Pass vector, P^χ P_χ prospective fields, effect/authority and handoff bindings Complete head, accepted records 12 h′,dh′h ,d_h / CompleteHeadV1 hc,dℓ,drCh_c,d_ ,d_r_C Outcome, branch row, effect, handoff result, directory binding 13 OutcomeV1; O[pkey]O[pkey] pkeypkey, Commit tag, drC,h′d_r_C,h Retry, inclusion 14 EffectRecordV1; E[eid]E[eid] eid,pkeyeid,pkey, operation index/digest, drC,dh′d_r_C,d_h Inclusion, duplicate exclusion 15 HandoffResultV1; HR[KH]H_R[K_H] pkey,hidpkey,hid, input/output revision digests, drC,h′d_r_C,h Retry, inclusion 16 BranchRowV1; B[k]B[k] k,h′k,h , status, writer, epoch, dirSeqdirSeq, open pointer, immutable createdFromcreatedFrom Authoritative lookup 17 DirectoryBindingV1; G[KG]G[K_G] k,pkey,χk,pkey,χ, pre/post dirSeqdirSeq, allocator/context versions, drC,dh′d_r_C,d_h Freshness, inclusion 18 i / InclusionProofV1, later Certified state containing rows 11–17 External verifier; never an input to h′h Here KH=(pkey,hid)K_H= HandoffResultKeyV1(pkey,hid) and KG=(k,dirSeq′)K_G= DirectoryKeyV1(k,dirSeq ); these are definitions, not aliases for differently keyed records. Every content reference uses a type- and version-separated digest dT(y)=H(CLOSE d_T(y)=H ( LP()∥LP(T)∥ ( CK) (T) u32(v)∥LP(CanonT(y))), 32(v) (Canon_T(y)) ), (14) where LP is an unambiguous length prefix. Logical proposal and effect identifiers are allocated names, not content digests. Equation 1 is the sole definition of immutable head core, complete head, and branch row; this appendix introduces no shortened head. The closed parent type is = LineageParent= (dh) AcceptedParent(d_h) ∣(dg). GenesisParent(d_g). (15) Exactly one branch-genesis edge uses the second variant. Every later edge uses the complete current head. A checkpoint, migration input, or handoff source is an auxiliary typed reference and can never occupy the parent field. A LineageEdgeV1 binds sid,bidsid,bid, transition kind, lineage parent, dhcd_h_c, dτd_τ, the proposal allocation key, policy and authority versions, epoch and sequence, plus the transition-kind-specific source, checkpoint, migration, or handoff references. A BranchGenesisV1 binds the authenticated creation request, absent-directory proof, initial state and admission roots, writer, epoch 0, sequence 0, and optional source provenance. Source provenance does not create cross-branch ancestry. In Table 12, every V1 name has version 1, that exact name as its domain tag, and its type-specific canonical encoder under Equation 14. Component roots carry their declared type/schema domain. Rows 3–10 and 12 are content-addressed by their displayed typed digest; rows 1–2, 11, and 13–17 use exactly the displayed map key. Map keys are allocated typed names, not hidden hash inputs. For HandoffActivate, TransitionV1 directly binds dfjSourceFenced_f_j^SourceFenced; AcquisitionV1 binds it transitively through dτd_τ, and the seal binds it directly. The revision must be the current open SourceFenced revision or HandoffRevision fails stale. hc.auxRefh_c.auxRef also names this input but never the output or seal. The head core has no direct seal dependency: h′h binds dseald_seal transitively through drCd_r_C. The same rule applies to BranchCreate with dξd_ξ: direct in the transition and seal, transitive through dτd_τ in the acquisition, and revalidated from Ξ[k] [k] at both freshness checks. The output revision binds the open input and dhcd_h_c; successful activation then clears the pointer while retaining both revisions in F. The order is (dξ?,dfjSourceFenced?) (d_ξ?,d_f_j^SourceFenced?) ≺dτ≺dW≺(X′,Γ′,ME) d_τ d_W (X , ,M_E) ≺dg?≺dseal≺hc≺dfj+1TargetActive? d_g? d_seal h_c d_f_j+1^TargetActive? ≺ℓ≺rC≺h′≺dh′ r_C h d_h ≺(O,E,HR?,B′,G′)≺i. (O,E,H_R?,B ,G ) Publish i. (16) The receipt binds the prospective unit P^χ P_χ, not the complete head; the complete head h′h then binds drCd_r_C, producing dh′d_h . The lineage edge likewise binds hch_c and typed predecessor, not the complete successor. Therefore every digest edge points left in Equation 16, and the audited graph is acyclic. Outcome, effect, handoff-result, branch, and directory records point only to named earlier digests; no earlier object points back. Inclusion evidence is constructed only after publication. Atomic publication changes visibility, not this hash order. B.2 Proof sketches Proposition 1. Every outcome-writing path first authenticates the proposal allocation and revalidates it in the proposal-scope serialization domain. Invalid outer requests never write an outcome. The first authorized write uniquely inserts O[pkey]O[pkey]; a compatible retry returns it, an incompatible retry conflicts, and a reclaimed identifier is rejected by the monotone watermark. A second durable disposition is therefore impossible under A1–A4 and A8. ∎ Proposition 2. The seal binds the proposal, evidence, interpreter, typed Present/Absent expectation, candidate root, and effect manifest. Activation serializes the branch key and compares either the complete head or continued absence plus dξd_ξ. The first Commit changes that serialization point atomically; every contender then fails exact-head or absence admission. Thus at most one sealed candidate becomes the exact successor or genesis under A1–A4. ∎ Proposition 3. The operation–manifest bijection rejects an effect identifier repeated within a proposal. Across proposals, Commit uniquely inserts E[eid]E[eid] while holding its scope. Reclamation advances the scope watermark before deleting online rows, and scopes are never recycled. Hence deletion cannot reopen an accepted identifier under A1, A4, and A8. ∎ These are conditional serialization arguments. They establish neither content truth nor correctness of policy, canonicalization, cryptography, or storage implementations. Appendix C Total Lifecycle, Handoff, and Restoration Semantics C.1 Handoff Union Types and Kind-Specific Admission Equation 1 is normative for B. In particular, dirSeqdirSeq lives only in B; a revision records dirSeqIn,dirSeqOutdirSeqIn,dirSeqOut as snapshots. createdFrom∈,(dh)createdFrom∈\ None, SourceProvenance(d_h)\ is assigned at genesis and copied byte-for-byte thereafter. Pointer activity and revision state are distinct closed types: HPtr =⊥∣(hid,df), = Open(hid,d_f), (17) FState =∣ = Prepared SourceFenced |. Aborted TargetActive. Table 13: Transition-kind-specific head admission within the single ordered ActCheck vector. Kind Serialized GheadkindG^kind_head precondition Parent and disposition Ordinary, Migration, Restoration B=⟨h,,w,e,d,z,c⟩B= h, Active,w,e,d,z,c ; exact expected=hexpected=h, writer w, epoch e, and dirSeq=ddirSeq=d; an Open z must reference Prepared, never SourceFenced. (dh) AcceptedParent(d_h); one of the four proposal dispositions. HandoffActivate B=⟨hs,,⊥,ec,d,(hid,dfjSourceFenced),c⟩B= h_s, Frozen, ,e_c,d, Open(hid,d_f_j^SourceFenced),c ; exact fenced head, target writer, dirSeq=ddirSeq=d, input revision and current context; the revision separately binds reservedEpoch=erreservedEpoch=e_r, and admission requires the proposal to bind both ec,ere_c,e_r with ec=ere_c=e_r. (dhs) AcceptedParent(d_h_s); an ordinary Commit/Reject/Quarantine/Defer outcome under O[pkey]O[pkey]. BranchCreate B[k]B[k] absent, expected=expected= Absent, and exact serialized Ξ[k]=ξk [k]= _k; authenticated allocation/absence proof and zero initial counters. (dg) GenesisParent(d_g); ordinary Commit with kind BranchCreate. An ordinary Commit during Prepared is nonconflicting but makes that revision’s source-head binding stale. Fence then returns StaleHead; Abort followed by a fresh Prepare is required before fencing. Any change to target, epoch, dirSeqdirSeq, input revision, dGd_G, or the current admission versions similarly invalidates an older target package. C.2 Authoritative State Postconditions Let b=⟨h,s,w,e,d,z,c⟩b= h,s,w,e,d,z,c follow the field order of Equation 1; b[a←x]b[a← x] copies b and explicitly replaces field a. The HResult map is HRH_R. Let KL=(hid,lid)K_L= LifecycleKeyV1(hid,lid) and KH=(pkey,hid)K_H= HandoffResultKeyV1(pkey,hid) be disjoint typed keys; lidlid and pidpid are owner-allocated, non-recycled names. A unique insert makes each HRH_R key immutable: an exact retry returns the stored value and a variant conflicts. “Append rLr_L” below means ℛ[drL]=rLR[d_r_L]=r_L in the same atomic unit. For compactness, let =⟨X,Γ,rev,issuer,policy,Ξ,h,L,O,E,G⟩S= X, ,rev,issuer,policy, ,h,L,O,E,G ; ′=S =S explicitly copies every listed family, including Ξ′=Ξ = . Table 14: Total lifecycle postconditions. Every authoritative family is assigned explicitly or through the complete accepted unit; Ξ′=Ξ = holds for all rows. Action Exact precondition Complete authoritative poststate Receipt/result records Genesis B[k]B[k] absent; BranchCreate row of Table 13 Install accept()U_accept( BranchCreate): X0,Γ0,g,h0,L,E[ME],Gχ′X_0, _0,g,h_0,L,E[M_E],G _χ and B′[k]=⟨h0,,wt,0,0,⊥,c0⟩B [k]= h_0, Active,w_t,0,0, ,c_0 ; Ξ′=Ξ = ; F,HRF,H_R not written. O[pkey]=(,drC,h0)O[pkey]= OutcomeV1( Commit,d_r_C,h_0) and ℛ[drC]=rCR[d_r_C]=r_C. Prepare b.status=b.status= Active, b.writer=wsb.writer=w_s, exact head/epoch/dirSeqdirSeq, and b.handoff=⊥b.handoff= ′=S =S; B′=b[dirSeq←d+1,handoff←(hid,dfj+1Prepared)]B =b[dirSeq← d+1,handoff← Open(hid,d_f_j+1^Prepared)], preserving createdFromcreatedFrom; append fj+1Preparedf_j+1^Prepared to F and reserve er=e+1e_r=e+1. Append rL=rbL()r_L=rb_L( Applied) and HR[KL]=(drL,⊥,dfj+1Prepared)H_R[K_L]= Lifecycle(d_r_L, ,d_f_j+1^Prepared). Abort Exact fjPreparedf_j^Prepared; Active, writer wsw_s, epoch e, dirSeq=ddirSeq=d, and matching Open pointer ′=S =S; B′=b[dirSeq←d+1,handoff←⊥]B =b[dirSeq← d+1,handoff← ], preserving createdFromcreatedFrom; append the Aborted revision to F and cancel ere_r. Append rLr_L and HR[KL]=(drL,dfjPrepared,dfj+1Aborted)H_R[K_L]= Lifecycle(d_r_L,d_f_j^Prepared,d_f_j+1^Aborted). Fence Exact fjPreparedf_j^Prepared, its final h, and active source tuple ′=S =S; preserve createdFromcreatedFrom and set B′.status=B .status= Frozen, writer=⊥writer= , epoch=erepoch=e_r, dirSeq=d+1dirSeq=d+1, and handoff=(hid,dfj+1SourceFenced)handoff= Open(hid,d_f_j+1^SourceFenced); append SourceFenced revision with old epoch e and new/reserved epoch ere_r. Append rLr_L and HR[KL]=(drL,dfjPrepared,dfj+1SourceFenced)H_R[K_L]= Lifecycle(d_r_L,d_f_j^Prepared,d_f_j+1^SourceFenced). Retarget Exact fjSourceFencedf_j^SourceFenced; Frozen, writer ⊥ , epoch e, dirSeq=ddirSeq=d, and matching Open pointer ′=S =S; preserve status, writer, head, and createdFromcreatedFrom; set epoch e+1e+1, dirSeq=d+1dirSeq=d+1, and handoff=(hid,dfj+1SourceFenced)handoff= Open(hid,d_f_j+1^SourceFenced); append SourceFenced revision naming the new target and reserved epoch e+1e+1. Append rLr_L and HR[KL]=(drL,dfjSourceFenced,dfj+1SourceFenced)H_R[K_L]= Lifecycle(d_r_L,d_f_j^SourceFenced,d_f_j+1^SourceFenced). Activate HandoffActivate row of Table 13 Install accept()U_accept( HandoffActivate): XT′,h′,L,E[ME],Gχ′X _T,h ,L,E[M_E],G _χ, append fj+1TargetActivef_j+1^TargetActive, set Ξ′=Ξ = and B′=⟨h′,,wt,ec,d+1,⊥,c⟩B = h , Active,w_t,e_c,d+1, ,c ; install the current-or-authorized ΓT,revT,issuerT,policyT _T,rev_T,issuer_T,policy_T. ℛ[drC]=rCR[d_r_C]=r_C, O[pkey]=(,drC,h′)O[pkey]= OutcomeV1( Commit,d_r_C,h ), and HR[KH]=(dfjSourceFenced,dfj+1TargetActive,drC,h′)H_R[K_H]= Activation(d_f_j^SourceFenced, d_f_j+1^TargetActive, d_r_C, h ): the receipt digest is identical. Restore Ordinary-kind row; authenticated checkpoint/proof/mask and optional pinned migrator Install accept()U_accept( Restoration) with X′=RestoreM(Xc,Mμ(Xk))X =Restore_M(X_c,M_μ(X_k)), new h′,L,E[ME],Gχ′h ,L,E[M_E],G _χ, Ξ′=Ξ = and B′=b[head←h′]B =b[head← h ]; status, writer, epoch, dirSeqdirSeq, handoff, createdFromcreatedFrom, and protected authority families stay current. Ordinary Commit in O and ℛR; no HRH_R or F write; checkpoint is auxiliary lineage, never a parent. Failure Any authenticated maintenance action whose exact precondition fails ′=S =S, B′=B =B, and F′=F =F; no accepted state, effect, directory, or lifecycle-revision write. Append rL=rbL(qL)r_L=rb_L(q_L) and the action-indexed HR[KL]H_R[K_L] from Appendix A; the output revision is forbidden. Every HandoffRevisionV1 binds its predecessor revision, action/state, branch key, source head/writer, target writer, old/new and reserved epochs, dirSeqIn,dirSeqOutdirSeqIn,dirSeqOut, pinned policy/authority/revocation versions, digests of Γ,G ,G, optional dhcd_h_c, reason, and trusted time. F[hid,j]F[hid,j] is append-only. Maintenance changes only the fields and indexes assigned in Table 14; it never creates an O entry. The consumed target package is PH=⟨ P_H= pkey,dτ,dW,dseal,hid,dfjSourceFenced,dhs, pkey,d_τ,d_W,d_seal,hid,d_f_j^SourceFenced,d_h_s, wt,ec,er,dirSeq,policyV,authV,revV,dΓ,dG⟩, w_t,e_c,e_r,dirSeq,policyV,authV,revV,d_ ,d_G , (18) where ece_c is the pre-activation canonical epoch and ere_r is the separately reserved successor epoch. Admission requires both to remain exact and equal. The accepted unit creates the distinct output fj+1TargetActivef_j+1^TargetActive; Appendix B fixes every digest placement. Precisely, ΓT=Γcurrent _T= _current when no separately authorized authority transition exists, and ΓT=Γ′ _T= only when the same accepted proposal authorizes and binds Γ′ . The identical rule applies to revocation, issuer, and policy; the fenced historical head is never their source. C.3 Restoration Path Mask and Protected Semantics Restoration binds auxR=⟨ aux_R= dhc,drootc,dhk,drootk, d_h_c,d_root_c,d_h_k,d_root_k, proofk,dμ,M,componentRoots⟩ proof_k,d_μ,M,componentRoots (19) and computes X′=RestoreM(Xc,Mμ(Xk))X =Restore_M(X_c,M_μ(X_k)). For protected paths P= P=\ authority,policy,revocation,issuer, authority,policy,revocation,issuer, writer,epoch,dirSeq,lifecycle,createdFrom, writer,epoch,dirSeq,lifecycle,createdFrom\, M∩P M∩ P =∅,X′|P=Xc|P. = , 18.49988ptX |_P=X_c|_P. (20) Malformed or unauthenticated outer lifecycle requests create no receipt. Appendix D Deterministic Resource Profile and Artifact Table 15: Exact counter increments. An occurrence is counted even if later deduplicated; tests happen before the event that would exceed its bound. Counter Increment or depth event Counter Increment or depth event inputOctets Before consuming each primary or supplied-context octet; duplicate packaged objects count again. decodeDepth Entering a JSON array/object; root depth is 1 and exit decrements it. decodedItems Decoder emits each member, array element, or scalar occurrence in the primary or each supplied context object. expandedTerms JSON-LD expansion emits each node, property, or value occurrence. contextUrls Before each JSON-LD Context Processing URL attempt after base resolution; repeated URLs, repeated references, and cache hits count. contextDepth Entering each logical nested Context Processing call; root is 1, cache use changes neither entry nor exit. expansionDepth Entering a recursive JSON-LD expansion call; root is 1 and exit decrements it. quads RDF conversion emits each quad occurrence, before set deduplication. blankNodes First allocation or capture of each distinct blank-node identifier. nDegreeCalls Entry to each RDFC Hash N-Degree Quads invocation. permutationBranches Before exploring each RDFC permutation candidate. issuerEntries Before a logical issuer state first becomes reachable, charge every mapping in that state: a fresh insertion charges one and a clone charges its full inherited mapping cardinality. Equal mappings in distinct issuers or clones count again; structural sharing gives no discount. pathUnits Each identifier, position, or digest token appended to an N-degree path. intermediateUnits Simultaneously with each increment of decodedItems, expandedTerms, quads, permutationBranches, issuerEntries, or pathUnits; hence it is their running sum. D.1 Canonicalization resource profile Canonicalization is governed by the signed, versioned profile κ=⟨ κ= jsonldV,rdfcV,contextDigests, jsonldV,rdfcV,contextDigests, maxContextUrls,maxContextDepth, maxContextUrls,maxContextDepth, maxBytes,maxDecodeDepth, maxBytes,maxDecodeDepth, maxDecodedItems,maxQuads, maxDecodedItems,maxQuads, maxExpandedTerms,maxExpansionDepth, maxExpandedTerms,maxExpansionDepth, maxBlankNodes,maxNDegreeCalls, maxBlankNodes,maxNDegreeCalls, maxPermutationBranches,maxIssuerEntries, maxPermutationBranches,maxIssuerEntries, maxPathUnits,maxIntermediateUnits⟩. maxPathUnits,maxIntermediateUnits . (21) jsonldVjsonldV pins the 16 July 2020 JSON-LD 1.1 Processing Algorithms and API Recommendation: processingMode=json-ld-1.1, its Context Processing and Expansion algorithms, ordered=true, rdfDirection=null, a signed absolute base IRI, and produceGeneralizedRdf=false. Input is UTF-8 application/ld+json containing one JSON object or array; HTML extraction and ambient bases are forbidden [18, 17]. Remote contexts are digest-pinned package objects, never network-fetched. Each reference resolves against the signed base to one exact URL–digest manifest entry; redirects, negotiation, and unlisted URLs are rejected. Primary and all supplied context bytes are charged at RawScreen and decoded at Decode. Duplicate supplied objects are charged separately; repeated references and cache hits do not recharge bytes but do count logical context-processing attempts. rdfcVrdfcV pins RDFC-1.0 [10]. The path is JSON decode, Context Processing/Expansion, RDF emission, then RDFC canonicalization. Table 15 defines mathematical nonnegative counters, not implementation allocations. All cumulative counters reset once per proposal and sum occurrences across its datasets; they never reset per recursive invocation. Depth counters are active recursion gauges. inputOctets belongs to RawScreen, decodeDepth/decodedItems to Decode, and the remaining counters to Canonicalize. Every bound is tested before its event; context URL/depth exhaustion terminates at Canonicalize before lookup or recursive entry, with CanonicalizationLimit and no partial candidate. For a clone, the full inherited charge is tested before the clone becomes reachable; for insertion, the unit charge is tested before insertion. Either failure terminates at Canonicalize with the same CanonicalizationLimit receipt and no partial issuer state. Crossing any other limit terminates at its governing RawScreen, Decode, or Canonicalize stage with CanonicalizationLimit, produces no partial candidate, and binds drawd_raw rather than a nonexistent dτd_τ. RDFC-1.0 separately identifies adversarially expensive graph structure as a denial-of-service risk [10]; this is canonicalization complexity poisoning, not a semantic claim that the resulting graph is false. A local wall-clock, memory, or process watchdog may stop work earlier, but that event is a transient operational failure with no durable disposition unless the implementation can translate it into the deterministic counters above. D.2 Conditional assumptions All safety claims are conditional on: A1 Mediation. No bypass credential or API can advance an authoritative head or protocol index. A2 Encoding and cryptography. Canonical encodings, typed hash domains, and signature schemes have their stated security and interoperability properties. A3 Key custody. Proposal, allocator, evaluator, preparation-service, candidate-seal, and kernel keys are protected and restricted to their declared principals and scopes. A4 Atomic serialization. The complete accepted unit, lifecycle changes, and reclamation changes serialize over every named mutable key and are durably all-or-none. A5 Complete context. Policy, evaluator, authority, revocation, dependency, allocation, and lifecycle versions are locally lockable or transactionally revalidated. A6 Trusted time. Activation obtains a conservative commit-time interval or an equivalent storage-enforced deadline. A7 Lifecycle order. Branch creation, epochs, handoff, and recovery share one order observed by writers. A8 Non-recycled scopes. Authenticated allocators issue monotone proposal/effect identifiers; retirement watermarks advance before covered rows are deleted. A9 Verification objects. Replay and inclusion are claimed only when their required objects, interpreters, keys, and certified-state proofs are available. Availability is not assumed. Receipt structural authenticity and kernel attestation use A1–A3; independent replay additionally uses the relevant A5–A6 objects and A9; durable inclusion additionally uses A4, A8, and A9. D.3 Executable Model and Artifact Specification The formal state-space exploration of Section 5 is provided as an executable Python artifact (artifacts/bounded_model.py). The artifact imports only standard library modules (collections, dataclasses, typing) and executes an exhaustive breadth-first search (BFS) state exploration over the finite protocol state space. The executable model verifies that across all 2,808,230 reachable states and 5,526,474 state-changing transitions: (1) no encoded invariant is violated; (2) every named protocol coverage witness is reached; and (3) all terminal dispositions, 17-stage check sequences, pre-state authority rules, writer fencing, and forward restoration postconditions hold. Reproduction instructions and SHA-256 integrity digests are documented in artifacts/README.md.