diff --git a/research/distinguished-echo-factor/PROOF.md b/research/distinguished-echo-factor/PROOF.md
new file mode 100644
index 0000000000..1319e37b4d
--- /dev/null
+++ b/research/distinguished-echo-factor/PROOF.md
@@ -0,0 +1,171 @@
+# Exact distinguished-factor invocation tariff
+
+This scoped written proof concerns the static ordered, parent-reserved dirty
+array grammar of Koroffstrogov's PR758. It does not claim optimality among
+arbitrary reversible programs. The contribution was produced by Nick Petalas.
+
+## Model and theorem
+
+A leaf is one complete signed invocation of a fixed factor. Every internal
+node has k>=2 nonempty consecutive children. Its complete echo invokes the
+first and last child twice and each interior child four times, including all
+inverses and restoration. Its reserved-array requirement is
+
+    S(leaf)=0,
+    S(node)=k-1+max_child S(child).
+
+The invocation multiplicity of a leaf is the product of its child multipliers
+along its path from the root. This is exactly the quantity multiplying that
+factor's fixed positive invocation price. Factors retain their original order.
+
+The complete echo identity, source preservation and arbitrary dirty-array
+restoration are cited from PR758, Section 1, with androolloyd's PR673 credit
+retained. For ideal linear factors, every admitted tree realizes the same
+ordered product. No new assertion is made that different trees have identical
+rounded nonlinear errors or dirt-dependent increments.
+
+Let s>=0, 1<=n<=2^s, and 0<=i<n be integers. Put L=i and R=n-1-i. For d=0,...,s
+set u_d=2^(s-d). Define d_* as the first depth satisfying
+
+    ceil(L/u_d)+ceil(R/u_d) <= 2^d-1.                  (1)
+
+There is such a depth, since d=s gives L+R=n-1<=2^s-1.
+
+**Theorem.** Among all admitted trees on n leaves with S<=s, the least complete
+invocation multiplicity of factor i is exactly 2^d_*. A binary tree attains it.
+Thus higher arities cannot improve this one-factor objective, even though
+PR758 shows they can improve the sum of all factor prices.
+
+The theorem gives at most s+1 integer tests, once the powers of two are
+available. This is an arithmetic operation count, not a bit-complexity or
+physical tape implementation bound. The bounded reference accepts s<=10.
+The proof itself has no upper bound on s.
+
+## Capacity and replacement along one path
+
+We use PR758, Section 2, as a cited capacity lemma: a tree of requirement at
+most t has at most 2^t leaves, and every positive number at most 2^t fits in a
+binary tree of requirement at most t. The latter also follows by pruning a
+complete height-t binary tree and suppressing unary vertices. This citation
+is a premise, not a replay of the predecessor optimizer or its numerical table.
+
+We first prove that every marked tree of budget s has a binary replacement,
+with the same ordered leaves, budget at most s, and no greater multiplicity
+at its marked leaf. Induct on the number of leaves. At a k-child root let
+r=s-k+1>=0. Every child has at most 2^r leaves.
+
+If the marked child is an endpoint, combine all other children into one
+ordered group. That group has at most
+
+    (k-1)2^r <= 2^(s-1)
+
+leaves, since k-1<=2^(k-2) for k>=2. A binary root can host this group and the
+marked child, each with budget s-1. Replace the group by a fitting binary tree
+and replace the marked child by induction. The marked multiplier at this root
+is still two. The case k=2 is included.
+
+If the marked child is interior then k>=3. Suppose p children precede it and
+q=k-1-p follow it, with p,q>=1. Let A and B be the leaf counts in those two
+ordered groups. Then
+
+    max(A,B) <= (k-2)2^r <= 2^(s-1),
+    min(A,B) <= floor((k-1)/2)2^r <= 2^(s-2).       (2)
+
+For the second inequality use floor((k-1)/2)<=2^(k-3), valid at k=3 and for
+all larger k. The first uses k-2<=2^(k-2). Both are elementary integer
+inequalities and can also be proved by induction on k.
+
+Put the larger group in one child of a binary root. Its other child is a
+binary node containing the smaller group and the marked child, in the order
+required by the original factors. If the left group is larger the shape is
+`(left,(marked,right))`; otherwise it is `((left,marked),right)`. The side
+groups fit by (2), and the marked child fits at budget s-2 because r<=s-2.
+Replace the marked child by induction, using that budget. The distinguished
+path now has two binary edges, with multiplier four, equal to its old
+interior-child multiplier. Its ordered factors and total budget are preserved.
+
+The induction decreases the size of the marked child. Unmarked groups use
+only the cited fitting lemma. This proves binary replacement. No assertion
+about the other factors' multiplicities is made or needed.
+
+## The exact binary depth condition
+
+In a binary tree S is its height and a leaf at depth d has multiplicity 2^d.
+Consider a marked leaf at depth d<=s. At path level j=1,...,d, its sibling
+has capacity at most 2^(s-j). It lies entirely before or entirely after the
+marked leaf in the ordered factor list. Therefore the capacities on the two
+sides have the form
+
+    u_d m,     u_d(2^d-1-m)
+
+for some integer m between zero and 2^d-1. Indeed the sibling capacities are
+u_d times 2^(d-1),...,1, assigned to the two sides according to the path bits.
+Every factor before the marked leaf belongs to a preceding sibling, and the
+same holds for factors after it. Hence
+
+    L <= u_d m,     R <= u_d(2^d-1-m),
+
+which implies (1). Any binary marked leaf consequently has depth at least d_*.
+The replacement result transfers this lower bound to every original arity:
+its binary multiplicity is at least 2^d_* and at most the original multiplicity.
+
+For attainment, choose d=d_* and m=ceil(L/u_d). By (1), there are at least L
+positions in the first m dyadic blocks of size u_d and at least R positions in
+the blocks strictly after block m. In a complete height-s ordered binary tree,
+keep any L leaves in those preceding blocks, one leaf in block m, and any R
+leaves in the following blocks. Delete all other leaves and suppress every
+unary vertex. The resulting ordered tree has exactly n leaves and height at
+most s. All branching inside the marked block disappears, so the marked leaf
+has depth at most d. The already proved lower bound makes its depth exactly d.
+This is a constructive proof for every permitted n,s,i, including n=1,s=0.
+The reference chooses the leftmost available positions on each side and
+constructs the compressed tree bottom up, without recursion.
+
+## A sharp position effect and weighted consequence
+
+For s>=2 and n=2^s-1, the theorem simplifies to
+
+    min multiplicity at i = 2^(s-1), if i is even,
+                            2^s,     if i is odd.   (3)
+
+For d<=s-2, u_d>=4. Even ignoring the separate ceilings, (1) would require
+n-1<=2^s-u_d, but n-1=2^s-2, so it fails. At d=s-1, u_d=2 and L+R=2^s-2.
+When i is even, both sides are even and the ceiling sum is 2^(s-1)-1. When
+i is odd, both are odd and the sum is 2^(s-1). Only the former satisfies (1).
+Depth s always works. This proves (3) without extrapolating from finite checks.
+For seven factors and three arrays the exact vector of individual minima is
+
+    (4,8,4,8,4,8,4).
+
+For any fixed positive prices c_0,...,c_(n-1), every complete schedule costs
+at least sum_i c_i 2^d_*(n,s,i). This follows by applying the individual lower
+bounds to the same tree and adding them. The bound need not be jointly
+attainable. The theorem constructs an optimum for one designated factor at
+a time; it does not solve arbitrary weighted total-cost optimization.
+
+## Evidence boundary and credit
+
+The universal result rests on the replacement and capacity proof above.
+`verify.py` gives finite corroboration of this new quantity using a complete
+all-arity marked recurrence, a separate enumeration of whole ordered trees,
+and emitted binary witnesses. It does not import or replay any predecessor
+executable, counts, supplier or scientific verifier.
+
+Koroffstrogov / PR758 supplies the ordered all-arity weighted grammar and its
+capacity lemma. androolloyd / PR673 supplies the multiway echo and restoration.
+Dillon Amburgey / PR689, Sagar Thakrar / PR730, Ali Romman / PR744, Alexander
+Schwartzman / PR784 and Gareth Davidson / PR887 retain their optimization,
+budget and formalization credit, as does Chafik Boukhalfa / PR628 for the
+rounded-leaf lineage. Nick Petalas / PR4862 concerns maximal equality of a
+total-unit-cost bound; none of its results is used in this proof. Dyadic trees,
+ordered prefix codes and unary suppression are classical. No general
+literature priority is claimed for those methods.
+
+Static parent reservation, nonempty ordered children and complete signed calls
+are essential. Connector reuse, clean checkpoints, changed restoration words,
+opened child bodies, reordered or commuting factors and general reversible
+circuits have different contracts. Physical data movement, actual coefficient
+prices, precision, stock, compiler/native admission, analytic recovery and all
+five selected framework assumptions remain separate. No new kappa, completed
+supplier or complete multiplication theorem follows. Independent human and
+formal proof-kernel review are unclaimed.
diff --git a/research/distinguished-echo-factor/README.md b/research/distinguished-echo-factor/README.md
new file mode 100644
index 0000000000..6cccad4a37
--- /dev/null
+++ b/research/distinguished-echo-factor/README.md
@@ -0,0 +1,124 @@
+# Exact invocation prices for a distinguished dirty-echo factor
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. In the
+ordered parent-reserved dirty-echo tree grammar of Koroffstrogov's
+[PR758](https://github.com/CrocSwap/integer-mult-bounds/pull/758), the exact
+minimum completed invocation multiplicity of factor i among n factors, with
+at most s arbitrary dirty arrays, is
+
+```text
+2^d, where d is the first integer in 0..s satisfying
+ceil(i / 2^(s-d)) + ceil((n-1-i) / 2^(s-d)) <= 2^d - 1.
+```
+
+The domain is `s>=0`, `1<=n<=2^s`, `0<=i<n`. A binary tree attains the minimum,
+even though higher arities can improve the total cost. This is an exact new
+individual-factor price law, not another replay of a predecessor total-cost
+table. All inverses and dirty restoration calls remain in the multipliers.
+
+For `n=2^s-1`, `s>=2`, even-position factors have minimum `2^(s-1)` and
+odd-position factors have minimum `2^s`. For seven factors and three arrays,
+the individual minima are `(4,8,4,8,4,8,4)`. A position-free capacity bound
+misses this factor-of-two difference. Multiplying each individual minimum by
+its fixed invocation price and adding gives a necessary weighted bill; these
+individual optima need not share an attaining tree.
+
+[PROOF.md](PROOF.md) proves the all-size theorem by binary replacement along
+the distinguished path and separate dyadic prefix/suffix capacities.
+`verify.py` supplies a bounded constructor and exact corroboration of the new
+quantity. No predecessor executable, optimizer, count or scientific suite is
+replayed. The source contract and capacity lemma are cited premises.
+
+## Reproduce
+
+From the worktree root with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/distinguished-echo-factor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/distinguished-echo-factor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/distinguished-echo-factor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/distinguished-echo-factor --check-source-history --check-modes
+```
+
+Substitute another CPython 3.12 executable on other machines. The direct check
+prints `PASS_DISTINGUISHED_ECHO_FACTOR` inside a generated JSON receipt with
+computed coverage and SHA256 hashes of all six package files and the one
+source proof. It writes nothing. No receipt is handwritten. Both registered
+commands have a 120-second timeout. The universal theorem rests on the written
+proof; finite execution is not formal proof-kernel acceptance.
+
+The finite checks cover 2,794 all-arity marked optima through space six,
+5,440 whole ordered trees through eight leaves with 93,266 factor comparisons,
+and 43,946 emitted binary witnesses containing 6,435,096 leaf occurrences
+through space eight. The separate parity specialization checks 2,035 positions
+through space ten. Thirteen invalid inputs/trees are rejected and four semantic
+controls pass. Explicit input/tree rejection and semantic controls distinguish
+ceilings from floors, positional from total capacity, and the singleton and
+saturated endpoints. All checks remain active with optimized Python.
+
+## Scope, provenance and credit
+
+The original `joint-query-controller` card is changed to a static composition
+side theorem. It does not fulfill the complete native caller acceptance gate.
+The baseline binding-only check passed; selected PR6030 remains unchanged.
+[SOURCES.json](SOURCES.json) pins canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision eight, and the
+unchanged source proof used as a live text input. The
+[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362439)
+was posted before substantial work. Current main, open/merged/account PR
+searches, active Discussions, handoffs and local reservations were checked.
+Sparse notes, arbitrary historical diffs and unpublished work remain coverage
+limits; these checks do not establish global novelty. The cached card scan
+covered 394 open PRs and 6,334 Discussion records with complete remote paging,
+but only 112 of 8,917 tracked notes were locally materialized at scan time.
+
+Credit Koroffstrogov / PR758 for the ordered all-arity weighted grammar and
+capacity lemma; androolloyd / PR673 for the multiway echo and restoration;
+Dillon Amburgey / PR689, Sagar Thakrar / PR730, Ali Romman / PR744, Alexander
+Schwartzman / PR784, Gareth Davidson / PR887 and Chafik Boukhalfa / PR628 for
+the retained optimization, budget, formalization and rounded-leaf lineage.
+Nick Petalas / PR4862 concerns total-unit-cost equality and is related context,
+without being a theorem used or extended here. Dyadic trees and prefix coding
+are classical. The new contribution is the exact individual multiplicity law,
+its universal replacement/attainment proof and its standalone checker.
+
+The result keeps static parent-reserved arrays, nonempty ordered factors,
+fixed signed invocation prices and complete restoration words. It does not
+cover connector reuse, clean checkpoints, interleaved lifetimes, alternative
+echo identities, opened children, factor reordering or arbitrary reversible
+programs. It does not assert identical rounded errors for different trees.
+The predecessor's unfavorable full-transform adapter remains unfavorable;
+this local theorem does not reopen that unchanged supplier.
+
+No actual native caller, physical movement/storage bill, precision/stock proof,
+compiler admission, analytic recovery or new kappa is supplied. The five
+selected framework assumptions remain. Independent human and formal proof-kernel
+review, predecessor or selected cold replay, Lean and Docker are unrun.
+
+## Open next questions
+
+When can several expensive factors attain their individual minima in one tree?
+Start with two positions and their dyadic path capacities, retaining every
+parent reservation. This theorem supplies no joint-attainment classification
+or complete weighted optimum. The structured question and blocker are in
+[TASK.json](TASK.json). A physical application also needs a distinct favorable
+complete supplier contract before any expansion.
+
+## Verifier bounds
+
+The verifier uses bounded iterative traversals and no recursion, subprocesses,
+network, dynamic code evaluation or file writes. Public constructor inputs are
+capped at 1024 leaves and ten arrays. Witnesses have at most 2047 nodes. The
+all-arity oracle stops at six arrays; whole-tree enumeration stops at eight
+leaves. Every function is below sixty physical lines. Exceptions keep the
+mathematical invariants active under optimization. Each receipt input is a
+regular nonsymlink file of at most 256 KiB.
+
+Power of Ten rules 3 and 9 have managed-runtime deviations: CPython allocates
+integers, tuples, dictionaries and lists, and uses standard-library dispatch.
+Fixed finite domains bound algorithmic live data; no allocation instrumenter
+or separate static type analyzer is claimed. Warning-strict ordinary and
+optimized execution, source inspection and the rejection controls provide the
+available diagnostics. There is no production deployment or fixed-storage claim.
diff --git a/research/distinguished-echo-factor/SOURCES.json b/research/distinguished-echo-factor/SOURCES.json
new file mode 100644
index 0000000000..8588eefe65
--- /dev/null
+++ b/research/distinguished-echo-factor/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/space-capped-dirty-echo/PROOF.md",
+      "usage": "input",
+      "git_blob": "e256de5db9bb947aa15ba5f6c60f3f7927cbcf63",
+      "sha256": "14c90c13b171d3e137560b550b61938e3fdc1a618e69b739d64f862d57bacf09"
+    }
+  ]
+}
diff --git a/research/distinguished-echo-factor/TASK.json b/research/distinguished-echo-factor/TASK.json
new file mode 100644
index 0000000000..805ac10a35
--- /dev/null
+++ b/research/distinguished-echo-factor/TASK.json
@@ -0,0 +1,94 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "joint-query-controller",
+    "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "query demand",
+      "active mode",
+      "5720",
+      "5745",
+      "5747",
+      "caller"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.",
+        "evidence": "research/qq16-caller-install/README.md",
+        "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.",
+        "status": "author-checked",
+        "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact minimum complete invocation multiplicity of one distinguished ordered factor in the all-arity parent-reserved dirty-echo tree grammar, with a binary attaining constructor.",
+  "scope_change_reason": "Original weighted composition side question. This changes the card from a complete selected native caller to a scoped static scheduling theorem; it does not meet supplier admission.",
+  "bottleneck_link": "An expensive factor is charged by its complete invocation multiplicity. The position-sensitive minimum gives a necessary lower bound for any weighted composition invoice. The unchanged unfavorable full-transform adapter is not reopened.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first proved exact multiplicity law and bounded corroboration; package rather than extend to a complete weighted optimization.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and standalone verify.py; exact all-arity marked recurrence, whole-tree enumeration, constructed witnesses and semantic rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "When are the individual multiplicity minima jointly attainable for a specified set of expensive factors?",
+      "why_it_matters": "The sum of the individual weighted bounds may be strict, so a complete priced optimum needs a compatibility condition.",
+      "first_step": "Specify two marked positions and combine their dyadic path capacities, retaining every parent reservation and complete restoration multiplier.",
+      "blocked_by": "This theorem optimizes only one marked factor. No joint attainment classification or complete weighted optimum is supplied."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362439",
+  "overlap_coverage": {
+    "fetched_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "open_prs": 394,
+    "discussion_records": 6334,
+    "remote_pagination_complete": true,
+    "local_notes_searched": 112,
+    "local_notes_tracked": 8917,
+    "scope": "Open remote PR bodies; main README and merged distinctive-term searches supplement sparse local note coverage. No novelty certificate."
+  }
+}
diff --git a/research/distinguished-echo-factor/VERIFY.json b/research/distinguished-echo-factor/VERIFY.json
new file mode 100644
index 0000000000..ced34ef688
--- /dev/null
+++ b/research/distinguished-echo-factor/VERIFY.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/space-capped-dirty-echo/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete all-arity marked recurrence, whole ordered trees, attaining binary witnesses, position/parity law and rejected inputs."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete check under optimized Python, with every explicit invariant active."
+    }
+  ]
+}
diff --git a/research/distinguished-echo-factor/verify.py b/research/distinguished-echo-factor/verify.py
new file mode 100644
index 0000000000..bed332dab5
--- /dev/null
+++ b/research/distinguished-echo-factor/verify.py
@@ -0,0 +1,250 @@
+#!/usr/bin/env python3
+"""Exact distinguished-factor tariffs in ordered reserved-scratch echo trees."""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from pathlib import Path
+
+MAX_SPACE = 10
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def validate(n: int, space: int, index: int) -> None:
+    require(all(type(v) is int for v in (n, space, index)), "integer inputs required")
+    require(0 <= space <= MAX_SPACE, "space outside bounded reference domain")
+    require(1 <= n <= 1 << space, "infeasible factor count")
+    require(0 <= index < n, "factor index outside word")
+
+
+def minimum(n: int, space: int, index: int) -> tuple[int, int]:
+    """Return the exact invocation minimum and its binary depth."""
+    validate(n, space, index)
+    for depth in range(space + 1):
+        unit = 1 << (space - depth)
+        left = (index + unit - 1) // unit
+        right = (n - 1 - index + unit - 1) // unit
+        if left + right <= (1 << depth) - 1:
+            return 1 << depth, depth
+    raise ValueError("feasible word had no admissible depth")
+
+
+def construct(n: int, space: int, index: int) -> tuple[tuple[int, ...], ...]:
+    """Return a postorder binary witness; nodes 0..n-1 are ordered leaves."""
+    _, depth = minimum(n, space, index)
+    unit = 1 << (space - depth)
+    block = (index + unit - 1) // unit
+    positions = list(range(index)) + [block * unit]
+    positions += list(range((block + 1) * unit, (block + 1) * unit + n - 1 - index))
+    require(len(set(positions)) == n and max(positions) < 1 << space, "bad slots")
+    nodes: list[tuple[int, ...]] = [()] * n
+    level = dict(zip(positions, range(n)))
+    for _ in range(space):
+        parents: dict[int, list[int]] = {}
+        for address in sorted(level):
+            parents.setdefault(address // 2, []).append(level[address])
+        level = {}
+        for address, children in parents.items():
+            if len(children) == 1:
+                level[address] = children[0]
+            else:
+                require(len(children) == 2, "nonbinary compressed trie")
+                nodes.append(tuple(children))
+                level[address] = len(nodes) - 1
+    require(list(level.values()) == [len(nodes) - 1], "bad witness root")
+    return tuple(nodes)
+
+
+def inspect_tree(nodes: tuple[tuple[int, ...], ...]) -> tuple[int, tuple[int, ...]]:
+    """Independently evaluate reserved space and all complete-call multipliers."""
+    require(1 <= len(nodes) <= 2047, "tree capacity exceeded")
+    spaces: list[int] = []
+    parents = [0] * len(nodes)
+    leaves = []
+    for number, children in enumerate(nodes):
+        require(isinstance(children, tuple), "children must be immutable")
+        if not children:
+            spaces.append(0)
+            leaves.append(number)
+            continue
+        require(2 <= len(children) <= MAX_SPACE + 1, "invalid arity")
+        require(len(set(children)) == len(children), "duplicate child")
+        require(all(type(c) is int and 0 <= c < number for c in children), "bad edge")
+        for child in children:
+            parents[child] += 1
+        spaces.append(len(children) - 1 + max(spaces[c] for c in children))
+    require(parents == [1] * (len(nodes) - 1) + [0], "not one tree")
+    counts = [0] * len(nodes)
+    counts[-1] = 1
+    order = []
+    stack = [len(nodes) - 1]
+    for _ in range(len(nodes)):
+        require(bool(stack), "early traversal exhaustion")
+        node = stack.pop()
+        children = nodes[node]
+        if not children:
+            order.append(node)
+        for j, child in enumerate(children):
+            counts[child] = counts[node] * (2 if j in (0, len(children) - 1) else 4)
+        stack.extend(reversed(children))
+    require(not stack and order == leaves, "wrong ordered leaf sequence")
+    return spaces[-1], tuple(counts[leaf] for leaf in leaves)
+
+
+def all_arity_oracle(max_space: int) -> list[dict[tuple[int, int], int]]:
+    """Minimize one leaf's count over all root arities and sibling sizes."""
+    require(0 <= max_space <= 6, "oracle capacity exceeded")
+    tables: list[dict[tuple[int, int], int]] = []
+    for space in range(max_space + 1):
+        table = {(0, 0): 1}
+        for arity in range(2, space + 2):
+            remaining = space - arity + 1
+            capacity = 1 << remaining
+            for slot in range(arity):
+                multiplier = 2 if slot in (0, arity - 1) else 4
+                for (a, b), price in tables[remaining].items():
+                    for left in range(slot, slot * capacity + 1):
+                        after = arity - 1 - slot
+                        for right in range(after, after * capacity + 1):
+                            key = (a + left, b + right)
+                            candidate = multiplier * price
+                            table[key] = min(table.get(key, (1 << space) + 1), candidate)
+        require(len(table) == (1 << space) * ((1 << space) + 1) // 2, "oracle coverage")
+        tables.append(table)
+    return tables
+
+
+def whole_trees(limit: int) -> list[list[tuple[int, tuple[int, ...]]]]:
+    """Enumerate every ordered tree, retaining space and its entire count vector."""
+    require(1 <= limit <= 8, "whole-tree capacity exceeded")
+    families: list[list[tuple[int, tuple[int, ...]]]] = [[], [(0, (1,))]]
+    for size in range(2, limit + 1):
+        rows = []
+        for arity in range(2, size + 1):
+            # A partial ordered forest stores used leaves, peak child space and counts.
+            forest = [(0, 0, ())]
+            for slot in range(arity):
+                next_forest = []
+                for used, peak, counts in forest:
+                    remaining = arity - slot - 1
+                    for child_size in range(1, size - used - remaining + 1):
+                        for child_space, child_counts in families[child_size]:
+                            factor = 2 if slot in (0, arity - 1) else 4
+                            new_counts = counts + tuple(factor * c for c in child_counts)
+                            next_forest.append((used + child_size, max(peak, child_space), new_counts))
+                forest = next_forest
+            rows.extend((arity - 1 + peak, counts) for used, peak, counts in forest if used == size)
+        families.append(rows)
+    return families
+
+
+def check_oracles() -> dict[str, int]:
+    tables = all_arity_oracle(6)
+    oracle_cases = 0
+    for space, table in enumerate(tables):
+        for (left, right), price in table.items():
+            require(price == minimum(left + right + 1, space, left)[0], "oracle disagreement")
+            oracle_cases += 1
+    tree_count = comparisons = 0
+    best: dict[tuple[int, int, int], int] = {}
+    for size, family in enumerate(whole_trees(8)):
+        for used, counts in family:
+            tree_count += 1
+            for space in range(used, 8):
+                for index, price in enumerate(counts):
+                    key = (size, space, index)
+                    best[key] = min(best.get(key, price), price)
+                    require(price >= minimum(size, space, index)[0], "whole-tree lower bound")
+                    comparisons += 1
+    for (size, space, index), price in best.items():
+        require(price == minimum(size, space, index)[0], "whole-tree optimum")
+    return {"all_arity_cases": oracle_cases, "whole_trees": tree_count,
+            "whole_tree_factor_comparisons": comparisons, "whole_tree_optima": len(best)}
+
+
+def check_witnesses() -> dict[str, int]:
+    witnesses = leaves = 0
+    for space in range(9):
+        for size in range(1, (1 << space) + 1):
+            for index in range(size):
+                nodes = construct(size, space, index)
+                used, counts = inspect_tree(nodes)
+                require(used <= space and len(counts) == size, "witness contract")
+                require(counts[index] == minimum(size, space, index)[0], "nonattaining witness")
+                witnesses += 1
+                leaves += size
+    parity_cases = 0
+    for space in range(2, 11):
+        size = (1 << space) - 1
+        for index in range(size):
+            expected = (1 << space) if index % 2 else (1 << (space - 1))
+            require(minimum(size, space, index)[0] == expected, "parity corollary")
+            parity_cases += 1
+    require([minimum(7, 3, i)[0] for i in range(7)] == [4, 8, 4, 8, 4, 8, 4], "fixture")
+    return {"constructed_witnesses": witnesses, "witness_leaf_occurrences": leaves,
+            "parity_cases": parity_cases}
+
+
+def check_controls() -> dict[str, int]:
+    bad = ((0, 0, 0), (2, 0, 0), (1, -1, 0), (1, 11, 0), (2, 1, -1),
+           (2, 1, 2), (True, 1, 0), (1, 1.0, 0))
+    rejected = 0
+    for args in bad:
+        try:
+            minimum(*args)
+        except ValueError:
+            rejected += 1
+    require(rejected == len(bad), "input control accepted")
+    invalid_trees = ((), ((), (0,)), ((), (0, 0)), ((), (0, 2)), ((), (), (1, 0)))
+    for nodes in invalid_trees:
+        try:
+            inspect_tree(nodes)
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("malformed tree accepted")
+    # Position-free capacity and one-floor rounding give false cheap odd positions.
+    require(minimum(7, 3, 1)[0] > 4, "position-free false tariff survived")
+    require(1 // 2 + 5 // 2 <= 3 and minimum(7, 3, 1)[0] == 8, "floor mutant survived")
+    require(minimum(1, 0, 0) == (1, 0), "single-factor boundary")
+    require(minimum(8, 3, 0)[0] == 8, "saturated-capacity boundary")
+    return {"rejected_inputs_and_trees": rejected, "semantic_controls": 4}
+
+
+def source_hashes() -> dict[str, str]:
+    package = Path(__file__).resolve().parent
+    source_manifest = json.loads((package / "SOURCES.json").read_text())
+    sources = source_manifest["files"]
+    require(len(sources) <= 8, "source capacity exceeded")
+    files = [package / name for name in
+             ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")]
+    for row in sources:
+        if row["usage"] == "input":
+            path = package.parent.parent / row["path"]
+            require(path.is_file() and not path.is_symlink(), "missing source proof")
+            require(path.stat().st_size <= 262144, "source size exceeded")
+            require(hashlib.sha256(path.read_bytes()).hexdigest() == row["sha256"], "source hash")
+            files.append(path)
+    require(len(files) == 7, "unexpected receipt inputs")
+    hashes = {}
+    for path in files:
+        require(path.is_file() and not path.is_symlink(), "invalid receipt file")
+        require(path.stat().st_size <= 262144, "receipt input too large")
+        hashes[str(path.relative_to(package.parent.parent))] = hashlib.sha256(path.read_bytes()).hexdigest()
+    return hashes
+
+
+def main() -> None:
+    hashes = source_hashes()
+    result = {"status": "PASS_DISTINGUISHED_ECHO_FACTOR", "no_new_kappa": True,
+              **check_oracles(), **check_witnesses(), **check_controls(), "sha256": hashes}
+    print(json.dumps(result, sort_keys=True, indent=2))
+
+
+if __name__ == "__main__":
+    main()