From 40e6519b11e88de919ab9add445040bf9c366edd Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 11 Aug 2026 19:22:15 +0000
Subject: [PATCH 1/8] Add adaptive interval policy; progress 20260811T192156Z

---
 HexInterval/Experiment/AdaptivePolicy.lean    | 155 ++++++++++++++++++
 HexInterval/SPEC/hex-interval.md              |  14 ++
 .../HexInterval/StagedPolicyConformance.lean  | 142 ++++++++++++++++
 lakefile.lean                                 |   1 +
 progress/20260811T192156Z.md                  |  29 ++++
 5 files changed, 341 insertions(+)
 create mode 100644 HexInterval/Experiment/AdaptivePolicy.lean
 create mode 100644 progress/20260811T192156Z.md

diff --git a/HexInterval/Experiment/AdaptivePolicy.lean b/HexInterval/Experiment/AdaptivePolicy.lean
new file mode 100644
index 000000000..51348ab65
--- /dev/null
+++ b/HexInterval/Experiment/AdaptivePolicy.lean
@@ -0,0 +1,155 @@
+/-
+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.StagedPolicy
+
+@[expose] public section
+
+/-!
+# A feedback-guided interval-search policy
+
+This policy refines `StagedPolicy` without inspecting facts, operation names,
+or package keys.  It learns only from engine-authenticated observations: actual
+fact-version changes and deterministic logical work.  Untried actions receive
+an optimism bonus, repeated fixed points decay, and a bounded age tier prevents
+continuous eligible work from starving.
+
+The scores choose search order only.  Every selected offer is revalidated by
+`PolicySession`, and proof replay is independent of this module.
+-/
+
+namespace Hex.Interval.Experiment.AdaptivePolicy
+
+open Propagator Propagator.Policy TargetRun
+
+/-- Replaceable integer coefficients for the first feedback experiment. -/
+structure Config where
+  staged : StagedPolicy.Config := {}
+  optimism : Nat := 32
+  gainWeight : Nat := 64
+  noChangePenalty : Nat := 8
+  ageBonusCap : Nat := 16
+  fairnessAge : Nat := 32
+  deriving DecidableEq, Repr
+
+/-- Package-opaque identity at which feedback is accumulated.  Input versions
+remain part of `invocation`, so a newly woken action is sampled afresh. -/
+inductive Key where
+  | invocation (invocation : InvocationKey)
+  | equality (equality : EqualityWorkKey)
+  deriving DecidableEq
+
+/-- Exact, bounded observations accumulated for one selectable transition. -/
+structure Record where
+  key : Key
+  runs : Nat := 0
+  improvements : Nat := 0
+  noChanges : Nat := 0
+  work : Nat := 0
+
+structure State where
+  config : Config
+  records : List Record := []
+
+def State.initial (config : Config := {}) : State := { config }
+
+def work (cost : CostObservation) : Nat :=
+  cost.arithmeticWork + cost.visitedEntries + cost.estimatedProofNodes
+
+def ruleKey (invocation : InvocationKey) : Key := .invocation invocation
+
+def offerKey? : OfferKey -> Option Key
+  | .invoke invocation => some (.invocation invocation)
+  | .equality equality => some (.equality equality)
+  | .retry source effort => some (.invocation { source with effort })
+  | .instantiate _ _ | .split _ _ _ _ => none
+
+def find? (records : List Record) (key : Key) : Option Record :=
+  records.find? fun record => record.key == key
+
+def replace (records : List Record) (record : Record) : List Record :=
+  record :: records.filter fun old => old.key != record.key
+
+def alter (records : List Record) (key : Key) (change : Record -> Record) : List Record :=
+  replace records (change ((find? records key).getD { key }))
+
+def recordRule (records : List Record) (observation : RuleObservation Fact) : List Record :=
+  alter records (.invocation observation.invocation) fun record =>
+    { record with
+      runs := record.runs + 1
+      improvements := record.improvements + observation.changes.size
+      noChanges := record.noChanges + if observation.outcome == .noChange then 1 else 0
+      work := record.work + work observation.cost }
+
+def recordEquality (records : List Record)
+    (observation : EqualityObservation Fact) : List Record :=
+  alter records (.equality observation.key) fun record =>
+    { record with
+      runs := record.runs + 1
+      improvements := record.improvements + observation.changes.size
+      noChanges := record.noChanges + if observation.outcome == .noChange then 1 else 0
+      work := record.work + observation.narrowCalls }
+
+def update : State -> Event Fact -> State
+  | state, .rule observation =>
+      { state with records := recordRule state.records observation }
+  | state, .equality observation =>
+      { state with records := recordEquality state.records observation }
+  | state, .instance _ | state, .dismissed | state, .rejected _ |
+      state, .invalidPayload _ | state, .rejectedPayload _ => state
+
+/-- Learned benefit before fairness.  All arithmetic is deterministic `Nat`
+arithmetic; subtraction saturates at zero. -/
+def learnedScore (config : Config) (record : Option Record) (age : Nat) : Nat :=
+  let ageBonus := Nat.min age config.ageBonusCap
+  match record with
+  | none => config.optimism + ageBonus
+  | some record =>
+      let gain := config.gainWeight * record.improvements / (record.work + record.runs + 1)
+      gain + ageBonus - config.noChangePenalty * record.noChanges
+
+structure Ranked where
+  offer : OfferView
+  fair : Bool
+  stage : Nat
+  score : Nat
+
+def rankOffer (state : State) (offer : OfferView) : Ranked :=
+  let record := (offerKey? offer.key).bind (find? state.records)
+  { offer
+    fair := state.config.fairnessAge <= offer.age
+    stage := StagedPolicy.rank offer
+    score := learnedScore state.config record offer.age }
+
+/-- Fair offers form the first tier.  Within one tier the staged semantic class
+still wins, then learned score, age, and finally stable input order. -/
+def better (candidate current : Ranked) : Bool :=
+  (candidate.fair && !current.fair) ||
+    (candidate.fair == current.fair && candidate.stage < current.stage) ||
+    (candidate.fair == current.fair && candidate.stage == current.stage &&
+      (current.score < candidate.score ||
+        (current.score == candidate.score && current.offer.age < candidate.offer.age)))
+
+def choose? (state : State) (offers : Array OfferView) : Option OfferView :=
+  (offers.foldl (fun best offer =>
+    if !StagedPolicy.allowed state.config.staged offer then best
+    else
+      let candidate := rankOffer state offer
+      match best with
+      | none => some candidate
+      | some current => if better candidate current then some candidate else best) none).map
+    (fun ranked => ranked.offer)
+
+def controller : TargetRun.Controller Fact State where
+  update := update
+  choose := fun state view =>
+    match choose? state view.offers with
+    | some offer => .select offer state
+    | none => .stop state
+
+end Hex.Interval.Experiment.AdaptivePolicy
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 30ea42ebe..0ca1714d5 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -3379,6 +3379,20 @@ changes, no-change and inapplicable outcomes,
 extensions, failures, dismissals, and rejected selections. These counters are
 diagnostic inputs for later scoring, not evidence.
 
+The first feedback-guided variant keeps the same function- and
+representation-independent stages but records observations per complete
+engine invocation or equality key. Its bounded integer score rewards actual
+installed fact-version changes relative to deterministic arithmetic, traversal,
+proof-node, or equality-narrowing work. Untried work receives an optimism bonus,
+and repeated `noChange` observations subtract a configurable penalty. Because
+the complete input versions remain part of an invocation key, newly woken work
+is sampled afresh instead of inheriting a stale fixed-point result. An explicit
+age tier eventually selects continuously eligible work independently of its
+learned score; stable offer order remains the last tie-break. This policy still
+does not interpret interval width, target distance, mathematical function, or
+package key. It tests the upgradeable feedback seam before domain-specific
+potential features are admitted through an equally bounded interface.
+
 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
diff --git a/conformance/HexInterval/StagedPolicyConformance.lean b/conformance/HexInterval/StagedPolicyConformance.lean
index ead102a83..8e3f0fc42 100644
--- a/conformance/HexInterval/StagedPolicyConformance.lean
+++ b/conformance/HexInterval/StagedPolicyConformance.lean
@@ -7,6 +7,7 @@ Authors: Kim Morrison
 import HexInterval.Experiment.StagedPolicy
 import HexInterval.Experiment.ExpSign
 import HexInterval.Experiment.SemanticReplay
+import HexInterval.Experiment.AdaptivePolicy
 
 /-!
 # Staged policy conformance
@@ -145,4 +146,145 @@ private def splitOffer : Policy.OfferView :=
   (StagedPolicy.choose? { allowSplits := false }
       #[splitProbe, splitOffer]).isNone
 
+/-! ## Feedback-guided policy -/
+
+namespace Adaptive
+
+open AdaptivePolicy
+
+private def invocation (index effort : Nat) (kind : ActionKind := .forward) :
+    Policy.InvocationKey :=
+  { scope := { index := 0 }
+    programVersion := 0
+    application := { index }
+    rule := { name := "adaptive-policy.synthetic" }
+    anchor := node index
+    kind
+    effort
+    inputs := [] }
+
+private def offer (index age : Nat) (key : Policy.OfferKey) : Policy.OfferView :=
+  { id := .application { index }, key, offerClass := key.offerClass, age }
+
+private def change (index : Nat) : Policy.FactDelta Nat :=
+  { node := node index
+    before := 0
+    after := 1
+    beforeVersion := 0
+    afterVersion := 1 }
+
+private def observation (key : Policy.InvocationKey)
+    (outcome : Policy.OutcomeTag) (changes : Array (Policy.FactDelta Nat))
+    (cost : CostObservation := {}) : Policy.RuleObservation Nat :=
+  { invocation := key
+    outcome
+    changes
+    contradiction := false
+    cost
+    suggestionPlan := {}
+    emittedSuggestions := #[] }
+
+private def config : AdaptivePolicy.Config :=
+  { optimism := 16
+    gainWeight := 96
+    noChangePenalty := 12
+    ageBonusCap := 4
+    fairnessAge := 20 }
+
+private def productiveKey := invocation 0 0
+private def quietKey := invocation 1 0
+private def freshKey := invocation 2 0
+
+private def learned : AdaptivePolicy.State :=
+  let initial := AdaptivePolicy.State.initial config
+  let afterProductive := AdaptivePolicy.update initial <|
+    .rule (observation productiveKey .success #[change 0]
+      { arithmeticWork := 1 })
+  AdaptivePolicy.update afterProductive <|
+    .rule (observation quietKey .noChange #[] { arithmeticWork := 1 })
+
+private def productiveOffer := offer 0 1 (.invoke productiveKey)
+private def quietOffer := offer 1 4 (.invoke quietKey)
+private def freshOffer := offer 2 0 (.invoke freshKey)
+
+/- Actual gain beats a somewhat older fixed-point action. -/
+#guard
+  (AdaptivePolicy.choose? learned #[quietOffer, productiveOffer]).map
+      (fun selected => selected.key) == some productiveOffer.key
+
+/- An untried action receives optimism rather than inheriting a sibling's
+fixed-point history. -/
+#guard
+  (AdaptivePolicy.choose? learned #[quietOffer, freshOffer]).map
+      (fun selected => selected.key) == some freshOffer.key
+
+/- Fairness is a separate tier and eventually samples an old eligible action
+even when its learned score is poor. -/
+private def fairQuiet := { quietOffer with age := 20 }
+
+#guard
+  (AdaptivePolicy.choose? learned #[productiveOffer, fairQuiet]).map
+      (fun selected => selected.key) == some fairQuiet.key
+
+/- Learning never lets a speculative split leapfrog unsaturated cheap
+propagation merely because it is untried. -/
+private def splitOffer : Policy.OfferView :=
+  offer 3 0 (.split (invocation 3 0 .split)
+    { node := node 0, version := 0 } 0 .midpoint)
+
+#guard
+  (AdaptivePolicy.choose? learned #[splitOffer, quietOffer]).map
+      (fun selected => selected.key) == some quietOffer.key
+
+/- Equality contractions use the same authenticated feedback channel. -/
+private def equalityKey : Policy.EqualityWorkKey :=
+  { scope := { index := 0 }
+    programVersion := 0
+    equality := { index := 0 }
+    left := { node := node 0, version := 0 }
+    right := { node := node 1, version := 0 } }
+
+private def equalityLearned : AdaptivePolicy.State :=
+  AdaptivePolicy.update (AdaptivePolicy.State.initial config) <|
+    .equality
+      { key := equalityKey
+        outcome := .improved
+        changes := #[change 0]
+        narrowCalls := 2 }
+
+private def equalityOffer : Policy.OfferView :=
+  { id := .equality { index := 0 }
+    key := .equality equalityKey
+    offerClass := .equality
+    age := 0 }
+
+#guard
+  (AdaptivePolicy.choose? equalityLearned #[freshOffer, equalityOffer]).map
+      (fun selected => selected.key) == some equalityOffer.key
+
+private def live? : Option (TargetRun.Result Bound AdaptivePolicy.State) := do
+  let session <- session?
+  pure <| TargetRun.drive factDomain input.target.node input.target.fact
+    AdaptivePolicy.controller 16 session (AdaptivePolicy.State.initial config)
+
+private def totalRuns (state : AdaptivePolicy.State) : Nat :=
+  state.records.foldl (fun total record => total + record.runs) 0
+
+private def totalImprovements (state : AdaptivePolicy.State) : Nat :=
+  state.records.foldl (fun total record => total + record.improvements) 0
+
+/- The live arbitrary-function graph supplies three independent observations;
+the generic feedback table records two actual fact improvements. -/
+#guard
+  live?.any fun result =>
+    result.events.size == 3 && result.session.state.engine.history.size == 2 &&
+      result.policyState.records.length == 3 &&
+      totalRuns result.policyState == 3 &&
+      totalImprovements result.policyState == 2 &&
+      match result.stop with
+      | .split plan => plan.node == node 0 && plan.reason == .smallLandmark
+      | _ => false
+
+end Adaptive
+
 end Hex.Interval.StagedPolicyConformance
diff --git a/lakefile.lean b/lakefile.lean
index 8e8fa300e..ed0405c31 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -308,6 +308,7 @@ lean_lib HexIntervalExperiment where
     `HexInterval.Experiment.PolicySession,
     `HexInterval.Experiment.TargetRun,
     `HexInterval.Experiment.StagedPolicy,
+    `HexInterval.Experiment.AdaptivePolicy,
     `HexInterval.Experiment.BranchStart,
     `HexInterval.Experiment.BranchTree,
     `HexInterval.Experiment.BranchProof,
diff --git a/progress/20260811T192156Z.md b/progress/20260811T192156Z.md
new file mode 100644
index 000000000..a2eeff99c
--- /dev/null
+++ b/progress/20260811T192156Z.md
@@ -0,0 +1,29 @@
+# Accomplished
+
+- Added a function- and fact-representation-independent adaptive policy on top
+  of the staged controller.
+- Recorded engine-authenticated fact improvements, fixed points, and bounded
+  logical work per complete invocation or equality key.
+- Added deterministic optimism, no-change decay, age bonuses, and a separate
+  fairness tier without making any policy result part of proof evidence.
+- Exercised productive, fixed-point, untried, fair, split-stage, equality, and
+  live arbitrary-function cases in conformance.
+- Updated the SPEC and passed focused builds plus copyright, line-count,
+  dependency, trust-surface, phase-four, factor-freshness, diff, and banned-
+  construct checks.
+
+# Current frontier
+
+The policy can learn when opaque actions have paid off, but its gain signal is
+still the number of installed fact versions. It does not yet receive bounded
+domain-specific width, goal-distance, or virtual-split features.
+
+# Next step
+
+Compare this policy with the staged baseline on the subtraction and useful
+branch-dependent canaries, then design a package-contributed bounded feature
+interface for width and worst-child split estimates.
+
+# Blockers
+
+None.

From 4ebd90701cca010ec18ee91008e66c4cc2b97543 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 11 Aug 2026 19:31:32 +0000
Subject: [PATCH 2/8] Restack adaptive interval policy; progress
 20260811T193116Z

---
 progress/20260811T193116Z.md                  | 20 +++++++++++++++++++
 .../bench/proof_only_runtime_exemptions.json  |  6 ++++++
 2 files changed, 26 insertions(+)
 create mode 100644 progress/20260811T193116Z.md

diff --git a/progress/20260811T193116Z.md b/progress/20260811T193116Z.md
new file mode 100644
index 000000000..9febc183f
--- /dev/null
+++ b/progress/20260811T193116Z.md
@@ -0,0 +1,20 @@
+# Accomplished
+
+- Restacked the adaptive policy on the exact-subtraction and useful
+  contraction-to-split proof canaries without changing its policy behavior.
+- Added the exact proof-only Lake blob exemption for the isolated adaptive
+  module and revalidated focused builds and factor-data freshness.
+
+# Current frontier
+
+The adaptive policy is ready to become the next stacked experiment after the
+arithmetic and branch-dependent canaries.
+
+# Next step
+
+Finish the independent policy review, open the stacked PR, and compare its
+choices with the staged baseline on the new live examples.
+
+# Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index f80dd261a..b55a1626f 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -221,6 +221,12 @@
     "current_blob": "8e8fa300e9bc27e82b168e7f4cc3e24989994339",
     "reason": "Additionally registers the proof-only exact contraction-to-split conformance module on top of the retained 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": "3c125625e17c9d609d8d10f6484e78615dd103dd",
+    "reason": "Additionally registers the isolated Mathlib-free adaptive interval-policy experiment; the factorization service target and executable dependency graph are unchanged."
+  },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",

From 2990b2df3293d33d14d0947631f19a156284c2e3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 11 Aug 2026 19:45:25 +0000
Subject: [PATCH 3/8] fix(interval): make adaptive feedback reachable

---
 HexInterval/Experiment/AdaptivePolicy.lean    | 94 +++++++++++++------
 HexInterval/SPEC/hex-interval.md              | 39 +++++---
 .../HexInterval/StagedPolicyConformance.lean  | 73 ++++++++++++++
 progress/20260811T194503Z.md                  | 26 +++++
 4 files changed, 192 insertions(+), 40 deletions(-)
 create mode 100644 progress/20260811T194503Z.md

diff --git a/HexInterval/Experiment/AdaptivePolicy.lean b/HexInterval/Experiment/AdaptivePolicy.lean
index 51348ab65..263519b3c 100644
--- a/HexInterval/Experiment/AdaptivePolicy.lean
+++ b/HexInterval/Experiment/AdaptivePolicy.lean
@@ -15,9 +15,9 @@ public import HexInterval.Experiment.StagedPolicy
 
 This policy refines `StagedPolicy` without inspecting facts, operation names,
 or package keys.  It learns only from engine-authenticated observations: actual
-fact-version changes and deterministic logical work.  Untried actions receive
-an optimism bonus, repeated fixed points decay, and a bounded age tier prevents
-continuous eligible work from starving.
+fact-version changes and deterministic logical work.  Stable application sites
+retain useful history across changed input versions, while the exact invocation
+snapshot prevents an old fixed point from suppressing newly woken work.
 
 The scores choose search order only.  Every selected offer is revalidated by
 `PolicySession`, and proof replay is independent of this module.
@@ -30,16 +30,24 @@ open Propagator Propagator.Policy TargetRun
 /-- Replaceable integer coefficients for the first feedback experiment. -/
 structure Config where
   staged : StagedPolicy.Config := {}
-  optimism : Nat := 32
-  gainWeight : Nat := 64
-  noChangePenalty : Nat := 8
-  ageBonusCap : Nat := 16
-  fairnessAge : Nat := 32
+  optimism : Nat := 16
+  gainWeight : Nat := 96
+  noChangePenalty : Nat := 12
+  ageBonusCap : Nat := 4
+  fairnessAge : Nat := 20
+  maxRecords : Nat := 256
   deriving DecidableEq, Repr
 
-/-- Package-opaque identity at which feedback is accumulated.  Input versions
-remain part of `invocation`, so a newly woken action is sampled afresh. -/
+/-- Stable, package-opaque identity at which feedback is accumulated.  The
+changing invocation snapshot is stored separately in `Record.last`. -/
 inductive Key where
+  | invocation (scope : ScopeId) (application : ApplicationId) (rule : RuleKey)
+      (anchor : NodeId) (kind : ActionKind) (effort generation : Nat)
+  | equality (scope : ScopeId) (equality : EqualityId)
+  deriving DecidableEq
+
+/-- The exact engine snapshot on which an observation was made. -/
+inductive Snapshot where
   | invocation (invocation : InvocationKey)
   | equality (equality : EqualityWorkKey)
   deriving DecidableEq
@@ -50,7 +58,11 @@ structure Record where
   runs : Nat := 0
   improvements : Nat := 0
   noChanges : Nat := 0
+  /-- Consecutive fixed points on the exact last snapshot.  This resets when
+  input versions change, so stale fixed points do not demote new work. -/
+  stagnant : Nat := 0
   work : Nat := 0
+  last : Option Snapshot := none
 
 structure State where
   config : Config
@@ -61,9 +73,20 @@ def State.initial (config : Config := {}) : State := { config }
 def work (cost : CostObservation) : Nat :=
   cost.arithmeticWork + cost.visitedEntries + cost.estimatedProofNodes
 
-def ruleKey (invocation : InvocationKey) : Key := .invocation invocation
+def ruleKey (invocation : InvocationKey) : Key :=
+  .invocation invocation.scope invocation.application invocation.rule invocation.anchor
+    invocation.kind invocation.effort invocation.generation
+
+def equalityKey (equality : EqualityWorkKey) : Key :=
+  .equality equality.scope equality.equality
 
 def offerKey? : OfferKey -> Option Key
+  | .invoke invocation => some (ruleKey invocation)
+  | .equality equality => some (equalityKey equality)
+  | .retry source effort => some (ruleKey { source with effort })
+  | .instantiate _ _ | .split _ _ _ _ => none
+
+def offerSnapshot? : OfferKey -> Option Snapshot
   | .invoke invocation => some (.invocation invocation)
   | .equality equality => some (.equality equality)
   | .retry source effort => some (.invocation { source with effort })
@@ -72,46 +95,58 @@ def offerKey? : OfferKey -> Option Key
 def find? (records : List Record) (key : Key) : Option Record :=
   records.find? fun record => record.key == key
 
-def replace (records : List Record) (record : Record) : List Record :=
-  record :: records.filter fun old => old.key != record.key
+def replace (limit : Nat) (records : List Record) (record : Record) : List Record :=
+  (record :: records.filter fun old => old.key != record.key).take limit
 
-def alter (records : List Record) (key : Key) (change : Record -> Record) : List Record :=
-  replace records (change ((find? records key).getD { key }))
+def alter (limit : Nat) (records : List Record) (key : Key)
+    (change : Record -> Record) : List Record :=
+  replace limit records (change ((find? records key).getD { key }))
 
-def recordRule (records : List Record) (observation : RuleObservation Fact) : List Record :=
-  alter records (.invocation observation.invocation) fun record =>
+def recordRule (limit : Nat) (records : List Record)
+    (observation : RuleObservation Fact) : List Record :=
+  let snapshot := Snapshot.invocation observation.invocation
+  alter limit records (ruleKey observation.invocation) fun record =>
     { record with
       runs := record.runs + 1
       improvements := record.improvements + observation.changes.size
       noChanges := record.noChanges + if observation.outcome == .noChange then 1 else 0
-      work := record.work + work observation.cost }
+      stagnant := if observation.outcome != .noChange then 0
+        else if record.last == some snapshot then record.stagnant + 1 else 1
+      work := record.work + work observation.cost
+      last := some snapshot }
 
-def recordEquality (records : List Record)
+def recordEquality (limit : Nat) (records : List Record)
     (observation : EqualityObservation Fact) : List Record :=
-  alter records (.equality observation.key) fun record =>
+  let snapshot := Snapshot.equality observation.key
+  alter limit records (equalityKey observation.key) fun record =>
     { record with
       runs := record.runs + 1
       improvements := record.improvements + observation.changes.size
       noChanges := record.noChanges + if observation.outcome == .noChange then 1 else 0
-      work := record.work + observation.narrowCalls }
+      stagnant := if observation.outcome != .noChange then 0
+        else if record.last == some snapshot then record.stagnant + 1 else 1
+      work := record.work + observation.narrowCalls
+      last := some snapshot }
 
 def update : State -> Event Fact -> State
   | state, .rule observation =>
-      { state with records := recordRule state.records observation }
+      { state with records := recordRule state.config.maxRecords state.records observation }
   | state, .equality observation =>
-      { state with records := recordEquality state.records observation }
+      { state with records := recordEquality state.config.maxRecords state.records observation }
   | state, .instance _ | state, .dismissed | state, .rejected _ |
       state, .invalidPayload _ | state, .rejectedPayload _ => state
 
 /-- Learned benefit before fairness.  All arithmetic is deterministic `Nat`
 arithmetic; subtraction saturates at zero. -/
-def learnedScore (config : Config) (record : Option Record) (age : Nat) : Nat :=
+def learnedScore (config : Config) (record : Option Record)
+    (snapshot : Option Snapshot) (age : Nat) : Nat :=
   let ageBonus := Nat.min age config.ageBonusCap
   match record with
   | none => config.optimism + ageBonus
   | some record =>
       let gain := config.gainWeight * record.improvements / (record.work + record.runs + 1)
-      gain + ageBonus - config.noChangePenalty * record.noChanges
+      if record.last != snapshot then Nat.max config.optimism gain + ageBonus
+      else gain + ageBonus - config.noChangePenalty * record.stagnant
 
 structure Ranked where
   offer : OfferView
@@ -121,13 +156,16 @@ structure Ranked where
 
 def rankOffer (state : State) (offer : OfferView) : Ranked :=
   let record := (offerKey? offer.key).bind (find? state.records)
+  let snapshot := offerSnapshot? offer.key
   { offer
     fair := state.config.fairnessAge <= offer.age
     stage := StagedPolicy.rank offer
-    score := learnedScore state.config record offer.age }
+    score := learnedScore state.config record snapshot offer.age }
 
-/-- Fair offers form the first tier.  Within one tier the staged semantic class
-still wins, then learned score, age, and finally stable input order. -/
+/-- Offers at or beyond `fairnessAge` form the first tier.  On a finite frontier,
+selection consumes offers, so this tier ensures every continuously eligible
+offer is eventually sampled.  Within one tier the staged semantic class still
+wins, then learned score, age, and finally stable input order. -/
 def better (candidate current : Ranked) : Bool :=
   (candidate.fair && !current.fair) ||
     (candidate.fair == current.fair && candidate.stage < current.stage) ||
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 0ca1714d5..f05c08f55 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -3380,18 +3380,33 @@ extensions, failures, dismissals, and rejected selections. These counters are
 diagnostic inputs for later scoring, not evidence.
 
 The first feedback-guided variant keeps the same function- and
-representation-independent stages but records observations per complete
-engine invocation or equality key. Its bounded integer score rewards actual
-installed fact-version changes relative to deterministic arithmetic, traversal,
-proof-node, or equality-narrowing work. Untried work receives an optimism bonus,
-and repeated `noChange` observations subtract a configurable penalty. Because
-the complete input versions remain part of an invocation key, newly woken work
-is sampled afresh instead of inheriting a stale fixed-point result. An explicit
-age tier eventually selects continuously eligible work independently of its
-learned score; stable offer order remains the last tie-break. This policy still
-does not interpret interval width, target distance, mathematical function, or
-package key. It tests the upgradeable feedback seam before domain-specific
-potential features are admitted through an equally bounded interface.
+representation-independent stages but accumulates observations at a stable
+engine-owned application or equality site. Its bounded integer score rewards
+actual installed fact-version changes relative to deterministic arithmetic,
+traversal, proof-node, or equality-narrowing work. The record also retains the
+last complete invocation snapshot. A repeated `noChange` on that exact snapshot
+subtracts a configurable penalty, while changed input versions reset that
+consecutive fixed-point penalty and receive at least the untried optimism score.
+Thus useful history survives an ordinary wake-up without letting an obsolete
+fixed point suppress newly eligible work. The shipped coefficients are covered
+by conformance: one unit-cost improvement outranks an untried peer, a repeated
+fixed point falls below it, and a changed-version wake-up reuses the stable gain.
+The fixed-point penalty applies only when an already observed exact invocation
+is offered again without a snapshot change. Ordinary wake-ups change the
+snapshot, so this first policy promotes historically productive sites but does
+not generally demote unproductive sites across successive input versions.
+
+The feedback table has an explicit deterministic record bound and evicts the
+least recently updated stable site when full. Instantiation and split offers
+retain
+their staged rank but do not yet have feedback records; invocation, retry, and
+equality work do. Offers at or beyond the configured fairness age form the first
+tier. On the normative finite frontier, where selection consumes an offer, this
+eventually samples every continuously eligible item; stable offer order remains
+the last tie-break. This policy still does not interpret interval width, target
+distance, mathematical function, or package key. It tests the upgradeable
+feedback seam before domain-specific potential features are admitted through an
+equally bounded interface.
 
 A live Mathlib-free arbitrary-function canary presents two exponential
 forward contractors and one source split rule in the same frontier. The policy
diff --git a/conformance/HexInterval/StagedPolicyConformance.lean b/conformance/HexInterval/StagedPolicyConformance.lean
index 8e3f0fc42..009b21928 100644
--- a/conformance/HexInterval/StagedPolicyConformance.lean
+++ b/conformance/HexInterval/StagedPolicyConformance.lean
@@ -218,6 +218,79 @@ fixed-point history. -/
   (AdaptivePolicy.choose? learned #[quietOffer, freshOffer]).map
       (fun selected => selected.key) == some freshOffer.key
 
+/- The shipped coefficients reward one unit-cost improvement over an untried
+peer.  This guard deliberately constructs `Config := {}` so later fixture
+tuning cannot silently replace coverage of the public defaults. -/
+private def defaultLearned : AdaptivePolicy.State :=
+  AdaptivePolicy.update (AdaptivePolicy.State.initial {}) <|
+    .rule (observation productiveKey .success #[change 0]
+      { arithmeticWork := 1 })
+
+#guard
+  (AdaptivePolicy.choose? defaultLearned #[freshOffer, { productiveOffer with age := 0 }]).map
+      (fun selected => selected.key) == some productiveOffer.key
+
+/- A repeated fixed point on one exact snapshot decays below an untried peer. -/
+private def defaultStagnant : AdaptivePolicy.State :=
+  AdaptivePolicy.update defaultLearned <|
+    .rule (observation productiveKey .noChange #[] { arithmeticWork := 1 })
+
+#guard
+  (AdaptivePolicy.choose? defaultStagnant
+      #[{ productiveOffer with age := 0 }, freshOffer]).map
+      (fun selected => selected.key) == some freshOffer.key
+
+/- A changed input version keeps stable-site gain history but resets the
+exact-snapshot fixed-point penalty. -/
+private def rewokenProductiveKey : Policy.InvocationKey :=
+  { productiveKey with inputs := [{ node := node 0, version := 1 }] }
+
+private def rewokenProductiveOffer : Policy.OfferView :=
+  offer 0 0 (.invoke rewokenProductiveKey)
+
+#guard
+  (AdaptivePolicy.choose? defaultStagnant #[freshOffer, rewokenProductiveOffer]).map
+      (fun selected => selected.key) == some rewokenProductiveOffer.key
+
+/- A changed snapshot with no accumulated gain receives the optimism floor;
+without the `Nat.max` branch this score would be zero. -/
+private def noGain : AdaptivePolicy.State :=
+  AdaptivePolicy.update (AdaptivePolicy.State.initial {}) <|
+    .rule (observation productiveKey .noChange #[] { arithmeticWork := 1 })
+
+#guard
+  (AdaptivePolicy.find? noGain.records
+      (AdaptivePolicy.ruleKey rewokenProductiveKey)).isSome &&
+    (AdaptivePolicy.rankOffer noGain rewokenProductiveOffer).score ==
+      ({} : AdaptivePolicy.Config).optimism
+
+private def accumulated : AdaptivePolicy.State :=
+  AdaptivePolicy.update defaultStagnant <|
+    .rule (observation rewokenProductiveKey .success #[change 0]
+      { arithmeticWork := 1 })
+
+#guard
+  accumulated.records.length == 1 &&
+    (AdaptivePolicy.find? accumulated.records
+      (AdaptivePolicy.ruleKey rewokenProductiveKey)).any fun record =>
+        record.runs == 3 && record.improvements == 2 &&
+          record.noChanges == 1 && record.stagnant == 0
+
+/- The feedback table has an explicit deterministic capacity. -/
+private def bounded : AdaptivePolicy.State :=
+  let state := AdaptivePolicy.State.initial { maxRecords := 2 }
+  let state := AdaptivePolicy.update state <|
+    .rule (observation productiveKey .success #[change 0])
+  let state := AdaptivePolicy.update state <|
+    .rule (observation quietKey .success #[change 1])
+  AdaptivePolicy.update state <|
+    .rule (observation freshKey .success #[change 2])
+
+#guard
+  bounded.records.length == 2 &&
+    (AdaptivePolicy.find? bounded.records
+      (AdaptivePolicy.ruleKey productiveKey)).isNone
+
 /- Fairness is a separate tier and eventually samples an old eligible action
 even when its learned score is poor. -/
 private def fairQuiet := { quietOffer with age := 20 }
diff --git a/progress/20260811T194503Z.md b/progress/20260811T194503Z.md
new file mode 100644
index 000000000..d7e668df8
--- /dev/null
+++ b/progress/20260811T194503Z.md
@@ -0,0 +1,26 @@
+# Adaptive policy feedback repair
+
+## Accomplished
+
+- Separated stable application/equality identities from exact invocation
+  snapshots, so feedback survives changed input versions while stale
+  fixed-point penalties do not.
+- Chose and tested shipped coefficients for productive, fresh, stagnant, and
+  reawakened work.
+- Added a deterministic bound and least-recently-updated eviction to the
+  feedback table.
+- Narrowed the fairness and unsupported-offer claims in the SPEC.
+
+## Current frontier
+
+The adaptive policy now has reachable feedback in ordinary live wake-up paths.
+It remains package-agnostic and affects ordering only.
+
+## Next step
+
+Obtain a fresh exact-head review, then layer bounded package-provided potential
+features over this repaired feedback state.
+
+## Blockers
+
+None.

From 6aba8e9c74509090c3756b4146558404422fbf19 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Fri, 14 Aug 2026 23:56:29 +0000
Subject: [PATCH 4/8] docs(interval): distinguish adaptive work hints

---
 HexInterval/Experiment/AdaptivePolicy.lean    | 13 ++++---
 HexInterval/SPEC/hex-interval.md              | 13 ++++---
 progress/20260814T235554Z.md                  | 34 +++++++++++++++++++
 .../bench/proof_only_runtime_exemptions.json  |  2 +-
 4 files changed, 51 insertions(+), 11 deletions(-)
 create mode 100644 progress/20260814T235554Z.md

diff --git a/HexInterval/Experiment/AdaptivePolicy.lean b/HexInterval/Experiment/AdaptivePolicy.lean
index 263519b3c..43b4b1258 100644
--- a/HexInterval/Experiment/AdaptivePolicy.lean
+++ b/HexInterval/Experiment/AdaptivePolicy.lean
@@ -14,10 +14,11 @@ public import HexInterval.Experiment.StagedPolicy
 # A feedback-guided interval-search policy
 
 This policy refines `StagedPolicy` without inspecting facts, operation names,
-or package keys.  It learns only from engine-authenticated observations: actual
-fact-version changes and deterministic logical work.  Stable application sites
-retain useful history across changed input versions, while the exact invocation
-snapshot prevents an old fixed point from suppressing newly woken work.
+or package keys. It learns from observations attached to engine-authenticated
+events: engine-derived fact-version changes and bounded, package-reported
+logical work. Stable application sites retain useful history across changed
+input versions, while the exact invocation snapshot prevents an old fixed
+point from suppressing newly woken work.
 
 The scores choose search order only.  Every selected offer is revalidated by
 `PolicySession`, and proof replay is independent of this module.
@@ -52,7 +53,7 @@ inductive Snapshot where
   | equality (equality : EqualityWorkKey)
   deriving DecidableEq
 
-/-- Exact, bounded observations accumulated for one selectable transition. -/
+/-- Bounded search observations accumulated for one selectable transition. -/
 structure Record where
   key : Key
   runs : Nat := 0
@@ -70,6 +71,8 @@ structure State where
 
 def State.initial (config : Config := {}) : State := { config }
 
+/-- Package-reported deterministic work is a bounded scheduling hint, never
+proof evidence or an engine-independent measurement. -/
 def work (cost : CostObservation) : Nat :=
   cost.arithmeticWork + cost.visitedEntries + cost.estimatedProofNodes
 
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index f05c08f55..ae660e2a8 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -3382,11 +3382,14 @@ diagnostic inputs for later scoring, not evidence.
 The first feedback-guided variant keeps the same function- and
 representation-independent stages but accumulates observations at a stable
 engine-owned application or equality site. Its bounded integer score rewards
-actual installed fact-version changes relative to deterministic arithmetic,
-traversal, proof-node, or equality-narrowing work. The record also retains the
-last complete invocation snapshot. A repeated `noChange` on that exact snapshot
-subtracts a configurable penalty, while changed input versions reset that
-consecutive fixed-point penalty and receive at least the untried optimism score.
+engine-derived installed fact-version changes relative to bounded,
+package-reported deterministic arithmetic, traversal, proof-node, or
+equality-narrowing work. That reported work is only a search hint and is not
+proof evidence or an independently measured engine cost. The record also
+retains the last complete invocation snapshot. A repeated `noChange` on that
+exact snapshot subtracts a configurable penalty, while changed input versions
+reset that consecutive fixed-point penalty and receive at least the untried
+optimism score.
 Thus useful history survives an ordinary wake-up without letting an obsolete
 fixed point suppress newly eligible work. The shipped coefficients are covered
 by conformance: one unit-cost improvement outranks an untried peer, a repeated
diff --git a/progress/20260814T235554Z.md b/progress/20260814T235554Z.md
new file mode 100644
index 000000000..6063ac8ee
--- /dev/null
+++ b/progress/20260814T235554Z.md
@@ -0,0 +1,34 @@
+# Accomplished
+
+- Replayed the feedback-guided search policy onto exact local #9233 boundary
+  `58051fabf3ec92b433585a469828b0094e6a9df9` while preserving all prior
+  policy, arithmetic, branch-proof, PNT, Table 12, and function-package work.
+- Audited stable site keys, exact invocation snapshots, installed-change
+  feedback, fixed-point decay, wake-up resets, equality feedback, deterministic
+  eviction, staged gates, fairness, and stable-order fallback.
+- Corrected the trust wording: fact deltas are engine-derived, whereas logical
+  work is a bounded package-reported scheduling hint attached to the checked
+  event, never proof evidence or an independently measured engine cost.
+- Confirmed conformance makes shipped productive, fresh, stagnant, reawakened,
+  equality, fairness, capacity, split-stage, and live arbitrary-function cases
+  load-bearing.
+- Refreshed the exact proof-only Lake exemption and passed the focused 2,234-job
+  build plus structural, trust, Phase 4, PNT inventory, factor-freshness, diff,
+  and banned-proof checks.
+
+# Current frontier
+
+The local #9234 candidate supplies bounded feedback within each staged semantic
+class without inspecting fact representations or function names. Search scores
+remain completely outside proof evidence and kernel replay.
+
+# Next step
+
+After #9233 lands, rebase this candidate once onto its final merged lineage,
+refresh the Lake exemption, then push and obtain exact-head review and CI.
+
+# Blockers
+
+None. Accumulated clean preparation checkouts initially exhausted local disk;
+their committed branches were retained while superseded worktrees were removed,
+and the focused rebuild then passed.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index b55a1626f..d58cac621 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -224,7 +224,7 @@
   {
     "path": "lakefile.lean",
     "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
-    "current_blob": "3c125625e17c9d609d8d10f6484e78615dd103dd",
+    "current_blob": "9595b5335e7568bcc2c3e18d4c66c763ed855a44",
     "reason": "Additionally registers the isolated Mathlib-free adaptive interval-policy experiment; the factorization service target and executable dependency graph are unchanged."
   },
   {

From 11910389ee3445454f9069c1e34dbf9e9767a884 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sat, 15 Aug 2026 02:21:00 +0000
Subject: [PATCH 5/8] docs(progress): record local adaptive-policy preparation

---
 progress/20260815T022041Z.md | 46 ++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 progress/20260815T022041Z.md

diff --git a/progress/20260815T022041Z.md b/progress/20260815T022041Z.md
new file mode 100644
index 000000000..aa3e8f2ff
--- /dev/null
+++ b/progress/20260815T022041Z.md
@@ -0,0 +1,46 @@
+# Local #9234 adaptive-policy preparation
+
+## Accomplished
+
+- Replayed the four #9234 adaptive feedback-policy commits onto exact prepared
+  #9233 head `38c00630c5b7d20e14d60380e7070256ad8c2004`.
+- Preserved the current experiment and conformance registrations while adding
+  only `HexInterval.Experiment.AdaptivePolicy`; refreshed the narrow exact-blob
+  proof-only freshness exemption for the combined Lake file.
+- Confirmed the adaptive policy and extended staged-policy conformance sources
+  are byte-for-byte identical to the previously audited repaired #9234 state.
+- Audited feedback accounting. Stable engine-owned application/equality keys
+  accumulate engine-derived fact-version changes and bounded reported work,
+  while the exact invocation snapshot is retained separately. Repeated fixed
+  points decay only on the same snapshot; a changed version ignores that stale
+  penalty and receives the configured optimism floor.
+- Confirmed deterministic record eviction, the explicit `maxRecords` bound,
+  staged feature gates, live equality/rule observations, and finite-frontier
+  fairness canaries. The SPEC accurately treats package cost as a scheduling
+  hint, limits the fairness statement to a consuming finite frontier, and
+  disclaims function-, width-, target-, and package-specific scoring.
+- Verified selected offers still pass `PolicySession` serial, program-version,
+  expected-key, freshness, and resource validation. Scores and records affect
+  order only and do not enter proof replay.
+- Built `HexIntervalExperiment` and the extended staged-policy conformance.
+  Rebuilt exact-branch, subtraction, centered, large-cosine, precision-log, and
+  full PNT conformance targets.
+- Passed file, copyright, DAG, trust-surface, conformance-target, PNT inventory,
+  factor-freshness, release-manifest, manual-split, release-sync, Phase 4, and
+  Mathlib-free bench checks. The explicit banned-mechanism scan is clean.
+
+## Current frontier
+
+- The local #9234 candidate is clean on top of the prepared #9233 boundary.
+  All earlier arithmetic, branch, PNT, log, and cosine sources and registrations
+  remain unchanged.
+
+## Next step
+
+- After the preceding stack edges land, rebase this feature boundary onto its
+  final parent, refresh the exact Lake exemption, then push for exact-head
+  review and CI.
+
+## Blockers
+
+- None. Remote PR and CI state were intentionally left untouched.

From 2afac2df6801cb4511ed64f9512413bd3e310713 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sat, 15 Aug 2026 13:00:24 +0000
Subject: [PATCH 6/8] test(interval): pin adaptive policy retention

---
 HexInterval/SPEC/hex-interval.md              |  3 +-
 .../HexInterval/StagedPolicyConformance.lean  | 33 +++++++++++++++++++
 progress/20260815T130007Z.md                  | 31 +++++++++++++++++
 .../bench/proof_only_runtime_exemptions.json  |  2 +-
 4 files changed, 66 insertions(+), 3 deletions(-)
 create mode 100644 progress/20260815T130007Z.md

diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index ae660e2a8..346bf7397 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -3401,8 +3401,7 @@ not generally demote unproductive sites across successive input versions.
 
 The feedback table has an explicit deterministic record bound and evicts the
 least recently updated stable site when full. Instantiation and split offers
-retain
-their staged rank but do not yet have feedback records; invocation, retry, and
+retain their staged rank but do not yet have feedback records; invocation, retry, and
 equality work do. Offers at or beyond the configured fairness age form the first
 tier. On the normative finite frontier, where selection consumes an offer, this
 eventually samples every continuously eligible item; stable offer order remains
diff --git a/conformance/HexInterval/StagedPolicyConformance.lean b/conformance/HexInterval/StagedPolicyConformance.lean
index 009b21928..244121387 100644
--- a/conformance/HexInterval/StagedPolicyConformance.lean
+++ b/conformance/HexInterval/StagedPolicyConformance.lean
@@ -291,6 +291,39 @@ private def bounded : AdaptivePolicy.State :=
     (AdaptivePolicy.find? bounded.records
       (AdaptivePolicy.ruleKey productiveKey)).isNone
 
+/- Updating an existing site moves it to the MRU front, so the next insertion
+evicts the other retained site deterministically. -/
+private def touchedBounded : AdaptivePolicy.State :=
+  let state := AdaptivePolicy.State.initial { maxRecords := 2 }
+  let state := AdaptivePolicy.update state <|
+    .rule (observation productiveKey .success #[change 0])
+  let state := AdaptivePolicy.update state <|
+    .rule (observation quietKey .success #[change 1])
+  let state := AdaptivePolicy.update state <|
+    .rule (observation productiveKey .noChange #[])
+  AdaptivePolicy.update state <|
+    .rule (observation freshKey .success #[change 2])
+
+#guard
+  touchedBounded.records.length == 2 &&
+    (AdaptivePolicy.find? touchedBounded.records
+      (AdaptivePolicy.ruleKey productiveKey)).any (fun record => record.runs == 2) &&
+    (AdaptivePolicy.find? touchedBounded.records
+      (AdaptivePolicy.ruleKey quietKey)).isNone &&
+    (AdaptivePolicy.find? touchedBounded.records
+      (AdaptivePolicy.ruleKey freshKey)).isSome
+
+/- Stable input order is the final tie-breaker for otherwise equal offers. -/
+private def tiedKey := invocation 4 0
+private def tiedOffer := offer 4 0 (.invoke tiedKey)
+private def unlearned := AdaptivePolicy.State.initial config
+
+#guard
+  (AdaptivePolicy.choose? unlearned #[freshOffer, tiedOffer]).map
+      (fun selected => selected.key) == some freshOffer.key &&
+    (AdaptivePolicy.choose? unlearned #[tiedOffer, freshOffer]).map
+      (fun selected => selected.key) == some tiedOffer.key
+
 /- Fairness is a separate tier and eventually samples an old eligible action
 even when its learned score is poor. -/
 private def fairQuiet := { quietOffer with age := 20 }
diff --git a/progress/20260815T130007Z.md b/progress/20260815T130007Z.md
new file mode 100644
index 000000000..f080e7eb1
--- /dev/null
+++ b/progress/20260815T130007Z.md
@@ -0,0 +1,31 @@
+# Accomplished
+
+- Restacked the adaptive staged-policy experiment onto the exact branch-proof
+  candidate while preserving current public interval and PNT registrations.
+- Kept stable application/equality site keys separate from full invocation
+  snapshots, so same-snapshot fixed points decay while changed snapshots reuse
+  gain history without inheriting stale stagnation.
+- Confirmed live feedback originates in events returned by the validated
+  policy-session path and affects scheduling only, never proof evidence.
+- Added load-bearing guards for update-to-MRU retention, deterministic bounded
+  eviction, and stable input order as the final complete-tie breaker.
+- Retained the deliberately narrow fairness claim for finite frontiers whose
+  selections consume offers.
+- Rebuilt adaptive-policy, branch, arithmetic, public interval, and PNT targets
+  and ran the repository formatting, DAG, trust, registration, PNT, and
+  freshness checks.
+
+# Current frontier
+
+The local policy learns bounded integer scheduling scores from authenticated
+rule and equality observations. Every selected offer remains independently
+revalidated by `PolicySession`, and proof replay is policy-independent.
+
+# Next step
+
+Complete the normal remote review and CI cycle after the preceding stack edges
+land.
+
+# Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index d58cac621..c8ad3e82a 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -224,7 +224,7 @@
   {
     "path": "lakefile.lean",
     "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
-    "current_blob": "9595b5335e7568bcc2c3e18d4c66c763ed855a44",
+    "current_blob": "79027f494a8353cf4a8cc485c925bb9734931fb7",
     "reason": "Additionally registers the isolated Mathlib-free adaptive interval-policy experiment; the factorization service target and executable dependency graph are unchanged."
   },
   {

From a0c00056921552416444c77f17ccaa3f015a4a74 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sun, 16 Aug 2026 00:23:01 +0000
Subject: [PATCH 7/8] docs(interval): prepare adaptive policy after branch
 proof

---
 progress/20260816T002246Z.md                  | 24 +++++++++++++++++++
 .../bench/proof_only_runtime_exemptions.json  |  4 ++--
 2 files changed, 26 insertions(+), 2 deletions(-)
 create mode 100644 progress/20260816T002246Z.md

diff --git a/progress/20260816T002246Z.md b/progress/20260816T002246Z.md
new file mode 100644
index 000000000..19e4d5ffc
--- /dev/null
+++ b/progress/20260816T002246Z.md
@@ -0,0 +1,24 @@
+# Prepare adaptive policy after exact branch proof
+
+## Accomplished
+
+- Replayed the audited adaptive feedback policy directly onto exact #9233
+  candidate `921d08ca9bb72f00a752aba26e123d24a2d4317b`.
+- Preserved stable site keys, authenticated snapshots, bounded MRU retention,
+  finite consuming-frontier fairness, and proof-independent policy behavior.
+- Preserved the exact-branch, subtraction, staged-policy, complete LogTables,
+  PNT, and public interval registrations and refreshed the exact Lake exemption.
+
+## Current frontier
+
+The local branch contains only the adaptive-policy edge above #9233. The raster
+and policy-feature forks and all later controller refs remain unchanged.
+
+## Next step
+
+After #9233 merges, replay this prepared edge onto its literal merge commit and
+publish PR #9234 as a direct-main branch.
+
+## Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index c8ad3e82a..651d81571 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -224,8 +224,8 @@
   {
     "path": "lakefile.lean",
     "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
-    "current_blob": "79027f494a8353cf4a8cc485c925bb9734931fb7",
-    "reason": "Additionally registers the isolated Mathlib-free adaptive interval-policy experiment; the factorization service target and executable dependency graph are unchanged."
+    "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": "HexBerlekamp/FactorTacticTests.lean",

From 4f1b51f2a63c629fd1ef4b646c994c0b7d74b4ca Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Sun, 16 Aug 2026 00:37:42 +0000
Subject: [PATCH 8/8] docs(interval): record merged branch policy restack

---
 progress/20260816T003732Z.md | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 progress/20260816T003732Z.md

diff --git a/progress/20260816T003732Z.md b/progress/20260816T003732Z.md
new file mode 100644
index 000000000..da5c4896d
--- /dev/null
+++ b/progress/20260816T003732Z.md
@@ -0,0 +1,25 @@
+# Restack adaptive policy onto merged exact branch proof
+
+## Accomplished
+
+- Replayed the prepared adaptive-policy edge onto literal #9233 merge commit
+  `4616ae07b80465e1a9eb3cef8b965c963476974b`.
+- Preserved the merged 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 its narrow proof-only runtime
+  exemption remain unchanged by the merge-parent restack.
+
+## Current frontier
+
+PR #9234 is a direct-main adaptive-policy edge. The raster and policy-feature
+forks and all later controller refs remain independent and unchanged.
+
+## Next step
+
+Run focused adaptive, controller, inventory, trust, freshness, and diff gates;
+then publish the direct-main PR head and monitor automatic CI.
+
+## Blockers
+
+None.