diff --git a/research/pr540-pending-range-derivation/README.md b/research/pr540-pending-range-derivation/README.md
new file mode 100644
index 0000000000..42080384c3
--- /dev/null
+++ b/research/pr540-pending-range-derivation/README.md
@@ -0,0 +1,93 @@
+# Deriving PR540's pending ranges from PR442's schedule
+
+**Independent source-binding check for an open Lean PR. No new κ; the selected record is unchanged.**
+
+[PR540](https://github.com/CrocSwap/integer-mult-bounds/pull/540) (cheesegrader, head
+`acc1917034d10f464271ab115fda314fd4eee7a3`) formalizes one literal PR442 bit invocation (stage 2,
+replica 0, pair 0, forward). Its `PhysicalSourceConnection.pendingTag` supplies the pending
+coordinates by hand: child 1 owns axes `[15,22)` and child 2 owns `[1,29)`. Its README states that
+"Neither Lean nor the source-extraction check binds these ranges to the source schedule." Lean's
+`tag_pending_contains` only shows that the ranges *contain* the hosted target masks. The extractor
+`generate_ownership_data.py` hard-codes the bases 15 and 1. The
+[handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166) lists this as a next task.
+
+## Result
+
+`verify.py` derives both ranges from PR442's hosted bit template and PR434's geometry. It is
+standard-library code that imports nothing from PR434, PR442 or PR540. **Both ranges are exactly the
+derived pending sets.**
+
+| Child (template `idx`) | Pair | Level advance | Window stages | Derived pending axes | PR540 range | Hosted width used by the stage-2 call |
+|---|---:|---|---|---|---|---:|
+| 1 | 1 | 1 → 2 | {2} | `[15,22)` = exterior block E₂ | `[15,22)` | 7 of 7 |
+| 2 | 2 | −1 → 3 | {0,1,2,3} | `[1,29)` = q⊥ ⊕ E₁ ⊕ E₂ ⊕ E₃ | `[1,29)` | 28 of 28 |
+
+The derivation has five steps.
+
+1. **Binding.** The hosted template's uncompressed SHA256 equals `bit_template_sha256` in PR442's
+   [`EXPECTED.json`](../idle-axis-hosting/EXPECTED.json) on main. The geometry's hash equals the
+   template's `geometry_sha256`. The two vendored inputs in `inputs/` are byte-identical to PR540's
+   `research/lean-multi-host-source/inputs/` files with the same names.
+2. **Coordinates.** All 120 ports' stage-s routes give one common exterior block layout:
+   E_s = `[8+7(s−1), 8+7s)`. The blocks partition axes 8..63. For every port, `[q/2 | A_q]` is
+   checked to be an exactly orthogonal 8×8 matrix. This is the `B_port ⊕ I₅₆` chart in which axis 0
+   is span(q) and axes 1..7 are q⊥.
+3. **Levels.** The level model follows PR386's geometry (ρ_(s,q) sends (P_q, E_s) to (I₈, E_(s−1))):
+   L₋₁ = span(q) = {0} and L_ℓ = Q⁸ ⊕ E₁ ⊕ … ⊕ E_ℓ = `[0, 8+7ℓ)` in chart axes. The rank of every
+   idle event in the schedule (all 10, including the rank-0 terminal child) equals dim L_b − dim L_a.
+4. **Windows.** The windows are recomputed from the schedule with the PR442 rule: local invocations
+   strictly after the last local or bridge touch of the pair. Stage 2 lies in both windows, and the
+   host pairs differ from the active pair 0.
+5. **Routes.** Each of the 747 hosted routes `(child, off, w)` of the selected call maps to
+   `pending[off:off+w]`. This equals PR540's `base+off .. base+off+w` for every route. Each
+   PR540 range equals the full derived pending set, not just a superset of its targets.
+
+Six mutations are rejected:
+
+- child 1 placed on the previous level's block `[8,15)`;
+- child 2 shifted to include the q axis;
+- the two children's ranges swapped;
+- L₋₁ = {} (rank mismatch);
+- a route offset moved past the pending rank;
+- stage 2 removed from child 1's window.
+
+## Limits
+
+- This is a Python derivation, not a kernel proof. It closes the stated gap as **external evidence**.
+  Moving the derivation into Lean remains open.
+- The idle ranks fix only the *dimensions* of the level spaces. Identifying L₋₁ with span(q), rather
+  than another line, uses PR386's route identity, which this package does not re-prove. A wrong
+  choice of line would break the q⊥ chart; that chart is checked.
+- Within one child, PR442 requires only disjoint width-w subsets of its pending set. The ascending
+  axis order that maps `off` to axes is the shared convention of PR540's extractor and this check;
+  the source does not fix it.
+- Only the selected invocation is checked. This says nothing about other calls, the cover sweep,
+  costs or κ.
+
+## Reproduce
+
+```sh
+python3 -I -B research/pr540-pending-range-derivation/verify.py   # ~0.5 s, prints PASS_…
+python3 scripts/research_package.py --package research/pr540-pending-range-derivation
+```
+
+`verify.py --write` regenerates `RESULT.json`. Without that flag, the script requires the existing file to
+match byte for byte.
+
+## Open next questions
+
+- **Can `pendingTag` be defined from the schedule inside Lean?** This would turn the hand-supplied
+  ranges into a theorem. A first step is to encode the 10 idle events and the level map
+  `L_ℓ = [0, 8+7ℓ)`, then prove `pendingTag t = L_b \ L_a` by `decide`. The blocker is that the
+  level model must be stated as a definition and linked to the route identities in Lean.
+- **Does the same derivation hold for a second selected call?** That would test whether the
+  convention generalises before PR540 is extended. A first step is to run `derive` with another
+  `SELECTED` (for example, stage 3 on pair 1, whose children have different windows). This is not
+  blocked, but it is outside this session.
+
+## Credit
+
+The construction and hosting rule are PR434/PR442 (`research/e8-early-reset-kernel`,
+`research/idle-axis-hosting`). The bit geometry is PR386. The Lean formalization and the
+identification of this gap are cheesegrader's PR540. Prepared by Douglas Colkitt with substantial
+Claude (Anthropic) assistance. Apache-2.0.
diff --git a/research/pr540-pending-range-derivation/RESULT.json b/research/pr540-pending-range-derivation/RESULT.json
new file mode 100644
index 0000000000..16ce7f8245
--- /dev/null
+++ b/research/pr540-pending-range-derivation/RESULT.json
@@ -0,0 +1,100 @@
+{
+ "controls": {
+  "child1_previous_level_block": "rejected: route ['hosted', 1, 0, 7]: derived [15, 16, 17, 18, 19, 20, 21] != Lean [8, 9, 10, 11, 12, 13, 14]",
+  "child2_includes_q_axis": "rejected: route ['hosted', 2, 16, 8]: derived [17, 18, 19, 20, 21, 22, 23, 24] != Lean [16, 17, 18, 19, 20, 21, 22, 23]",
+  "children_swapped": "rejected: route ['hosted', 2, 16, 8]: derived [17, 18, 19, 20, 21, 22, 23, 24] != Lean [31, 32, 33, 34, 35, 36, 37, 38]",
+  "level_minus_one_empty": "rejected: idle 0 rank 14 != dim difference",
+  "route_offset_past_rank": "rejected: route ['hosted', 1, 1, 7] exceeds pending rank",
+  "stage2_outside_window": "rejected: stage 2 outside window of child 1"
+ },
+ "exterior_blocks": {
+  "1": [
+   8,
+   15
+  ],
+  "2": [
+   15,
+   22
+  ],
+  "3": [
+   22,
+   29
+  ],
+  "4": [
+   29,
+   36
+  ],
+  "5": [
+   36,
+   43
+  ],
+  "6": [
+   43,
+   50
+  ],
+  "7": [
+   50,
+   57
+  ],
+  "8": [
+   57,
+   64
+  ]
+ },
+ "hosted_children": {
+  "1": {
+   "derived_pending_axes": [
+    15,
+    22
+   ],
+   "hosted_axes_used": 7,
+   "lean_range": [
+    15,
+    22
+   ],
+   "levels": [
+    1,
+    2
+   ],
+   "pair": 1,
+   "pending_rank": 7,
+   "window_stages": [
+    2
+   ]
+  },
+  "2": {
+   "derived_pending_axes": [
+    1,
+    29
+   ],
+   "hosted_axes_used": 28,
+   "lean_range": [
+    1,
+    29
+   ],
+   "levels": [
+    -1,
+    3
+   ],
+   "pair": 2,
+   "pending_rank": 28,
+   "window_stages": [
+    0,
+    1,
+    2,
+    3
+   ]
+  }
+ },
+ "hosted_routes": 747,
+ "idle_ranks_checked": 10,
+ "ports_checked": 120,
+ "scope": "Python derivation from the source schedule and geometry. Not kernel checked. The level model L_-1=span(q), L_l=Q^8+E_1..E_l is PR386 geometry, checked here against every idle rank and route; the ascending order of pending axes within a child is the shared offset convention.",
+ "selected_call": {
+  "orientation": "forward",
+  "pair": 0,
+  "replica": 0,
+  "stage": 2
+ },
+ "status": "PASS_PR540_PENDING_RANGES_DERIVED_FROM_PR442_SCHEDULE"
+}
diff --git a/research/pr540-pending-range-derivation/SOURCES.json b/research/pr540-pending-range-derivation/SOURCES.json
new file mode 100644
index 0000000000..13edba3413
--- /dev/null
+++ b/research/pr540-pending-range-derivation/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    },
+    {
+      "path": "research/idle-axis-hosting/EXPECTED.json",
+      "usage": "input",
+      "git_blob": "1b0811df29bc2eabdabb51219e9b2382da9a48f6",
+      "sha256": "ed83c1bf1ca2d01eaab5149a34520806a07ef375dfa9e3ed69d123f4be4c9960"
+    }
+  ]
+}
diff --git a/research/pr540-pending-range-derivation/TASK.json b/research/pr540-pending-range-derivation/TASK.json
new file mode 100644
index 0000000000..dd58133aa0
--- /dev/null
+++ b/research/pr540-pending-range-derivation/TASK.json
@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 2,
+  "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Audit one theorem-to-source binding of open PR540: derive its hand-supplied pendingTag ranges [15,22) and [1,29) from PR442's bit schedule and PR434 geometry, instead of formalizing a new lemma.",
+  "scope_change_reason": "The card allows narrowing to one theorem-to-certificate binding. PR540's README and the handoff thread name this exact unbound premise.",
+  "bottleneck_link": "Side result for the conditional gap, not kappa: it removes one hand-supplied premise from the only literal Lean invocation of the hosting interface by tying it to the source schedule as external evidence.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the single selected invocation; do not extend to other calls or attempt the Lean port in this session.",
+  "outcome": "completed",
+  "evidence": "RESULT.json: both PR540 ranges equal the derived pending sets for all 747 hosted routes; 6/6 mutations rejected",
+  "author": "Douglas Colkitt",
+  "ai_assistance": "Substantial: Claude (Anthropic, Claude Code) selected the task, wrote verify.py and drafted the README; the author reviewed the result.",
+  "open_questions": [
+    {
+      "question": "Can pendingTag be defined from the schedule inside Lean?",
+      "why_it_matters": "It turns a hand-supplied premise of PR540 into a kernel-checked theorem.",
+      "first_step": "Encode the 10 idle events and L_l=[0,8+7l); prove pendingTag t = L_b minus L_a by decide.",
+      "blocked_by": "The level model must be stated in Lean and linked to the route identities."
+    },
+    {
+      "question": "Does the derivation hold for a second selected call?",
+      "why_it_matters": "It tests whether the convention generalises before PR540 is extended.",
+      "first_step": "Run derive() with another SELECTED, e.g. stage 3 on pair 1.",
+      "blocked_by": "Nothing; out of this session's budget."
+    }
+  ]
+}
diff --git a/research/pr540-pending-range-derivation/VERIFY.json b/research/pr540-pending-range-derivation/VERIFY.json
new file mode 100644
index 0000000000..f2af1e1462
--- /dev/null
+++ b/research/pr540-pending-range-derivation/VERIFY.json
@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/idle-axis-hosting/EXPECTED.json",
+    "research/pr540-pending-range-derivation/inputs/geometry.json.gz",
+    "research/pr540-pending-range-derivation/inputs/hosted-template.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Pins and PR442/geometry binding; derived pending sets equal PR540 ranges for all 747 routes; RESULT.json byte match; six rejection controls"
+    }
+  ]
+}
diff --git a/research/pr540-pending-range-derivation/inputs/geometry.json.gz b/research/pr540-pending-range-derivation/inputs/geometry.json.gz
new file mode 100644
index 0000000000..016ed9ed8c
Binary files /dev/null and b/research/pr540-pending-range-derivation/inputs/geometry.json.gz differ
diff --git a/research/pr540-pending-range-derivation/inputs/hosted-template.json.gz b/research/pr540-pending-range-derivation/inputs/hosted-template.json.gz
new file mode 100644
index 0000000000..e4ba0d1bfe
Binary files /dev/null and b/research/pr540-pending-range-derivation/inputs/hosted-template.json.gz differ
diff --git a/research/pr540-pending-range-derivation/verify.py b/research/pr540-pending-range-derivation/verify.py
new file mode 100644
index 0000000000..093444d507
--- /dev/null
+++ b/research/pr540-pending-range-derivation/verify.py
@@ -0,0 +1,221 @@
+#!/usr/bin/env python3
+"""Derive PR540's hand-supplied pending ranges from PR442's bit schedule and geometry.
+
+PR540 (`PhysicalSourceConnection.pendingTag`, head acc19170) states that idle
+child 1 owns pending axes [15,22) and child 2 owns [1,29) in the selected
+invocation (stage 2, replica 0, pair 0). Lean checks only that these ranges
+contain the hosted target masks. This script derives the ranges from the source
+schedule instead, with standard-library code that imports nothing from PR442,
+PR434 or PR540.
+
+  1. Bind the hosted template to PR442's EXPECTED.json on main, and bind the
+     geometry to the template.
+  2. Read the exterior 7-block layout from every port route. Check every chart
+     [q/2 | A_q] as an exact orthogonal matrix, so axis 0 is span(q) and axes
+     1..7 are q-perp.
+  3. Level model (PR386 geometry: rho_(s,q) sends (P_q,E_s) to (I_8,E_(s-1))):
+     L_-1 = span(q) = {0} and L_l = Q^8 + E_1..E_l = [0, 8+7l) in chart axes.
+     Every idle event's rank must equal dim L_b - dim L_a.
+  4. The pending set of a child a->b is L_b minus L_a. Recompute the windows
+     from the schedule, then map each hosted route (child, off, w) of the
+     selected call to axes pending[off:off+w].
+  5. Require PR540's ranges to equal the derived pending sets, not merely
+     contain the targets. Six mutations must be rejected.
+
+Douglas Colkitt, with Claude (Anthropic) assistance. Apache-2.0.
+"""
+import gzip, hashlib, json, sys
+from fractions import Fraction as Q
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+PINS = {  # compressed sha256; byte-identical to PR540 research/lean-multi-host-source/inputs/
+    'hosted-template.json.gz': '6e18a9ce240229c34556ba43fd6ec28f83200dfcf85e5584d4a670aeb605aeb0',
+    'geometry.json.gz': 'c2bdd236e44fb868e4d2260b1fd7820aa7a565119532781904ebff90b9e852d7',
+}
+# Literal constants of PR540 PhysicalSourceConnection.pendingTag (blob 9a78d48f at head acc19170)
+LEAN_PENDING = {1: range(15, 22), 2: range(1, 29)}
+SELECTED = dict(stage=2, replica=0, pair=0, orientation='forward')
+H, M, BLOCK = 8, 64, 7
+
+
+class Reject(Exception):
+    pass
+
+
+def require(ok, why):
+    if not ok:
+        raise Reject(why)
+
+
+def load():
+    raw = {}
+    for name, pin in PINS.items():
+        b = (HERE / 'inputs' / name).read_bytes()
+        require(hashlib.sha256(b).hexdigest() == pin, f'pin {name}')
+        raw[name] = gzip.decompress(b)
+    expected = json.loads((ROOT / 'research/idle-axis-hosting/EXPECTED.json').read_text())
+    require(hashlib.sha256(raw['hosted-template.json.gz']).hexdigest() == expected['bit_template_sha256'],
+            'template is not PR442 bit_template_sha256')
+    t = json.loads(raw['hosted-template.json.gz'])
+    require(hashlib.sha256(raw['geometry.json.gz']).hexdigest() == t['geometry_sha256'], 'geometry not bound by template')
+    return t, json.loads(raw['geometry.json.gz'])
+
+
+def exterior_blocks(geo):
+    """Exterior block l from the stage-l route axes of every port (stage 0: local block only)."""
+    require((geo['h'], geo['m'], geo['stages']) == (H, M, 9), 'h, m, stages')
+    blocks = {}
+    for port in geo['ports']:
+        for r in port['routes']:
+            s, ax = r['stage'], r['axes']
+            require(ax[:H] == list(range(H)), 'route must contain the local block')
+            ext = ax[H:]
+            if s == 0:
+                require(ext == [] and r.get('identity'), 'stage-0 route is the identity')
+                continue
+            require(len(ext) == BLOCK, 'exterior block width')
+            require(blocks.setdefault(s, ext) == ext, 'ports disagree on exterior block')
+    require(sorted(blocks) == list(range(1, 9)), 'exterior blocks 1..8')
+    require(sorted(a for b in blocks.values() for a in b) == list(range(H, M)), 'blocks partition axes 8..63')
+    require(all(blocks[s] == list(range(H + BLOCK * (s - 1), H + BLOCK * s)) for s in blocks), 'block order')
+    return blocks
+
+
+def check_charts(geo):
+    """[q/2 | A_q] is exactly orthogonal: axis 0 <-> span(q), axes 1..7 <-> q-perp (form I_8/2 rescaled)."""
+    require(len(geo['ports']) == 120, '120 ports')
+    for port in geo['ports']:
+        q = [Q(x) for x in port['q']]
+        A = [[Q(x) for x in row] for row in port['complement_columns']]
+        require(len(A) == H and all(len(row) == BLOCK for row in A), 'A_q shape')
+        cols = [[x / 2 for x in q]] + [[A[i][j] for i in range(H)] for j in range(BLOCK)]
+        for i in range(H):
+            for j in range(H):
+                require(sum(a * b for a, b in zip(cols[i], cols[j])) == (1 if i == j else 0),
+                        f'port {port["port"]} chart not orthogonal')
+    return True
+
+
+def level(l, blocks):
+    """Chart axes of data level l. L_-1 = span(q) = axis 0; L_l = local block + E_1..E_l."""
+    if l == -1:
+        return {0}
+    return set(range(H)) | {a for s in range(1, l + 1) for a in blocks[s]}
+
+
+def pending_sets(t, blocks, level_fn=level):
+    idle = [e for e in t['schedule'] if e['kind'] == 'idle']
+    require([e['idx'] for e in idle] == list(range(len(idle))), 'idle indices')
+    out = {}
+    for e in idle:
+        lo, hi = level_fn(e['source_level'], blocks), level_fn(e['target_level'], blocks)
+        require(lo <= hi, 'levels nested')
+        require(len(hi) - len(lo) == e['rank'], f'idle {e["idx"]} rank {e["rank"]} != dim difference')
+        out[e['idx']] = dict(pair=e['pair'], levels=(e['source_level'], e['target_level']), axes=sorted(hi - lo))
+    return out
+
+
+def windows(schedule):
+    """Stages of local invocations strictly between the pair's last local/bridge touch and its idle child."""
+    last, done, out = {}, [], {}
+    for pos, e in enumerate(schedule):
+        if e['kind'] == 'local_cover_sweep':
+            done.append((pos, e['stage'], e['pair'])); last[e['pair']] = pos
+        elif e['kind'] == 'bridge':
+            last[e['dst']] = last[e['src']] = pos
+        elif e['kind'] == 'idle':
+            lo = last.get(e['pair'], -1)
+            out[e['idx']] = {s for p_, s, pr in done if lo < p_ < pos and pr != e['pair']}
+    return out
+
+
+def derive(t, geo, lean=LEAN_PENDING, level_fn=level, routes=None, win_fn=windows):
+    blocks = exterior_blocks(geo)
+    check_charts(geo)
+    pend = pending_sets(t, blocks, level_fn)
+    win = win_fn(t['schedule'])
+    calls = [c for c in t['calls'] if all(c[k] == v for k, v in SELECTED.items())]
+    require(len(calls) == 1, 'selected call unique')
+    owners = calls[0]['owners']
+    require(len(owners) == 987, '987 roles')
+    routes = routes if routes is not None else [o[1] for o in owners[240:]]
+    used = {}
+    for r in routes:
+        if r[0] != 'hosted':
+            continue
+        _, child, off, w = r
+        require(SELECTED['stage'] in win[child], f'stage 2 outside window of child {child}')
+        require(pend[child]['pair'] != SELECTED['pair'], 'host pair is active')
+        require(0 <= off and off + w <= len(pend[child]['axes']), f'route {r} exceeds pending rank')
+        axes = pend[child]['axes'][off:off + w]
+        lean_axes = list(range(lean[child].start + off, lean[child].start + off + w))
+        require(axes == lean_axes, f'route {r}: derived {axes} != Lean {lean_axes}')
+        used.setdefault(child, set()).update(axes)
+    require(sorted(used) == sorted(lean), 'hosted children differ from Lean tags')
+    for child, rng in lean.items():
+        require(list(rng) == pend[child]['axes'], f'Lean range of child {child} != derived pending set')
+        require(used[child] <= set(rng), 'target outside pending range')
+    return dict(
+        exterior_blocks={str(s): [b[0], b[-1] + 1] for s, b in sorted(blocks.items())},
+        hosted_children={str(c): dict(pair=pend[c]['pair'], levels=list(pend[c]['levels']),
+                                      window_stages=sorted(win[c]),
+                                      derived_pending_axes=[pend[c]['axes'][0], pend[c]['axes'][-1] + 1],
+                                      lean_range=[lean[c].start, lean[c].stop],
+                                      hosted_axes_used=len(used[c]),
+                                      pending_rank=len(pend[c]['axes'])) for c in sorted(lean)},
+        idle_ranks_checked=len(pend),
+        hosted_routes=sum(1 for r in routes if r[0] == 'hosted'),
+        ports_checked=len(geo['ports']))
+
+
+def controls(t, geo):
+    owners = next(c for c in t['calls'] if all(c[k] == v for k, v in SELECTED.items()))['owners']
+    base = [o[1] for o in owners[240:]]
+    def shifted_off(rs):
+        out = [list(r) for r in rs]
+        i = next(i for i, r in enumerate(out) if r[0] == 'hosted' and r[1] == 1)
+        out[i][2] += 1
+        return out
+    def no_stage2(s):
+        w = windows(s); w[1] = w[1] - {2}; return w
+    cases = {
+        'child1_previous_level_block': dict(lean={1: range(8, 15), 2: range(1, 29)}),
+        'child2_includes_q_axis': dict(lean={1: range(15, 22), 2: range(0, 28)}),
+        'children_swapped': dict(lean={1: range(1, 29), 2: range(15, 22)}),
+        'level_minus_one_empty': dict(level_fn=lambda l, b: set() if l == -1 else level(l, b)),
+        'route_offset_past_rank': dict(routes=shifted_off(base)),
+        'stage2_outside_window': dict(win_fn=no_stage2),
+    }
+    out = {}
+    for name, kw in cases.items():
+        try:
+            derive(t, geo, **kw)
+            out[name] = 'ACCEPTED'
+        except Reject as e:
+            out[name] = 'rejected: ' + str(e)
+    require(all(v.startswith('rejected') for v in out.values()), f'control accepted: {out}')
+    return out
+
+
+def main():
+    t, geo = load()
+    result = dict(status='PASS_PR540_PENDING_RANGES_DERIVED_FROM_PR442_SCHEDULE',
+                  selected_call=SELECTED, **derive(t, geo), controls=controls(t, geo),
+                  scope='Python derivation from the source schedule and geometry. Not kernel checked. The level model '
+                        'L_-1=span(q), L_l=Q^8+E_1..E_l is PR386 geometry, checked here against every idle rank and '
+                        'route; the ascending order of pending axes within a child is the shared offset convention.')
+    text = json.dumps(result, indent=1, sort_keys=True) + '\n'
+    if len(sys.argv) > 1 and sys.argv[1] == '--write':
+        (HERE / 'RESULT.json').write_text(text)
+    else:
+        require((HERE / 'RESULT.json').read_text() == text, 'RESULT.json differs')
+    print(result['status'])
+
+
+if __name__ == '__main__':
+    try:
+        main()
+    except Reject as e:
+        print('FAIL:', e); sys.exit(1)