diff --git a/HexInterval/Experiment/AdaptivePolicy.lean b/HexInterval/Experiment/AdaptivePolicy.lean
new file mode 100644
index 000000000..43b4b1258
--- /dev/null
+++ b/HexInterval/Experiment/AdaptivePolicy.lean
@@ -0,0 +1,196 @@
+/-
+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 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.
+-/
+
+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 := 16
+  gainWeight : Nat := 96
+  noChangePenalty : Nat := 12
+  ageBonusCap : Nat := 4
+  fairnessAge : Nat := 20
+  maxRecords : Nat := 256
+  deriving DecidableEq, Repr
+
+/-- 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
+
+/-- Bounded search observations accumulated for one selectable transition. -/
+structure Record where
+  key : Key
+  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
+  records : List Record := []
+
+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
+
+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 })
+  | .instantiate _ _ | .split _ _ _ _ => none
+
+def find? (records : List Record) (key : Key) : Option Record :=
+  records.find? fun record => record.key == 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 (limit : Nat) (records : List Record) (key : Key)
+    (change : Record -> Record) : List Record :=
+  replace limit records (change ((find? records key).getD { key }))
+
+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
+      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 (limit : Nat) (records : List Record)
+    (observation : EqualityObservation Fact) : List 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
+      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.config.maxRecords state.records observation }
+  | state, .equality 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)
+    (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)
+      if record.last != snapshot then Nat.max config.optimism gain + ageBonus
+      else gain + ageBonus - config.noChangePenalty * record.stagnant
+
+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)
+  let snapshot := offerSnapshot? offer.key
+  { offer
+    fair := state.config.fairnessAge <= offer.age
+    stage := StagedPolicy.rank offer
+    score := learnedScore state.config record snapshot offer.age }
+
+/-- 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) ||
+    (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..346bf7397 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -3379,6 +3379,37 @@ 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 accumulates observations at a stable
+engine-owned application or equality site. Its bounded integer score rewards
+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
+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
 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..244121387 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,251 @@ 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
+
+/- 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
+
+/- 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 }
+
+#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.
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/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.
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/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.
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/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/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.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index f80dd261a..651d81571 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": "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",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",