diff --git a/HexInterval/Experiment/PolicySession.lean b/HexInterval/Experiment/PolicySession.lean
new file mode 100644
index 000000000..aee5ca6ab
--- /dev/null
+++ b/HexInterval/Experiment/PolicySession.lean
@@ -0,0 +1,399 @@
+/-
+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
+public import HexInterval.Experiment.Policy
+
+@[expose] public section
+
+/-!
+# Proof-producing policy sessions
+
+This experiment is the ownership boundary shared by arbitrary function
+packages and an external search policy.  One private-constructor session owns
+the policy state, the exact heterogeneous package registry which compiled its
+engine, the immutable proof-payload arena, every configured resource envelope,
+and the monotone liveness and completeness state.
+
+The policy can only echo a checked offer through `Session.choose`. A selected
+rule or retry is routed through `Registry.invokePlanned`; the resulting plan
+and exact handler replay snapshot stay paired through bounded format checking,
+prospective freezing, and relocation through the snapshot's sealed `freeze`
+operation. The new arena is committed only after `Policy.State.submit` accepts
+the relocated reply. Malformed evidence and package-local use, atom, or schema
+excess, including draft-count and draft-cell excess, consume a failed reply and
+preserve a live incomplete session; remaining whole-run entry or body-cell
+exhaustion after earlier commits is fatal. Instantiation, equality contraction,
+dismissal, and split preparation stay inside the same session boundary. No
+public operation accepts a separately assembled engine, registry, or arena.
+-/
+
+namespace Hex.Interval.Experiment.PolicySession
+
+open Propagator
+
+/-- All deterministic envelopes used to assemble one policy session. -/
+structure Limits where
+  engine : Propagator.Limits
+  policy : Propagator.Policy.Limits
+  arena : PayloadArena.Limits
+  deriving DecidableEq, Repr
+
+/-- Failure while assembling one coherent policy-controlled run. -/
+inductive StartError where
+  | registry (error : RegistryError)
+  | programRejected
+  | incoherentLimits
+  | limitsRejected
+  | engine (error : Propagator.StartError)
+  deriving DecidableEq, Repr
+
+/-- A proof-producing policy state. `state` privately owns the engine together
+with its policy frontier. Public projections support inspection, while the
+private constructor prevents a caller from replacing that engine, the exact
+registry, or the arena with a component from another run. -/
+structure Session (Fact : Type) where
+  private mk ::
+  state : Propagator.Policy.State Fact
+  registry : Registry Fact
+  arena : PayloadArena.Arena
+  limits : Limits
+  /-- Required work was lost outside the policy state's own accounting. -/
+  droppedWork : Bool
+  live : Bool
+
+private def make (state : Propagator.Policy.State Fact)
+    (registry : Registry Fact) (limits : Limits) : Session Fact :=
+  { state
+    registry
+    arena := .empty
+    limits
+    droppedWork := false
+    live := true }
+
+/-- A sound upper bound on proof-payload traversal for any engine-valid
+reply.  It charges every candidate and suggestion and the maximum number of
+equalities which may be nested below each suggestion. -/
+def requiredUses (limits : Propagator.Limits) : Nat :=
+  limits.maxOutcomeCandidates +
+    limits.maxOutcomeSuggestions * (limits.maxProposalItems + 1)
+
+/-- Every engine-valid payload position may carry a distinct draft, exact
+coverage bounds valid draft count by use count, and any locally valid reply
+must fit an empty arena. -/
+def limitsCoherent (limits : Limits) : Bool :=
+  requiredUses limits.engine ≤ limits.arena.maxUses &&
+    requiredUses limits.engine ≤ limits.arena.maxDrafts &&
+    limits.arena.maxDrafts ≤ limits.arena.maxUses &&
+    limits.arena.maxDrafts ≤ limits.arena.maxEntries &&
+    limits.arena.maxDraftCells ≤ limits.arena.maxBodyCells
+
+/-- Assemble the exact registry first, validate its signatures and package
+configuration, then compile the engine and put it under policy control. -/
+opaque Session.start (factDomain : FactDomain Fact) (program : Program)
+    (packages : Array (Package Fact)) (facts : Array Fact) (limits : Limits)
+    (scope : Propagator.Policy.ScopeId := { index := 0 }) :
+    Except StartError (Session Fact) :=
+  match Registry.buildWithin limits.engine packages with
+  | .error error => .error (.registry error)
+  | .ok registry =>
+      match preflightStart program registry.registrations facts.size limits.engine with
+      | .error error => .error (.engine error)
+      | .ok () =>
+          if !registry.acceptsProgram program then
+            .error .programRejected
+          else if !limitsCoherent limits then
+            .error .incoherentLimits
+          else if !registry.acceptsLimits program limits.engine limits.arena then
+            .error .limitsRejected
+          else
+            match Engine.start factDomain program registry.registrations facts limits.engine with
+            | .error error => .error (.engine error)
+            | .ok engine =>
+                .ok (make (Propagator.Policy.State.start engine limits.policy scope)
+                  registry limits)
+
+private def withState (session : Session Fact)
+    (state : Propagator.Policy.State Fact) : Session Fact :=
+  { session with state }
+
+private def halt (session : Session Fact) (state : Propagator.Policy.State Fact)
+    (registry : Registry Fact := session.registry) : Session Fact :=
+  { session with state, registry, live := false }
+
+private def commit (session : Session Fact) (state : Propagator.Policy.State Fact)
+    (registry : Registry Fact) (arena : PayloadArena.Arena)
+    (droppedWork : Bool := session.droppedWork) : Session Fact :=
+  { session with state, registry, arena, droppedWork }
+
+private def hasApplication (state : Propagator.Policy.State Fact) : Nat -> Bool
+  | 0 => false
+  | count + 1 =>
+      (state.offer? (.application { index := count })).isSome ||
+        hasApplication state count
+
+private def hasEquality (state : Propagator.Policy.State Fact) : Nat -> Bool
+  | 0 => false
+  | count + 1 =>
+      (state.offer? (.equality { index := count })).isSome ||
+        hasEquality state count
+
+private def hasNarrowingSuggestion
+    (state : Propagator.Policy.State Fact) : Nat -> Bool
+  | 0 => false
+  | count + 1 =>
+      ((state.offer? (.suggestion { index := count })).isSome &&
+        (state.engine.suggestions[count]?).any fun retained =>
+          Suggestion.affectsClosure retained.suggestion) ||
+        hasNarrowingSuggestion state count
+
+/-- Whether this live snapshot has reached propagation closure.  Optional
+split offers do not affect closure, while any live invocation, equality,
+retry, instantiation, earlier failed work, contradiction, or pending reply
+prevents the claim. -/
+opaque Session.complete (session : Session Fact) : Bool :=
+  session.live && !session.droppedWork && !session.state.incomplete &&
+    session.state.engine.pending.isNone && !session.state.engine.contradictory &&
+    !hasApplication session.state session.state.applications.size &&
+    !hasEquality session.state session.state.equalities.size &&
+    !hasNarrowingSuggestion session.state session.state.suggestions.size
+
+/-- A policy can select any checked offer or explicitly dismiss it. -/
+inductive Choice where
+  | select (selection : Propagator.Policy.Selection)
+  | dismiss (selection : Propagator.Policy.Selection)
+
+/-- A bounded policy view also returns the same owned session with traversal
+accounting committed. -/
+inductive ViewStep (Fact : Type) where
+  | ready (view : Propagator.Policy.View Fact) (session : Session Fact)
+  | resource (error : Propagator.Policy.ViewError) (session : Session Fact)
+  | contradiction (session : Session Fact)
+  | invalidSession (session : Session Fact)
+
+/-- Obtain the next external-policy view without exposing a replaceable policy
+state. -/
+opaque Session.view (session : Session Fact) : ViewStep Fact :=
+  if !session.live || session.state.engine.pending.isSome then
+    .invalidSession session
+  else if session.state.engine.contradictory then
+    .contradiction session
+  else
+    match session.state.view with
+    | .error error => .resource error { session with live := false }
+    | .ok (view, state) => .ready view (withState session state)
+
+/-- Result of one policy-owned choice.  Every successful constructor returns
+the next coherent session rather than separable components. -/
+inductive Step (Fact : Type) where
+  | rule (selection : Propagator.Policy.Selection)
+      (observation : Propagator.Policy.RuleObservation Fact)
+      (session : Session Fact)
+  | equality (selection : Propagator.Policy.Selection)
+      (observation : Propagator.Policy.EqualityObservation Fact)
+      (session : Session Fact)
+  | instance (selection : Propagator.Policy.Selection)
+      (completion : Propagator.Policy.Completed) (session : Session Fact)
+  | dismissed (selection : Propagator.Policy.Selection) (session : Session Fact)
+  | split (selection : Propagator.Policy.Selection)
+      (plan : Propagator.Policy.SplitPlan Fact) (session : Session Fact)
+  | rejected (selection : Propagator.Policy.Selection)
+      (reason : Propagator.Policy.Rejection) (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 policy choices remain available. -/
+  | rejectedPayload (resource : PayloadArena.Resource) (session : Session Fact)
+  /-- A whole-run payload arena bound was exhausted. -/
+  | payloadResource (resource : PayloadArena.Resource) (session : Session Fact)
+  | invalidSession (session : Session Fact)
+
+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 bounded diagnostic used to clear a request whose package evidence
+was malformed or exceeded a package-local encoding bound. -/
+def rejected : Nat := 0
+
+end PayloadFailureCode
+
+private def failPayload (session : Session Fact)
+    (state : Propagator.Policy.State Fact) (registry : Registry Fact)
+    (action : Action) (error : PayloadArena.Invalid) : Step Fact :=
+  match state.submit (action.reply (.failed PayloadFailureCode.rejected)) with
+  | .accepted _ next =>
+      .invalidPayload error
+        (commit session next registry session.arena true)
+  | .invalid replyError next =>
+      .invalidReply replyError (halt session next registry)
+  | .engineResource resource next =>
+      .engineResource resource (halt session next registry)
+  | .factResource budget next =>
+      .factResource budget (halt session next registry)
+  | .malformedState next =>
+      .invalidSession (halt session next registry)
+
+/-- A use, draft, draft-cell, atom, or schema excess is local to one package
+reply. Consume that reply as a bounded failure, discard its prospective arena,
+and preserve the live session while permanently withholding completeness. -/
+private def rejectPayload (session : Session Fact)
+    (state : Propagator.Policy.State Fact) (registry : Registry Fact)
+    (action : Action) (resource : PayloadArena.Resource) : Step Fact :=
+  match state.submit (action.reply (.failed PayloadFailureCode.rejected)) with
+  | .accepted _ next =>
+      .rejectedPayload resource
+        (commit session next registry session.arena true)
+  | .invalid replyError next =>
+      .invalidReply replyError (halt session next registry)
+  | .engineResource engineResource next =>
+      .engineResource engineResource (halt session next registry)
+  | .factResource budget next =>
+      .factResource budget (halt session next registry)
+  | .malformedState next =>
+      .invalidSession (halt session next registry)
+
+/-- A whole-run arena limit is fatal. Clear the selected request through the
+ordinary policy reply boundary, retain no prospective arena state, and return
+a non-live session which cannot later claim saturation. -/
+private def exhaustPayload (session : Session Fact)
+    (state : Propagator.Policy.State Fact) (registry : Registry Fact)
+    (action : Action) (resource : PayloadArena.Resource) : Step Fact :=
+  match state.submit (action.reply (.failed PayloadFailureCode.rejected)) with
+  | .accepted _ next =>
+      .payloadResource resource (halt session next registry)
+  | .invalid replyError next =>
+      .invalidReply replyError (halt session next registry)
+  | .engineResource engineResource next =>
+      .engineResource engineResource (halt session next registry)
+  | .factResource budget next =>
+      .factResource budget (halt session next registry)
+  | .malformedState next =>
+      .invalidSession (halt session next registry)
+
+private def rejectedSession (session : Session Fact)
+    (state : Propagator.Policy.State Fact)
+    (reason : Propagator.Policy.Rejection) : Session Fact :=
+  match reason with
+  | .decisionLimit | .actionLimit | .malformedState =>
+      halt session state
+  | .wrongScope | .staleSerial | .staleProgram | .missingOffer | .wrongKey =>
+      withState session state
+
+private def finishEquality (session : Session Fact)
+    (selection : Propagator.Policy.Selection)
+    (observation : Propagator.Policy.EqualityObservation Fact)
+    (state : Propagator.Policy.State Fact) : Step Fact :=
+  match observation.outcome with
+  | .engineResource resource =>
+      .engineResource resource (halt session state)
+  | .factResource budget =>
+      .factResource budget (halt session state)
+  | .invalid _ =>
+      .invalidSession (halt session state)
+  | .noChange | .improved | .contradiction =>
+      .equality selection observation (withState session state)
+
+private def submitInvocation (session : Session Fact)
+    (selection : Propagator.Policy.Selection)
+    (request : RuleRequest Fact) (state : Propagator.Policy.State Fact)
+    (invocation : Invocation Fact) (registry : Registry Fact) : Step Fact :=
+  let plan := invocation.plan
+  let replay := invocation.replay
+  if !outcomeListsBounded session.limits.engine plan.outcome then
+    match state.submit (request.action.reply plan.outcome) with
+    | .accepted _ next =>
+        .invalidSession (halt session next registry)
+    | .invalid error next =>
+        .invalidReply error (halt session next registry)
+    | .engineResource resource next =>
+        .engineResource resource (halt session next registry)
+    | .factResource budget next =>
+        .factResource budget (halt session next registry)
+    | .malformedState next =>
+        .invalidSession (halt session next registry)
+  else
+    match replay.freeze session.limits.arena session.arena request.action
+        plan.outcome plan.drafts with
+    | .invalid error _ =>
+        failPayload session state registry request.action error
+    | .resourceLimit resource _ =>
+        match resource with
+        | .uses | .drafts | .draftCells | .atom | .schema =>
+            rejectPayload session state registry request.action resource
+        | .entries | .bodyCells =>
+            exhaustPayload session state registry request.action resource
+    | .ready arena outcome =>
+        match state.submit (request.action.reply outcome) with
+        | .accepted observation next =>
+            .rule selection observation (commit session next registry arena)
+        | .invalid error next =>
+            .invalidReply error (halt session next registry)
+        | .engineResource resource next =>
+            .engineResource resource (halt session next registry)
+        | .factResource budget next =>
+            .factResource budget (halt session next registry)
+        | .malformedState next =>
+            .invalidSession (halt session next registry)
+
+private def select (session : Session Fact)
+    (selection : Propagator.Policy.Selection) : Step Fact :=
+  match session.state.select selection with
+  | .request request state =>
+      let (invocation, registry) := session.registry.invokePlanned request
+      submitInvocation session selection request state invocation registry
+  | .equality observation state =>
+      finishEquality session selection observation state
+  | .completed completion state =>
+      match completion with
+      | .dismissed => .invalidSession (halt session state)
+      | .instanceAdmitted _ | .instanceDuplicate | .instanceRejected _ =>
+          .instance selection completion (withState session state)
+  | .split plan state =>
+      .split selection plan (withState session state)
+  | .rejected reason state =>
+      .rejected selection reason (rejectedSession session state reason)
+  | .engineResource resource state =>
+      .engineResource resource (halt session state)
+  | .factResource budget state =>
+      .factResource budget (halt session state)
+
+private def dismiss (session : Session Fact)
+    (selection : Propagator.Policy.Selection) : Step Fact :=
+  match session.state.dismiss selection with
+  | .completed .dismissed state =>
+      .dismissed selection (withState session state)
+  | .rejected reason state =>
+      .rejected selection reason (rejectedSession session state reason)
+  | .engineResource resource state =>
+      .engineResource resource (halt session state)
+  | .factResource budget state =>
+      .factResource budget (halt session state)
+  | .request _ state | .equality _ state | .completed _ state | .split _ state =>
+      .invalidSession (halt session state)
+
+/-- Execute one external-policy choice through the single proof-producing
+ownership boundary. -/
+opaque Session.choose (session : Session Fact) (choice : Choice) : Step Fact :=
+  if !session.live || session.state.engine.pending.isSome then
+    .invalidSession session
+  else if session.state.engine.contradictory then
+    .contradiction session
+  else
+    match choice with
+    | .select selection => select session selection
+    | .dismiss selection => dismiss session selection
+
+end Hex.Interval.Experiment.PolicySession
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 7a69769c0..fb128293c 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1071,6 +1071,14 @@ experimental. The older direct registry and engine interfaces remain available
 for search experiments, but proof-producing execution goes through the
 session.
 
+`PolicySession.Session` is the corresponding proof-producing policy canary.
+Its checked start stores one bundle containing the engine, policy, and arena
+limits and owns the resulting `Policy.State`, exact registry, and arena.
+`Session.view` returns the same owned session with traversal accounting
+committed, while `Session.choose` accepts only a checked selection or
+dismissal and returns the next coherent session. No public transition accepts
+separately assembled engine, registry, policy state, or arena values.
+
 The explicit registration and validation boundary is fixed. Discovery and
 scheduling above it remain empirical: one arm uses an incremental registry
 worklist to share facts and retain state, while a second traverses the same
@@ -1207,9 +1215,9 @@ 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 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
+Both private sessions commit that returned arena only if submission of the
+relocated outcome also succeeds. Before freezing, they check 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
@@ -1315,14 +1323,31 @@ 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.
+into saturation.
+
+The policy session now preserves the same transaction while allowing an
+external policy to select invocations and retries, instantiations, equality
+contractors, and splits, or to dismiss any live offer. A selected invocation
+or retry routes through `Registry.invokePlanned`, which returns the plan paired
+with the exact selected handler's replay snapshot. The session calls that
+sealed snapshot's paired freeze operation, submits the relocated reply through
+`Policy.State`, and commits the new arena only for an accepted reply. A missing
+or malformed format and package-local payload-use, draft-count, draft-cell,
+atom, or schema excess consume a bounded synthetic failed reply: the cache may
+record the attempt, the arena, facts, and history do not commit, and the
+private session remains live but permanently incomplete. Exhausting remaining
+whole-run entry or body-cell capacity after an earlier commit instead returns
+a non-live session after clearing the selected request while preserving the
+preceding arena and history.
+The policy can observe a bounded view and echo a semantic selection, but
+cannot extract and later recombine the engine, registry, arena, or policy
+bookkeeping. Its `Session.complete` predicate additionally scans for live
+invocation and equality work and treats retries and instantiations, but not
+optional splits, as closure obligations. The policy state's monotone
+incompleteness bit covers failed replies, rejected or stale narrowing
+suggestions, and required dismissals; the session bit covers evidence lost
+outside those policy transitions. Engine-resource or structurally invalid
+snapshots also become non-live.
 
 ### Action kinds
 
@@ -1844,15 +1869,20 @@ The policy experiment proceeds in replaceable increments:
    retryable enclosure, a structure-triggered alternate form, equality
    contraction, and a function-owned split landmark.
 
-The concrete package canary reaches step 6 with the unchanged external driver.
-One deterministic schedule selects subtraction and multiplication propagation,
-the structure matcher, instantiation admission, the centered function's split
-handler and forward propagator, equality contraction, reciprocal propagation,
-a precision retry, and finally the centered function's split suggestion. It
-adds the centered node at generation one, narrows both representations to
-`[0,1/4]`, improves the enclosure of `1/3` at effort one, and returns a prepared
-plan at `x = 1/2` while the effort-two retry remains live. No branch is
-executed, so this is evidence for policy routing and freshness, not for scope
+The concrete package canary reaches step 6 in both search-only and
+proof-producing modes. One deterministic schedule selects subtraction and
+multiplication propagation, the structure matcher, instantiation admission,
+the centered function's split handler and forward propagator, equality
+contraction, reciprocal propagation, a precision retry, and finally the
+centered function's split suggestion. It adds the centered node at generation
+one, narrows both representations to `[0,1/4]`, improves the enclosure of
+`1/3` at effort one, and returns a prepared plan at `x = 1/2`. The
+proof-producing schedule also dismisses the effort-two retry and therefore
+retains an honest incomplete marker. Its arena contains the exact sequence of
+fact, instance, and equality roles; the admitted instance event, equality
+edge, and centered fact provenance resolve to entries owned by their
+originating package actions. No branch is executed, so this is evidence for
+policy routing, ownership, evidence freezing, and freshness, not for scope
 creation or split interiority.
 
 Once policy control begins, the wrapper is the sole scheduling authority for
@@ -2417,6 +2447,13 @@ typical, boundary, and adversarial inputs. In particular it includes:
   and a function-owned split in a checked event order; it returns an
   endpoint-resource-checked plan at `1/2`, leaves the next retry offer live,
   and performs no branch/interiority step;
+- the proof-producing policy session over those same packages, selecting every
+  offer class through one private owner, retaining exact fact, instance, and
+  equality replay formats, rolling back a prospectively frozen rejected write
+  and both malformed and undeclared formats, keeping package-local payload
+  use, draft-count, draft-cell, atom, and schema bounds live but incomplete,
+  making genuine mid-run whole-arena exhaustion fatal, and exposing an empty
+  failed frontier as incomplete rather than saturated;
 - undirected equality transport, including incomparable endpoint facts that
   improve both sides atomically, equality chains, reactivation after a later
   function improvement, and an original expression transferring its bound to
diff --git a/conformance/HexInterval/PolicySessionConformance.lean b/conformance/HexInterval/PolicySessionConformance.lean
new file mode 100644
index 000000000..ef7ecaa15
--- /dev/null
+++ b/conformance/HexInterval/PolicySessionConformance.lean
@@ -0,0 +1,746 @@
+/-
+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.DyadicRules
+import HexInterval.Experiment.PolicySession
+
+/-!
+End-to-end conformance for the proof-producing policy session.  A scripted
+external policy uses only session views and choices while arbitrary packages
+introduce a centered expression, prove its equality to an existing product,
+propagate its sharper bound, retry an unrelated function, dismiss remaining
+narrowing work, and prepare a split.
+-/
+
+namespace Hex.Interval.PolicySessionConformance
+
+open Experiment Propagator
+open DyadicRules
+open PolicySession
+
+def d (value : Int) : Dyadic := Dyadic.ofInt value
+
+def real : DomainId := { index := 0 }
+def sourceOp : OpKey := { name := "policy-session.source" }
+
+def endpointLimit : EndpointLimit where
+  maxEndpointHeight := 128
+  maxAlignmentShift := 64
+
+def config : Config :=
+  { endpointLimit
+    reciprocalBasePrecision := 2
+    maxReciprocalEffort := 4 }
+
+def engineLimits : Propagator.Limits :=
+  { maxOperations := 24
+    maxNodes := 32
+    maxRules := 16
+    maxRegistryEntries := 96
+    maxReplayFormats := 32
+    maxArity := 4
+    maxApplications := 64
+    maxQueueEntries := 256
+    maxActions := 128
+    maxAcceptedFacts := 128
+    maxRetainedSuggestions := 32
+    maxEffort := 8
+    maxObservationValue := 256
+    maxDiagnosticValue := 256
+    maxOutcomeCandidates := 4
+    maxOutcomeSuggestions := 4
+    maxProposalItems := 16
+    maxInstances := 8
+    maxGeneration := 4
+    maxNodeDepth := 16
+    maxEqualities := 8
+    splitEndpointLimit := endpointLimit }
+
+def policyLimits : Propagator.Policy.Limits :=
+  { maxDecisions := 128
+    maxTraversal := 16384
+    maxLiveOffers := 512 }
+
+def arenaLimits : PayloadArena.Limits :=
+  { maxEntries := 72
+    maxBodyCells := 0
+    maxDrafts := 72
+    maxDraftCells := 0
+    maxAtom := 0
+    maxSchema := 0
+    maxUses := 72 }
+
+def limits : PolicySession.Limits :=
+  { engine := engineLimits
+    policy := policyLimits
+    arena := arenaLimits }
+
+def operations : Array Operation :=
+  ((arithmeticOperations real).append (centeredOperations real)).push
+    { key := sourceOp, inputs := [], output := real }
+
+def node (index : Nat) : NodeId := { index }
+
+def instruction (operation : Nat) (args : List NodeId := []) : Node :=
+  { domain := real, op := { index := operation }, args }
+
+/-- Nodes are `x`, `1`, `1-x`, `x*(1-x)`, `3`, and `1/3`.  The centered
+instance is appended at node six. -/
+def program : Program :=
+  { operations
+    nodes :=
+      #[instruction 7,
+        instruction 0,
+        instruction 2 [node 1, node 0],
+        instruction 3 [node 0, node 2],
+        instruction 7,
+        instruction 5 [node 4]] }
+
+def finite (lower upper : Int) : Raw :=
+  .bounds (.finite (d lower) false) (.finite (d upper) false)
+
+def whole : Raw := .bounds .unbounded .unbounded
+
+def initialFacts? : Option (Array Fact) :=
+  match DyadicInterval.importInitialFacts endpointLimit 0
+      [finite 0 1, finite 1 1, whole, whole, finite 3 3, whole] with
+  | .ok facts => some facts.toArray
+  | .error _ => none
+
+def start? : Option (PolicySession.Session Fact) :=
+  match initialFacts? with
+  | none => none
+  | some facts =>
+      match PolicySession.Session.start (DyadicInterval.factDomain endpointLimit)
+          program #[arithmeticPackage config real, centeredPackage config real]
+          facts limits with
+      | .ok session => some session
+      | .error _ => none
+
+inductive Command
+  | invoke (key : RuleKey)
+  | instantiate (key : RuleKey)
+  | retry (key : RuleKey) (effort : Nat)
+  | equality
+  | dismissRetry (key : RuleKey) (effort : Nat)
+  | split (key : RuleKey)
+
+def commandMatches : Command -> Propagator.Policy.OfferView -> Bool
+  | .invoke key, { key := .invoke source, .. } => source.rule == key
+  | .instantiate key, { key := .instantiate source _, .. } => source.rule == key
+  | .retry key effort, { key := .retry source offered, .. } =>
+      source.rule == key && offered == effort
+  | .equality, { key := .equality _, .. } => true
+  | .dismissRetry key effort, { key := .retry source offered, .. } =>
+      source.rule == key && offered == effort
+  | .split key, { key := .split source _ _ _, .. } => source.rule == key
+  | _, _ => false
+
+def selection? (session : PolicySession.Session Fact) (command : Command) :
+    Option (Propagator.Policy.Selection × PolicySession.Session Fact) :=
+  match session.view with
+  | .ready view viewed =>
+      match view.offers.toList.find? (commandMatches command) with
+      | none => none
+      | some offer =>
+          some
+            ({ scope := view.scope
+               serial := view.serial
+               programVersion := view.programVersion
+               id := offer.id
+               expected := offer.key },
+             viewed)
+  | .resource _ _ | .contradiction _ | .invalidSession _ => none
+
+structure Run where
+  session : PolicySession.Session Fact
+  split : Option (Propagator.Policy.SplitPlan Fact)
+
+def execute? (session : PolicySession.Session Fact) (command : Command) :
+    Option Run := do
+  let (selection, viewed) <- selection? session command
+  match command with
+  | .invoke _ =>
+      match viewed.choose (.select selection) with
+      | .rule _ _ next => some { session := next, split := none }
+      | _ => none
+  | .retry _ _ =>
+      match viewed.choose (.select selection) with
+      | .rule _ _ next => some { session := next, split := none }
+      | _ => none
+  | .instantiate _ =>
+      match viewed.choose (.select selection) with
+      | .instance _ (.instanceAdmitted [fresh]) next =>
+          if fresh == node 6 then some { session := next, split := none } else none
+      | _ => none
+  | .equality =>
+      match viewed.choose (.select selection) with
+      | .equality _ observation next =>
+          if observation.outcome == .improved then
+            some { session := next, split := none }
+          else
+            none
+      | _ => none
+  | .dismissRetry _ _ =>
+      match viewed.choose (.dismiss selection) with
+      | .dismissed _ next => some { session := next, split := none }
+      | _ => none
+  | .split _ =>
+      match viewed.choose (.select selection) with
+      | .split _ plan next => some { session := next, split := some plan }
+      | _ => none
+
+def run : List Command -> PolicySession.Session Fact -> Option Run
+  | [], session => some { session, split := none }
+  | command :: commands, session => do
+      let step <- execute? session command
+      match commands, step.split with
+      | [], _ => some step
+      | _ :: _, some _ => none
+      | _ :: _, none => run commands step.session
+
+def commands : List Command :=
+  [.invoke subForwardKey,
+    .invoke mulForwardKey,
+    .invoke centeredInstantiateKey,
+    .instantiate centeredInstantiateKey,
+    .invoke centeredSplitKey,
+    .invoke centeredForwardKey,
+    .equality,
+    .invoke reciprocalForwardKey,
+    .retry reciprocalForwardKey 1,
+    .dismissRetry reciprocalForwardKey 2,
+    .split centeredSplitKey]
+
+def final? : Option Run := do
+  let session <- start?
+  run commands session
+
+def exactFact (session : PolicySession.Session Fact) (index : Nat)
+    (expected : Raw) : Bool :=
+  (session.state.engine.facts[index]?).any fun fact => fact.view == expected
+
+def factPayload? (session : PolicySession.Session Fact) (target : NodeId)
+    (key : RuleKey) : Option PayloadId := do
+  let event <- session.state.engine.history.toList.find? fun event =>
+    event.node == target &&
+      match event.cause with
+      | .rule action _ _ => action.key == key
+      | .transport _ _ => false
+  match event.cause with
+  | .rule _ _ payload => some payload
+  | .transport _ _ => none
+
+def ownsV0 (session : PolicySession.Session Fact) (payload : PayloadId)
+    (role : PayloadArena.Role) (key : RuleKey) : Bool :=
+  (session.arena.entry? payload role).any fun entry =>
+    entry.origin.key == key && entry.schema == 0 && entry.body.isEmpty
+
+/-! # Prospective arena rejection -/
+
+def badProgram : Program :=
+  { operations :=
+      #[{ key := centeredOp, inputs := [real], output := real },
+        { key := sourceOp, inputs := [], output := real }]
+    nodes := #[instruction 1, instruction 0 [node 0]] }
+
+def badPlan (request : RuleRequest Fact) : Plan Fact :=
+  match request.inputs with
+  | [input] =>
+      { outcome :=
+          .success
+            [{ node := node 0, fact := input.fact, payload := factLabel }]
+            [] {}
+        drafts := [emptyDraft factLabel .fact] }
+  | _ => withoutPayloads (.failed 70)
+
+def badPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward badPlan #[emptyFormat .fact]] }
+
+def malformedFormat : ReplayFormat :=
+  { role := .fact
+    schema := 0
+    validateBody := fun _ => false }
+
+def malformedPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward badPlan #[malformedFormat]] }
+
+def missingFormatPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers := #[Handler.statelessPlanned centeredForward badPlan] }
+
+def oneCellPlan (atom : Nat) (request : RuleRequest Fact) : Plan Fact :=
+  match request.inputs with
+  | [input] =>
+      { outcome :=
+          .success
+            [{ node := node 0, fact := input.fact, payload := factLabel }]
+            [] {}
+        drafts :=
+          [{ label := factLabel, role := .fact, schema := 0, body := [atom] }] }
+  | _ => withoutPayloads (.failed 70)
+
+def oneCellFormat : ReplayFormat :=
+  { role := .fact
+    schema := 0
+    validateBody := fun body =>
+      match body with
+      | [_] => true
+      | _ => false }
+
+def atomPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward (oneCellPlan 1) #[oneCellFormat]] }
+
+def bodyPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward (oneCellPlan 0) #[oneCellFormat]] }
+
+def schemaPlan (request : RuleRequest Fact) : Plan Fact :=
+  match request.inputs with
+  | [input] =>
+      { outcome :=
+          .success
+            [{ node := node 0, fact := input.fact, payload := factLabel }]
+            [] {}
+        drafts :=
+          [{ label := factLabel, role := .fact, schema := 1, body := [] }] }
+  | _ => withoutPayloads (.failed 70)
+
+def schemaFormat : ReplayFormat :=
+  { role := .fact
+    schema := 1
+    validateBody := fun body => body.isEmpty }
+
+def schemaPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward schemaPlan #[schemaFormat]] }
+
+def usesPlan (request : RuleRequest Fact) : Plan Fact :=
+  let equality : ProposedEquality :=
+    { left := .existing request.action.node
+      right := .existing request.action.node
+      payload := equalityLabel }
+  { outcome :=
+      .success []
+        [.instantiate
+          { key := 91
+            nodes := []
+            equalities := List.replicate arenaLimits.maxUses equality
+            payload := instanceLabel }]
+        {}
+    drafts := [] }
+
+def usesPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward usesPlan #[emptyFormat .fact]] }
+
+def draftsPlan (_request : RuleRequest Fact) : Plan Fact :=
+  { outcome := .noChange {}
+    drafts :=
+      List.replicate (arenaLimits.maxDrafts + 1) (emptyDraft factLabel .fact) }
+
+def draftsPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward draftsPlan #[emptyFormat .fact]] }
+
+def badFacts? : Option (Array Fact) :=
+  match DyadicInterval.importInitialFacts endpointLimit 0 [finite 0 1, whole] with
+  | .ok facts => some facts.toArray
+  | .error _ => none
+
+def badStartWith? (package : Package Fact)
+    (sessionLimits : PolicySession.Limits := limits) :
+    Option (PolicySession.Session Fact) :=
+  match badFacts? with
+  | none => none
+  | some facts =>
+      match PolicySession.Session.start (DyadicInterval.factDomain endpointLimit)
+          badProgram #[package] facts sessionLimits with
+      | .ok session => some session
+      | .error _ => none
+
+def badStart? : Option (PolicySession.Session Fact) :=
+  badStartWith? badPackage
+
+def missingFormatStart? : Option (PolicySession.Session Fact) :=
+  badStartWith? missingFormatPackage
+
+def capacityProgram : Program :=
+  { badProgram with
+    nodes :=
+      #[instruction 1,
+        instruction 0 [node 0],
+        instruction 0 [node 0]] }
+
+def capacityPlan (body : List Nat) (request : RuleRequest Fact) : Plan Fact :=
+  match request.inputs, request.writes with
+  | [input], [target] =>
+      { outcome :=
+          .success
+            [{ node := target, fact := input.fact, payload := factLabel }]
+            [] {}
+        drafts :=
+          [{ label := factLabel, role := .fact, schema := 0, body }] }
+  | _, _ => withoutPayloads (.failed 70)
+
+def entryPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward (capacityPlan []) #[emptyFormat .fact]] }
+
+def cellPackage : Package Fact :=
+  { Cache := Unit
+    cache := ()
+    operations := centeredOperations real
+    handlers :=
+      #[Handler.statelessPlanned centeredForward (capacityPlan [0]) #[oneCellFormat]] }
+
+def capacityFacts? : Option (Array Fact) :=
+  match
+      DyadicInterval.importInitialFacts endpointLimit 0
+        [finite 0 1, whole, whole] with
+  | .ok facts => some facts.toArray
+  | .error _ => none
+
+def capacityEngineLimits : Propagator.Limits :=
+  { engineLimits with
+    maxOutcomeCandidates := 1
+    maxOutcomeSuggestions := 0
+    maxProposalItems := 0 }
+
+def entryArena : PayloadArena.Limits :=
+  { maxEntries := 1
+    maxBodyCells := 0
+    maxDrafts := 1
+    maxDraftCells := 0
+    maxAtom := 0
+    maxSchema := 0
+    maxUses := 1 }
+
+def cellArena : PayloadArena.Limits :=
+  { maxEntries := 2
+    maxBodyCells := 1
+    maxDrafts := 1
+    maxDraftCells := 1
+    maxAtom := 0
+    maxSchema := 0
+    maxUses := 1 }
+
+def capacityLimits (arena : PayloadArena.Limits) : PolicySession.Limits :=
+  { engine := capacityEngineLimits, policy := policyLimits, arena }
+
+def capacityStartWith? (package : Package Fact)
+    (arena : PayloadArena.Limits) : Option (PolicySession.Session Fact) :=
+  match capacityFacts? with
+  | none => none
+  | some facts =>
+      match PolicySession.Session.start (DyadicInterval.factDomain endpointLimit)
+          capacityProgram #[package] facts (capacityLimits arena) with
+      | .ok session => some session
+      | .error _ => none
+
+def incompleteView (session : PolicySession.Session Fact) : Bool :=
+  match session.view with
+  | .ready view next =>
+      view.offers.isEmpty && view.incomplete && next.live && !next.complete
+  | .resource _ _ | .contradiction _ | .invalidSession _ => false
+
+#guard program.check
+#guard capacityProgram.check
+#guard
+  PolicySession.requiredUses engineLimits == 72 &&
+    PolicySession.limitsCoherent limits
+#guard
+  !PolicySession.limitsCoherent
+    { limits with
+      arena :=
+        { arenaLimits with
+          maxEntries := 73
+          maxDrafts := 73
+          maxUses := 72 } }
+#guard PolicySession.limitsCoherent (capacityLimits entryArena)
+#guard PolicySession.limitsCoherent (capacityLimits cellArena)
+
+-- The policy never obtains a free-standing engine, registry, or arena.  The
+-- single session route freezes all seven fact/instance/equality recipes,
+-- admits the centered node and edge, and transports `[0,1/4]` back to the
+-- dependency-losing product.  Dismissing retry effort two is remembered as
+-- incomplete even though the later split is still selectable.
+#guard
+  match final? with
+  | none => false
+  | some result =>
+      let session := result.session
+      session.live && !session.droppedWork && session.state.incomplete &&
+        !session.complete &&
+        session.state.metrics.decisions == 11 &&
+        session.state.metrics.selectedInvocations == 6 &&
+        session.state.metrics.selectedRetries == 1 &&
+        session.state.metrics.selectedInstances == 1 &&
+        session.state.metrics.selectedEqualities == 1 &&
+        session.state.metrics.selectedSplits == 1 &&
+        session.state.metrics.dismissals == 1 &&
+        session.state.engine.programVersion == 1 &&
+        session.state.engine.program.nodes.size == 7 &&
+        session.state.engine.equalities.size == 1 &&
+        session.state.engine.instanceHistory.size == 1 &&
+        session.arena.entries.size == 7 && session.arena.bodyCells == 0 &&
+        session.arena.entries.toList.map (fun entry => entry.role) ==
+          [.fact, .fact, .instance, .equality, .fact, .fact, .fact] &&
+        exactFact session 3
+          (.bounds (.finite 0 false) (.finite quarter false)) &&
+        exactFact session 6
+          (.bounds (.finite 0 false) (.finite quarter false)) &&
+        match session.state.engine.instanceHistory[0]?,
+            session.state.engine.equalities[0]?,
+            factPayload? session (node 6) centeredForwardKey,
+            result.split with
+        | some instanceEvent, some equality, some factPayload, some split =>
+            instanceEvent.payload.index == 2 && equality.payload.index == 3 &&
+              factPayload.index == 4 &&
+              ownsV0 session instanceEvent.payload .instance centeredInstantiateKey &&
+              ownsV0 session equality.payload .equality centeredInstantiateKey &&
+              ownsV0 session factPayload .fact centeredForwardKey &&
+              equality.left == node 3 && equality.right == node 6 &&
+              split.node == node 0 && split.point == half &&
+              split.reason == .criticalPoint &&
+              split.origin.key == centeredSplitKey
+        | _, _, _, _ => false
+
+-- Freezing an otherwise well-formed fact draft is prospective.  The package's
+-- undeclared write is rejected by policy-state submission, and the returned
+-- non-live session retains neither the new arena entry nor any fact history.
+#guard
+  match badStart? with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .invalidReply (.undeclaredWrite target) stopped =>
+              target == node 0 && !stopped.live &&
+                stopped.arena.entries.isEmpty &&
+                stopped.arena.bodyCells == 0 &&
+                stopped.state.engine.history.isEmpty &&
+                stopped.state.engine.pending.isNone
+          | _ => false
+
+-- A declared format which rejects the bounded body takes the same atomic,
+-- live-but-incomplete path. No partially frozen entry, fact, or history item
+-- survives, and the empty next view is explicitly incomplete rather than a
+-- false saturation claim.
+#guard
+  match badStartWith? malformedPackage with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .invalidPayload (.invalidBody key) next =>
+              key.rule == centeredForwardKey && key.role == .fact &&
+                key.schema == 0 && next.live && next.droppedWork &&
+                next.state.incomplete && !next.complete &&
+                next.arena.entries.isEmpty && next.arena.bodyCells == 0 &&
+                next.state.engine.history.isEmpty &&
+                next.state.engine.pending.isNone &&
+                next.state.engine.metrics.ruleFailures == 1 &&
+                incompleteView next
+          | _ => false
+
+-- The same plan without its handler-owned fact format fails before arena or
+-- engine admission. The synthetic failed reply clears the latch and keeps the
+-- session usable, while permanently preventing a completeness claim.
+#guard
+  match missingFormatStart? with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .invalidPayload (.undeclaredFormat key) next =>
+              key.rule == centeredForwardKey && key.role == .fact &&
+                key.schema == 0 && next.live && next.droppedWork &&
+                next.state.incomplete && !next.complete &&
+                next.arena.entries.isEmpty && next.arena.bodyCells == 0 &&
+                next.state.engine.history.isEmpty &&
+                next.state.engine.pending.isNone &&
+                next.state.engine.metrics.ruleFailures == 1 &&
+                incompleteView next &&
+                (next.registry.packages[0]?).any fun package =>
+                  package.invocations == 1
+          | _ => false
+
+-- Payload-use, draft-count, draft-cell, atom, and schema bounds are
+-- package-local encoding failures. Each rejected plan consumes a bounded
+-- failed reply, keeps the private owner live for later choices, rolls back the
+-- prospective arena, and makes the now-empty policy frontier explicitly
+-- incomplete.
+#guard
+  match badStartWith? usesPackage with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .rejectedPayload .uses next =>
+              next.live && next.droppedWork && next.state.incomplete &&
+                next.state.engine.pending.isNone &&
+                next.state.engine.metrics.ruleFailures == 1 &&
+                next.arena.entries.isEmpty &&
+                next.state.engine.history.isEmpty && incompleteView next
+          | _ => false
+
+#guard
+  match badStartWith? draftsPackage with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .rejectedPayload .drafts next =>
+              next.live && next.droppedWork && next.state.incomplete &&
+                next.state.engine.pending.isNone &&
+                next.state.engine.metrics.ruleFailures == 1 &&
+                next.arena.entries.isEmpty &&
+                next.state.engine.history.isEmpty && incompleteView next
+          | _ => false
+
+#guard
+  match badStartWith? atomPackage
+      { limits with arena := { arenaLimits with maxBodyCells := 1 } } with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .rejectedPayload .atom next =>
+              next.live && next.droppedWork && next.state.incomplete &&
+                next.state.engine.pending.isNone &&
+                next.state.engine.metrics.ruleFailures == 1 &&
+                next.arena.entries.isEmpty &&
+                next.state.engine.history.isEmpty && incompleteView next
+          | _ => false
+
+#guard
+  match badStartWith? bodyPackage with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .rejectedPayload .draftCells next =>
+              next.live && next.droppedWork && next.state.incomplete &&
+                next.state.engine.pending.isNone &&
+                next.state.engine.metrics.ruleFailures == 1 &&
+                next.arena.entries.isEmpty &&
+                next.state.engine.history.isEmpty && incompleteView next
+          | _ => false
+
+#guard
+  match badStartWith? schemaPackage with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .rejectedPayload .schema next =>
+              next.live && next.droppedWork && next.state.incomplete &&
+                next.state.engine.pending.isNone &&
+                next.state.engine.metrics.ruleFailures == 1 &&
+                next.arena.entries.isEmpty &&
+                next.state.engine.history.isEmpty && incompleteView next
+          | _ => false
+
+-- Entry and body-cell budgets become fatal only when an otherwise valid reply
+-- no longer fits after a prior policy-selected commit. The earlier arena and
+-- fact history remain intact, but the returned private snapshot cannot resume
+-- or claim completeness.
+#guard
+  match capacityStartWith? entryPackage entryArena with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .rule _ _ first =>
+              first.arena.entries.size == 1 &&
+                first.state.engine.history.size == 1 &&
+                match selection? first (.invoke centeredForwardKey) with
+                | none => false
+                | some (nextSelection, nextViewed) =>
+                    match nextViewed.choose (.select nextSelection) with
+                    | .payloadResource .entries stopped =>
+                        !stopped.live && !stopped.complete &&
+                          stopped.state.incomplete &&
+                          stopped.state.engine.pending.isNone &&
+                          stopped.arena.entries.size == 1 &&
+                          stopped.state.engine.history.size == 1
+                    | _ => false
+          | _ => false
+
+#guard
+  match capacityStartWith? cellPackage cellArena with
+  | none => false
+  | some session =>
+      match selection? session (.invoke centeredForwardKey) with
+      | none => false
+      | some (selection, viewed) =>
+          match viewed.choose (.select selection) with
+          | .rule _ _ first =>
+              first.arena.entries.size == 1 && first.arena.bodyCells == 1 &&
+                first.state.engine.history.size == 1 &&
+                match selection? first (.invoke centeredForwardKey) with
+                | none => false
+                | some (nextSelection, nextViewed) =>
+                    match nextViewed.choose (.select nextSelection) with
+                    | .payloadResource .bodyCells stopped =>
+                        !stopped.live && !stopped.complete &&
+                          stopped.state.incomplete &&
+                          stopped.state.engine.pending.isNone &&
+                          stopped.arena.entries.size == 1 &&
+                          stopped.arena.bodyCells == 1 &&
+                          stopped.state.engine.history.size == 1
+                    | _ => false
+          | _ => false
+
+end Hex.Interval.PolicySessionConformance
diff --git a/lakefile.lean b/lakefile.lean
index 83ab30541..66bf29124 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -234,7 +234,8 @@ lean_lib HexIntervalExperiment where
     `HexInterval.Experiment.PackageRegistry,
     `HexInterval.Experiment.DyadicInterval,
     `HexInterval.Experiment.DyadicRules,
-    `HexInterval.Experiment.PayloadArena, `HexInterval.Experiment.PayloadSession]
+    `HexInterval.Experiment.PayloadArena, `HexInterval.Experiment.PayloadSession,
+    `HexInterval.Experiment.PolicySession]
 
 lean_lib HexIntervalMathlibExperiment where
   globs := #[`HexIntervalMathlib.Experiment.Center]
@@ -301,7 +302,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, `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
+  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, `HexInterval.PolicySessionConformance, `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/20260728T055329Z.md b/progress/20260728T055329Z.md
new file mode 100644
index 000000000..db951a6ba
--- /dev/null
+++ b/progress/20260728T055329Z.md
@@ -0,0 +1,43 @@
+# Proof-producing policy session
+
+## Accomplished
+
+- Rebased the stale child branch onto the hardened payload-session stack and
+  retained the policy completeness corrections.
+- Added a private-constructor policy session which owns one
+  `Policy.State`, its exact heterogeneous package registry, the immutable
+  payload arena, all three resource envelopes, and monotone liveness and
+  completeness state.
+- Routed selected invocations and retries through `Registry.invokePlanned`,
+  prospective proof-draft freezing, relocation, and `Policy.State.submit`.
+  The prospective arena commits only after reply acceptance.
+- Kept instantiation admission, equality contraction, dismissal, and split
+  preparation inside the same session choice API.
+- Added a centered-function conformance trace which exercises every choice
+  class, creates the alternate expression and equality, contracts the sharper
+  bound back to the original product, and checks exact fact, instance, and
+  equality arena roles.
+- Added an atomicity canary showing that a fully frozen prospective fact draft
+  is discarded when policy-state submission rejects an undeclared write.
+- Restored the final completeness accounting for dropped narrowing
+  suggestions and consumed invalid or resource-limited replies.
+- Built the policy session, its conformance target, all related policy and
+  payload-session conformance targets, and `HexIntervalExperiment`.
+
+## Current frontier
+
+Arbitrary propagators, structural instantiation, policy choice, proof-payload
+ownership, and equality transport now compose through one unforgeable session.
+Payload bodies are still opaque: packages do not yet carry their semantic
+replay decoders or theorems.
+
+## Next step
+
+Add package-owned replay dispatch to the exact registry snapshot, then replay
+the centered instance, equality, and fact entries against the immutable
+history prefix. Branch construction from a prepared split remains a separate
+scope-layer experiment.
+
+## Blockers
+
+None.
diff --git a/progress/20260728T060219Z.md b/progress/20260728T060219Z.md
new file mode 100644
index 000000000..4b81e49e3
--- /dev/null
+++ b/progress/20260728T060219Z.md
@@ -0,0 +1,38 @@
+# Replay-aware policy session
+
+## Accomplished
+
+- Rebased the private policy-session stack onto the package-owned replay-format
+  experiment, dropping the superseded payload-session commits.
+- Updated selected rule and retry execution to retain the complete
+  `Invocation`: its plan and exact handler replay snapshot now pass together
+  through `PayloadArena.freezeChecked`.
+- Preserved prospective arena atomicity. A registered-format plan which the
+  engine rejects commits no arena entry, while an undeclared format clears the
+  reply latch through a synthetic failed reply, keeps the session live, marks
+  it incomplete, and commits neither arena nor fact history.
+- Kept the centered all-choice trace green with the real packages' registered
+  fact, instance, and equality formats.
+- Incorporated the latest policy invariant: adopting an open pending latch is
+  incomplete, and every unsuccessful reply uses the shared pending-latch
+  discriminator rather than assuming all resource failures consume work.
+- Built the focused policy, frontier, package-format, payload-arena,
+  payload-session, dyadic-package, and policy-session conformance targets plus
+  `HexIntervalExperiment`.
+
+## Current frontier
+
+The external policy can now compose arbitrary package invocation, structural
+instantiation, equality propagation, retry, dismissal, and split preparation
+without separating search state from replay-format validation or payload
+ownership.
+
+## Next step
+
+Add package-owned semantic decoders and replay the centered fact, instance,
+and equality entries against the validated history prefix. Keep branch
+construction from a prepared split in the later scope layer.
+
+## Blockers
+
+None.
diff --git a/progress/20260729T052733Z.md b/progress/20260729T052733Z.md
new file mode 100644
index 000000000..d713677a9
--- /dev/null
+++ b/progress/20260729T052733Z.md
@@ -0,0 +1,36 @@
+# Policy-owned payload session restack
+
+## Accomplished
+
+- Restacked the policy-session tail from `219e460b` onto package replay
+  `dd81fd53`, dropping the superseded package and replay commits.
+- Preserved the merged generic policy invariants: closure relevance is shared
+  through `Suggestion.affectsClosure`, and retained-suggestion admission and
+  completeness accounting use the engine's exact kept/dropped boundary.
+- Routed proof freezing through the sealed `ReplaySnapshot.freeze` operation
+  and supplied the registry-entry and replay-format limits added by the base.
+- Made payload-use, atom, and schema excess consume a failed reply and return a
+  live incomplete policy session, while entry and body-cell exhaustion returns
+  a non-live fatal snapshot.
+- Extended the private-owner canary across centered instantiation, structural
+  equality admission and contraction, invocation, retry, instantiation,
+  equality, dismissal, and split choices, prospective engine rollback,
+  malformed and undeclared replay formats, all five payload resource classes,
+  and an empty frontier which remains explicitly incomplete.
+- Built the focused policy, policy-driver, frontier, package-registry,
+  payload-arena, payload-session, dyadic-interval, dyadic-rules, and
+  policy-session conformance targets together with `HexIntervalExperiment`.
+
+## Current frontier
+
+The restacked policy session is locally green and ready to publish as a draft
+stacked on `agent/interval-package-replay`.
+
+## Next step
+
+Push the branch, open the stacked draft PR, and inspect its job-level CI state
+for any integration failure not covered by the focused local graph.
+
+## Blockers
+
+None.
diff --git a/progress/20260729T062058Z.md b/progress/20260729T062058Z.md
new file mode 100644
index 000000000..0526703ca
--- /dev/null
+++ b/progress/20260729T062058Z.md
@@ -0,0 +1,31 @@
+# Accomplished
+
+- Restacked the policy-owned payload session on package replay head
+  `2e85abd17a049152ba1e7ba8b23111566ead8517`, retaining only the three
+  policy-session commits and dropping duplicate lower-stack completeness fixes.
+- Mirrored payload-arena local/global limit invariants in session startup and
+  classified use, draft-count, draft-cell, atom, and schema excess as
+  recoverable reply failures while reserving entry and body-cell exhaustion for
+  genuine whole-run capacity failures.
+- Added conformance coverage for every resource class and for fatal entry and
+  body-cell exhaustion after a prior accepted commit, preserving the earlier
+  arena and policy history.
+- Preserved the eleven-choice end-to-end policy canary, including centered
+  invocation, instantiation, equality, dismissal, split, and exact sealed
+  replay formats.
+- Passed the focused 28-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+The policy session now owns the exact package registry, replay snapshot, and
+prospective payload arena through all semantic policy choices.
+
+# Next step
+
+Mechanically restack this branch again after the newly refreshed lower
+dependency chain is available.
+
+# Blockers
+
+None.
diff --git a/progress/20260729T062719Z.md b/progress/20260729T062719Z.md
new file mode 100644
index 000000000..128fb1c04
--- /dev/null
+++ b/progress/20260729T062719Z.md
@@ -0,0 +1,25 @@
+# Accomplished
+
+- Restacked the policy-owned payload session on refreshed package-replay head
+  `d152dc5be99ae02ed1394a53fc1576b8b369c733`.
+- Migrated its conformance fixture to the engine-owned structural-depth and
+  instantiation-generation API.
+- Preserved the eleven-choice end-to-end canary, exact fact, instance, and
+  equality replay formats, all five recoverable local resource classes, and
+  genuine mid-run fatal entry and body-cell exhaustion.
+- Passed the focused 28-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+The complete payload-arena, payload-session, sealed package-replay, and
+policy-session chain is green on refreshed payload-arena head
+`7d37887de186282fc23a8ecc3d4b68ec50c84d04`.
+
+# Next step
+
+Review CI results for the refreshed pull-request stack.
+
+# Blockers
+
+None.
diff --git a/progress/20260729T065149Z.md b/progress/20260729T065149Z.md
new file mode 100644
index 000000000..848074d19
--- /dev/null
+++ b/progress/20260729T065149Z.md
@@ -0,0 +1,27 @@
+# Accomplished
+
+- Restacked the policy-owned payload session on package-replay head
+  `6ec486da1f84c665806599365b89b01f85b0ee19`.
+- Removed the obsolete package-supplied instantiation trigger from the
+  payload-use stress fixture; dependency discovery remains engine-owned.
+- Preserved the eleven-choice policy canary, exact fact/instance/equality
+  replay formats, five recoverable local resource classes, and genuine
+  non-resumable mid-run entry/body exhaustion.
+- Inherited the reviewed opaque draft transaction and exact sealed validation
+  order unchanged.
+- Passed the focused 28-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+The policy-owned payload session is green on the final package-replay and
+suggestion-recovery stack.
+
+# Next step
+
+Verify the independent semantic-replay sibling on the same package-replay
+head, then review CI for the completed stack.
+
+# Blockers
+
+None.
diff --git a/progress/20260729T071511Z.md b/progress/20260729T071511Z.md
new file mode 100644
index 000000000..eb616c259
--- /dev/null
+++ b/progress/20260729T071511Z.md
@@ -0,0 +1,26 @@
+# Accomplished
+
+- Restacked the policy-owned payload session on final package-replay head
+  `79e3c9f33527de90e2fd9400f3e81453b409db5a`.
+- Inherited exact accepted suggestion plans, capacity/depth drop provenance,
+  opaque draft accounting, and sealed validation order without policy-session
+  changes.
+- Preserved the eleven-choice policy canary, exact replay formats, five
+  recoverable local resource classes, and non-resumable cumulative
+  entry/body-cell exhaustion.
+- Passed the focused 28-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+Policy-owned payload sessions are green on the final arbitrary-propagator and
+package-replay stack.
+
+# Next step
+
+Verify the semantic-replay sibling on the same package-replay head and review
+CI for the completed stack.
+
+# Blockers
+
+None.