diff --git a/research/lean-pending-derivation/PendingBinding.lean b/research/lean-pending-derivation/PendingBinding.lean
new file mode 100644
index 0000000000..13c202f374
--- /dev/null
+++ b/research/lean-pending-derivation/PendingBinding.lean
@@ -0,0 +1,48 @@
+import PhysicalSourceConnection
+import PendingDerivation
+
+/-!
+Binds PR540's hand-supplied `PhysicalSourceConnection.pendingTag` to the
+schedule-derived pending sets of `PendingDerivation`. It restates the
+selected-invocation completion theorem with the derived mask. No existing
+definition or theorem is changed.
+
+Apache-2.0. Douglas Colkitt, with Claude (Anthropic) assistance.
+-/
+namespace PendingBinding
+open TreeReplay WholeHosting SourceConnection PhysicalSourceConnection
+
+/-- The hand-supplied ranges `[15,22)` and `[1,29)` are exactly the derived sets. -/
+theorem pendingTag_derived : ∀ (t : SourceOwnership.Tag) (i : SourceOwnership.Axis),
+    pendingTag t i = PendingDerivation.derivedPendingTag t i := by
+  decide +kernel
+
+/-- Pending mask of every host, derived from the source schedule. -/
+def derivedPending : MultiHosting.HostMask Host SourceOwnership.Axis :=
+  fun h => PendingDerivation.derivedPendingTag (SourceOwnership.tag (role h))
+
+theorem pending_eq_derived : pending = derivedPending := by
+  funext h i
+  exact pendingTag_derived _ _
+
+/-- `selected_invocation_completion` with the schedule-derived pending mask. -/
+theorem selected_invocation_completion_derived {K : Type} {Tail : Type v}
+    (gauges : Gauges K) (geometry : HelperRelative gauges)
+    (dataInput dataOutput : Data → Streams K → Streams K)
+    (oldInput oldOutput : Host → Streams K → Streams K)
+    (s : MultiHosting.WindowState Host SourceOwnership.Axis K Bool (Retained K Tail))
+    (oldBank : Host → Streams K) (newBank : Unit) :
+    MultiHosting.onHosts
+        (MultiHosting.remainders derivedPending [event (Tail := Tail) gauges dataInput dataOutput])
+        (relocated gauges dataInput dataOutput (s, newBank)).1 =
+      MultiHosting.onHosts derivedPending
+        (original gauges dataInput dataOutput oldInput oldOutput (s, oldBank)).1 := by
+  rw [← pending_eq_derived]
+  exact selected_invocation_completion gauges geometry dataInput dataOutput oldInput oldOutput
+    s oldBank newBank
+
+end PendingBinding
+
+#print axioms PendingBinding.pendingTag_derived
+#print axioms PendingBinding.pending_eq_derived
+#print axioms PendingBinding.selected_invocation_completion_derived
diff --git a/research/lean-pending-derivation/PendingDerivation.lean b/research/lean-pending-derivation/PendingDerivation.lean
new file mode 100644
index 0000000000..f866a7fa9f
--- /dev/null
+++ b/research/lean-pending-derivation/PendingDerivation.lean
@@ -0,0 +1,106 @@
+import PendingScheduleData
+import OwnershipDatumCore
+
+/-!
+Pending coordinates of the selected invocation, derived from the literal PR442
+schedule instead of supplied by hand.
+
+Level model (PR386 bit geometry, chart `B_port ⊕ I₅₆`): level −1 is span(q),
+which is axis 0; level `l ≥ 0` is the local block `[0,8)` together with the
+exterior route blocks of stages `1..l`. An idle child advancing a pair from
+level `a` to level `b` has pending set `L_b \ L_a`. Its window is the set of
+local invocations strictly after the pair's last local/bridge touch.
+
+What is checked here:
+* every idle event's rank is the size of its derived pending set, and levels nest;
+* the selected stage lies in the window of every hosted child, whose pair is idle;
+* every hosted target mask is the `[offset, offset+width)` slice of its child's
+  ascending derived pending axes.
+
+What is not: the identification of level −1 with span(q) and of these levels
+with the PR386 frames is the stated model, not a theorem here. The schedule and
+blocks are extracted literals (`generate_pending_schedule.py`).
+
+Apache-2.0. Douglas Colkitt, with Claude (Anthropic) assistance.
+-/
+namespace PendingDerivation
+open PendingSchedule
+
+/-- Membership of axis `i` in level `l - 1` (levels are shifted: `0` is level −1). -/
+def inLevel (l i : Nat) : Bool :=
+  if l = 0 then i == 0
+  else i < 8 || (exteriorBlocks.take (l - 1)).any (fun b => b.contains i)
+
+/-- `(pair, rank, source, target)` of the idle child with index `idx`. -/
+def idleData (idx : Nat) : Option (Nat × Nat × Nat × Nat) :=
+  schedule.findSome? fun
+    | .idle j p r s t => if j = idx then some (p, r, s, t) else none
+    | _ => none
+
+/-- Ascending derived pending axes `L_target \ L_source` of an idle child. -/
+def pendingAxes (idx : Nat) : List Nat :=
+  match idleData idx with
+  | some (_, _, s, t) => (List.range 64).filter fun i => inLevel t i && !inLevel s i
+  | none => []
+
+def windowGo (idx p : Nat) : List Event → List Nat → List Nat
+  | [], _ => []
+  | .local s q :: es, acc => if q = p then windowGo idx p es [] else windowGo idx p es (acc ++ [s])
+  | .bridge d s :: es, acc =>
+      if d = p ∨ s = p then windowGo idx p es [] else windowGo idx p es acc
+  | .idle j _ _ _ _ :: es, acc => if j = idx then acc else windowGo idx p es acc
+  | .exchange :: es, acc => windowGo idx p es acc
+
+/-- Stages of the local invocations strictly between the last touch of the
+child's pair and the child. Idle children are not touches. -/
+def window (idx : Nat) : List Nat :=
+  match idleData idx with
+  | some (p, _, _, _) => windowGo idx p schedule []
+  | none => []
+
+def idleConsistent : List Event → Bool
+  | [] => true
+  | .idle idx _ r s t :: es =>
+      s ≤ t && (List.range 64).all (fun i => !inLevel s i || inLevel t i) &&
+        (pendingAxes idx).length == r && idleConsistent es
+  | _ :: es => idleConsistent es
+
+theorem idle_ranks_and_nesting : idleConsistent schedule = true := by decide
+
+theorem top_level_is_ambient : (List.range 64).all (inLevel 9) = true := by decide
+
+theorem pending_child1 : pendingAxes 1 = List.range' 15 7 := by decide
+theorem pending_child2 : pendingAxes 2 = List.range' 1 28 := by decide
+
+/-- Idle child hosting a role tag. -/
+def child (t : SourceOwnership.Tag) : Nat := SourceOwnership.lookup SourceOwnership.tagChild t.val
+
+def derivedPendingTag (t : SourceOwnership.Tag) (i : SourceOwnership.Axis) : Bool :=
+  (pendingAxes (child t)).contains i.val
+
+def derivedTarget (t : SourceOwnership.Tag) (i : SourceOwnership.Axis) : Bool :=
+  (((pendingAxes (child t)).drop (SourceOwnership.lookup SourceOwnership.tagOffset t.val)).take
+    (SourceOwnership.lookup SourceOwnership.tagWidth t.val)).contains i.val
+
+theorem hosted_windows : ∀ t : SourceOwnership.Tag,
+    selectedStage ∈ window (child t) ∧
+      (idleData (child t)).map (·.1) ≠ some selectedPair ∧
+      SourceOwnership.lookup SourceOwnership.tagOffset t.val +
+          SourceOwnership.lookup SourceOwnership.tagWidth t.val ≤ (pendingAxes (child t)).length := by
+  decide
+
+/-- The extracted target masks are exactly slices of the derived pending axes. -/
+theorem target_derived : ∀ (t : SourceOwnership.Tag) (i : SourceOwnership.Axis),
+    SourceOwnership.targetMask t i = derivedTarget t i := by
+  decide +kernel
+
+theorem target_in_derived_pending : ∀ (t : SourceOwnership.Tag) (i : SourceOwnership.Axis),
+    SourceOwnership.targetMask t i = true → derivedPendingTag t i = true := by
+  decide +kernel
+
+end PendingDerivation
+
+#print axioms PendingDerivation.idle_ranks_and_nesting
+#print axioms PendingDerivation.hosted_windows
+#print axioms PendingDerivation.target_derived
+#print axioms PendingDerivation.target_in_derived_pending
diff --git a/research/lean-pending-derivation/PendingScheduleData.lean b/research/lean-pending-derivation/PendingScheduleData.lean
new file mode 100644
index 0000000000..d802ccd221
--- /dev/null
+++ b/research/lean-pending-derivation/PendingScheduleData.lean
@@ -0,0 +1,65 @@
+import Std
+
+/-! Literal PR442 hosted bit schedule and PR434 exterior route blocks.
+Generated by generate_pending_schedule.py from ../lean-multi-host-source/inputs/hosted-template.json.gz
+(uncompressed sha256 dd7833dcaff8c84b258847f4c4d65b6402c702700ae37d2c464083ee37b24126) and inputs/geometry.json.gz
+(uncompressed sha256 fc7b29b16ee754ca9717973b745d6322bbf8351a5e35e3fc9e0fbf7a88dc0317). The extractor is not kernel verified; every
+port's routes agree on the exterior blocks. Idle levels are shifted by one.
+Apache-2.0. Douglas Colkitt, with Claude (Anthropic) assistance. -/
+namespace PendingSchedule
+
+inductive Event where
+  | local (stage pair : Nat)
+  | bridge (dst src : Nat)
+  /-- `idle idx pair rank (sourceLevel + 1) (targetLevel + 1)` -/
+  | idle (idx pair rank source target : Nat)
+  | exchange
+  deriving DecidableEq, Repr
+
+def schedule : List Event := [
+  .local 0 0,
+  .local 1 0,
+  .idle 0 1 14 0 2,
+  .bridge 0 1,
+  .local 2 0,
+  .idle 1 1 7 2 3,
+  .bridge 0 1,
+  .local 3 1,
+  .idle 2 2 28 0 4,
+  .bridge 1 2,
+  .local 4 1,
+  .idle 3 2 7 4 5,
+  .bridge 1 2,
+  .local 5 2,
+  .idle 4 3 42 0 6,
+  .bridge 2 3,
+  .local 6 2,
+  .idle 5 3 7 6 7,
+  .bridge 2 3,
+  .local 7 3,
+  .local 8 3,
+  .idle 6 0 42 3 9,
+  .idle 7 1 28 5 9,
+  .idle 8 2 14 7 9,
+  .idle 9 3 0 9 9,
+  .bridge 3 2,
+  .bridge 2 1,
+  .bridge 1 0,
+  .exchange]
+
+/-- Exterior axes of the stage-s route (s = 1..8), identical for all 120 ports. -/
+def exteriorBlocks : List (List Nat) := [
+  [8, 9, 10, 11, 12, 13, 14],
+  [15, 16, 17, 18, 19, 20, 21],
+  [22, 23, 24, 25, 26, 27, 28],
+  [29, 30, 31, 32, 33, 34, 35],
+  [36, 37, 38, 39, 40, 41, 42],
+  [43, 44, 45, 46, 47, 48, 49],
+  [50, 51, 52, 53, 54, 55, 56],
+  [57, 58, 59, 60, 61, 62, 63]]
+
+/-- The selected invocation of PR540: stage 2, replica 0, pair 0, forward. -/
+def selectedStage : Nat := 2
+def selectedPair : Nat := 0
+
+end PendingSchedule
diff --git a/research/lean-pending-derivation/README.md b/research/lean-pending-derivation/README.md
new file mode 100644
index 0000000000..039b4ee9d0
--- /dev/null
+++ b/research/lean-pending-derivation/README.md
@@ -0,0 +1,84 @@
+# PR540's pending ranges, derived in Lean
+
+**Lean companion to [#540](https://github.com/CrocSwap/integer-mult-bounds/pull/540), stacked on its head
+`acc1917034d10f464271ab115fda314fd4eee7a3`. No new κ. No PR540 file is changed.**
+
+PR540's `PhysicalSourceConnection.pendingTag` supplies the pending coordinates of the selected
+invocation (stage 2, replica 0, pair 0) by hand: `[15,22)` for idle child 1 and `[1,29)` for child 2.
+Lean checked only that they contain the target masks. [#1228](https://github.com/CrocSwap/integer-mult-bounds/pull/1228)
+derived them in Python. This package moves that derivation into Lean 4.21 and binds it to PR540's
+actual definition.
+
+## What is proved
+
+From the literal PR442 schedule and route blocks (`PendingScheduleData.lean`), `PendingDerivation.lean` defines:
+
+- **Levels:** `L₋₁ = {0}` and `L_ℓ = [0,8) ∪ E₁ ∪ … ∪ E_ℓ`, with `E_s` the exterior axes of the
+  stage-s route.
+- **Pending axes:** `pendingAxes idx = L_target \ L_source`, ascending.
+- **Windows:** the stages strictly after the pair's last local or bridge touch.
+
+The following are proved by `decide`, using only `propext` and `Quot.sound` (or no axioms):
+
+| Theorem | Statement |
+|---|---|
+| `idle_ranks_and_nesting` | All 10 idle events: levels nest and `|pendingAxes idx| = rank` |
+| `pending_child1`, `pending_child2` | `pendingAxes 1 = [15..21]`, `pendingAxes 2 = [1..28]` |
+| `hosted_windows` | For all 16 tags: stage 2 is in the child's window, the host pair is not pair 0, and `offset+width ≤ |pending|` |
+| `target_derived` | For all tags and axes, `targetMask t i` is the `[offset, offset+width)` slice of the derived pending axes |
+| `PendingBinding.pendingTag_derived` | PR540's `pendingTag t i = derivedPendingTag t i` for all tags and axes |
+| `PendingBinding.pending_eq_derived` | `PhysicalSourceConnection.pending = derivedPending` |
+| `PendingBinding.selected_invocation_completion_derived` | PR540's completion theorem, stated with the derived mask |
+
+As a result, the hand-written ranges and the extractor's hard-coded bases 15 and 1 are no longer
+unchecked premises. Both are equal to schedule-derived definitions inside Lean.
+
+Six mutations each fail because `decide` refutes the mutated statement:
+
+- L₋₁ empty;
+- L₋₁ set to the whole local block;
+- exterior blocks off by one stage;
+- the first two exterior blocks swapped;
+- child 1 advanced before the selected call;
+- child 1 claimed on the previous block.
+
+## Remaining trust boundary
+
+- **Literal data.** `PendingScheduleData.lean` is a Python extraction from the pinned template and
+  geometry, the same boundary as PR540's other literal data. `generate_pending_schedule.py --check`
+  regenerates it byte for byte.
+- **Level model.** The model is a definition. Its agreement with the PR386 frames (in particular
+  L₋₁ = span(q) in the `B_port ⊕ I₅₆` chart) is not proved here. The checks above pin it down only
+  through ranks, nesting and the extracted target masks.
+- **Axis order.** The ascending axis order within a child is the offset convention shared with
+  PR540's extractor.
+- **Scope.** One invocation only. No cover sweep, cost, all-size or κ claim.
+
+## Reproduce
+
+```sh
+cd research/lean-multi-host-source && lake exe cache get Mathlib.Data.Matrix.Mul \
+  Mathlib.Algebra.BigOperators.Fin Mathlib.Tactic.FieldSimp Mathlib.Tactic.Ring Mathlib.Tactic.NormNum
+lake build PhysicalSourceConnection          # PR540's own build; 3.5 min measured with the Mathlib cache
+cd ../.. && python3 research/lean-pending-derivation/verify.py
+```
+
+Building the three new modules takes seconds, and the controls about 15 s. `verify.py` runs the
+generator check, compiles the modules against PR540's build through `lake env`, audits the axioms
+of all seven theorems and runs the controls.
+
+## Open next questions
+
+- **Can the level model be proved from the PR386 frames?** Proving `L_ℓ` from the route identity
+  ρ_(s,q): (P_q, E_s) → (I₈, E_(s−1)) and PR540's port charts would remove the last modelling
+  premise. A first step is to state the route identity for port 0 over PR540's `Address` type. The
+  blocker is that the geometry's rational route matrices are not yet Lean data.
+- **Does this generalise to a second invocation?** `PendingDerivation` is parametric in the tag's
+  child. A second selected call needs its own ownership literals from PR540's extractor.
+
+## Credit
+
+The Lean formalization, ownership literals and identification of this gap are cheesegrader's #540.
+The construction and hosting rule are #434/#442, and the bit geometry is PR386. The Python
+predecessor is #1228. Prepared by Douglas Colkitt with substantial Claude (Anthropic) assistance.
+Apache-2.0.
diff --git a/research/lean-pending-derivation/generate_pending_schedule.py b/research/lean-pending-derivation/generate_pending_schedule.py
new file mode 100644
index 0000000000..134bac65ca
--- /dev/null
+++ b/research/lean-pending-derivation/generate_pending_schedule.py
@@ -0,0 +1,99 @@
+#!/usr/bin/env python3
+"""Emit the literal PR442 bit schedule and exterior route blocks for PendingDerivation.lean.
+
+Offline provenance bridge, not a kernel-verified JSON parser. The Lean modules
+derive the pending coordinates from these literals; nothing here computes a
+pending set. Douglas Colkitt, with Claude (Anthropic) assistance. Apache-2.0.
+
+usage: generate_pending_schedule.py [--check]
+"""
+import argparse, gzip, hashlib, json
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parent / 'lean-multi-host-source'   # PR540's pinned inputs
+OUT = HERE / 'PendingScheduleData.lean'
+
+
+def load(name):
+    versions = json.loads((ROOT / 'source-versions.json').read_text())['inputs'][name]
+    blob = (ROOT / 'inputs' / name).read_bytes()
+    assert hashlib.sha256(blob).hexdigest() == versions['sha256_compressed'], name
+    raw = gzip.decompress(blob)
+    assert hashlib.sha256(raw).hexdigest() == versions['sha256_uncompressed'], name
+    return json.loads(raw), hashlib.sha256(raw).hexdigest()
+
+
+def render():
+    t, t_sha = load('hosted-template.json.gz')
+    g, g_sha = load('geometry.json.gz')
+    assert t['geometry_sha256'] == g_sha and (t['m'], t['h']) == (64, 8) == (g['m'], g['h'])
+    events = []
+    for e in t['schedule']:
+        k = e['kind']
+        if k == 'local_cover_sweep':
+            events.append(f'.local {e["stage"]} {e["pair"]}')
+        elif k == 'bridge':
+            events.append(f'.bridge {e["dst"]} {e["src"]}')
+        elif k == 'idle':
+            # levels are stored shifted by one so that source level -1 is 0
+            events.append(f'.idle {e["idx"]} {e["pair"]} {e["rank"]} {e["source_level"] + 1} {e["target_level"] + 1}')
+        else:
+            assert k == 'exchange'
+            events.append('.exchange')
+    blocks = {}
+    for port in g['ports']:
+        for r in port['routes']:
+            ax = r['axes']
+            assert ax[:8] == list(range(8))
+            if r['stage'] == 0:
+                assert ax == list(range(8)) and r.get('identity')
+            else:
+                assert blocks.setdefault(r['stage'], ax[8:]) == ax[8:], 'ports disagree'
+    assert len(g['ports']) == 120 and sorted(blocks) == list(range(1, 9))
+    calls = [c for c in t['calls'] if c['stage'] == 2 and c['replica'] == 0]
+    assert len(calls) == 1 and calls[0]['pair'] == 0 and calls[0]['orientation'] == 'forward'
+    lst = lambda xs, ind: '[\n' + ',\n'.join(ind + x for x in xs) + ']'
+    return f'''import Std
+
+/-! Literal PR442 hosted bit schedule and PR434 exterior route blocks.
+Generated by generate_pending_schedule.py from ../lean-multi-host-source/inputs/hosted-template.json.gz
+(uncompressed sha256 {t_sha}) and inputs/geometry.json.gz
+(uncompressed sha256 {g_sha}). The extractor is not kernel verified; every
+port's routes agree on the exterior blocks. Idle levels are shifted by one.
+Apache-2.0. Douglas Colkitt, with Claude (Anthropic) assistance. -/
+namespace PendingSchedule
+
+inductive Event where
+  | local (stage pair : Nat)
+  | bridge (dst src : Nat)
+  /-- `idle idx pair rank (sourceLevel + 1) (targetLevel + 1)` -/
+  | idle (idx pair rank source target : Nat)
+  | exchange
+  deriving DecidableEq, Repr
+
+def schedule : List Event := {lst(events, '  ')}
+
+/-- Exterior axes of the stage-s route (s = 1..8), identical for all 120 ports. -/
+def exteriorBlocks : List (List Nat) := {lst([json.dumps(blocks[s]).replace(' ', '') .replace(',', ', ') for s in range(1, 9)], '  ')}
+
+/-- The selected invocation of PR540: stage 2, replica 0, pair 0, forward. -/
+def selectedStage : Nat := 2
+def selectedPair : Nat := 0
+
+end PendingSchedule
+'''
+
+
+def main():
+    ap = argparse.ArgumentParser(); ap.add_argument('--check', action='store_true'); a = ap.parse_args()
+    text = render()
+    if a.check:
+        assert OUT.read_text() == text, 'PendingScheduleData.lean differs from the pinned inputs'
+        print('PASS: PendingScheduleData.lean matches the pinned schedule and geometry')
+    else:
+        OUT.write_text(text); print('wrote', OUT.name)
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/lean-pending-derivation/lean-toolchain b/research/lean-pending-derivation/lean-toolchain
new file mode 100644
index 0000000000..980709bbba
--- /dev/null
+++ b/research/lean-pending-derivation/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.21.0
diff --git a/research/lean-pending-derivation/pending_controls.py b/research/lean-pending-derivation/pending_controls.py
new file mode 100644
index 0000000000..0834a01b0a
--- /dev/null
+++ b/research/lean-pending-derivation/pending_controls.py
@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+"""Mutation controls for PendingDerivation.lean: each mutated copy must fail to compile.
+
+usage: pending_controls.py LEAN OLEAN_DIR
+OLEAN_DIR must already hold PendingScheduleData.olean and OwnershipDatumCore.olean.
+Douglas Colkitt, with Claude (Anthropic) assistance. Apache-2.0.
+"""
+import os, subprocess, sys, tempfile
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent
+SRC = (ROOT / 'PendingDerivation.lean').read_text()
+DATA = (ROOT / 'PendingScheduleData.lean').read_text()
+MUTATIONS = {
+    'level_minus_one_empty': ('PendingDerivation', 'if l = 0 then i == 0', 'if l = 0 then false'),
+    'level_minus_one_whole_local_block': ('PendingDerivation', 'if l = 0 then i == 0', 'if l = 0 then i < 8'),
+    'exterior_block_off_by_one_stage': ('PendingDerivation', 'exteriorBlocks.take (l - 1)', 'exteriorBlocks.take l'),
+    'child1_advanced_before_selected_call': ('PendingScheduleData', '  .local 2 0,\n  .idle 1 1 7 2 3,',
+                                             '  .idle 1 1 7 2 3,\n  .local 2 0,'),
+    'child1_previous_block_claimed': ('PendingDerivation', 'pendingAxes 1 = List.range\' 15 7',
+                                      'pendingAxes 1 = List.range\' 8 7'),
+    'swapped_exterior_blocks': ('PendingScheduleData', '  [8, 9, 10, 11, 12, 13, 14],\n  [15, 16, 17, 18, 19, 20, 21],',
+                                '  [15, 16, 17, 18, 19, 20, 21],\n  [8, 9, 10, 11, 12, 13, 14],'),
+}
+
+
+def main(lean, olean):
+    results = {}
+    for name, (module, old, new) in MUTATIONS.items():
+        with tempfile.TemporaryDirectory() as tmp:
+            tmp = Path(tmp)
+            env = dict(os.environ, LEAN_PATH=f'{tmp}{os.pathsep}{olean}')
+            src = SRC
+            if module == 'PendingScheduleData':
+                assert DATA.count(old) == 1, name
+                (tmp / 'd.lean').write_text(DATA.replace(old, new))
+                r = subprocess.run([lean, f'--root={tmp}', '-o', str(tmp / 'PendingScheduleData.olean'), str(tmp / 'd.lean')],
+                                   env=env, capture_output=True, text=True)
+                assert r.returncode == 0, r.stdout + r.stderr
+            else:
+                assert src.count(old) == 1, name
+                src = src.replace(old, new)
+            (tmp / 'm.lean').write_text(src)
+            r = subprocess.run([lean, f'--root={tmp}', str(tmp / 'm.lean')], env=env, capture_output=True, text=True)
+            err = next((l for l in r.stdout.splitlines() if 'error' in l), '')
+            assert 'unknown' not in err and 'object file' not in err, err   # fail on a proof, not on setup
+            results[name] = ('rejected: ' + err.split('error: ', 1)[-1][:90]) if r.returncode != 0 else 'ACCEPTED'
+            print(f'{name}: {results[name]}', flush=True)
+    assert all(v.startswith('rejected') for v in results.values()), results
+    print('PASS: all', len(results), 'mutations rejected')
+
+
+if __name__ == '__main__':
+    main(sys.argv[1], sys.argv[2])
diff --git a/research/lean-pending-derivation/verify.py b/research/lean-pending-derivation/verify.py
new file mode 100644
index 0000000000..892832f118
--- /dev/null
+++ b/research/lean-pending-derivation/verify.py
@@ -0,0 +1,68 @@
+#!/usr/bin/env python3
+"""Build and audit the schedule-derived pending ranges for PR540's selected invocation.
+
+Prerequisite: PR540's project is built, e.g.
+  (cd research/lean-multi-host-source && lake build PhysicalSourceConnection)
+
+Steps:
+  1. generate_pending_schedule.py --check (literal schedule matches the pinned inputs);
+  2. compile PendingScheduleData, PendingDerivation and PendingBinding with Lean 4.21
+     against PR540's build (LEAN_PATH from `lake env`), with no change to PR540's files;
+  3. require the axiom audit to list only propext, Quot.sound and Classical.choice;
+  4. run the six mutation controls (each must fail by `decide`).
+
+usage: verify.py [--lake LAKE]
+Douglas Colkitt, with Claude (Anthropic) assistance. Apache-2.0.
+"""
+import argparse, os, re, subprocess, sys, tempfile
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+PROJECT = HERE.parent / 'lean-multi-host-source'
+MODULES = ['PendingScheduleData', 'PendingDerivation', 'PendingBinding']
+EXPECTED_THEOREMS = {
+    'PendingDerivation.idle_ranks_and_nesting', 'PendingDerivation.hosted_windows',
+    'PendingDerivation.target_derived', 'PendingDerivation.target_in_derived_pending',
+    'PendingBinding.pendingTag_derived', 'PendingBinding.pending_eq_derived',
+    'PendingBinding.selected_invocation_completion_derived',
+}
+ALLOWED = {'propext', 'Quot.sound', 'Classical.choice'}
+
+
+def run(cmd, **kw):
+    r = subprocess.run(cmd, capture_output=True, text=True, **kw)
+    if r.returncode:
+        sys.exit(f'FAIL: {" ".join(map(str, cmd))}\n{r.stdout}{r.stderr}')
+    return r.stdout
+
+
+def main():
+    ap = argparse.ArgumentParser(); ap.add_argument('--lake', default='lake'); a = ap.parse_args()
+    print(run([sys.executable, '-I', '-B', HERE / 'generate_pending_schedule.py', '--check']).strip())
+    toolchain = (HERE / 'lean-toolchain').read_text().strip()
+    assert toolchain == (PROJECT / 'lean-toolchain').read_text().strip() == 'leanprover/lean4:v4.21.0'
+    base = run([a.lake, 'env', 'printenv', 'LEAN_PATH'], cwd=PROJECT).strip()
+    lean = run([a.lake, 'env', 'which', 'lean'], cwd=PROJECT).strip()
+    assert (PROJECT / '.lake/build/lib/lean/PhysicalSourceConnection.olean').exists(), \
+        'build PR540 first: lake build PhysicalSourceConnection'
+    audit = {}
+    with tempfile.TemporaryDirectory() as tmp:
+        path = f'{tmp}{os.pathsep}{base}'
+        env = dict(os.environ, LEAN_PATH=path)
+        for m in MODULES:
+            out = run([lean, f'--root={HERE}', '-o', f'{tmp}/{m}.olean', HERE / f'{m}.lean'], env=env)
+            for line in out.splitlines():
+                mt = re.search(r"'([\w.]+)' (does not depend on any axioms|depends on axioms: \[([^\]]*)\])", line)
+                if mt:
+                    audit[mt[1]] = sorted(x.strip() for x in (mt[3] or '').split(',') if x.strip())
+            print(f'compiled {m}')
+        assert set(audit) == EXPECTED_THEOREMS, sorted(set(audit) ^ EXPECTED_THEOREMS)
+        assert all(set(v) <= ALLOWED for v in audit.values()), audit
+        for k in sorted(audit):
+            print(f'  {k}: {audit[k] or "no axioms"}')
+        print(run([sys.executable, '-I', '-B', HERE / 'pending_controls.py', lean, path]).strip())
+    print('PASS_PR540_PENDING_RANGES_DERIVED_IN_LEAN')
+
+
+if __name__ == '__main__':
+    main()