diff --git a/HexInterval/Experiment/DyadicRules.lean b/HexInterval/Experiment/DyadicRules.lean
index 0b6bcde65..3b80b6a5b 100644
--- a/HexInterval/Experiment/DyadicRules.lean
+++ b/HexInterval/Experiment/DyadicRules.lean
@@ -473,7 +473,7 @@ def arithmeticPackage (config : Config) (real : DomainId) : Package Fact :=
         Handler.statelessPlanned squareForward (invokeSquareForward config),
         Handler.statelessPlanned reciprocalForward (invokeReciprocalForward config),
         Handler.statelessPlanned reciprocalBackward (invokeReciprocalBackward config)]
-    acceptsLimits := fun _ limits =>
+    acceptsLimits := fun _ limits _ =>
       config.maxReciprocalEffort ≤ limits.maxEffort &&
         config.reciprocalPrecisionsAllowed &&
         2 ≤ limits.maxObservationValue && 60 ≤ limits.maxDiagnosticValue &&
@@ -491,7 +491,7 @@ def centeredPackage (config : Config) (real : DomainId) : Package Fact :=
       #[Handler.statelessPlanned centeredForward (invokeCenteredForward config),
         Handler.statelessDroppingDrafts centeredSplit invokeCenteredSplit,
         Handler.statelessPlanned centeredInstantiate invokeCenteredInstantiate]
-    acceptsLimits := fun _ limits =>
+    acceptsLimits := fun _ limits _ =>
       4 ≤ limits.maxObservationValue &&
         71 ≤ limits.maxDiagnosticValue &&
         1 ≤ limits.maxOutcomeCandidates && 1 ≤ limits.maxOutcomeSuggestions &&
@@ -505,6 +505,19 @@ def buildRegistry (config : Config) (real : DomainId) (limits : Limits) :
   Propagator.Registry.buildWithin limits
     #[arithmeticPackage config real, centeredPackage config real]
 
+/-- The legacy search-only driver allocates no proof payloads. Packages used
+through it must therefore accept the empty arena envelope as well as the
+engine limits. Proof-producing execution supplies its real envelope through
+`PayloadSession`. -/
+def searchArenaLimits : PayloadArena.Limits :=
+  { maxEntries := 0
+    maxBodyCells := 0
+    maxDrafts := 0
+    maxDraftCells := 0
+    maxAtom := 0
+    maxSchema := 0
+    maxUses := 0 }
+
 inductive StartError where
   | incompatibleLimits
   | registry (error : RegistryError)
@@ -524,7 +537,8 @@ def start (config : Config) (real : DomainId) (program : Program)
       | .error error => .error (.engine (.engine error))
       | .ok () =>
           if !registry.acceptsProgram program then .error .operationMismatch
-          else if !registry.acceptsLimits program limits then .error .incompatibleLimits
+          else if !registry.acceptsLimits program limits searchArenaLimits then
+            .error .incompatibleLimits
           else
             match DyadicInterval.start config.endpointLimit program registry.registrations
                 rawFacts limits with
diff --git a/HexInterval/Experiment/PackageRegistry.lean b/HexInterval/Experiment/PackageRegistry.lean
index baa282930..238410140 100644
--- a/HexInterval/Experiment/PackageRegistry.lean
+++ b/HexInterval/Experiment/PackageRegistry.lean
@@ -97,15 +97,17 @@ introduced by this package, while `requiredOperations` records exact
 signatures supplied elsewhere but interpreted by its matchers.  A handler may
 target such an external operation; final head validation remains the engine's
 responsibility once the complete program is available.  `acceptsLimits` is a
-package-owned configuration preflight, not a soundness boundary: every reply
-is still checked against the engine limits. -/
+package-owned configuration preflight over the engine and payload-arena
+envelopes, not a soundness boundary: every reply is still checked by both
+owners. -/
 structure Package (Fact : Type) where
   Cache : Type
   cache : Cache
   operations : Array Operation := #[]
   requiredOperations : Array Operation := #[]
   handlers : Array (Handler Fact Cache)
-  acceptsLimits : Program -> Limits -> Bool := fun _ _ => true
+  acceptsLimits : Program -> Limits -> PayloadArena.Limits -> Bool :=
+    fun _ _ _ => true
   /-- Non-semantic routing telemetry used to check that only the selected
   package snapshot changes. -/
   invocations : Nat := 0
@@ -256,12 +258,13 @@ def acceptsProgram (registry : Registry Fact) (program : Program) : Bool :=
     registry.packages.all fun package =>
       package.requiredOperations.all (operationAccepted program)
 
-/-- Run every package-owned configuration preflight over the final program and
-engine resource envelope. -/
+/-- Run every package-owned configuration preflight over the final program,
+engine resource envelope, and proof-payload arena envelope. -/
 def acceptsLimits (registry : Registry Fact) (program : Program)
-    (limits : Limits) : Bool :=
+    (limits : Limits) (arenaLimits : PayloadArena.Limits) : Bool :=
   DispatchCode.requestMismatch ≤ limits.maxDiagnosticValue &&
-    registry.packages.all fun package => package.acceptsLimits program limits
+    registry.packages.all fun package =>
+      package.acceptsLimits program limits arenaLimits
 
 end Registry
 
diff --git a/HexInterval/Experiment/PayloadArena.lean b/HexInterval/Experiment/PayloadArena.lean
index d5ad31d68..216078bcd 100644
--- a/HexInterval/Experiment/PayloadArena.lean
+++ b/HexInterval/Experiment/PayloadArena.lean
@@ -87,12 +87,19 @@ def wellFormed (arena : Arena) : Bool :=
 
 end Arena
 
-/-- Trusted bounds for the prospective whole arena. -/
+/-- Trusted per-reply and whole-run bounds for prospective freezing. -/
 structure Limits where
+  /-- Cumulative frozen entries retained by the whole run. -/
   maxEntries : Nat
+  /-- Cumulative encoded body cells retained by the whole run. -/
   maxBodyCells : Nat
+  /-- Drafts supplied by one package reply. -/
+  maxDrafts : Nat
+  /-- Encoded body cells supplied by one package reply. -/
+  maxDraftCells : Nat
   maxAtom : Nat
   maxSchema : Nat
+  /-- Payload-bearing proposal positions traversed in one reply. -/
   maxUses : Nat
   deriving DecidableEq, Repr
 
@@ -106,8 +113,14 @@ inductive Invalid where
 
 /-- A trusted arena limit exhausted before allocation. -/
 inductive Resource where
+  /-- The remaining whole-run entry capacity is exhausted. -/
   | entries
+  /-- The remaining whole-run body-cell capacity is exhausted. -/
   | bodyCells
+  /-- One reply supplied too many drafts. -/
+  | drafts
+  /-- One reply supplied too many encoded body cells. -/
+  | draftCells
   | atom
   | schema
   | uses
@@ -243,13 +256,26 @@ def validate (uses : List Use) (drafts : List Draft) : Option Invalid :=
       | some error => some error
       | none => checkCoverage uses drafts
 
-/-- Consume a body-cell budget while checking every encoded recipe atom. -/
+/-- One exact draft list after reply-local bounds have been checked. Its
+private constructor prevents callers from pairing an invented cell count with
+different drafts before cumulative preflight or freezing. -/
+structure BoundedDrafts where
+  private mk ::
+  drafts : List Draft
+  cells : Nat
+
+/-- Traverse a reply body through the first cell beyond its local budget.
+Every visited atom is checked before its cell is charged, so an oversized
+boundary atom reports `.atom`. Cells after a `.draftCells` stop are
+deliberately not inspected. -/
 def consumeBody (maxAtom : Nat) : Nat -> List Nat -> Except Resource Nat
   | remaining, [] => pure remaining
-  | 0, _ :: _ => throw .bodyCells
-  | remaining + 1, atom :: atoms =>
+  | remaining, atom :: atoms =>
       if maxAtom < atom then throw .atom
-      else consumeBody maxAtom remaining atoms
+      else
+        match remaining with
+        | 0 => throw .draftCells
+        | remaining + 1 => consumeBody maxAtom remaining atoms
 
 def consumeDrafts (maxAtom : Nat) :
     Nat -> List Draft -> Except Resource Nat
@@ -258,26 +284,35 @@ def consumeDrafts (maxAtom : Nat) :
       let remaining ← consumeBody maxAtom remaining draft.body
       consumeDrafts maxAtom remaining drafts
 
-/-- Check aggregate entry, draft-work, schema, and cell limits before
-constructing any new entry.  In particular the draft list is bounded by both
-remaining arena room and `maxUses` before the quadratic exact-coverage checks
-run. -/
-def preflight (limits : Limits) (arena : Arena) (drafts : List Draft) :
-    Except Resource Nat := do
+/-- Check only reply-local draft, schema, atom, and cell bounds. The returned
+opaque transaction retains the exact list whose cell count was derived.
+Exact draft coverage must still be validated before whole-run capacity is
+consulted. -/
+opaque preflightLocal (limits : Limits) (drafts : List Draft) :
+    Except Resource BoundedDrafts := do
+  if !listWithin limits.maxDrafts drafts then
+    throw .drafts
+  if drafts.any (fun draft => limits.maxSchema < draft.schema) then
+    throw .schema
+  let remaining ← consumeDrafts limits.maxAtom limits.maxDraftCells drafts
+  pure { drafts, cells := limits.maxDraftCells - remaining }
+
+/-- Compare an already locally bounded and exactly validated transaction with
+remaining whole-run capacity. Consequently `.entries` and `.bodyCells` mean
+genuine cumulative exhaustion by otherwise valid evidence. -/
+def preflightWhole (limits : Limits) (arena : Arena)
+    (bounded : BoundedDrafts) : Except Resource Unit := do
   if limits.maxEntries < arena.entries.size then
     throw .entries
   let entryRoom := limits.maxEntries - arena.entries.size
-  if !listWithin limits.maxUses drafts then
-    throw .uses
-  if !listWithin entryRoom drafts then
+  if !listWithin entryRoom bounded.drafts then
     throw .entries
-  if drafts.any (fun draft => limits.maxSchema < draft.schema) then
-    throw .schema
   if limits.maxBodyCells < arena.bodyCells then
     throw .bodyCells
   let cellRoom := limits.maxBodyCells - arena.bodyCells
-  let remaining ← consumeDrafts limits.maxAtom cellRoom drafts
-  pure (cellRoom - remaining)
+  if cellRoom < bounded.cells then
+    throw .bodyCells
+  pure ()
 
 structure Relocation where
   source : PayloadId
@@ -310,9 +345,10 @@ def appendDrafts (origin : Action) :
       (entries, { source := draft.label, global } :: relocations)
 
 def freezeDrafts (arena : Arena) (origin : Action)
-    (drafts : List Draft) (addedCells : Nat) : Arena × List Relocation :=
-  let (entries, relocations) := appendDrafts origin arena.entries drafts
-  ({ entries, bodyCells := arena.bodyCells + addedCells }, relocations)
+    (bounded : BoundedDrafts) : Arena × List Relocation :=
+  let (entries, relocations) :=
+    appendDrafts origin arena.entries bounded.drafts
+  ({ entries, bodyCells := arena.bodyCells + bounded.cells }, relocations)
 
 /-- Validate and freeze every reply-local payload reference in an outcome.
 
@@ -327,17 +363,20 @@ def freeze (limits : Limits) (arena : Arena) (origin : Action)
   | .error resource => .resourceLimit resource arena
   | .ok _ =>
       let uses := outcomeUses outcome
-      match preflight limits arena drafts with
+      match preflightLocal limits drafts with
       | .error resource => .resourceLimit resource arena
-      | .ok addedCells =>
-          match validate uses drafts with
+      | .ok bounded =>
+          match validate uses bounded.drafts with
           | some error => .invalid error arena
           | none =>
-              let (prospective, relocations) :=
-                freezeDrafts arena origin drafts addedCells
-              match relocateOutcome relocations outcome with
-              | .error error => .invalid error arena
-              | .ok outcome =>
-                  .ready prospective outcome
+              match preflightWhole limits arena bounded with
+              | .error resource => .resourceLimit resource arena
+              | .ok _ =>
+                  let (prospective, relocations) :=
+                    freezeDrafts arena origin bounded
+                  match relocateOutcome relocations outcome with
+                  | .error error => .invalid error arena
+                  | .ok outcome =>
+                      .ready prospective outcome
 
 end Hex.Interval.Experiment.PayloadArena
diff --git a/HexInterval/Experiment/PayloadSession.lean b/HexInterval/Experiment/PayloadSession.lean
new file mode 100644
index 000000000..676c83ac8
--- /dev/null
+++ b/HexInterval/Experiment/PayloadSession.lean
@@ -0,0 +1,327 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexInterval.Experiment.PackageRegistry
+
+@[expose] public section
+
+/-!
+# Session-owned interval propagation and proof payloads
+
+A session binds the checked engine, the exact function-package registry that
+compiled it, and one immutable proof-payload arena. Its private constructor
+prevents callers from pairing independently assembled values.
+
+For a rule action, `advance` invokes the routed package, freezes and relocates
+all reply-local proof labels prospectively, and submits the relocated outcome.
+The new arena commits only when engine submission succeeds. Package caches may
+still record a failed invocation because they are explicitly non-semantic;
+engine facts, expression nodes, provenance, and the arena remain atomic.
+Malformed package evidence is submitted to the engine as a failed rule reply:
+the request latch is cleared, the session remains usable, and completeness is
+permanently lost. Exceeding a package-local payload-use, draft, draft-cell,
+atom, or schema bound has the same recoverable behavior. Exhausting remaining
+whole-run arena entry or body capacity after earlier commits, or encountering
+an engine-invalid transition, instead returns a non-live session snapshot
+which cannot later be resumed and mislabeled saturated. This cumulative stop
+is an intentional conservative policy for the eager prototype: an otherwise
+valid selected transition could not be retained, so the session treats it like
+global engine-resource exhaustion rather than skipping required work. Package
+failure and unprocessed narrowing suggestions likewise make the final status
+incomplete.
+-/
+
+namespace Hex.Interval.Experiment.PayloadSession
+
+open Propagator
+
+/-- Failure while assembling one coherent run snapshot. -/
+inductive StartError where
+  | registry (error : RegistryError)
+  | programRejected
+  | incoherentLimits
+  | limitsRejected
+  | engine (error : Propagator.StartError)
+  deriving DecidableEq, Repr
+
+/-- Engine, package registry, and proof arena with a private pairing
+constructor. Public projections permit inspection without permitting a forged
+session. -/
+structure Session (Fact : Type) where
+  private mk ::
+  engine : Engine Fact
+  registry : Registry Fact
+  arena : PayloadArena.Arena
+  arenaLimits : PayloadArena.Limits
+  /-- Some rule or narrowing work was dropped rather than retained. -/
+  droppedWork : Bool
+  live : Bool
+
+private def make (engine : Engine Fact) (registry : Registry Fact)
+    (arenaLimits : PayloadArena.Limits) : Session Fact :=
+  { engine
+    registry
+    arena := .empty
+    arenaLimits
+    droppedWork := false
+    live := true }
+
+/-- A sound upper bound on payload-arena work in any engine-valid reply:
+every candidate, every suggestion constructor, and at most
+`maxProposalItems` nested equalities for each suggestion. -/
+def requiredUses (limits : Propagator.Limits) : Nat :=
+  limits.maxOutcomeCandidates +
+    limits.maxOutcomeSuggestions * (limits.maxProposalItems + 1)
+
+/-- The count envelope admits one distinct draft for every engine-valid
+payload use. `maxDrafts ≤ maxUses` also bounds malformed pre-coverage draft
+lists by the use-traversal envelope, while the local draft and cell caps must
+fit an empty arena. Therefore only capacity consumed by earlier commits can
+produce a whole-run exhaustion. -/
+def limitsCoherent (limits : Propagator.Limits)
+    (arenaLimits : PayloadArena.Limits) : Bool :=
+  requiredUses limits ≤ arenaLimits.maxDrafts &&
+    arenaLimits.maxDrafts ≤ arenaLimits.maxUses &&
+    arenaLimits.maxDrafts ≤ arenaLimits.maxEntries &&
+    arenaLimits.maxDraftCells ≤ arenaLimits.maxBodyCells
+
+/-- Bound package metadata, compile and validate the engine-owned program,
+then run package-specific program checks and start with an empty proof arena.
+The generic engine preflight precedes any package callback which may traverse
+the program. -/
+opaque Session.start (factDomain : FactDomain Fact) (program : Program)
+    (packages : Array (Package Fact)) (facts : Array Fact)
+    (limits : Propagator.Limits) (arenaLimits : PayloadArena.Limits) :
+    Except StartError (Session Fact) :=
+  match Registry.buildWithin limits packages with
+  | .error error => .error (.registry error)
+  | .ok registry =>
+      if !limitsCoherent limits arenaLimits then
+        .error .incoherentLimits
+      else
+        match Engine.start factDomain program registry.registrations facts limits with
+        | .error error => .error (.engine error)
+        | .ok engine =>
+            if !registry.acceptsProgram program then
+              .error .programRejected
+            else if !registry.acceptsLimits program limits arenaLimits then
+              .error .limitsRejected
+            else
+              .ok (make engine registry arenaLimits)
+
+/-- Result of one session-owned rule or equality transition. -/
+inductive Step (Fact : Type) where
+  | advanced (session : Session Fact)
+  | saturated (session : Session Fact)
+  | incomplete (session : Session Fact)
+  | contradiction (session : Session Fact)
+  | engineResource (resource : Propagator.Resource) (session : Session Fact)
+  | factResource (budget : Nat) (session : Session Fact)
+  | invalidReply (error : ReplyError) (session : Session Fact)
+  | invalidPayload (error : PayloadArena.Invalid) (session : Session Fact)
+  /-- A package exceeded a per-reply payload encoding bound. The failed reply
+  is consumed and other independent work may continue. -/
+  | rejectedPayload (resource : PayloadArena.Resource) (session : Session Fact)
+  /-- An otherwise valid reply exhausted a cumulative arena bound. The eager
+  session intentionally stops instead of skipping selected required work. -/
+  | payloadResource (resource : PayloadArena.Resource) (session : Session Fact)
+  | invalidEngine (session : Session Fact)
+
+private def withEngine (session : Session Fact) (engine : Engine Fact) :
+    Session Fact :=
+  { session with engine }
+
+private def haltEngine (session : Session Fact) (engine : Engine Fact) :
+    Session Fact :=
+  { session with engine, live := false }
+
+private def haltRegistry (session : Session Fact) (engine : Engine Fact)
+    (registry : Registry Fact) : Session Fact :=
+  { session with engine, registry, live := false }
+
+private def commit (session : Session Fact) (engine : Engine Fact)
+    (registry : Registry Fact) (arena : PayloadArena.Arena)
+    (droppedWork : Bool) : Session Fact :=
+  { session with engine, registry, arena, droppedWork }
+
+/-- Whether the session still has all work required for a propagation fixed
+point. This deliberately covers fatal snapshots, previously dropped work, and
+retained narrowing suggestions; callers need not reconstruct those conditions
+from public projections. -/
+def Session.complete (session : Session Fact) : Bool :=
+  session.live && !session.droppedWork &&
+    !session.engine.suggestions.any fun retained =>
+      retained.suggestion.affectsClosure
+
+/-- Negative package outcomes which explicitly abandon required rule work.
+Suggestion loss is taken from the engine-returned admission plan instead. -/
+private def outcomeDropsWork : Outcome Fact -> Bool
+  | .resourceLimit _ | .failed _ => true
+  | .success _ _ _ | .noChange _ | .inapplicable => false
+
+/-- Check the two outer reply lists using the engine's own trusted bounds
+before the arena traverses payload uses or drafts. Nested instantiation lists
+remain bounded by the arena cap here and by `maxProposalItems` during engine
+admission. -/
+private def outcomeListsBounded (limits : Propagator.Limits) : Outcome Fact -> Bool
+  | .success candidates suggestions _ =>
+      listWithin limits.maxOutcomeCandidates candidates &&
+        listWithin limits.maxOutcomeSuggestions suggestions
+  | .noChange _ | .inapplicable | .resourceLimit _ | .failed _ => true
+
+namespace PayloadFailureCode
+
+/-- Stable engine diagnostic for a package plan rejected before semantic
+admission, whether for malformed drafts or a per-reply encoding bound. Zero is
+valid under every diagnostic limit. -/
+def rejected : Nat := 0
+
+end PayloadFailureCode
+
+/-- Clear a malformed package reply through the ordinary engine protocol.
+The typed payload error remains visible in the one-step result, while bounded
+drivers continue the live session and ultimately report incompleteness. -/
+private def failPayload (session : Session Fact) (engine : Engine Fact)
+    (registry : Registry Fact) (action : Action)
+    (error : PayloadArena.Invalid) : Step Fact :=
+  match engine.submit (action.reply (.failed PayloadFailureCode.rejected)) with
+  | .accepted _ next =>
+      .invalidPayload error
+        (commit session next registry session.arena true)
+  | .invalid replyError next =>
+      .invalidReply replyError (haltRegistry session next registry)
+  | .resourceLimit resource next =>
+      .engineResource resource (haltRegistry session next registry)
+  | .factResourceLimit budget next =>
+      .factResource budget (haltRegistry session next registry)
+
+/-- Treat a package-local payload bound violation like malformed package
+evidence: consume a bounded failed reply, retain no prospective arena entries,
+continue independent work, and permanently withhold completeness. -/
+private def rejectPayload (session : Session Fact) (engine : Engine Fact)
+    (registry : Registry Fact) (action : Action)
+    (resource : PayloadArena.Resource) : Step Fact :=
+  match engine.submit (action.reply (.failed PayloadFailureCode.rejected)) with
+  | .accepted _ next =>
+      .rejectedPayload resource
+        (commit session next registry session.arena true)
+  | .invalid replyError next =>
+      .invalidReply replyError (haltRegistry session next registry)
+  | .resourceLimit engineResource next =>
+      .engineResource engineResource (haltRegistry session next registry)
+  | .factResourceLimit budget next =>
+      .factResource budget (haltRegistry session next registry)
+
+/-- Run one checked transition. A prospective arena is discarded for every
+engine rejection or resource refusal. -/
+opaque Session.advance (session : Session Fact) : Step Fact :=
+  if !session.live then
+    .invalidEngine session
+  else match session.engine.poll with
+  | .request request engine =>
+      let (plan, registry) := session.registry.invokePlanned request
+      if !outcomeListsBounded engine.limits plan.outcome then
+        match engine.submit (request.action.reply plan.outcome) with
+        | .accepted _ _ =>
+            -- Defensive against validation drift: never retain an unfrozen
+            -- accepted outcome from this pre-screen rejection path.
+            .invalidEngine (haltRegistry session engine.finishReply registry)
+        | .invalid error next =>
+            .invalidReply error (haltRegistry session next registry)
+        | .resourceLimit resource next =>
+            .engineResource resource (haltRegistry session next registry)
+        | .factResourceLimit budget next =>
+            .factResource budget (haltRegistry session next registry)
+      else
+        match PayloadArena.freeze session.arenaLimits session.arena request.action
+            plan.outcome plan.drafts with
+        | .invalid error _ =>
+            failPayload session engine registry request.action error
+        | .resourceLimit resource _ =>
+            match resource with
+            | .uses | .drafts | .draftCells | .atom | .schema =>
+                rejectPayload session engine registry request.action resource
+            | .entries | .bodyCells =>
+                .payloadResource resource
+                  (haltRegistry session engine.finishReply registry)
+        | .ready arena outcome =>
+            match engine.submit (request.action.reply outcome) with
+            | .accepted admission next =>
+                .advanced
+                  (commit session next registry arena
+                    (session.droppedWork || outcomeDropsWork outcome ||
+                      admission.affectsClosure))
+            | .invalid error next =>
+                .invalidReply error (haltRegistry session next registry)
+            | .resourceLimit resource next =>
+                .engineResource resource (haltRegistry session next registry)
+            | .factResourceLimit budget next =>
+                .factResource budget (haltRegistry session next registry)
+  | .equality equality engine =>
+      match engine.contractEquality equality with
+      | .advanced _ next => .advanced (withEngine session next)
+      | .invalid _ _ next => .invalidEngine (haltEngine session next)
+      | .resourceLimit resource _ next =>
+          .engineResource resource (haltEngine session next)
+      | .factResourceLimit budget _ next =>
+          .factResource budget (haltEngine session next)
+  | .saturated engine =>
+      let session := withEngine session engine
+      if session.complete then
+        .saturated session
+      else
+        .incomplete session
+  | .contradiction engine => .contradiction (withEngine session engine)
+  | .resourceLimit resource engine =>
+      .engineResource resource (haltEngine session engine)
+  | .awaitingReply engine | .invalidState engine =>
+      .invalidEngine (haltEngine session engine)
+
+/-- Why a bounded session run stopped. -/
+inductive Stop where
+  | saturated
+  | incomplete
+  | contradiction
+  | engineResource (resource : Propagator.Resource)
+  | factResource (budget : Nat)
+  | invalidReply (error : ReplyError)
+  | payloadResource (resource : PayloadArena.Resource)
+  | invalidEngine
+  | driverFuel
+  deriving DecidableEq, Repr
+
+structure Run (Fact : Type) where
+  private mk ::
+  session : Session Fact
+  stop : Stop
+
+private def runSteps : Nat -> Session Fact -> Run Fact
+  | 0, session => { session, stop := .driverFuel }
+  | fuel + 1, session =>
+      match session.advance with
+      | .advanced next => runSteps fuel next
+      | .saturated next => { session := next, stop := .saturated }
+      | .incomplete next => { session := next, stop := .incomplete }
+      | .contradiction next => { session := next, stop := .contradiction }
+      | .engineResource resource next =>
+          { session := next, stop := .engineResource resource }
+      | .factResource budget next =>
+          { session := next, stop := .factResource budget }
+      | .invalidReply error next =>
+          { session := next, stop := .invalidReply error }
+      | .invalidPayload _ next => runSteps fuel next
+      | .rejectedPayload _ next => runSteps fuel next
+      | .payloadResource resource next =>
+          { session := next, stop := .payloadResource resource }
+      | .invalidEngine next => { session := next, stop := .invalidEngine }
+
+/-- Bounded FIFO execution through the session-owned evidence transaction. -/
+opaque Session.drive (fuel : Nat) (session : Session Fact) : Run Fact :=
+  runSteps fuel session
+
+end Hex.Interval.Experiment.PayloadSession
diff --git a/HexInterval/Experiment/Policy.lean b/HexInterval/Experiment/Policy.lean
index 218873afc..376d3b5ae 100644
--- a/HexInterval/Experiment/Policy.lean
+++ b/HexInterval/Experiment/Policy.lean
@@ -297,7 +297,7 @@ private def pruneSuggestions (state : State Fact) : State Fact := Id.run do
           clocks := clocks.set! index { clock with active := false }
           match state.engine.suggestions[index]? with
           | some retained =>
-              if retained.suggestion.affectsClosure then incomplete := true
+              if Suggestion.affectsClosure retained.suggestion then incomplete := true
           | none => pure ()
     | none => pure ()
   return { state with suggestions := clocks, incomplete }
@@ -734,7 +734,7 @@ closure of the current scope. -/
 opaque State.dismiss (state : State Fact) (selection : Selection) : SelectResult Fact :=
   match state.validate selection with
   | .error reason => reject state reason
-  | .ok offer =>
+  | .ok _ =>
       let next := match selection.id with
         | .application application =>
             let engine :=
@@ -747,10 +747,13 @@ opaque State.dismiss (state : State Fact) (selection : Selection) : SelectResult
             { advanceState (chargeDecision state .dismissal) engine with incomplete := true }
         | .suggestion suggestion =>
             let next := chargeDecision (consumeSuggestion state suggestion) .dismissal
-            match offer.key with
-            | .split _ _ _ _ => next
-            | .retry _ _ | .instantiate _ _ | .invoke _ | .equality _ =>
-                { next with incomplete := true }
+            match state.engine.suggestions[suggestion.index]? with
+            | some retained =>
+                if Suggestion.affectsClosure retained.suggestion then
+                  { next with incomplete := true }
+                else
+                  next
+            | none => { next with incomplete := true }
       .completed .dismissed next
 
 /-! # Exact rule observations -/
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index b8face770..7ffcf8c5c 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -994,12 +994,13 @@ packages. The current canary chooses an ordered `Array (Package Fact)`. Each
 package existentially owns one private `Cache` shared by its handlers and
 contributes owned operation signatures, exact external signatures required by
 its matchers, `(Registration, callback)` pairs, and a package-owned limit
-preflight. A handler head must be declared as owned or required.
+preflight over both the engine and proof-arena envelopes. A handler head must
+be declared as owned or required.
 `Registry.buildWithin` bounds package and metadata counts plus arities before
 flattening, builds a `Route` from each compact `RuleId` back to its package and
 handler, and rejects undeclared heads and duplicate `OpKey`s or `RuleKey`s.
 Program size and arity are bounded before exact signature lookup. The checked
-start then validates every owned and required signature against the final
+session start validates every owned and required signature against the final
 frontend program, runs each package's configuration preflight, and starts the
 engine with the registry's exact flattened registration array. Registry-owned
 dispatch diagnostics impose their own `maxDiagnosticValue` floor even when
@@ -1026,10 +1027,12 @@ registrations, callback routes, configuration validation, and the
 payload-freezing/replay schema implementations as one coherent snapshot.
 Whether that snapshot retains existential packages, compiles one dispatch
 function, supports hot replacement, or uses another lookup structure remains
-experimental. The present experiment exposes its constructors and returns a
-separable engine/registry pair, so its checked start is a conformance canary
-rather than the final encapsulation boundary. A production session should
-prevent accidentally pairing an engine with an unrelated registry; a
+experimental. `PayloadSession.Session` now has a
+private constructor and its checked start owns the matching engine, registry,
+arena, and arena limits; the bounded `Run` result also has a private
+constructor, so its stop classification can only come from session execution.
+The older direct registry and engine interfaces remain available for search
+experiments, but proof-producing execution goes through the session. A
 different callback implementation under the same versioned rule schema
 remains valid only when its retained payloads replay under that schema.
 
@@ -1078,8 +1081,9 @@ alternatives to compare once the behavior is established.
 2. The external function-package registry executes the routed callback and
    owns its private cache; the Mathlib companion is responsible for semantic
    replay, not hot-loop dispatch.
-3. The registry returns an `Outcome` containing candidate facts, alternatives,
-   suggestions, cost observations, and an opaque proof recipe identifier.
+3. The registry returns a `Plan` containing an `Outcome` plus exactly the
+   reply-local recipe drafts referenced by its fact, instantiation, and
+   equality payload identifiers.
 4. A reply echoes the request serial, snapshot, and application. A delayed or
    transplanted reply is rejected without clearing the current request.
 5. The solver validates every candidate target against the application's
@@ -1092,10 +1096,9 @@ alternatives to compare once the behavior is established.
    Only companion replay of the retained payload can do that.
 6. In the production replay protocol, every value needed to justify an
    accepted fact is frozen into an immutable per-run payload arena, and the
-   retained `PayloadId` points there rather than into a mutable cache. A
-   separate arena experiment now validates and relocates a complete reply
-   prospectively; it is not yet joined to package invocation and engine
-   admission in one opaque session.
+   retained `PayloadId` points there rather than into a mutable cache. Session
+   execution validates and relocates the complete reply prospectively before
+   engine admission.
 7. The solver records the snapshot, concrete application, anchor, action kind,
    effort, input versions, target's preceding fact version, proposed fact,
    installed fact, and frozen payload in provenance. The preceding target fact
@@ -1144,22 +1147,84 @@ checked global-reference draft, and accepting bounded cross-reply duplication
 are alternatives to measure rather than assumptions of the final format.
 
 The first executable arena uses an eager but prospective transaction:
-package-local labels in the outcome are matched exactly against package-local
-drafts, checked for duplicate, missing, extra, and wrong-role entries,
-preflighted against whole-arena entry, body-cell, atom, schema, and
-total-proposal limits, relocated to fresh global identifiers, and appended to
-a new arena value. The total-proposal budget charges every candidate, every
-suggestion constructor (including retry and split), and every equality nested
-under an instantiation. Repeated references count as work even when they share
-one draft. Before any quadratic label/coverage scan, the draft list is bounded
-both by the remaining arena-entry capacity and by the same trusted proposal
-limit. Entry construction and identifier assignment are one traversal, so a
-relocated identifier denotes exactly the entry appended for its local draft.
+it preflights total-proposal work and the per-reply draft, draft-cell, atom,
+and schema limits, then matches package-local labels exactly against
+package-local drafts and checks duplicate, missing, extra, and wrong-role
+entries. Only a locally bounded, exactly covered reply is compared with
+remaining whole-arena entry and body-cell capacity, relocated to fresh global
+identifiers, and appended to a new arena value. Thus malformed local evidence
+cannot be classified as cumulative exhaustion merely because earlier valid
+replies filled part of the arena. Local preflight returns an opaque
+bounded-draft transaction whose constructor is private; it carries the exact
+draft list together with its derived cell count, and both cumulative preflight
+and append consume that same value. No public caller can supply a separate
+cell count for unrelated drafts. The total-proposal budget charges every
+candidate, every suggestion constructor (including retry and split), and
+every equality nested under an instantiation. Repeated references count as
+work even when they share one draft. Before any quadratic label/coverage scan,
+`maxDrafts` bounds the draft list independently of proposal traversal. Every
+atom reached by the bounded body traversal is range-checked before its cell is
+charged. The traversal stops at the first in-range cell beyond
+`maxDraftCells`; later atoms are deliberately not inspected. Entry
+construction and identifier assignment are one traversal, so a relocated
+identifier denotes exactly the entry appended for its local draft.
 Candidate, instantiation, and equality roles are distinct, and ordinary replay
 lookup checks the expected role. Failure returns the old arena.
-The surrounding session must commit that returned arena only if submission of
-the relocated outcome also succeeds, so this experiment does not prejudge the
-one-phase versus two-phase production choice.
+The session commits that returned arena only if submission of the relocated
+outcome also succeeds. Before freezing, it checks the candidate and suggestion
+list lengths against the engine's own trusted limits. Let
+`requiredUses = maxOutcomeCandidates + maxOutcomeSuggestions *
+(maxProposalItems + 1)`: every candidate and suggestion costs one payload use,
+and every suggestion may be an instantiation with at most
+`maxProposalItems` nested equalities. Session start requires
+`requiredUses ≤ maxDrafts`, `maxDrafts ≤ maxUses`,
+`maxDrafts ≤ maxEntries`, and `maxDraftCells ≤ maxBodyCells`. The first
+inequality permits one distinct draft for every engine-valid payload use.
+The second both implies that the use traversal can inspect every such position
+and bounds even malformed pre-coverage draft lists by the same envelope.
+The remaining inequalities ensure that any reply inside the local draft/cell
+envelope fits a fresh arena. `maxEntries` and `maxBodyCells` remain cumulative
+whole-run bounds: only capacity spent by an earlier committed reply can make a
+later locally valid reply exhaust them.
+Packages see the complete engine and arena envelopes and may impose stronger
+method-specific requirements.
+Before any package-specific program check traverses nodes, session start runs
+the generic engine preflight and compilation, so the engine's operation, node,
+rule, arity, application, and queue bounds already hold.
+
+The eager protocol's `maxEntries` and `maxBodyCells` are separate whole-run
+waste bounds. They must cover drafts frozen for every invoked action up to the
+action limit, including entries later unused because a candidate was not
+improving or a suggestion was dropped, dismissed, stale, invalid, or
+duplicate. Sizing either from `maxAcceptedFacts` is therefore unsound. A coarse
+safe envelope multiplies the corresponding per-reply cap by the action limit;
+tighter package-declared envelopes and two-phase freezing remain experiments
+to compare.
+
+Engine rejection, fact-domain or engine resource refusal, and exhaustion of
+the remaining whole-run arena entry or body-cell capacity retain the preceding
+arena, facts, program, and proof history and make the returned session
+non-live. Start-time coherence means these arena stops occur only after an
+earlier commit has consumed capacity. A caller cannot resume that snapshot and
+later relabel the partial run saturated. Treating cumulative arena exhaustion
+as fatal is an intentional conservative liveness policy, aligned with global
+engine-resource exhaustion: the selected reply is otherwise valid, but its
+required proof data cannot be retained. Proof soundness could also permit a
+recoverable session which permanently records dropped work and remains
+incomplete, but that would broaden scheduling behavior; the eager prototype
+does not do so. Malformed package evidence and
+package-local payload-use, draft-count, draft-cell, atom, or schema excess are
+different: the prospective arena is discarded, but the session submits a
+bounded synthetic `failed` outcome through the ordinary engine reply path.
+This clears the request latch, retains non-semantic cache telemetry, leaves
+facts and history unchanged, keeps the session live, and records that required
+work was dropped. The FIFO driver may therefore continue other independent
+rules, including later successful arena and fact commits, but the monotone
+`droppedWork` flag survives and the run must eventually report incomplete.
+The selected package's cache may record either kind of attempt because caches
+and invocation telemetry are explicitly non-semantic.
+This executable eager protocol does not foreclose measuring a two-phase
+production protocol.
 
 An invalid rule outcome may mislead search, but it cannot produce a theorem.
 The companion reconstructs every retained fact from the rule's soundness
@@ -1189,16 +1254,32 @@ than present placeholder weights as exact operation counts.
 
 The standalone arena experiment gives fact, instantiation, and equality
 `PayloadId`s checked array-index meaning and bounds entry count, opaque
-recipe-body cells, schemas, atoms, and total proposal work before allocation.
+recipe-body cells, schemas, atoms, draft count, and total proposal work before
+allocation. Reply-local draft and cell caps are distinguished from cumulative
+entry and cell capacity.
 Each frozen entry stores its originating action, semantic role, numeric
 payload schema, and uninterpreted `List Nat` body. It derives the rule owner
 only from `origin.key`, avoiding two stored identities which could disagree.
 Package-owned decoding and schema lookup, typed atom encodings, byte limits,
 and semantic replay are still missing. Instantiation family labels and custom
-split-reason numbers also remain untyped representation gaps. The next session
-experiment must ensure that no unrelocated package-local identifier can enter
-retained provenance and that an arena from one registry snapshot cannot be
-paired with another.
+split-reason numbers also remain untyped representation gaps. The FIFO session
+turns any positive compatibility callback whose local identifier lacks a
+draft into a failed rule transition, so no unrelocated package-local
+identifier reaches its retained provenance. Its monotone `droppedWork` flag
+means exactly that required work was lost; it is not itself a terminal-state
+claim. The exported `Session.complete` predicate additionally requires a live
+session and no retained retry or instantiation. At a FIFO fixed point this
+predicate is the sole gate between saturated and incomplete. Package
+`failed`/`resourceLimit` results, malformed evidence, dropped narrowing
+suggestions, and unprocessed retained narrowing therefore cannot be laundered
+into saturation. The next policy experiment must preserve this same session
+transaction while allowing an external policy to choose invocations,
+instantiations, equalities, retries, and splits; it must not regain access to
+separable engine, registry, and arena values. The FIFO session can already
+freeze an instantiation and its nested equality payloads, but it deliberately
+has no public admission escape hatch. Honest session-level execution coverage
+for the resulting equality contractor therefore belongs to that private
+policy-session layer, not to a test-only constructor or engine replacement.
 
 ### Action kinds
 
@@ -1568,7 +1649,11 @@ One `balancedV1` candidate uses a versioned priority queue over these offers.
 Changed facts insert or invalidate only affected offers; stale entries are
 discarded lazily when popped. Policies intended for diagnostics may use a
 simpler complete scan, but their complexity is reported honestly. An empty
-frontier means saturation only when no narrowing-capable work was dismissed.
+frontier means saturation only when no narrowing-capable work was dismissed,
+dropped from the engine's bounded retained prefix, or tombstoned by a failed
+freshness guard. `Suggestion.affectsClosure` is the single classification used
+for all three paths, while `Engine.keptSuggestions` and
+`Engine.droppedSuggestions` define the exact shared retention boundary.
 Declining an invocation, equality contractor, retry, or instantiation makes
 the run incomplete; declining a split does not, because it changes proof
 search rather than the propagation closure of the current scope. An empty
@@ -2237,6 +2322,12 @@ typical, boundary, and adversarial inputs. In particular it includes:
   duplicate operation/rule-key and undeclared-head rejection, cache-preserving
   rejection of wrong routes, and a `Type 1` registry threaded through both
   drivers;
+- a private package session which freezes and relocates reply-local evidence,
+  continues independent work after malformed or locally oversized drafts,
+  retains incompleteness across a later successful reply, charges nested
+  equality payload uses, keeps derived draft-cell accounting tied to the exact
+  bounded transaction, and intentionally reserves fatal entry/body-cell stops
+  for genuine remaining-capacity exhaustion after an earlier arena commit;
 - an anchor-local opaque shape rule which distinguishes `x * (one - x)` from
   products with a reversed difference or a different repeated input, proposes
   the exact existing node identifiers while receiving no fact inputs, repeats
diff --git a/conformance/HexInterval/DyadicRulesConformance.lean b/conformance/HexInterval/DyadicRulesConformance.lean
index 0935646ca..d5f3ffa2b 100644
--- a/conformance/HexInterval/DyadicRulesConformance.lean
+++ b/conformance/HexInterval/DyadicRulesConformance.lean
@@ -324,6 +324,8 @@ def falseOneRun? : Option (RunResult Fact ConcreteRegistry) := do
 def payloadLimits : PayloadArena.Limits :=
   { maxEntries := 3
     maxBodyCells := 0
+    maxDrafts := 3
+    maxDraftCells := 0
     maxAtom := 0
     maxSchema := 0
     maxUses := 3 }
diff --git a/conformance/HexInterval/PackageRegistryConformance.lean b/conformance/HexInterval/PackageRegistryConformance.lean
index c3b4fb55f..cc41b27b4 100644
--- a/conformance/HexInterval/PackageRegistryConformance.lean
+++ b/conformance/HexInterval/PackageRegistryConformance.lean
@@ -118,8 +118,9 @@ def limitedPackage : Package Nat :=
     cache := false
     operations := #[limitedOperation]
     handlers := #[Handler.bareDroppingDrafts limitedRegistration limitedInvoke]
-    acceptsLimits := fun _ limits =>
-      8 ≤ limits.maxObservationValue && 1000000 ≤ limits.maxDiagnosticValue }
+    acceptsLimits := fun _ limits arenaLimits =>
+      8 ≤ limits.maxObservationValue && 1000000 ≤ limits.maxDiagnosticValue &&
+        4 ≤ arenaLimits.maxEntries && 8 ≤ arenaLimits.maxUses }
 
 /-- A package may attach a handler to a signature supplied only by the final
 frontend program, but it must declare the exact dependency. -/
@@ -257,6 +258,15 @@ def limits : Limits :=
       { maxEndpointHeight := 16
         maxAlignmentShift := 8 } }
 
+def arenaLimits : Experiment.PayloadArena.Limits :=
+  { maxEntries := 4
+    maxBodyCells := 8
+    maxDrafts := 4
+    maxDraftCells := 8
+    maxAtom := 100
+    maxSchema := 10
+    maxUses := 8 }
+
 def registry? : Option (Registry Nat) :=
   match Registry.buildWithin limits #[sharedPackage, thirdPackage, limitedPackage] with
   | .ok registry => some registry
@@ -270,6 +280,9 @@ def externalRegistry? : Option (Registry Nat) :=
 def lowDiagnosticLimits : Limits :=
   { limits with maxDiagnosticValue := 999999 }
 
+def shortArenaLimits : Experiment.PayloadArena.Limits :=
+  { arenaLimits with maxEntries := 3 }
+
 def shortRuleLimits : Limits :=
   { limits with maxRules := 3 }
 
@@ -286,7 +299,8 @@ def run? : Option (RunResult Nat (Registry Nat)) :=
   match registry? with
   | none => none
   | some registry =>
-      if !registry.acceptsProgram program || !registry.acceptsLimits program limits then none
+      if !registry.acceptsProgram program ||
+          !registry.acceptsLimits program limits arenaLimits then none
       else
         match Engine.start factDomain program registry.registrations #[0, 0, 0, 0] limits with
         | .error _ => none
@@ -310,7 +324,9 @@ def policyDriverTypecheck {PolicyState : Type}
 
 #guard
   match registry? with
-  | some registry => !registry.acceptsLimits program lowDiagnosticLimits
+  | some registry =>
+      !registry.acceptsLimits program lowDiagnosticLimits arenaLimits &&
+        !registry.acceptsLimits program limits shortArenaLimits
   | none => false
 
 -- Registry-owned dispatch failures have a diagnostic floor independent of
@@ -319,9 +335,11 @@ def policyDriverTypecheck {PolicyState : Type}
   match Registry.buildWithin limits #[sharedPackage] with
   | .ok registry =>
       !registry.acceptsLimits program
-          { limits with maxDiagnosticValue := DispatchCode.requestMismatch - 1 } &&
+          { limits with maxDiagnosticValue := DispatchCode.requestMismatch - 1 }
+          arenaLimits &&
         registry.acceptsLimits program
           { limits with maxDiagnosticValue := DispatchCode.requestMismatch }
+          arenaLimits
   | .error _ => false
 
 #guard
@@ -355,7 +373,8 @@ def policyDriverTypecheck {PolicyState : Type}
   | none => false
   | some registry =>
       registry.operations.size == 4 && registry.registrations.size == 4 &&
-        registry.acceptsProgram program && registry.acceptsLimits program limits &&
+        registry.acceptsProgram program &&
+        registry.acceptsLimits program limits arenaLimits &&
         registry.acceptsProgram reorderedProgram &&
         !registry.acceptsProgram mismatchedProgram &&
         registry.routes ==
diff --git a/conformance/HexInterval/PayloadArenaConformance.lean b/conformance/HexInterval/PayloadArenaConformance.lean
index 25261f6b7..571a1c3ea 100644
--- a/conformance/HexInterval/PayloadArenaConformance.lean
+++ b/conformance/HexInterval/PayloadArenaConformance.lean
@@ -33,6 +33,8 @@ def action (serial : Nat) : Action :=
 def generous : PayloadArena.Limits :=
   { maxEntries := 16
     maxBodyCells := 32
+    maxDrafts := 16
+    maxDraftCells := 32
     maxAtom := 100
     maxSchema := 10
     maxUses := 16 }
@@ -49,6 +51,12 @@ def equalityDraft (label : Nat) (body : List Nat := [30]) (schema : Nat := 3) :
 def factOutcome (label : Nat) : Outcome Nat :=
   .success [{ node := node 0, fact := 7, payload := payload label }] [] {}
 
+def pairOutcome : Outcome Nat :=
+  .success
+    [{ node := node 0, fact := 7, payload := payload 0 },
+      { node := node 1, fact := 8, payload := payload 1 }]
+    [] {}
+
 def retainedSeed : Entry :=
   { origin := action 9
     role := .fact
@@ -165,6 +173,59 @@ def mixedRequest : InstantiationRequest :=
       label.index == 1 && seedPreserved arena
   | _ => false
 
+-- Exact draft coverage is checked before remaining whole-run entry capacity:
+-- malformed local evidence cannot masquerade as fatal cumulative exhaustion.
+#guard
+  match freeze { generous with maxEntries := 1 } seeded (action 0)
+      (factOutcome 0) [factDraft 0, equalityDraft 1] with
+  | .invalid (.extraDraft label) arena =>
+      label.index == 1 && seedPreserved arena
+  | _ => false
+
+-- The same ordering holds when an unused draft carries a body which would
+-- exceed the partly filled arena's remaining cell capacity.
+#guard
+  match freeze { generous with maxBodyCells := 1 } seeded (action 0)
+      (factOutcome 0) [factDraft 0, equalityDraft 1 [4, 5]] with
+  | .invalid (.extraDraft label) arena =>
+      label.index == 1 && seedPreserved arena
+  | _ => false
+
+-- Local preflight derives one cell count from the exact bounded draft list.
+-- The same opaque transaction drives both cumulative capacity and the
+-- committed aggregate, so there is no independent cell count to mismatch.
+#guard
+  match
+      freeze
+        { generous with
+          maxEntries := 3
+          maxBodyCells := 4
+          maxDrafts := 2
+          maxDraftCells := 3
+          maxUses := 2 }
+        seeded (action 0) pairOutcome
+        [factDraft 0 [4], factDraft 1 [5, 6]] with
+  | .ready arena (.success [first, second] [] _) =>
+      first.payload.index == 1 && second.payload.index == 2 &&
+        arena.entries.size == 3 && arena.bodyCells == 4 && arena.wellFormed
+  | _ => false
+
+-- Reducing only the remaining cumulative cell capacity rejects that same
+-- locally bounded transaction and preserves the original cached aggregate.
+#guard
+  match
+      freeze
+        { generous with
+          maxEntries := 3
+          maxBodyCells := 3
+          maxDrafts := 2
+          maxDraftCells := 3
+          maxUses := 2 }
+        seeded (action 0) pairOutcome
+        [factDraft 0 [4], factDraft 1 [5, 6]] with
+  | .resourceLimit .bodyCells arena => seedPreserved arena
+  | _ => false
+
 -- Each resource limit is exactly one below the required prospective value.
 #guard
   match freeze { generous with maxEntries := 0 } seeded (action 0)
@@ -190,8 +251,20 @@ def mixedRequest : InstantiationRequest :=
   | .resourceLimit .bodyCells arena => seedPreserved arena
   | _ => false
 
+-- A single oversized recipe is a reply-local failure even though the
+-- cumulative arena has room.
 #guard
-  match freeze { generous with maxAtom := 4 } seeded (action 0)
+  match freeze { generous with maxDraftCells := 1 } seeded (action 0)
+      (factOutcome 0) [factDraft 0 [4, 5]] with
+  | .resourceLimit .draftCells arena => seedPreserved arena
+  | _ => false
+
+-- The first cell beyond the local cap is still atom-checked before local
+-- refusal; whole-run capacity is never consulted for that invalid reply.
+#guard
+  match freeze
+      { generous with maxBodyCells := 1, maxDraftCells := 0, maxAtom := 4 }
+      seeded (action 0)
       (factOutcome 0) [factDraft 0 [5]] with
   | .resourceLimit .atom arena => seedPreserved arena
   | _ => false
@@ -230,14 +303,16 @@ def mixedRequest : InstantiationRequest :=
   | .resourceLimit .uses arena => seedPreserved arena
   | _ => false
 
--- Drafts are independently bounded by `maxUses` before exact-coverage scans,
--- even when the arena has ample entry room.
+-- Draft count has its own reply-local cap before exact-coverage scans, even
+-- when both proposal traversal and the cumulative arena have ample room.
 #guard
-  match freeze { generous with maxUses := 1 } seeded (action 0)
+  match freeze { generous with maxDrafts := 1 } seeded (action 0)
       (factOutcome 0) [factDraft 0, factDraft 1] with
-  | .resourceLimit .uses arena => seedPreserved arena
+  | .resourceLimit .drafts arena => seedPreserved arena
   | _ => false
 
+-- Nested equalities are charged as payload uses in addition to their
+-- containing instantiation suggestion.
 #guard
   match freeze { generous with maxUses := 1 } seeded (action 0)
       (.success [] [.instantiate mixedRequest] {} : Outcome Nat)
diff --git a/conformance/HexInterval/PayloadSessionConformance.lean b/conformance/HexInterval/PayloadSessionConformance.lean
new file mode 100644
index 000000000..d7d15eb91
--- /dev/null
+++ b/conformance/HexInterval/PayloadSessionConformance.lean
@@ -0,0 +1,868 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+import HexInterval.Experiment.PayloadSession
+
+/-!
+Focused checks for package invocation, payload freezing, and engine admission
+under one private session boundary.
+-/
+
+namespace Hex.Interval.PayloadSessionConformance
+
+open Experiment Propagator PayloadArena PayloadSession
+
+def real : DomainId := { index := 0 }
+def sourceOp : OpKey := { name := "payload-session.source" }
+def mysteryOp : OpKey := { name := "payload-session.mystery" }
+
+def goodKey : RuleKey := { name := "payload-session.mystery.good" }
+def badReplyKey : RuleKey := { name := "payload-session.mystery.bad-reply" }
+def badPayloadKey : RuleKey := { name := "payload-session.mystery.bad-payload" }
+def bareKey : RuleKey := { name := "payload-session.mystery.bare" }
+def negativeKey : RuleKey := { name := "payload-session.mystery.negative" }
+def failedKey : RuleKey := { name := "payload-session.mystery.failed" }
+def retryKey : RuleKey := { name := "payload-session.mystery.retry" }
+def longCandidatesKey : RuleKey := { name := "payload-session.mystery.long-candidates" }
+def longSuggestionsKey : RuleKey := { name := "payload-session.mystery.long-suggestions" }
+def nestedKey : RuleKey := { name := "payload-session.mystery.nested-instance" }
+def nestedUsesKey : RuleKey := { name := "payload-session.mystery.nested-uses" }
+def atomKey : RuleKey := { name := "payload-session.mystery.atom" }
+def schemaKey : RuleKey := { name := "payload-session.mystery.schema" }
+def draftsKey : RuleKey := { name := "payload-session.mystery.drafts" }
+def bodyKey : RuleKey := { name := "payload-session.mystery.body" }
+def overflowKey : RuleKey := { name := "payload-session.mystery.overflow" }
+def recoverKey : RuleKey := { name := "payload-session.mystery.recover" }
+def lateExtraKey : RuleKey := { name := "payload-session.mystery.late-extra" }
+
+def sourceOperation : Operation :=
+  { key := sourceOp, inputs := [], output := real }
+
+def mysteryOperation : Operation :=
+  { key := mysteryOp, inputs := [real], output := real }
+
+def node (index : Nat) : NodeId := { index }
+def payload (index : Nat) : PayloadId := { index }
+
+def instruction (operation : Nat) (args : List NodeId := []) : Node :=
+  { domain := real, op := { index := operation }, args }
+
+/-- Two applications intentionally reuse the same package-local payload label. -/
+def program : Program :=
+  { operations := #[sourceOperation, mysteryOperation]
+    nodes :=
+      #[instruction 0,
+        instruction 1 [node 0],
+        instruction 1 [node 0]] }
+
+def registration (key : RuleKey) : Registration :=
+  { key
+    head := mysteryOp
+    kind := .forward
+    watches := [.argument 0]
+    writes := [.result] }
+
+def factDomain : FactDomain Nat where
+  top _ := 0
+  narrow _ current proposed :=
+    if current < proposed then .improved proposed else .noChange
+
+def contradictionDomain : FactDomain Nat where
+  top _ := 0
+  narrow _ _ proposed := .contradiction proposed
+
+def limits : Propagator.Limits :=
+  { maxOperations := 4
+    maxNodes := 4
+    maxRules := 2
+    maxArity := 2
+    maxApplications := 4
+    maxQueueEntries := 8
+    maxActions := 8
+    maxAcceptedFacts := 4
+    maxRetainedSuggestions := 2
+    maxEffort := 2
+    maxObservationValue := 8
+    maxDiagnosticValue := 300
+    maxOutcomeCandidates := 2
+    maxOutcomeSuggestions := 2
+    maxProposalItems := 2
+    maxInstances := 2
+    maxGeneration := 2
+    maxNodeDepth := 16
+    maxEqualities := 2
+    splitEndpointLimit :=
+      { maxEndpointHeight := 8
+        maxAlignmentShift := 8 } }
+
+def arenaLimits : PayloadArena.Limits :=
+  { maxEntries := 8
+    maxBodyCells := 16
+    maxDrafts := 8
+    maxDraftCells := 8
+    maxAtom := 100
+    maxSchema := 10
+    maxUses := 8 }
+
+def goodPlan (request : RuleRequest Nat) : Plan Nat :=
+  match request.writes with
+  | [target] =>
+      { outcome :=
+          .success
+            [{ node := target, fact := 7, payload := payload 700 }]
+            [] { estimatedProofNodes := 1 }
+        drafts :=
+          [{ label := payload 700
+             role := .fact
+             schema := 1
+             body := [request.action.node.index, 99] }] }
+  | _ => { outcome := .failed 1, drafts := [] }
+
+def goodPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration goodKey) goodPlan] }
+
+def lateExtraPlan (request : RuleRequest Nat) : Plan Nat :=
+  if request.action.node == node 1 then
+    goodPlan request
+  else
+    match request.writes with
+    | [target] =>
+        { outcome :=
+            .success
+              [{ node := target, fact := 7, payload := payload 700 }]
+              [] {}
+          drafts :=
+            [{ label := payload 700
+               role := .fact
+               schema := 1
+               body := [request.action.node.index, 99] },
+             { label := payload 701
+               role := .fact
+               schema := 1
+               body := [4, 5] }] }
+    | _ => { outcome := .failed 1, drafts := [] }
+
+def lateExtraPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration lateExtraKey) lateExtraPlan] }
+
+def badReplyPlan (_request : RuleRequest Nat) : Plan Nat :=
+  { outcome :=
+      .success
+        [{ node := node 0, fact := 9, payload := payload 700 }]
+        [] {}
+    drafts := [{ label := payload 700, role := .fact, schema := 1, body := [1] }] }
+
+def badReplyPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration badReplyKey) badReplyPlan] }
+
+def badPayloadPlan (request : RuleRequest Nat) : Plan Nat :=
+  match request.writes with
+  | [target] =>
+      { outcome :=
+          .success
+            [{ node := target, fact := 7, payload := payload 700 }]
+            [] {}
+        drafts := [{ label := payload 701, role := .fact, schema := 1, body := [1] }] }
+  | _ => { outcome := .failed 2, drafts := [] }
+
+def badPayloadPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration badPayloadKey) badPayloadPlan] }
+
+def barePackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessDroppingDrafts (registration bareKey) fun request =>
+          match request.writes with
+          | [target] =>
+              .success
+                [{ node := target, fact := 7, payload := payload 700 }]
+                [] {}
+          | _ => .failed 3] }
+
+def negativePackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessDroppingDrafts (registration negativeKey) fun _ => .noChange {}] }
+
+def failedPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessDroppingDrafts (registration failedKey) fun _ => .failed 4] }
+
+def retryPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessDroppingDrafts (registration retryKey) fun _ =>
+          .success [] [.retry 1] {}] }
+
+def longCandidatesPlan (request : RuleRequest Nat) : Plan Nat :=
+  match request.writes with
+  | [target] =>
+      { outcome :=
+          .success
+            [{ node := target, fact := 4, payload := payload 1 },
+              { node := target, fact := 5, payload := payload 1 },
+              { node := target, fact := 6, payload := payload 1 }]
+            [] {}
+        -- This deliberately malformed evidence must never be traversed:
+        -- engine list pre-screening rejects the outcome first.
+        drafts := [] }
+  | _ => { outcome := .failed 5, drafts := [] }
+
+def longCandidatesPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration longCandidatesKey) longCandidatesPlan] }
+
+def longSuggestionsPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration longSuggestionsKey) fun _ =>
+          { outcome := .success [] [.retry 0, .retry 1, .retry 2] {}
+            drafts := [] }] }
+
+def nestedPlan (request : RuleRequest Nat) : Plan Nat :=
+  { outcome :=
+      .success []
+        [.instantiate
+          { key := 44
+            nodes :=
+              [{ domain := real
+                 op := { index := 1 }
+                 args := [.existing request.action.node] }]
+            equalities :=
+              [{ left := .existing (node 0)
+                 right := .proposed 0
+                 payload := payload 702 }]
+            payload := payload 701 }]
+        {}
+    drafts :=
+      [{ label := payload 702, role := .equality, schema := 3, body := [12] },
+        { label := payload 701, role := .instance, schema := 2, body := [11] }] }
+
+def nestedPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration nestedKey) nestedPlan] }
+
+def nestedUsesPlan (request : RuleRequest Nat) : Plan Nat :=
+  { outcome :=
+      .success []
+        [.instantiate
+          { key := 45
+            nodes := []
+            equalities :=
+              [{ left := .existing (node 0)
+                 right := .existing request.action.node
+                 payload := payload 702 },
+               { left := .existing (node 0)
+                 right := .existing request.action.node
+                 payload := payload 703 }]
+            payload := payload 701 }]
+        {}
+    drafts :=
+      [{ label := payload 702, role := .equality, schema := 3, body := [12] },
+       { label := payload 703, role := .equality, schema := 3, body := [13] },
+       { label := payload 701, role := .instance, schema := 2, body := [11] }] }
+
+def nestedUsesPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration nestedUsesKey) nestedUsesPlan] }
+
+def draftPlan (schema : Nat) (body : List Nat)
+    (request : RuleRequest Nat) : Plan Nat :=
+  match request.writes with
+  | [target] =>
+      { outcome :=
+          .success
+            [{ node := target, fact := 7, payload := payload 700 }]
+            [] {}
+        drafts := [{ label := payload 700, role := .fact, schema, body }] }
+  | _ => { outcome := .failed 6, drafts := [] }
+
+def atomPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration atomKey) (draftPlan 1 [101])] }
+
+def schemaPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration schemaKey) (draftPlan 11 [1])] }
+
+def bodyPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration bodyKey)
+          (draftPlan 1 [1, 1, 1, 1, 1, 1, 1, 1, 1])] }
+
+def recoverPlan (request : RuleRequest Nat) : Plan Nat :=
+  if request.action.node == node 1 then
+    draftPlan 11 [1] request
+  else
+    goodPlan request
+
+def recoverPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration recoverKey) recoverPlan] }
+
+def excessDrafts : List PayloadArena.Draft :=
+  [{ label := payload 0, role := .fact, schema := 1, body := [] },
+   { label := payload 1, role := .fact, schema := 1, body := [] },
+   { label := payload 2, role := .fact, schema := 1, body := [] },
+   { label := payload 3, role := .fact, schema := 1, body := [] },
+   { label := payload 4, role := .fact, schema := 1, body := [] },
+   { label := payload 5, role := .fact, schema := 1, body := [] },
+   { label := payload 6, role := .fact, schema := 1, body := [] },
+   { label := payload 7, role := .fact, schema := 1, body := [] },
+   { label := payload 8, role := .fact, schema := 1, body := [] }]
+
+def draftsPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration draftsKey) fun _ =>
+          { outcome := .noChange {}, drafts := excessDrafts }] }
+
+def overflowPlan (request : RuleRequest Nat) : Plan Nat :=
+  { outcome :=
+      .success []
+        [.split { node := request.action.node, point := 0, reason := .midpoint },
+         .split { node := request.action.node, point := 1, reason := .midpoint },
+         .retry 1] {}
+    drafts := [] }
+
+def overflowPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration overflowKey) overflowPlan] }
+
+def arenaAwarePackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration goodKey) goodPlan]
+    acceptsLimits := fun _ _ payloadLimits =>
+      4 ≤ payloadLimits.maxEntries && 8 ≤ payloadLimits.maxUses &&
+        8 ≤ payloadLimits.maxDraftCells }
+
+def start (package : Package Nat)
+    (payloadLimits : PayloadArena.Limits := arenaLimits) :
+    Except PayloadSession.StartError (PayloadSession.Session Nat) :=
+  PayloadSession.Session.start factDomain program #[package] #[3, 0, 0]
+    limits payloadLimits
+
+def startWithin (package : Package Nat) (engineLimits : Propagator.Limits)
+    (payloadLimits : PayloadArena.Limits) :
+    Except PayloadSession.StartError (PayloadSession.Session Nat) :=
+  PayloadSession.Session.start factDomain program #[package] #[3, 0, 0]
+    engineLimits payloadLimits
+
+def oneReplyLimits : Propagator.Limits :=
+  { limits with
+    maxOutcomeCandidates := 1
+    maxOutcomeSuggestions := 0
+    maxProposalItems := 0 }
+
+def twoUseLimits : Propagator.Limits :=
+  { oneReplyLimits with maxOutcomeCandidates := 2 }
+
+def lateExtraArena : PayloadArena.Limits :=
+  { arenaLimits with
+    maxEntries := 2
+    maxBodyCells := 4
+    maxDrafts := 2
+    maxDraftCells := 4
+    maxUses := 2 }
+
+def nestedUsesLimits : Propagator.Limits :=
+  { limits with
+    maxOutcomeCandidates := 0
+    maxOutcomeSuggestions := 1
+    maxProposalItems := 1 }
+
+def nestedUsesArena : PayloadArena.Limits :=
+  { arenaLimits with
+    maxDrafts := PayloadSession.requiredUses nestedUsesLimits
+    maxUses := PayloadSession.requiredUses nestedUsesLimits }
+
+def overflowLimits : Propagator.Limits :=
+  { limits with maxOutcomeSuggestions := 3 }
+
+def overflowArenaLimits : PayloadArena.Limits :=
+  let required := PayloadSession.requiredUses overflowLimits
+  { arenaLimits with
+    maxEntries := required
+    maxDrafts := required
+    maxUses := required }
+
+def oversizedProgram : Program :=
+  { program with
+    nodes := program.nodes.push (instruction 1 [node 0]) |>.push (instruction 1 [node 0]) }
+
+def goodRun? : Option (PayloadSession.Run Nat) :=
+  match start goodPackage with
+  | .ok session => some (session.drive 8)
+  | .error _ => none
+
+-- Separate replies may use the same local label; the session commits distinct
+-- arena entries and only relocated global identifiers reach provenance.
+#guard
+  match goodRun? with
+  | some run =>
+      run.stop == .saturated &&
+        run.session.live && !run.session.droppedWork && run.session.complete &&
+        run.session.arena.entries.size == 2 &&
+        run.session.arena.bodyCells == 4 &&
+        run.session.engine.history.size == 2 &&
+        match run.session.engine.history[0]?, run.session.engine.history[1]?,
+            run.session.arena.entry? (payload 0) .fact,
+            run.session.arena.entry? (payload 1) .fact with
+        | some first, some second, some firstEntry, some secondEntry =>
+            first.node == node 1 && second.node == node 2 &&
+              firstEntry.origin.key == goodKey && secondEntry.origin.key == goodKey &&
+              firstEntry.origin.node == node 1 && secondEntry.origin.node == node 2 &&
+              firstEntry.schema == 1 && secondEntry.schema == 1 &&
+              firstEntry.body == [1, 99] && secondEntry.body == [2, 99] &&
+              match first.cause, second.cause with
+              | .rule _ proposed firstPayload, .rule _ proposed' secondPayload =>
+                  proposed == 7 && proposed' == 7 &&
+                    firstPayload == payload 0 && secondPayload == payload 1
+              | _, _ => false
+        | _, _, _, _ => false
+  | none => false
+
+-- A fully frozen prospective arena is discarded when engine admission rejects
+-- an undeclared write.
+#guard
+  match start badReplyPackage with
+  | .ok session =>
+      match session.advance with
+      | .invalidReply (.undeclaredWrite target) next =>
+          target == node 0 && next.arena.entries.isEmpty &&
+            next.engine.history.isEmpty && next.engine.pending.isNone &&
+            !next.live &&
+            (next.registry.packages[0]?).any fun package =>
+              package.invocations == 1 &&
+                match next.advance with
+                | .invalidEngine stopped => !stopped.live
+                | _ => false
+      | _ => false
+  | .error _ => false
+
+-- Malformed reply-local evidence clears the request latch but changes no
+-- semantic state. It becomes an ordinary failed rule transition: the session
+-- remains live, remembers dropped work, and the bounded driver continues.
+#guard
+  match start badPayloadPackage with
+  | .ok session =>
+      match session.advance with
+      | .invalidPayload (.danglingReference label) next =>
+          label == payload 700 && next.arena.entries.isEmpty &&
+            next.engine.history.isEmpty && next.engine.pending.isNone &&
+            next.live && next.droppedWork && !next.complete &&
+            next.engine.metrics.ruleFailures == 1 &&
+            (next.registry.packages[0]?).any fun package =>
+              package.invocations == 1 &&
+                let run := next.drive 8
+                run.stop == .incomplete && run.session.live &&
+                  run.session.droppedWork && !run.session.complete &&
+                  run.session.engine.metrics.ruleFailures == 2
+      | _ => false
+  | .error _ => false
+
+-- Per-reply encoding excess is a package failure, not exhaustion of the
+-- whole run. The prospective arena is discarded, the request is consumed,
+-- and independent work can continue, but completeness is permanently lost.
+#guard
+  match start atomPackage
+      { arenaLimits with maxBodyCells := 0, maxDraftCells := 0 } with
+  | .ok session =>
+      match session.advance with
+      | .rejectedPayload .atom next =>
+          next.arena.entries.isEmpty && next.engine.history.isEmpty &&
+            next.engine.pending.isNone && next.live && next.droppedWork &&
+            !next.complete && next.engine.metrics.ruleFailures == 1 &&
+            let run := next.drive 8
+            run.stop == .incomplete && run.session.live &&
+              run.session.engine.metrics.ruleFailures == 2
+      | _ => false
+  | .error _ => false
+
+#guard
+  match start schemaPackage with
+  | .ok session =>
+      match session.advance with
+      | .rejectedPayload .schema next =>
+          next.arena.entries.isEmpty && next.engine.history.isEmpty &&
+            next.engine.pending.isNone && next.live && next.droppedWork &&
+            !next.complete && next.engine.metrics.ruleFailures == 1
+      | _ => false
+  | .error _ => false
+
+#guard
+  match start draftsPackage with
+  | .ok session =>
+      match session.advance with
+      | .rejectedPayload .drafts next =>
+          next.arena.entries.isEmpty && next.engine.history.isEmpty &&
+            next.engine.pending.isNone && next.live && next.droppedWork &&
+            !next.complete && next.engine.metrics.ruleFailures == 1
+      | _ => false
+  | .error _ => false
+
+-- A nested equality beyond the engine-coherent proposal envelope is charged
+-- as a payload use before engine admission. The failed reply is recoverable.
+#guard
+  match startWithin nestedUsesPackage nestedUsesLimits nestedUsesArena with
+  | .ok session =>
+      match session.advance with
+      | .rejectedPayload .uses next =>
+          next.arena.entries.isEmpty && next.engine.history.isEmpty &&
+            next.engine.pending.isNone && next.live && next.droppedWork &&
+            !next.complete && next.engine.metrics.ruleFailures == 1
+      | _ => false
+  | .error _ => false
+
+-- One oversized encoded body is a package-local failure rather than
+-- exhaustion of the cumulative arena.
+#guard
+  match start bodyPackage with
+  | .ok session =>
+      match session.advance with
+      | .rejectedPayload .draftCells next =>
+          next.arena.entries.isEmpty && next.engine.history.isEmpty &&
+            next.engine.pending.isNone && next.live && next.droppedWork &&
+            !next.complete && next.engine.metrics.ruleFailures == 1
+      | _ => false
+  | .error _ => false
+
+-- Rejection does not stop unrelated queued work, and the monotone
+-- incompleteness flag survives a later successful arena and fact commit.
+#guard
+  match start recoverPackage with
+  | .ok session =>
+      match session.advance with
+      | .rejectedPayload .schema rejected =>
+          match rejected.advance with
+          | .advanced next =>
+              next.live && next.droppedWork && !next.complete &&
+                next.engine.metrics.ruleFailures == 1 &&
+                next.engine.history.size == 1 &&
+                next.arena.entries.size == 1 && next.arena.bodyCells == 2 &&
+                match next.engine.history[0]? with
+                | some event =>
+                    event.node == node 2 &&
+                      let run := next.drive 8
+                      run.stop == .incomplete && run.session.live &&
+                        run.session.droppedWork && !run.session.complete &&
+                        run.session.engine.history.size == 1
+                | none => false
+          | _ => false
+      | _ => false
+  | .error _ => false
+
+-- Whole-run exhaustion is reserved for a bounded reply which would fit an
+-- empty arena but not the capacity remaining after an earlier commit.
+#guard
+  match startWithin goodPackage oneReplyLimits
+      { arenaLimits with maxEntries := 1, maxDrafts := 1, maxUses := 1 } with
+  | .ok session =>
+      match session.advance with
+      | .advanced first =>
+          first.arena.entries.size == 1 && first.engine.history.size == 1 &&
+            match first.advance with
+            | .payloadResource .entries stopped =>
+                !stopped.live && !stopped.complete &&
+                  stopped.engine.pending.isNone &&
+                  stopped.arena.entries.size == 1 &&
+                  stopped.engine.history.size == 1 &&
+                  match stopped.advance with
+                  | .invalidEngine inert =>
+                      !inert.live && !inert.complete &&
+                        inert.arena.entries.size == 1 &&
+                        inert.engine.history.size == 1
+                  | _ => false
+            | _ => false
+      | _ => false
+  | .error _ => false
+
+#guard
+  match startWithin goodPackage oneReplyLimits
+      { arenaLimits with
+        maxEntries := 2
+        maxBodyCells := 3
+        maxDrafts := 1
+        maxDraftCells := 2
+        maxUses := 1 } with
+  | .ok session =>
+      match session.advance with
+      | .advanced first =>
+          first.arena.bodyCells == 2 && first.engine.history.size == 1 &&
+            match first.advance with
+            | .payloadResource .bodyCells stopped =>
+                !stopped.live && !stopped.complete &&
+                  stopped.engine.pending.isNone &&
+                  stopped.arena.entries.size == 1 &&
+                  stopped.arena.bodyCells == 2 &&
+                  stopped.engine.history.size == 1 &&
+                  match stopped.advance with
+                  | .invalidEngine inert =>
+                      !inert.live && !inert.complete &&
+                        inert.arena.entries.size == 1 &&
+                        inert.arena.bodyCells == 2 &&
+                        inert.engine.history.size == 1
+                  | _ => false
+            | _ => false
+      | _ => false
+  | .error _ => false
+
+-- After an earlier valid commit has partly filled both cumulative budgets, an
+-- extra draft with a junk body is still malformed local evidence. Exact
+-- coverage precedes remaining-capacity checks, so only this reply is rejected.
+#guard
+  match startWithin lateExtraPackage twoUseLimits lateExtraArena with
+  | .ok session =>
+      match session.advance with
+      | .advanced first =>
+          first.arena.entries.size == 1 && first.arena.bodyCells == 2 &&
+            first.engine.history.size == 1 &&
+            match first.advance with
+            | .invalidPayload (.extraDraft label) rejected =>
+                label.index == 701 && rejected.live && rejected.droppedWork &&
+                  !rejected.complete && rejected.arena.entries.size == 1 &&
+                  rejected.arena.bodyCells == 2 &&
+                  rejected.engine.history.size == 1 &&
+                  rejected.engine.metrics.ruleFailures == 1
+            | _ => false
+      | _ => false
+  | .error _ => false
+
+-- Completeness consumes the engine's exact admission plan. Here the two
+-- harmless splits fit, while a closure-relevant retry is the sole capacity
+-- drop (not a structural-depth drop).
+#guard
+  match PayloadSession.Session.start factDomain program #[overflowPackage]
+      #[3, 0, 0] overflowLimits overflowArenaLimits with
+  | .ok session =>
+      match session.advance with
+      | .advanced next =>
+          next.engine.suggestions.size == 2 &&
+            next.engine.metrics.droppedSuggestions == 1 &&
+            next.engine.metrics.capacityDrops == 1 &&
+            next.engine.metrics.depthDrops == 0 &&
+            next.droppedWork && !next.complete
+      | _ => false
+  | .error _ => false
+
+-- Compatibility handlers are safe for negative observations. A positive
+-- outcome carrying an unfrozen identifier is rejected rather than retained.
+#guard
+  match start negativePackage with
+  | .ok session =>
+      let run := session.drive 8
+      run.stop == .saturated && run.session.arena.entries.isEmpty &&
+        run.session.engine.history.isEmpty && !run.session.droppedWork &&
+        run.session.complete
+  | .error _ => false
+
+#guard
+  match start barePackage with
+  | .ok session =>
+      match session.advance with
+      | .invalidPayload (.danglingReference label) next =>
+          label == payload 700 && next.arena.entries.isEmpty &&
+            next.engine.history.isEmpty && next.live && next.droppedWork &&
+            !next.complete && next.engine.metrics.ruleFailures == 1
+      | _ => false
+  | .error _ => false
+
+-- A package failure and an unprocessed narrowing suggestion can never be
+-- laundered into a complete propagation fixed point.
+#guard
+  match start failedPackage with
+  | .ok session =>
+      let run := session.drive 8
+      run.stop == .incomplete && run.session.droppedWork &&
+        !run.session.complete && run.session.arena.entries.isEmpty
+  | .error _ => false
+
+#guard
+  match start retryPackage with
+  | .ok session =>
+      let run := session.drive 8
+      run.stop == .incomplete && !run.session.droppedWork &&
+        !run.session.complete && run.session.engine.suggestions.size == 2
+  | .error _ => false
+
+-- Count coherence lets every engine-valid payload use own a distinct draft,
+-- bounds malformed draft lists by the use envelope, and fits either local cap
+-- in a fresh arena. `requiredUses ≤ maxUses` follows transitively rather than
+-- appearing as a redundant condition. Packages may impose stronger bounds.
+#guard
+  PayloadSession.requiredUses limits == 8 &&
+    PayloadSession.limitsCoherent limits arenaLimits
+
+#guard
+  match start goodPackage { arenaLimits with maxDrafts := 7 } with
+  | .error .incoherentLimits => true
+  | _ => false
+
+-- This isolates `maxDrafts ≤ maxUses`: both still admit all eight required
+-- uses, and the fresh entry budget admits all nine locally allowed drafts.
+#guard
+  match start goodPackage
+      { arenaLimits with maxEntries := 9, maxDrafts := 9, maxUses := 8 } with
+  | .error .incoherentLimits => true
+  | _ => false
+
+#guard
+  match start goodPackage { arenaLimits with maxEntries := 7 } with
+  | .error .incoherentLimits => true
+  | _ => false
+
+#guard
+  match start goodPackage { arenaLimits with maxBodyCells := 7 } with
+  | .error .incoherentLimits => true
+  | _ => false
+
+#guard
+  match start arenaAwarePackage { arenaLimits with maxDraftCells := 7 } with
+  | .error .limitsRejected => true
+  | _ => false
+
+-- Generic engine bounds precede package-specific scans of the program.
+#guard
+  match PayloadSession.Session.start factDomain oversizedProgram #[arenaAwarePackage]
+      #[3, 0, 0, 0, 0] limits { arenaLimits with maxDraftCells := 7 } with
+  | .error (.engine (.resourceLimit .nodes)) => true
+  | _ => false
+
+-- Oversized outer lists are rejected by the engine before malformed or
+-- absent drafts can make the arena traverse the package plan.
+#guard
+  match start longCandidatesPackage with
+  | .ok session =>
+      match session.advance with
+      | .invalidReply .tooManyCandidates next =>
+          next.arena.entries.isEmpty && next.engine.pending.isNone && !next.live &&
+            !next.complete &&
+            (next.registry.packages[0]?).any fun package => package.invocations == 1
+      | _ => false
+  | .error _ => false
+
+#guard
+  match start longSuggestionsPackage with
+  | .ok session =>
+      match session.advance with
+      | .invalidReply .tooManySuggestions next =>
+          next.arena.entries.isEmpty && next.engine.pending.isNone && !next.live &&
+            !next.complete
+      | _ => false
+  | .error _ => false
+
+-- A fuel stop preserves the live, paired session and can be resumed without
+-- reusing local labels or losing the first committed proof entry.
+#guard
+  match start goodPackage with
+  | .ok session =>
+      let first := session.drive 1
+      first.stop == .driverFuel && first.session.live &&
+        first.session.arena.entries.size == 1 &&
+        first.session.engine.history.size == 1 &&
+        let resumed := first.session.drive 8
+        resumed.stop == .saturated && resumed.session.complete &&
+          resumed.session.arena.entries.size == 2 &&
+          resumed.session.engine.history.size == 2
+  | .error _ => false
+
+-- Contradiction is preserved as an ordinary accepted fact with frozen
+-- evidence, rather than confused with an incomplete or resource stop.
+#guard
+  match PayloadSession.Session.start contradictionDomain program #[goodPackage]
+      #[3, 0, 0] limits arenaLimits with
+  | .ok session =>
+      let run := session.drive 8
+      run.stop == .contradiction && run.session.live &&
+        run.session.complete && run.session.arena.entries.size == 1 &&
+        run.session.engine.history.size == 1 &&
+        run.session.engine.contradictory
+  | .error _ => false
+
+-- Nested instantiation and equality labels are both relocated before the
+-- narrowing suggestion enters retained engine state.
+#guard
+  match start nestedPackage with
+  | .ok session =>
+      match session.advance with
+      | .advanced next =>
+          next.live && !next.droppedWork && !next.complete &&
+            next.arena.entries.size == 2 && next.engine.suggestions.size == 1 &&
+            match next.engine.suggestions[0]? with
+            | some retained =>
+                match retained.suggestion with
+                | .instantiate request =>
+                    request.payload == payload 1 &&
+                      (next.arena.entry? request.payload .instance).any
+                        (fun entry => entry.schema == 2 && entry.body == [11]) &&
+                      match request.equalities with
+                      | [equality] =>
+                          equality.payload == payload 0 &&
+                            (next.arena.entry? equality.payload .equality).any
+                              (fun entry => entry.schema == 3 && entry.body == [12])
+                      | _ => false
+                | _ => false
+            | none => false
+      | _ => false
+  | .error _ => false
+
+end Hex.Interval.PayloadSessionConformance
diff --git a/conformance/HexInterval/PolicyConformance.lean b/conformance/HexInterval/PolicyConformance.lean
index 9788cf786..6373b18c9 100644
--- a/conformance/HexInterval/PolicyConformance.lean
+++ b/conformance/HexInterval/PolicyConformance.lean
@@ -130,6 +130,17 @@ def selectOffer (state : State Rank) (id : OfferId) : SelectResult Rank :=
           id
           expected := offer.key }
 
+def dismissOffer (state : State Rank) (id : OfferId) : Option (State Rank) := do
+  let offer <- state.offer? id
+  match state.dismiss
+      { scope := state.scope
+        serial := state.serial
+        programVersion := state.engine.programVersion
+        id
+        expected := offer.key } with
+  | .completed .dismissed next => some next
+  | _ => none
+
 def candidate (request : RuleRequest Rank) (rank : Rank) : Candidate Rank :=
   { node := request.action.node
     fact := rank
@@ -971,6 +982,39 @@ def startWithWeakRetry? : Option (State Rank) := do
           pair.1.offers.isEmpty && !pair.1.incomplete
   | none => false
 
+-- Dismissal uses the same closure classification as tombstoning and bounded
+-- retention. Removing the retry and instantiation makes an eventually empty
+-- frontier incomplete; removing the split does not erase or invent that fact.
+#guard
+  match afterInitial? with
+  | none => false
+  | some state =>
+      match dismissOffer state (.suggestion (suggestion 0)) with
+      | none => false
+      | some state =>
+          match dismissOffer state (.suggestion (suggestion 1)) with
+          | none => false
+          | some state =>
+              match dismissOffer state (.suggestion (suggestion 2)) with
+              | some state =>
+                  state.incomplete && state.metrics.dismissals == 3 &&
+                    (state.view).toOption.any fun pair =>
+                      pair.1.offers.isEmpty && pair.1.incomplete
+              | none => false
+
+-- A split-only frontier remains propagation-complete when its optional search
+-- advice is dismissed.
+#guard
+  match afterReplyWith? engineLimits overflowSplit with
+  | none => false
+  | some state =>
+      match dismissOffer state (.suggestion (suggestion 0)) with
+      | some next =>
+          !next.incomplete &&
+            (next.view).toOption.any fun pair =>
+              pair.1.offers.isEmpty && !pair.1.incomplete
+      | none => false
+
 def splitChangedTarget (request : RuleRequest Rank) : Outcome Rank :=
   .success [candidate request 1]
     [.split { node := request.action.node, point := 0, reason := .midpoint }]
diff --git a/lakefile.lean b/lakefile.lean
index 072b66b1c..83ab30541 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -234,7 +234,7 @@ lean_lib HexIntervalExperiment where
     `HexInterval.Experiment.PackageRegistry,
     `HexInterval.Experiment.DyadicInterval,
     `HexInterval.Experiment.DyadicRules,
-    `HexInterval.Experiment.PayloadArena]
+    `HexInterval.Experiment.PayloadArena, `HexInterval.Experiment.PayloadSession]
 
 lean_lib HexIntervalMathlibExperiment where
   globs := #[`HexIntervalMathlib.Experiment.Center]
@@ -301,7 +301,7 @@ lean_lib HexRCFProofProbeScientific where
 -- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`.
 lean_lib HexConformance where
   srcDir := "conformance"
-  globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one
+  globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one
 
 -- Public umbrellas intentionally contain only the supported API. Executable
 -- examples and regression tests are compiled through this separate target so
diff --git a/progress/20260728T052158Z.md b/progress/20260728T052158Z.md
new file mode 100644
index 000000000..6bae8c7ca
--- /dev/null
+++ b/progress/20260728T052158Z.md
@@ -0,0 +1,41 @@
+# Session-owned package evidence
+
+## Accomplished
+
+- Changed function-package callbacks to return a plan containing both their
+  ordinary outcome and complete reply-local proof drafts. Search-only
+  callbacks remain available through an adapter, but positive unfrozen
+  payloads are rejected by proof-producing execution.
+- Added a private-constructor session that assembles and owns the exact engine,
+  heterogeneous package registry, immutable payload arena, and arena limits.
+- Made package invocation, payload validation and relocation, engine reply
+  submission, and arena commit one checked transition. Engine rejection or
+  payload failure cannot commit a prospective arena.
+- Made error snapshots non-live, preventing a caller from resuming a failed
+  transition and later reporting a false fixed point.
+- Distinguished complete saturation from package failure, package resource
+  refusal, and retained retry or instantiation work.
+- Added conformance for local-label relocation across two arbitrary function
+  calls, arena/engine atomicity, malformed payloads, unfrozen compatibility
+  callbacks, resource refusal, non-live error snapshots, and incomplete runs.
+- Built the session, package-registry conformance, session conformance, and
+  complete `HexIntervalExperiment` target successfully. Added Lean code
+  contains no `native_decide`, `axiom`, or `sorry`.
+
+## Current frontier
+
+The FIFO session owns evidence correctly but does not yet let the external
+policy select retry, instantiation, equality, or split actions through the
+same private boundary. Payload bodies are still schema-independent data and
+are not replayed by a package-owned checker.
+
+## Next step
+
+Lift the external policy transitions into the session without exposing
+separable engine, registry, and arena values, then add a versioned
+package-owned payload decoder and replay one accepted arbitrary-function fact.
+
+## Blockers
+
+None. The payload-arena review fixes on the parent branch must be rebased into
+this branch before its PR is ready to merge.
diff --git a/progress/20260728T054105Z.md b/progress/20260728T054105Z.md
new file mode 100644
index 000000000..9e24217fb
--- /dev/null
+++ b/progress/20260728T054105Z.md
@@ -0,0 +1,41 @@
+# Payload-session review hardening
+
+## Accomplished
+
+- Replaced the ambiguous session `incomplete` bit with the monotone
+  `droppedWork` fact and added `Session.complete`, which also checks liveness
+  and retained retry / instantiation work.
+- Made bounded `Run` values constructible only by the opaque session driver.
+- Pre-screened candidate and suggestion list lengths against engine limits
+  before proof-arena traversal.
+- Converted malformed package evidence into an ordinary failed rule reply.
+  The arena and facts remain unchanged, the request clears, the session stays
+  live, and later saturation is classified incomplete.
+- Extended package limit preflight to receive the payload-arena envelope.
+  Session start now rejects an arena `maxUses` smaller than the sound
+  worst-valid-reply bound derived from engine limits.
+- Removed the unused registry update helper and expanded conformance for
+  package arena checks, one-short coherence, oversized outer replies,
+  malformed-evidence continuation, contradiction, fuel/resume, and nested
+  instantiation/equality payload relocation.
+- Built the focused session, registry, and dyadic conformance targets plus the
+  complete `HexIntervalExperiment` target successfully.
+
+## Current frontier
+
+The FIFO session can retain a fully frozen instantiation with nested equality
+evidence, but deliberately exposes no way to replace its private engine with
+the result of admitting that suggestion. Consequently its equality-transition
+branch cannot yet be exercised end-to-end without violating the pairing
+boundary.
+
+## Next step
+
+Add the private policy-session layer which owns instantiation admission and
+equality scheduling, then test the equality transition through that real API.
+Choose the package replay-dispatch key centrally before adding semantic
+decoders.
+
+## Blockers
+
+None.
diff --git a/progress/20260728T060455Z.md b/progress/20260728T060455Z.md
new file mode 100644
index 000000000..f1c31a560
--- /dev/null
+++ b/progress/20260728T060455Z.md
@@ -0,0 +1,38 @@
+# Package-failure isolation
+
+## Accomplished
+
+- Centralized the engine's retained and dropped suggestion prefixes and the
+  closure relevance of retry, instantiation, and split suggestions.
+- Made the proof-producing session use those exact engine decisions when
+  withholding a fixed-point claim after dropped work.
+- Converted package-local payload-use, atom, and schema excess into consumed
+  failed replies: the proof arena remains unchanged, independent propagation
+  continues, and completeness is permanently withheld.
+- Kept whole-run arena entry and body-cell exhaustion fatal and non-resumable.
+- Moved generic engine program preflight ahead of package-specific program
+  scans.
+- Added conformance cases for all resource classes, exact suggestion overflow,
+  continued execution after package rejection, and preflight precedence.
+- Documented that eager arena entries must be bounded from invoked actions and
+  possible unused drafts, not merely accepted facts.
+- Rebuilt the payload session conformance and complete interval experiment
+  successfully; the changed Lean files contain no `native_decide`, `axiom`, or
+  `sorry`.
+
+## Current frontier
+
+The FIFO session now isolates arbitrary package failures correctly, but the
+package-owned replay-format branch is still stacked on the preceding session
+version and must absorb these changes before the policy session can be the
+single end-to-end owner.
+
+## Next step
+
+Restack package-owned replay and the private policy session, then run the
+centered auxiliary-expression instantiation and its fact/equality proof replay
+through that one owner.
+
+## Blockers
+
+None.
diff --git a/progress/20260729T053139Z.md b/progress/20260729T053139Z.md
new file mode 100644
index 000000000..282e46ab6
--- /dev/null
+++ b/progress/20260729T053139Z.md
@@ -0,0 +1,26 @@
+# Interval package session restack
+
+## Accomplished
+
+- Restacked the package-session layer onto the current payload-arena branch.
+- Preserved the shared exact retained/dropped suggestion calculation used by
+  both scheduling policy and session completeness checks.
+- Rebuilt `HexIntervalExperiment` and the package-session conformance target.
+- Rechecked the generated conformance target matrix and the branch diff.
+
+## Current frontier
+
+The session now gives arbitrary registered propagator packages one private,
+transactional path from candidate generation through retained suggestions and
+frozen proof payloads.  The next layer seals the package-owned replay formats
+that validate those payloads.
+
+## Next step
+
+Restack the package-replay layer onto this branch, then connect its sealed
+package-specific checkers to the policy-driven session for an end-to-end
+auxiliary-expression proof.
+
+## Blockers
+
+None.
diff --git a/progress/20260729T055315Z.md b/progress/20260729T055315Z.md
new file mode 100644
index 000000000..293ea2d5a
--- /dev/null
+++ b/progress/20260729T055315Z.md
@@ -0,0 +1,34 @@
+# Payload-session review follow-up
+
+## Accomplished
+
+- Split reply-local payload limits (`maxDrafts`, `maxDraftCells`) from
+  cumulative arena limits (`maxEntries`, `maxBodyCells`), and made local
+  draft-count and draft-cell rejection recoverable in `PayloadSession`.
+- Made payload classification deterministic by checking atom size before
+  either local or cumulative body-cell capacity, while reserving fatal
+  entry/body-cell errors for genuine remaining whole-run exhaustion.
+- Unified closure-relevance classification for dismissed, dropped, and
+  tombstoned suggestions through `Suggestion.affectsClosure`; retained the
+  exact kept/dropped engine helpers at the policy boundary.
+- Added conformance coverage for nested-equality use accounting,
+  independent progress after a rejected reply, monotone `droppedWork`,
+  atom-vs-cell classification, sequential dismissal, and genuine mid-run
+  entry/body exhaustion.
+- Updated the interval SPEC and every affected limit literal. The focused
+  HexInterval experiment/conformance build, diff check, and banned-token
+  scan pass.
+
+## Current frontier
+
+The Opus review findings for the payload-session branch are addressed and
+the branch is ready to commit and push to PR #9038.
+
+## Next step
+
+Rebase the dependent frontier-admission work after this payload-session
+head, then let the PR CI validate the updated stack.
+
+## Blockers
+
+None.
diff --git a/progress/20260729T060908Z.md b/progress/20260729T060908Z.md
new file mode 100644
index 000000000..5fc597f2b
--- /dev/null
+++ b/progress/20260729T060908Z.md
@@ -0,0 +1,32 @@
+# Payload validation ordering follow-up
+
+## Accomplished
+
+- Split arena preflight into reply-local and remaining whole-run phases.
+- Moved exact duplicate, reference, role, and coverage validation between
+  those phases so malformed evidence cannot be reported as cumulative
+  exhaustion after earlier valid commits.
+- Required `maxDrafts ≤ maxUses` at session start, reflecting exact coverage
+  and keeping quadratic label validation within the trusted per-reply use cap.
+- Corrected atom-order documentation: every visited atom is checked before its
+  cell is charged, but traversal deliberately stops after local cell refusal.
+- Added partly filled arena and private-session canaries in which an extra
+  junk-body draft remains recoverable and preserves the earlier arena/history
+  commit.
+- Rebuilt the focused payload, policy, registry, dyadic, and experiment
+  conformance graph. The generated target matrix, diff check, and
+  banned-addition scan pass.
+
+## Current frontier
+
+Only a locally bounded, structurally valid payload transaction can reach
+remaining whole-run entry/body-cell comparison.
+
+## Next step
+
+Restack package-owned replay so package-format validation also occurs before
+whole-run capacity, then restack the private policy session.
+
+## Blockers
+
+None.
diff --git a/progress/20260729T062352Z.md b/progress/20260729T062352Z.md
new file mode 100644
index 000000000..e04063670
--- /dev/null
+++ b/progress/20260729T062352Z.md
@@ -0,0 +1,26 @@
+# Accomplished
+
+- Restacked the payload-session branch on refreshed payload-arena head
+  `7d37887de186282fc23a8ecc3d4b68ec50c84d04`.
+- Combined the upstream registry diagnostic floor with package-owned
+  engine-and-arena limit preflights.
+- Migrated payload-session conformance to the engine-owned structural-depth
+  and instantiation-generation API while preserving all payload validation,
+  rollback, and prior-arena-history canaries.
+- Rechecked that freezing orders reply-local use and draft bounds, exact
+  coverage and malformed-payload validation, then cumulative arena capacity.
+- Passed the focused 24-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+Payload-session ownership and exact payload validation are green on the
+refreshed payload-arena and propagator framework.
+
+# Next step
+
+Restack package replay on this refreshed payload-session head.
+
+# Blockers
+
+None.
diff --git a/progress/20260729T064252Z.md b/progress/20260729T064252Z.md
new file mode 100644
index 000000000..8ce3d2805
--- /dev/null
+++ b/progress/20260729T064252Z.md
@@ -0,0 +1,33 @@
+# Accomplished
+
+- Replaced the public bare derived-cell convention with `BoundedDrafts`, whose
+  private constructor and opaque local preflight keep the exact draft list
+  paired with its derived cell count through cumulative preflight and commit.
+- Preserved validation order: payload-use traversal, local draft/schema/body
+  bounds, exact coverage, cumulative entry/body capacity, then relocation and
+  append.
+- Removed the redundant explicit `requiredUses ≤ maxUses` coherence clause;
+  it now follows from `requiredUses ≤ maxDrafts ≤ maxUses`. Updated the
+  rationale and isolated each remaining inequality in conformance.
+- Documented cumulative entry/body exhaustion as an intentional conservative
+  fatal policy for the eager prototype, while noting that recoverable
+  incomplete continuation could be a separate sound scheduling policy.
+- Added public-API invariance guards tying multi-draft cell accounting to the
+  committed aggregate and cumulative refusal, plus non-resumability guards for
+  fatal mid-run entry and body-cell exhaustion.
+- Passed the focused 24-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+Payload-session freezing no longer exposes a forgeable cross-function cell
+count, and cumulative exhaustion behavior is explicit and tested.
+
+# Next step
+
+Mechanically restack package replay and the policy-owned payload session on
+this refreshed payload-session head.
+
+# Blockers
+
+None.
diff --git a/progress/20260729T064721Z.md b/progress/20260729T064721Z.md
new file mode 100644
index 000000000..7175e3e85
--- /dev/null
+++ b/progress/20260729T064721Z.md
@@ -0,0 +1,27 @@
+# Accomplished
+
+- Restacked payload sessions on refreshed payload-arena head
+  `cd03a363d768849502d6d9d24c02ec1098b1d7c7`.
+- Migrated session completeness accounting from prefix-only suggestion
+  dropping to the framework's exact `suggestionPlan`, preserving recovery from
+  individually unaffordable structural proposals.
+- Removed obsolete package-supplied instantiation triggers from payload-session
+  conformance; dependencies remain engine-owned.
+- Preserved the reviewed payload sequence and opaque `BoundedDrafts`
+  transaction: use traversal, local bounds, exact coverage, cumulative
+  capacity, relocation, and append.
+- Passed the focused 24-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+Payload sessions are green on the suggestion-recovery framework and refreshed
+payload arena.
+
+# Next step
+
+Restack sealed package replay on this payload-session head.
+
+# Blockers
+
+None.
diff --git a/progress/20260729T071129Z.md b/progress/20260729T071129Z.md
new file mode 100644
index 000000000..291ca6a41
--- /dev/null
+++ b/progress/20260729T071129Z.md
@@ -0,0 +1,26 @@
+# Accomplished
+
+- Restacked payload sessions on final payload-arena head
+  `e58c7df70d0dd21bdf91eef2df295c763ba3bb6a`.
+- Migrated every engine submission to the final accepted-result shape and now
+  consumes the engine-returned `SuggestionPlan` directly for closure loss,
+  avoiding recomputation of capacity and structural-depth drops.
+- Kept explicit failed/resource package outcomes incomplete independently of
+  suggestion admission.
+- Strengthened conformance to distinguish the expected capacity drop from
+  structural-depth drops while preserving the opaque draft transaction and
+  reviewed validation order.
+- Passed the focused 24-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+Payload sessions are green on the final exact suggestion-admission framework.
+
+# Next step
+
+Restack sealed package replay and its policy/semantic dependents.
+
+# Blockers
+
+None.