diff --git a/HexInterval/Experiment/PolicyFeature.lean b/HexInterval/Experiment/PolicyFeature.lean
new file mode 100644
index 000000000..9468430ed
--- /dev/null
+++ b/HexInterval/Experiment/PolicyFeature.lean
@@ -0,0 +1,209 @@
+/-
+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.Policy
+
+@[expose] public section
+
+/-!
+# Bounded package features for interval-search policies
+
+An interval or function package may know that one live offer is more useful
+than another, even though the generic scheduler must not know how to interpret
+its facts or operations.  This experiment gives such packages a stateless,
+versioned feature callback.  A callback receives one immutable policy snapshot
+and one engine-owned offer; the decorator accepts only bounded integer output.
+
+Callbacks are evaluated while a view is decorated; they are never retained in
+the policy state.  The decorated offer keeps the complete engine-owned offer,
+so choosing it still goes through the ordinary freshness and semantic-key
+checks.  A stale or dishonest feature can therefore change search order, but
+cannot authorize an engine transition, enter proof evidence, or bypass replay
+validation of the trace that search eventually generates.
+-/
+
+namespace Hex.Interval.Experiment.PolicyFeature
+
+open Propagator Propagator.Policy
+
+/-- Versioned identity of one independently registered feature provider.
+Changing the meaning of any local feature requires a new provider version. -/
+structure ProviderKey where
+  family : Nat
+  version : Nat
+  deriving DecidableEq, Repr
+
+/-- A provider-local feature before its owner is attached by the registry. -/
+structure LocalFeature where
+  key : Nat
+  value : Int
+  deriving DecidableEq, Repr
+
+/-- Globally unambiguous feature address and its bounded integer value. -/
+structure Feature where
+  provider : ProviderKey
+  key : Nat
+  value : Int
+  deriving DecidableEq, Repr
+
+/-- Exact immutable input to a feature provider.
+
+The request deliberately contains no package cache and grants no mutation
+authority.  A goal-oriented provider may close over a fixed frontend goal;
+the provider version must change when the interpretation of that configuration
+changes. -/
+structure Request (Fact : Type) where
+  scope : ScopeId
+  serial : Nat
+  programVersion : Nat
+  facts : Snapshot Fact
+  remaining : EngineBudgetView
+  incomplete : Bool
+  offer : OfferView
+
+/-- Stateless companion contribution from one interval or frontend package.
+Returning an empty array means this provider contributes nothing for the offer. -/
+structure Provider (Fact : Type) where
+  key : ProviderKey
+  features : Request Fact -> Array LocalFeature
+
+/-- Every accepted output/count dimension which a provider can make large has
+an independent cap.  Provider identities are opaque registry addresses. -/
+structure Limits where
+  maxProviders : Nat
+  maxProviderChecks : Nat
+  maxFeaturesPerProvider : Nat
+  maxFeaturesPerOffer : Nat
+  maxTotalFeatures : Nat
+  maxFeatureKey : Nat
+  maxFeatureValue : Nat
+  deriving DecidableEq, Repr
+
+/-- Exact rejection reason. Decoration is transactional: errors return no
+partially featured view. -/
+inductive Error where
+  | providerLimit
+  | duplicateProvider (key : ProviderKey)
+  | providerCheckLimit
+  | providerFeatureLimit (provider : ProviderKey) (offer : OfferId)
+  | offerFeatureLimit (offer : OfferId)
+  | totalFeatureLimit
+  | featureKeyLimit (provider : ProviderKey) (key : Nat)
+  | featureValueLimit (provider : ProviderKey) (key : Nat) (value : Int)
+  | duplicateFeature (provider : ProviderKey) (key : Nat) (offer : OfferId)
+  deriving DecidableEq, Repr
+
+/-- Immutable provider order established by successful registry assembly. -/
+structure Registry (Fact : Type) where
+  private mk ::
+  providers : Array (Provider Fact)
+
+private def makeRegistry (providers : Array (Provider Fact)) : Registry Fact :=
+  { providers }
+
+namespace Registry
+
+private def duplicateProvider? (providers : List (Provider Fact)) : Option ProviderKey :=
+  match providers with
+  | [] => none
+  | provider :: rest =>
+      if rest.any (fun other => other.key == provider.key) then
+        some provider.key
+      else
+        duplicateProvider? rest
+
+/-- Assemble providers in caller order after bounding and checking identities. -/
+opaque buildWithin (limits : Limits) (providers : Array (Provider Fact)) :
+    Except Error (Registry Fact) :=
+  if limits.maxProviders < providers.size then
+    .error .providerLimit
+  else
+    match duplicateProvider? providers.toList with
+    | some key => .error (.duplicateProvider key)
+    | none => .ok (makeRegistry providers)
+
+end Registry
+
+/-- One engine offer decorated with package data.  `base` is returned unchanged
+when a policy selects this item. -/
+structure FeaturedOffer where
+  base : OfferView
+  features : Array Feature
+
+/-- Deterministic callback/output counts reported by one successful decoration. -/
+structure Metrics where
+  providerChecks : Nat
+  emittedFeatures : Nat
+  deriving DecidableEq, Repr
+
+/-- A policy view plus aligned featured offers.  The base view remains the
+freshness authority. -/
+structure View (Fact : Type) where
+  base : Policy.View Fact
+  offers : Array FeaturedOffer
+  metrics : Metrics
+
+private def request (view : Policy.View Fact) (offer : OfferView) : Request Fact :=
+  { scope := view.scope
+    serial := view.serial
+    programVersion := view.programVersion
+    facts := view.facts
+    remaining := view.remaining
+    incomplete := view.incomplete
+    offer }
+
+private def validValue (limit : Nat) (value : Int) : Bool :=
+  value.natAbs <= limit
+
+/-- Attach package features in stable offer-major, provider-major, local order.
+
+The complete provider/offer cross product is preflight-counted before any
+callback is entered.  Returned arrays are then checked incrementally against
+per-provider, per-offer, whole-view, key, and value limits. -/
+opaque decorate (limits : Limits) (registry : Registry Fact)
+    (view : Policy.View Fact) : Except Error (View Fact) := do
+  if limits.maxProviders < registry.providers.size then throw .providerLimit
+  let checks := registry.providers.size * view.offers.size
+  if limits.maxProviderChecks < checks then throw .providerCheckLimit
+  let mut decorated := #[]
+  let mut total := 0
+  for offer in view.offers do
+    let mut features := #[]
+    for provider in registry.providers do
+      let emitted := provider.features (request view offer)
+      if limits.maxFeaturesPerProvider < emitted.size then
+        throw (.providerFeatureLimit provider.key offer.id)
+      for feature in emitted do
+        if limits.maxFeatureKey < feature.key then
+          throw (.featureKeyLimit provider.key feature.key)
+        if !validValue limits.maxFeatureValue feature.value then
+          throw (.featureValueLimit provider.key feature.key feature.value)
+        if features.any (fun old =>
+            old.provider == provider.key && old.key == feature.key) then
+          throw (.duplicateFeature provider.key feature.key offer.id)
+        if limits.maxFeaturesPerOffer <= features.size then
+          throw (.offerFeatureLimit offer.id)
+        if limits.maxTotalFeatures <= total then
+          throw .totalFeatureLimit
+        features := features.push
+          { provider := provider.key, key := feature.key, value := feature.value }
+        total := total + 1
+    decorated := decorated.push { base := offer, features }
+  pure
+    { base := view
+      offers := decorated
+      metrics := { providerChecks := checks, emittedFeatures := total } }
+
+/-- Exact lookup used by policies which understand a configured feature key.
+Unknown features remain inert. -/
+def FeaturedOffer.feature? (offer : FeaturedOffer)
+    (provider : ProviderKey) (key : Nat) : Option Int :=
+  (offer.features.find? fun feature =>
+    feature.provider == provider && feature.key == key).map (fun feature => feature.value)
+
+end Hex.Interval.Experiment.PolicyFeature
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 346bf7397..e87c942b5 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -2958,8 +2958,10 @@ inductive OfferKey
       (reason : SplitReason)
 
 structure PolicyFeature where
-  key   : Nat
-  value : Int
+  providerFamily  : Nat
+  providerVersion : Nat
+  key             : Nat
+  value           : Int
 
 structure ObservationSummary where
   outcome      : Nat
@@ -3410,6 +3412,40 @@ distance, mathematical function, or package key. It tests the upgradeable
 feedback seam before domain-specific potential features are admitted through an
 equally bounded interface.
 
+The first executable package-feature experiment supplies that interface
+without adding fact or function cases to the scheduler. Independently
+registered companion providers have a numeric family and compatibility
+version. A stateless provider receives one exact immutable policy snapshot and
+one engine-owned offer, and returns provider-local signed integer features; an
+empty result means that provider contributes nothing for the offer. The
+decorator attaches the provider identity to every local key. Package order,
+offer order, and local
+feature order determine one stable output order, while duplicate provider
+identities and duplicate local keys are rejected.
+
+The complete provider/offer cross product is preflight-counted before callbacks
+run.
+Independent limits bound provider count, provider checks, features from one
+provider for one offer, features attached to one offer, total features, local
+keys, and absolute feature values. Decoration is transactional: an oversized
+or duplicate result yields no partially featured view. The resulting object
+retains each complete original `OfferView`; a policy can only return that base
+offer through the existing selection path. Thus an inaccurate or stale feature
+can change scheduling and therefore which trace is generated, but it cannot
+authorize a transition, enter proof evidence, bypass replay, or weaken replay
+validation.
+
+This is deliberately a companion registry rather than a field added to every
+runtime package. It lets experiments compare interval-width, goal-distance,
+and split-potential vocabularies before fixing their keys or formulas. A
+production consolidation should assemble the feature companions alongside the
+runtime packages and expose the program structure needed for dependency-slice
+features. The callback is pure and accepted decorated output is bounded, but
+the current experiment cannot preempt excessive computation or candidate-array
+allocation inside a callback. Production providers therefore need either a
+restricted bounded builder or an auditable
+declared-work protocol in addition to these output bounds.
+
 A live Mathlib-free arbitrary-function canary presents two exponential
 forward contractors and one source split rule in the same frontier. The policy
 selects both fact improvements, then invokes the split probe, then returns its
@@ -3417,7 +3453,8 @@ split plan; it contains no reference to any of those rule keys. This establishes
 the replaceable staging seam. It does not yet claim that fixed stage order is
 the best policy, nor does it implement width- or goal-sensitive scoring.
 
-The prototype computes a goal-directed potential rather than summing raw widths.
+The planned scoring experiment computes a goal-directed potential rather than
+summing raw widths.
 Nodes on the backwards dependency slice from the desired comparison or current
 contradiction receive greater weight. A node's uncertainty records:
 
diff --git a/conformance/HexInterval/PolicyFeatureConformance.lean b/conformance/HexInterval/PolicyFeatureConformance.lean
new file mode 100644
index 000000000..120290251
--- /dev/null
+++ b/conformance/HexInterval/PolicyFeatureConformance.lean
@@ -0,0 +1,279 @@
+/-
+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.PolicyFeature
+
+/-!
+# Package policy-feature conformance
+
+Two unrelated providers decorate the same immutable policy view.  One reads a
+fact at an invocation anchor; the other recognizes a split offer.  The generic
+decorator contains neither interpretation.
+-/
+
+namespace Hex.Interval.PolicyFeatureConformance
+
+open Experiment Propagator Propagator.Policy PolicyFeature
+
+private def node (index : Nat) : NodeId := { index }
+
+private def invocation (index : Nat) : InvocationKey :=
+  { scope := { index := 0 }
+    programVersion := 7
+    application := { index }
+    rule := { name := "policy-feature.width", schema := 2 }
+    anchor := node index
+    kind := .forward
+    effort := 0
+    inputs := [] }
+
+private def invokeOffer : OfferView :=
+  { id := .application { index := 0 }
+    key := .invoke (invocation 0)
+    offerClass := .invoke
+    age := 3 }
+
+private def splitOffer : OfferView :=
+  { id := .suggestion { index := 0 }
+    key := .split (invocation 1) { node := node 1, version := 4 }
+      0 .smallLandmark
+    offerClass := .split
+    age := 1 }
+
+private def sameOffer (left right : OfferView) : Bool :=
+  left.id == right.id && left.key == right.key &&
+    left.offerClass == right.offerClass && left.age == right.age
+
+private def sameOffers : List OfferView -> List OfferView -> Bool
+  | [], [] => true
+  | left :: lefts, right :: rights =>
+      sameOffer left right && sameOffers lefts rights
+  | _, _ => false
+
+private def baseView : Policy.View Nat :=
+  { scope := { index := 0 }
+    serial := 9
+    programVersion := 7
+    offers := #[invokeOffer, splitOffer]
+    facts := { facts := #[6, 11], versions := #[2, 4], contradictory := false }
+    remaining :=
+      { actions := 8
+        matcherVisits := 8
+        acceptedFacts := 8
+        nodes := 8
+        applications := 8
+        equalities := 8
+        retainedSuggestions := 8
+        instances := 8
+        queueEntries := 8
+        generation := 8 }
+    incomplete := false }
+
+private def sameView (left right : Policy.View Nat) : Bool :=
+  left.scope == right.scope && left.serial == right.serial &&
+    left.programVersion == right.programVersion &&
+    sameOffers left.offers.toList right.offers.toList &&
+    left.facts.facts == right.facts.facts &&
+    left.facts.versions == right.facts.versions &&
+    left.facts.contradictory == right.facts.contradictory &&
+    left.remaining == right.remaining && left.incomplete == right.incomplete
+
+private def widthKey : ProviderKey := { family := 41, version := 2 }
+private def goalKey : ProviderKey := { family := 73, version := 1 }
+
+/-- A domain package can expose a bounded width surrogate without teaching
+the scheduler what a `Nat` fact means. -/
+private def widthProvider : Provider Nat :=
+  { key := widthKey
+    features := fun request =>
+      match request.offer.key with
+      | .invoke invocation =>
+          match request.facts.fact? invocation.anchor with
+          | some width => #[{ key := 0, value := Int.ofNat width }]
+          | none => #[]
+      | _ => #[] }
+
+/-- A frontend-owned goal provider can independently recognize a useful split
+and publish signed closing potential. -/
+private def goalProvider : Provider Nat :=
+  { key := goalKey
+    features := fun request =>
+      match request.offer.key with
+      | .invoke invocation =>
+          if invocation.anchor == node 0 then #[{ key := 1, value := -2 }] else #[]
+      | .split _ target point reason =>
+          if target.node == node 1 && point == 0 && reason == .smallLandmark then
+            #[{ key := 3, value := -4 }, { key := 5, value := 9 }]
+          else
+            #[]
+      | _ => #[] }
+
+private def limits : PolicyFeature.Limits :=
+  { maxProviders := 4
+    maxProviderChecks := 8
+    maxFeaturesPerProvider := 3
+    maxFeaturesPerOffer := 4
+    maxTotalFeatures := 6
+    maxFeatureKey := 10
+    maxFeatureValue := 10 }
+
+private def featured? : Option (PolicyFeature.View Nat) := do
+  let registry <- (Registry.buildWithin limits #[widthProvider, goalProvider]).toOption
+  (decorate limits registry baseView).toOption
+
+/- Stable order is offer-major, provider-major, and then provider-local.  Empty
+responses still consume one provider check. -/
+#guard
+  featured?.any fun view =>
+    sameView view.base baseView &&
+      view.metrics == { providerChecks := 4, emittedFeatures := 4 } &&
+      view.offers.size == 2 &&
+      match view.offers[0]?, view.offers[1]? with
+      | some first, some second =>
+          sameOffer first.base invokeOffer && first.features.size == 2 &&
+            first.feature? widthKey 0 == some 6 &&
+            first.features[0]?.any (fun feature => feature.provider == widthKey) &&
+            first.features[1]?.any (fun feature =>
+              feature.provider == goalKey && feature.key == 1 && feature.value == -2) &&
+            sameOffer second.base splitOffer && second.features.size == 2 &&
+            second.features[0]?.any (fun feature =>
+              feature.provider == goalKey && feature.key == 3 && feature.value == -4) &&
+            second.features[1]?.any (fun feature =>
+              feature.provider == goalKey && feature.key == 5 && feature.value == 9)
+      | _, _ => false
+
+private def duplicateRegistry : Except Error (Registry Nat) :=
+  Registry.buildWithin limits #[widthProvider, { widthProvider with features := fun _ => #[] }]
+
+#guard
+  match duplicateRegistry with
+  | .error (.duplicateProvider key) => key == widthKey
+  | _ => false
+
+/- Provider count is bounded when the immutable registry is assembled. -/
+#guard
+  match Registry.buildWithin { limits with maxProviders := 1 }
+      #[widthProvider, goalProvider] with
+  | .error .providerLimit => true
+  | _ => false
+
+private def duplicateOutput : Provider Nat :=
+  { key := { family := 99, version := 1 }
+    features := fun _ => #[{ key := 1, value := 2 }, { key := 1, value := 3 }] }
+
+#guard
+  match Registry.buildWithin limits #[duplicateOutput] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate limits registry baseView with
+      | .error (.duplicateFeature provider key offer) =>
+          provider == duplicateOutput.key && key == 1 && offer == invokeOffer.id
+      | _ => false
+
+private def oversizedValue : Provider Nat :=
+  { key := { family := 100, version := 1 }
+    features := fun _ => #[{ key := 2, value := -11 }] }
+
+#guard
+  match Registry.buildWithin limits #[oversizedValue] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate limits registry baseView with
+      | .error (.featureValueLimit provider key value) =>
+          provider == oversizedValue.key && key == 2 && value == -11
+      | _ => false
+
+private def oversizedKey : Provider Nat :=
+  { key := { family := 100, version := 2 }
+    features := fun _ => #[{ key := 11, value := 0 }] }
+
+#guard
+  match Registry.buildWithin limits #[oversizedKey] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate limits registry baseView with
+      | .error (.featureKeyLimit provider key) =>
+          provider == oversizedKey.key && key == 11
+      | _ => false
+
+private def tooMany : Provider Nat :=
+  { key := { family := 101, version := 1 }
+    features := fun _ =>
+      #[{ key := 0, value := 0 }, { key := 1, value := 0 },
+        { key := 2, value := 0 }, { key := 3, value := 0 }] }
+
+#guard
+  match Registry.buildWithin limits #[tooMany] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate limits registry baseView with
+      | .error (.providerFeatureLimit provider offer) =>
+          provider == tooMany.key && offer == invokeOffer.id
+      | _ => false
+
+/- The provider/offer cross product is rejected before any package output is
+accepted into a partial decorated view. -/
+#guard
+  match Registry.buildWithin limits #[widthProvider, goalProvider] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate { limits with maxProviderChecks := 3 } registry baseView with
+      | .error .providerCheckLimit => true
+      | _ => false
+
+/- Per-offer and whole-view caps are independent of the provider-local cap. -/
+#guard
+  match Registry.buildWithin limits #[widthProvider, goalProvider] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate { limits with maxFeaturesPerOffer := 1 } registry baseView with
+      | .error (.offerFeatureLimit offer) => offer == invokeOffer.id
+      | _ => false
+
+#guard
+  match Registry.buildWithin limits #[widthProvider, goalProvider] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate { limits with maxTotalFeatures := 3 } registry baseView with
+      | .error .totalFeatureLimit => true
+      | _ => false
+
+/- Decoration rechecks the provider-count limit rather than trusting the
+limits used by an earlier registry build. -/
+#guard
+  match Registry.buildWithin limits #[widthProvider] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate { limits with maxProviders := 0 } registry baseView with
+      | .error .providerLimit => true
+      | _ => false
+
+/- Zero providers are valid under zero count/check/feature limits and retain
+the complete base offers without manufacturing features. -/
+#guard
+  match Registry.buildWithin { limits with maxProviders := 0 } #[] with
+  | .error _ => false
+  | .ok registry =>
+      match decorate
+          { limits with
+            maxProviders := 0
+            maxProviderChecks := 0
+            maxFeaturesPerProvider := 0
+            maxFeaturesPerOffer := 0
+            maxTotalFeatures := 0 }
+          registry baseView with
+      | .ok view =>
+          sameView view.base baseView &&
+            view.offers.size == baseView.offers.size &&
+            view.metrics == { providerChecks := 0, emittedFeatures := 0 } &&
+            match view.offers[0]?, view.offers[1]? with
+            | some first, some second =>
+                sameOffer first.base invokeOffer && first.features.isEmpty &&
+                  sameOffer second.base splitOffer && second.features.isEmpty
+            | _, _ => false
+      | .error _ => false
+
+end Hex.Interval.PolicyFeatureConformance
diff --git a/lakefile.lean b/lakefile.lean
index ed0405c31..bceb32242 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -309,6 +309,7 @@ lean_lib HexIntervalExperiment where
     `HexInterval.Experiment.TargetRun,
     `HexInterval.Experiment.StagedPolicy,
     `HexInterval.Experiment.AdaptivePolicy,
+    `HexInterval.Experiment.PolicyFeature,
     `HexInterval.Experiment.BranchStart,
     `HexInterval.Experiment.BranchTree,
     `HexInterval.Experiment.BranchProof,
@@ -504,7 +505,8 @@ lean_lib HexConformance where
     ++ #[`HexInterval.MinMaxConformance,
       `HexIntervalMathlib.MinMaxConformance].map Glob.one
 
-    ++ #[`HexIntervalMathlib.ExactBranchConformance].map Glob.one
+    ++ #[`HexInterval.PolicyFeatureConformance,
+      `HexIntervalMathlib.ExactBranchConformance].map Glob.one
 
 -- The expensive complete-family Mathlib proofs are owned only by this
 -- non-default library. They are excluded from both merge-gating
diff --git a/progress/20260811T194022Z.md b/progress/20260811T194022Z.md
new file mode 100644
index 000000000..4ea47eb3e
--- /dev/null
+++ b/progress/20260811T194022Z.md
@@ -0,0 +1,30 @@
+# Accomplished
+
+- Added a Mathlib-free companion registry for stateless, versioned package
+  policy features over exact immutable policy snapshots.
+- Bounded provider count, provider/offer checks, per-provider and per-offer
+  output, total output, keys, and signed values; duplicate and oversized
+  results fail transactionally.
+- Added conformance with independent domain-width and goal/split providers,
+  stable composition order, exact accounting, and duplicate/resource guards.
+- Updated the interval SPEC to separate the implemented feature transport from
+  still-open scoring formulas and production package integration.
+- Built `HexIntervalExperiment` and `HexConformance` successfully.
+
+# Current frontier
+
+Packages can now publish bounded scoring inputs without adding fact or function
+cases to the generic scheduler. No width, goal, or split score formula has been
+chosen yet.
+
+# Next step
+
+Compare small configured scoring consumers over exact interval-width,
+goal-distance, and worst-child split features, then decide whether production
+providers should use a restricted builder or declared-work accounting.
+
+# Blockers
+
+The present output caps cannot preempt excessive computation inside a pure
+provider callback. This is harmless to proof soundness but must be addressed
+before treating the callback envelope as a hard runtime resource bound.
diff --git a/progress/20260815T000558Z.md b/progress/20260815T000558Z.md
new file mode 100644
index 000000000..d2d3f8fb8
--- /dev/null
+++ b/progress/20260815T000558Z.md
@@ -0,0 +1,31 @@
+# Accomplished
+
+- Replayed the bounded package-policy feature onto exact local #9235 head
+  `0f61efcd4bbd50299a50f02e6e10862d9b09f1a6`, preserving the verified-raster,
+  Table 12, and PNT example stack.
+- Audited the provider registry and decorator bounds: provider count, checks,
+  output counts, keys, and signed values are checked transactionally, including
+  when the decorator receives stricter limits than registry construction.
+- Confirmed that decorated offers retain the exact base offer and that the
+  implementation and SPEC honestly leave callback work and scoring formulas
+  outside the present bounded transport layer.
+- Refreshed the narrow proof-only Lake registration exemption to the combined
+  local stack and built the policy feature and its conformance target.
+- Ran repository structural, trust-surface, PNT inventory, freshness, and
+  banned-mechanism checks successfully.
+
+# Current frontier
+
+Package-defined bounded features can be transported in stable order without
+changing the generic scheduler. Choosing and evaluating scoring formulas remains
+future work.
+
+# Next step
+
+After #9235 lands, rebase this local feature onto its exact merge commit,
+recompute the Lake exemption, and then run the final PR review and CI cycle.
+
+# Blockers
+
+None. Disk pressure was handled by removing only clean superseded worktree
+checkouts; their local boundary branches remain available.
diff --git a/progress/20260815T022932Z.md b/progress/20260815T022932Z.md
new file mode 100644
index 000000000..37bd97b48
--- /dev/null
+++ b/progress/20260815T022932Z.md
@@ -0,0 +1,41 @@
+# Accomplished
+
+- Reconciled the #9236 bounded package-policy feature as a separate local fork
+  from exact preserved #9234 candidate
+  `caa81316cb814b93deb5126235b9a3e0f86a884f`, leaving the #9235 verified-raster
+  branch intact.
+- Preserved current PNT, Table 12, centered-function, arithmetic, branch-proof,
+  and adaptive-policy registrations while adding only `PolicyFeature` and its
+  conformance target.
+- Re-audited provider assembly and decoration. Both enforce `maxProviders`;
+  decoration retains the exact base view and complete offers in stable
+  offer-major/provider-major/local order, accounts for every provider/offer
+  check and emitted feature, and rejects duplicate providers, duplicate local
+  keys, oversized keys/values, and every count-bound overrun transactionally.
+- Strengthened conformance to compare the complete base snapshot and every
+  `OfferView` field, and to exercise construction-time provider count, key,
+  per-offer, and total-feature limits in addition to the existing stricter
+  decoration-limit guard.
+- Confirmed that callbacks cannot be preempted while running and that the SPEC
+  says so explicitly; accepted outputs alone are bounded. Policy features are
+  scheduling data only and are absent from engine transitions and proof
+  evidence.
+- Built the focused policy-feature targets and the preserved PNT/interval
+  conformance targets, then passed structural, trust-surface, freshness,
+  inventory, release, Mathlib-free bench, and banned-mechanism checks.
+
+# Current frontier
+
+The local #9236 fork transports bounded, versioned package features while
+retaining exact engine offers. It deliberately defines no scoring formula and
+does not integrate feature values into proof production.
+
+# Next step
+
+After the preceding branch lands, rebase this local candidate onto its exact
+merge commit, refresh the narrow Lake blob exemption, and run the final review
+and CI cycle.
+
+# Blockers
+
+None.
diff --git a/progress/20260815T073509Z.md b/progress/20260815T073509Z.md
new file mode 100644
index 000000000..c8aa28d90
--- /dev/null
+++ b/progress/20260815T073509Z.md
@@ -0,0 +1,19 @@
+# Accomplished
+
+- Recovered the audited PolicyFeature experiment as a separate `#9236` fork from exact prepared `#9234` head `77144c2ca2638330c0742c03022e1d92c0065182`, preserving the independent `#9234` and `#9235` branches.
+- Audited full base-view equality and every `OfferView` field, construction/decorate provider limits, all key/count/value caps, transactional failures, and stable offer-major/provider-major/local ordering.
+- Confirmed the SPEC states the callback non-preemptibility limitation and that PolicyFeature transports bounded scheduling metadata without width/goal scoring or proof authority.
+- Recomputed the exact Lake freshness exemption for blob `319283a50eba7d760cd305280e67ea2593dd8c04`.
+- Passed the focused PolicyFeature build, the full PNT conformance set, static/DAG/phase checks, trust-surface and release-manifest checks, source-pinned PNT inventory checks, unit tests, and factor-sweep freshness.
+
+# Current frontier
+
+`#9236` is a clean local-only PolicyFeature candidate on branch `codex/9236-prepare-current`; its feature and conformance coverage are reconciled with the current public arithmetic and PNT registrations.
+
+# Next step
+
+Retain this branch for the directed landing sequence; rebase and repeat exact-head review/CI only when explicitly requested.
+
+# Blockers
+
+None.
diff --git a/progress/20260815T131448Z.md b/progress/20260815T131448Z.md
new file mode 100644
index 000000000..09f74a19c
--- /dev/null
+++ b/progress/20260815T131448Z.md
@@ -0,0 +1,32 @@
+# Accomplished
+
+- Replayed the bounded `PolicyFeature` experiment as a separate local fork from
+  exact prepared #9234 head
+  `129a756cb1b606987b9480c5c1515b08e442bd31`, leaving the #9235 raster fork
+  separate.
+- Confirmed that successful decoration retains the complete immutable policy
+  view and every complete engine offer in stable offer-major,
+  provider-major, provider-local order.
+- Confirmed construction and decoration provider caps, the preflighted
+  provider/offer check cap, every output/key/value cap, duplicate rejection,
+  exact accounting, and fail-closed transactional errors.
+- Kept the callback limitation explicit: accepted output is bounded, but a
+  callback already in progress is not preemptible. Features remain scheduling
+  metadata and do not enter transitions, scoring, or proof evidence.
+- Refreshed the exact Lake registration exemption, built the 2281-job focused
+  policy/public/PNT target closure, and passed structural, trust, inventory,
+  release, freshness, and banned-mechanism checks.
+
+# Current frontier
+
+The local #9236 fork provides bounded package-owned scheduling features while
+leaving feature interpretation and scoring formulas uncommitted.
+
+# Next step
+
+Retain this fork for the directed landing sequence. Rebase it onto the eventual
+exact predecessor merge before any remote review or CI cycle.
+
+# Blockers
+
+None.
diff --git a/progress/20260816T004836Z.md b/progress/20260816T004836Z.md
new file mode 100644
index 000000000..15b80a28c
--- /dev/null
+++ b/progress/20260816T004836Z.md
@@ -0,0 +1,25 @@
+# Prepare package policy features after adaptive policy
+
+## Accomplished
+
+- Replayed the audited PolicyFeature fork directly onto exact #9234 candidate
+  `4f1b51f2a63c629fd1ef4b646c994c0b7d74b4ca`, excluding raster #9235.
+- Preserved full OfferView alignment, provider/count/key/value caps,
+  transactional ordering and failure, stable provider-local ordering, explicit
+  callback non-preemptibility, and proof- and scoring-independent decoration.
+- Preserved the adaptive, exact-branch, subtraction, staged-policy, complete
+  LogTables, PNT, and public registrations and refreshed the Lake exemption.
+
+## Current frontier
+
+The local branch contains only the PolicyFeature fork above #9234. Raster
+#9235 and FeaturePolicy #9237 and later refs remain unchanged.
+
+## Next step
+
+After #9234 merges, replay this prepared edge onto its literal merge commit and
+publish PR #9236 as a direct-main branch.
+
+## Blockers
+
+None.
diff --git a/progress/20260816T010238Z.md b/progress/20260816T010238Z.md
new file mode 100644
index 000000000..964d8c9d1
--- /dev/null
+++ b/progress/20260816T010238Z.md
@@ -0,0 +1,25 @@
+# Restack package policy features onto merged adaptive policy
+
+## Accomplished
+
+- Replayed the prepared PolicyFeature fork onto literal #9234 merge commit
+  `e82e3091d1e844e1cfe2d2dafa32454dbb345f12`, excluding raster #9235.
+- Preserved the merged adaptive policy, exact-branch proof, subtraction replay,
+  staged policy, complete source-pinned LogTables providers and inventory, PNT
+  examples, and current public interval registrations.
+- Confirmed that the exact combined Lake blob and narrow proof-only runtime
+  exemption remain unchanged by the merge-parent restack.
+
+## Current frontier
+
+PR #9236 is a direct-main PolicyFeature fork. Raster #9235 and FeaturePolicy
+#9237 and later refs remain independent and unchanged.
+
+## Next step
+
+Run focused policy, controller, inventory, trust, freshness, and diff gates;
+then publish the direct-main PR head and monitor automatic CI.
+
+## Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index 651d81571..78f2c3844 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -227,6 +227,12 @@
     "current_blob": "ed0405c31f37e4415031e8f020251d965ab344fb",
     "reason": "Additionally registers the isolated Mathlib-free adaptive interval-policy experiment on top of the retained exact-branch proof, subtraction replay, staged policy, complete LogTables, PNT, and public interval registrations; it does not enter the factorization service target or change its executable dependency graph."
   },
+  {
+    "path": "lakefile.lean",
+    "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
+    "current_blob": "bceb32242497ded4562672aad7e227161bcd5331",
+    "reason": "Additionally registers the isolated Mathlib-free package policy-feature experiment and its conformance module on top of the retained adaptive policy, exact-branch proof, subtraction replay, staged policy, complete LogTables, PNT, and public interval registrations; neither enters the factorization service target or changes its executable dependency graph."
+  },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",