diff --git a/research/mixed-rank-touching-envelope/EXAMPLE.json b/research/mixed-rank-touching-envelope/EXAMPLE.json
new file mode 100644
index 0000000000..5657901c04
--- /dev/null
+++ b/research/mixed-rank-touching-envelope/EXAMPLE.json
@@ -0,0 +1,24 @@
+{
+  "schema": "synchronized-invoice-envelope/v1",
+  "old": {
+    "schema": "integer-mult-recursive-invoice/v1",
+    "contract": {
+      "model": "synthetic signed power invoice",
+      "boundary": "arithmetic example; no physical supplier",
+      "rank_semantics": "H_r costs r^t"
+    },
+    "paid": {"4": 3, "9": 2, "7": 11},
+    "targets": {"5": 13}
+  },
+  "new": {
+    "schema": "integer-mult-recursive-invoice/v1",
+    "contract": {
+      "model": "synthetic signed power invoice",
+      "boundary": "arithmetic example; no physical supplier",
+      "rank_semantics": "H_r costs r^t"
+    },
+    "paid": {"1": 6, "36": 1, "7": 11},
+    "targets": {"5": 13}
+  },
+  "certificate": {"bases": [2, 3], "p": 1, "q": 2, "scale": 1, "offset": 0}
+}
diff --git a/research/mixed-rank-touching-envelope/PROOF.md b/research/mixed-rank-touching-envelope/PROOF.md
new file mode 100644
index 0000000000..da979b3ae5
--- /dev/null
+++ b/research/mixed-rank-touching-envelope/PROOF.md
@@ -0,0 +1,121 @@
+# Sharp synchronized mixed-rank invoice envelopes
+
+Let m be a positive even integer, let a_1,...,a_m be integers greater than
+one, let p,q be integers with 0<p<q, and let lambda>0 and epsilon>=0 be real.
+Define
+
+```text
+D(t) = epsilon + lambda product_(i=1)^m (a_i^(q t) - a_i^p).
+```
+
+Then D has global minimum epsilon on the whole real line. Its unique minimizer
+is t=p/q, which lies inside (0,1). If epsilon=0, its only real zero has exactly
+m-fold multiplicity. If epsilon>0, D is strictly positive everywhere.
+
+## Proof
+
+Each factor is strictly increasing. It vanishes exactly at p/q, is negative
+below p/q, and is positive above p/q. All m factors therefore have the same
+nonzero sign away from p/q. Their product is positive because m is even.
+At p/q the product vanishes. Positivity of lambda proves both the minimum
+and its unique location.
+
+The derivative of the i-th factor at p/q is
+q log(a_i) a_i^p>0. Its zero is simple. The product of m analytic functions
+with simple zeros at the same point has a zero of exact multiplicity m.
+Adding a positive epsilon removes all zeros, while leaving the minimizer
+and the sharp lower envelope unchanged. This proves every claim.
+
+## Exact signed invoices
+
+Suppose lambda and epsilon are nonnegative integers, with lambda positive.
+Expansion gives
+
+```text
+D(t) = epsilon + lambda sum_(S subset {1,...,m})
+          (-1)^(m-|S|) (product_(i not in S) a_i^p)
+                         (product_(i in S) a_i^q)^t.
+```
+
+All ranks and signed coefficients are integers. Equal subset products must be
+combined before comparison. No independence or distinctness of the bases is
+assumed. Put positive coefficients into the new paid histogram and negated
+negative coefficients into the old paid histogram. This realizes the signed
+difference as two nonnegative integer invoices. More generally, the checker
+accepts any placement in paid and target histograms whose full net difference
+is this polynomial. Identical arbitrary paid and target charges on both sides
+cancel. This is arithmetic realization, not a physical construction.
+
+For rational positive lambda and nonnegative epsilon, clearing their common
+denominator gives the same integer-certificate form with the correspondingly
+scaled envelope. The executable accepts the integer form only.
+
+## First mixed-rank example
+
+For m=2, a_1=2, a_2=3, p=1 and q=2,
+
+```text
+6 - 3*4^t - 2*9^t + 36^t = (4^t-2)(9^t-3) >= 0.
+```
+
+Equality holds only at t=1/2 and has exact multiplicity two. Thus the seven-job
+invoice 6 H1 + H36 costs at least the five-job invoice 3 H4 + 2 H9 for every
+power tariff, with equality at sqrt-rank pricing. Adding one H1 to the former
+gives sharp minimum gap one for every real t. Swapping the invoices reverses
+the ordering, but is not claimed to implement a cheaper physical circuit.
+
+The ranks 4 and 9 are not powers of a common integer greater than one, since
+that integer would have a prime divisor dividing both ranks. This supplies a
+genuinely mixed-rank example. There are two coefficient sign changes, and
+neither endpoint is zero. A closure rule using simple interior witnesses alone
+cannot spend a two-root budget on this double zero. The factor certificate
+supplies its multiplicity directly. This is an implication from the documented
+certificate rules in #5788, not a replay or audit of its implementation.
+
+With two distinct prime bases a,b, arbitrary 0<p<q, and offset epsilon, the
+four coefficients are epsilon+a^p b^p, -b^p, -a^p, and 1 at ranks
+1,a^q,b^q,(ab)^q. This gives an infinite family with the same sharp envelope.
+
+## Checker soundness and scope
+
+`envelope.py` parses both complete invoice histograms and identical declared
+contracts. It forms new-paid minus new-targets minus old-paid plus old-targets.
+It separately expands the supplied factors by repeated sparse multiplication,
+combines collisions, and requires exact coefficient equality. The theorem then
+justifies its reported envelope, minimizer and zero multiplicity. A matching
+contract string does not establish that either invoice describes a circuit.
+
+The verifier has no numeric root search, logarithm approximation or predecessor
+executable dependency. `verify.py` corroborates expansion independently by a
+literal subset formula, executes exact rational-power checks at exponents whose
+denominators divide q, tests target debits, and rejects mutated certificates.
+It does not use finite samples as the proof of a continuum claim.
+
+The executable bounds factors to an even count from two through eight, bases
+to 2..64, q to 2..16, expanded ranks to 10^9, histogram counts to 10^60,
+each histogram to 4096 keys, and each input to one MiB. Sparse multiplication
+has at most 256 terms per step; all loops have finite bounds from these
+capacities. The mathematical theorem has no such finite capacities. Managed
+Python allocation is a Power of Ten deviation, bounded here by input and
+support capacities; standard-library parser allocation is not statically
+preallocated. The isolated registered normal and optimized runs use the same
+explicit checks, which remain active without assertions. No shared modules
+or source pins are changed.
+
+## Predecessors and remaining obligations
+
+Ali Romman's [#5788](https://github.com/CrocSwap/integer-mult-bounds/pull/5788)
+poses the explicit touching-root continuation and supplies the general-rank
+root-budget context. Its proof and limitations are cited, not reverified.
+The signed-invoice interface is due to zxv, the moment-order context to
+mightyOil and predecessors, and the specialized T16 crossing work to woklerx.
+The factor expansion and elementary sign argument are standard algebra and
+calculus. The contribution is their exact synchronized-envelope application,
+integer invoice family and portable certificate checker; no literature
+priority for these elementary methods is claimed.
+
+There is no source-bound physical bill, native implementation, ownership or
+restoration proof, compiler admission, new kappa or complete multiplication
+theorem. Independent human and formal proof-kernel review are unclaimed.
+
+New work produced by Nick Petalas. Apache-2.0.
diff --git a/research/mixed-rank-touching-envelope/README.md b/research/mixed-rank-touching-envelope/README.md
new file mode 100644
index 0000000000..9830775193
--- /dev/null
+++ b/research/mixed-rank-touching-envelope/README.md
@@ -0,0 +1,118 @@
+# Sharp mixed-rank invoice envelopes with an interior touching point
+
+For every positive even m, integers a_i>1 and 0<p<q, lambda>0 and epsilon>=0,
+
+```text
+epsilon + lambda product_i (a_i^(q t) - a_i^p)
+```
+
+has sharp global minimum epsilon, attained uniquely at t=p/q. At epsilon=0,
+the unique zero has exact multiplicity m. The written [proof](PROOF.md) covers
+all real t and arbitrary finite even m. This is a **scoped algebraic proof**,
+with finite executable corroboration. It is an arithmetic side result, with
+no physical construction or new kappa claim.
+
+The first example is
+
+```text
+6 H1 + H36 - 3 H4 - 2 H9
+  = (4^t-2)(9^t-3) >= 0,
+```
+
+where H_r costs r^t. Equality holds only at t=1/2 and is a double zero. Adding
+one H1 makes the sharp minimum gap one. Ranks 4 and 9 have no common integer
+base. This resolves the touching-point obligation for this explicit infinite
+family without numeric root isolation or exhaustion of a global root budget.
+
+## Scope and predecessors
+
+The question is the touching-root continuation in Ali Romman's
+[#5788](https://github.com/CrocSwap/integer-mult-bounds/pull/5788), pinned at
+`56565b9aec29203bddb14f5d0e76a657d7090699`. Its
+[proof and limitation](https://github.com/aliromman/integer-mult-bounds/blob/56565b9aec29203bddb14f5d0e76a657d7090699/docs/research/recursive-power-variation.md)
+are cited, not audited or replayed. Credit zxv for signed-invoice accounting,
+mightyOil for the moment-order context, and woklerx for the specialized
+crossing predecessor. Elementary factorization and calculus retain their
+classical status; no literature priority is claimed for those methods.
+
+This changes the `independent-moment` card from checking an existing supplier
+to constructing a new exact invoice family and certificate. The card's first
+selected-baseline binding command passed; no scientific predecessor replay
+was run. [TASK.json](TASK.json) records the changed scope and source URL.
+[SOURCES.json](SOURCES.json) binds the revision-8 catalogue and selected record
+as historical provenance, with no live mathematical predecessor dependency.
+
+The complete signed difference is new paid minus new targets minus old paid
+plus old targets. `envelope.py` requires equal declared contracts and exact
+agreement with an independently supplied sparse factor certificate. Equal
+subset-product ranks are combined, including repeated bases. The executable
+reports the sharp envelope only after this identity check. Matching contract
+text does not prove a source-to-circuit interpretation.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/mixed-rank-touching-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/mixed-rank-touching-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mixed-rank-touching-envelope
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mixed-rank-touching-envelope --check-source-history
+```
+
+The first two commands print a generated JSON receipt with package/input hashes,
+then `PASS_MIXED_RANK_TOUCHING_ENVELOPE`. They enumerate 696 factor contexts,
+4,176 certificates, 49,944 expanded support entries and 23,472 exact
+rational-power evaluations, with 26 rejection or mathematical failure controls.
+Two-factor contexts use every ordered pair of bases in 2..7, q in 2..5 and
+1<=p<q. Higher-factor contexts use every tuple over {2,3} of lengths 4,6,8,
+with p=1,q=2. Each context uses scales 1,3 and offsets 0,1,7. Paid and target
+placement alternates across certificates. These are finite corroboration of
+the written proof, not a finite substitute for its continuum argument.
+
+Inspect the portable authored example directly:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/mixed-rank-touching-envelope/envelope.py research/mixed-rank-touching-envelope/EXAMPLE.json
+```
+
+Expected minimum is 0, unique minimizer is 1/2, and root multiplicity is 2.
+The checker and verifier write no files. Redirect receipts outside the checkout
+if needed. Local checks use CPython 3.12.15 on Darwin arm64; no native packages
+are required. Hosted CI status belongs to the PR, not to this proof.
+
+## Limits
+
+The checker accepts 2,4,6,8 synchronized factors, integer bases 2..64,
+2<=q<=16, 1<=p<q, integer scale in 1..10^60 and offset in 0..10^60.
+Expanded ranks must be at most 10^9 and coefficients at most 10^60.
+Each histogram has at most 4096 keys; input files have at most one MiB.
+The mathematical theorem is not restricted to these executable capacities.
+Certificate discovery, unsynchronized touching points and arbitrary
+exponential-polynomial classification remain outside the checker.
+
+The example is synthetic. Source extraction, native implementation, ownership,
+restoration, physical target independence, supplier/compiler admission, the
+selected cold replay, Lean and a complete multiplication theorem are unclaimed.
+Independent human and formal proof-kernel review are unclaimed. The selected
+frontier and its five framework assumptions retain their existing status.
+
+## Open next questions
+
+Can an actual changed construction's complete signed invoice admit this factor
+certificate after a justified common bill cancels? Start with one published
+source-bound old/new pair and test exact sparse divisibility. This would turn
+the arithmetic envelope into a useful source comparison. The blocker is a
+complete physical bill, not finer sampling of the synthetic example.
+
+Can exact factor certificates treat several distinct touching points without
+assuming a decidable equality test for arbitrary logarithmic root ratios?
+Start with factors whose roots are supplied rational exponents and group them
+by exact rational equality. This would broaden the certified class. Root
+recognition beyond that stated rational domain remains unresolved here.
+
+## Credit
+
+New proof application, integer invoice family and portable certificate checker
+produced by Nick Petalas. Predecessor credit is retained above and in the proof.
+New work is Apache-2.0.
diff --git a/research/mixed-rank-touching-envelope/SOURCES.json b/research/mixed-rank-touching-envelope/SOURCES.json
new file mode 100644
index 0000000000..fdb80ada25
--- /dev/null
+++ b/research/mixed-rank-touching-envelope/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}
diff --git a/research/mixed-rank-touching-envelope/TASK.json b/research/mixed-rank-touching-envelope/TASK.json
new file mode 100644
index 0000000000..dd6b1c2cf1
--- /dev/null
+++ b/research/mixed-rank-touching-envelope/TASK.json
@@ -0,0 +1,118 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?",
+    "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",
+      "docs/research/recursive-invoice-preflight.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": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.",
+    "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": [
+      "invoice",
+      "signed moment",
+      "productive target",
+      "independent recount"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "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": "Prove the sharp synchronized-factor mixed-rank invoice envelope, its unique rational minimizer and exact touching-root multiplicity; construct and check portable integer invoices.",
+  "scope_change_reason": "Take the explicit touching-root continuation in Ali Romman PR5788 as an arithmetic side result. This replaces auditing a supplier with a new invoice family and factor-certificate checker; no predecessor result is audited or replayed.",
+  "bottleneck_link": "Exact paid-minus-target envelopes can settle power-cost comparisons that lack simple-root witnesses. These synthetic invoices have no claimed physical supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first sharp proved envelope with a bounded exact certificate replay; leave source-bound installation and unsynchronized roots open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the all-real-exponent envelope and multiplicity. verify.py passes 696 contexts, 4176 certificates, 49944 expanded support entries, 23472 exact rational-power evaluations and 26 controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does an actual construction's complete signed invoice admit a synchronized factor certificate after a justified common bill cancels?",
+      "why_it_matters": "It would apply the sharp envelope to a physical source comparison.",
+      "first_step": "Choose one source-bound old/new invoice pair and test exact sparse divisibility.",
+      "blocked_by": "A complete physical old/new bill has not been supplied here."
+    },
+    {
+      "question": "Can several rational touching points be certified by exact factor groups?",
+      "why_it_matters": "It would broaden the handled invoice class without numerical root sampling.",
+      "first_step": "Require supplied rational root exponents and group factors by exact rational equality.",
+      "blocked_by": "Certificate discovery and roots outside that rational domain are unresolved."
+    }
+  ],
+  "question_source": {
+    "pr": 5788,
+    "author": "Ali Romman",
+    "head": "56565b9aec29203bddb14f5d0e76a657d7090699",
+    "url": "https://github.com/aliromman/integer-mult-bounds/blob/56565b9aec29203bddb14f5d0e76a657d7090699/docs/research/recursive-power-variation.md",
+    "usage": "Question and comparison context only; no live executable dependency."
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215603",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "Darwin arm64",
+    "requirements": "standard library only"
+  }
+}
diff --git a/research/mixed-rank-touching-envelope/VERIFY.json b/research/mixed-rank-touching-envelope/VERIFY.json
new file mode 100644
index 0000000000..9a4918022e
--- /dev/null
+++ b/research/mixed-rank-touching-envelope/VERIFY.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Independent subset expansion, complete stated 696-context domain, paid and target placements, exact rational-power points, bounded certificate controls and real CLI input hashes; generated stdout receipt binds package bytes."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Independent subset expansion, complete stated 696-context domain, paid and target placements, exact rational-power points, bounded certificate controls and real CLI input hashes; generated stdout receipt binds package bytes."
+    }
+  ]
+}
diff --git a/research/mixed-rank-touching-envelope/envelope.py b/research/mixed-rank-touching-envelope/envelope.py
new file mode 100644
index 0000000000..229f679ed2
--- /dev/null
+++ b/research/mixed-rank-touching-envelope/envelope.py
@@ -0,0 +1,150 @@
+"""Check a synchronized-factor lower envelope for signed power invoices.
+
+New work produced by Nick Petalas. Apache-2.0.
+"""
+
+import argparse
+import hashlib
+import json
+from pathlib import Path
+
+
+MAX_RANK = 10**9
+MAX_COUNT = 10**60
+MAX_BYTES = 1024**2
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def integer(value, low, high):
+    require(type(value) is int and low <= value <= high, "integer outside capacity")
+    return value
+
+
+def fields(value, names):
+    require(type(value) is dict and set(value) == set(names), "unexpected fields")
+
+
+def unique_object(pairs):
+    result = {}
+    for key, value in pairs:
+        require(key not in result, "duplicate JSON key")
+        result[key] = value
+    return result
+
+
+def reject_number(value):
+    raise ValueError("noninteger JSON number: " + value)
+
+
+def load(path):
+    with Path(path).open("rb") as stream:
+        raw = stream.read(MAX_BYTES + 1)
+    return decode(raw), hashlib.sha256(raw).hexdigest()
+
+
+def decode(raw):
+    require(len(raw) <= MAX_BYTES, "input exceeds one MiB")
+    return json.loads(raw, object_pairs_hook=unique_object,
+                      parse_float=reject_number, parse_constant=reject_number)
+
+
+def histogram(value):
+    require(type(value) is dict and len(value) <= 4096, "invalid histogram")
+    result = {}
+    for text, count in value.items():
+        require(type(text) is str and text.isascii() and text.isdecimal(), "invalid rank")
+        require(len(text) <= 10, "rank spelling exceeds capacity")
+        rank = integer(int(text), 1, MAX_RANK)
+        require(str(rank) == text, "noncanonical rank")
+        count = integer(count, 0, MAX_COUNT)
+        if count:
+            result[rank] = count
+    return result
+
+
+def invoice(value):
+    fields(value, ("schema", "contract", "paid", "targets"))
+    require(value["schema"] == "integer-mult-recursive-invoice/v1", "wrong invoice schema")
+    require(type(value["contract"]) is dict and bool(value["contract"]), "missing contract")
+    return histogram(value["paid"]), histogram(value["targets"])
+
+
+def difference(old, new):
+    old_paid, old_targets = invoice(old)
+    new_paid, new_targets = invoice(new)
+    # Canonical JSON distinguishes numeric values from Boolean aliases.
+    old_contract = json.dumps(old["contract"], sort_keys=True, separators=(",", ":"))
+    new_contract = json.dumps(new["contract"], sort_keys=True, separators=(",", ":"))
+    require(old_contract == new_contract, "accounting contracts differ")
+    result = {}
+    for values, sign in ((new_paid, 1), (new_targets, -1),
+                         (old_paid, -1), (old_targets, 1)):
+        for rank, count in values.items():
+            result[rank] = result.get(rank, 0) + sign * count
+    return {rank: count for rank, count in result.items() if count}
+
+
+def expand(certificate):
+    fields(certificate, ("bases", "p", "q", "scale", "offset"))
+    bases = certificate["bases"]
+    require(type(bases) is list and 2 <= len(bases) <= 8, "factor count outside capacity")
+    require(len(bases) % 2 == 0, "odd number of synchronized factors")
+    q = integer(certificate["q"], 2, 16)
+    p = integer(certificate["p"], 1, q - 1)
+    scale = integer(certificate["scale"], 1, MAX_COUNT)
+    offset = integer(certificate["offset"], 0, MAX_COUNT)
+    result = {1: scale}
+    for value in bases:
+        base = integer(value, 2, 64)
+        rank_factor, constant = base**q, base**p
+        next_result = {}
+        for rank, count in result.items():
+            require(rank * rank_factor <= MAX_RANK, "expanded rank outside capacity")
+            next_result[rank] = next_result.get(rank, 0) - constant * count
+            high_rank = rank * rank_factor
+            next_result[high_rank] = next_result.get(high_rank, 0) + count
+        result = {rank: count for rank, count in next_result.items() if count}
+        require(len(result) <= 256, "expanded support outside capacity")
+    result[1] = result.get(1, 0) + offset
+    require(all(abs(count) <= MAX_COUNT for count in result.values()), "coefficient outside capacity")
+    return {rank: count for rank, count in result.items() if count}
+
+
+def check(document):
+    fields(document, ("schema", "old", "new", "certificate"))
+    require(document["schema"] == "synchronized-invoice-envelope/v1", "wrong envelope schema")
+    expected = expand(document["certificate"])
+    actual = difference(document["old"], document["new"])
+    require(actual == expected, "signed invoice does not match factor certificate")
+    cert = document["certificate"]
+    return {
+        "claim_type": "scoped algebraic proof certificate",
+        "difference": "new paid-minus-target cost minus old paid-minus-target cost",
+        "domain": "every real t; in particular 0<t<1",
+        "minimum": cert["offset"],
+        "unique_minimizer": {"numerator": cert["p"], "denominator": cert["q"]},
+        "root_multiplicity": len(cert["bases"]) if cert["offset"] == 0 else 0,
+        "order": "nonnegative with one equality" if cert["offset"] == 0 else "strictly positive",
+        "support_size": len(expected),
+    }
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("input", type=Path)
+    args = parser.parse_args()
+    try:
+        document, digest = load(args.input)
+        result = check(document)
+    except (OSError, ValueError, TypeError, RecursionError) as error:
+        parser.error(str(error))
+    result["input_sha256"] = digest
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()
diff --git a/research/mixed-rank-touching-envelope/verify.py b/research/mixed-rank-touching-envelope/verify.py
new file mode 100644
index 0000000000..3f117b5412
--- /dev/null
+++ b/research/mixed-rank-touching-envelope/verify.py
@@ -0,0 +1,182 @@
+"""Finite corroboration of the synchronized-envelope proof; no files written.
+
+New work produced by Nick Petalas. Apache-2.0.
+"""
+
+import copy
+from fractions import Fraction
+import hashlib
+import itertools
+import json
+from math import prod
+from pathlib import Path
+import subprocess
+import sys
+
+import envelope
+
+
+ROOT = Path(__file__).resolve().parent
+
+
+def ensure(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def subset_expansion(bases, p, q, scale, offset):
+    """Independent literal subset formula, not repeated sparse multiplication."""
+    result = {1: offset}
+    for mask in range(1 << len(bases)):
+        chosen = [base for i, base in enumerate(bases) if mask & (1 << i)]
+        absent = [base for i, base in enumerate(bases) if not mask & (1 << i)]
+        rank = prod(chosen)**q
+        coefficient = scale * (-1)**len(absent) * prod(absent)**p
+        result[rank] = result.get(rank, 0) + coefficient
+    return {rank: count for rank, count in result.items() if count}
+
+
+def document(bases, p, q, scale, offset, use_targets):
+    values = subset_expansion(bases, p, q, scale, offset)
+    old = {"schema": "integer-mult-recursive-invoice/v1",
+           "contract": {"model": "finite synthetic power-invoice control"},
+           "paid": {"13": 17}, "targets": {"11": 19}}
+    new = copy.deepcopy(old)
+    for rank, count in values.items():
+        if use_targets:
+            owner, kind = (old, "targets") if count > 0 else (new, "targets")
+        else:
+            owner, kind = (new, "paid") if count > 0 else (old, "paid")
+        key = str(rank)
+        owner[kind][key] = owner[kind].get(key, 0) + abs(count)
+    return {"schema": "synchronized-invoice-envelope/v1", "old": old, "new": new,
+            "certificate": {"bases": list(bases), "p": p, "q": q,
+                            "scale": scale, "offset": offset}}
+
+
+def integer_root(value, q):
+    low, high = 1, value
+    for _ in range(31):
+        if low >= high:
+            break
+        middle = (low + high) // 2
+        if middle**q < value:
+            low = middle + 1
+        else:
+            high = middle
+    ensure(low == high and low**q == value, "rank is not an exact q-th power")
+    return low
+
+
+def exact_points(doc, coefficients):
+    cert = doc["certificate"]
+    p, q = cert["p"], cert["q"]
+    roots = {rank: integer_root(rank, q) for rank in coefficients}
+    count = 0
+    for numerator in sorted({-1, 0, p - 1, p, p + 1, q, q + 1}):
+        value = sum(Fraction(coefficient) * Fraction(roots[rank])**numerator
+                    for rank, coefficient in coefficients.items())
+        factor = Fraction(cert["scale"]) * prod(
+            Fraction(base)**numerator - base**p for base in cert["bases"])
+        ensure(value == factor + cert["offset"], "rational-power evaluation disagrees")
+        ensure(value >= cert["offset"], "claimed envelope fails at exact point")
+        ensure((value == cert["offset"]) == (numerator == p), "wrong equality point")
+        count += 1
+    return count
+
+
+def positive_cases():
+    contexts = [(bases, p, q) for bases in itertools.product(range(2, 8), repeat=2)
+                for q in range(2, 6) for p in range(1, q)]
+    for length in (4, 6, 8):
+        contexts.extend((bases, 1, 2) for bases in itertools.product((2, 3), repeat=length))
+    cases = points = terms = 0
+    for bases, p, q in contexts:
+        for scale, offset in itertools.product((1, 3), (0, 1, 7)):
+            doc = document(bases, p, q, scale, offset, bool(cases % 2))
+            coefficients = subset_expansion(bases, p, q, scale, offset)
+            result = envelope.check(doc)
+            ensure(envelope.expand(doc["certificate"]) == coefficients, "expansions differ")
+            ensure(result["minimum"] == offset, "wrong minimum")
+            ensure(result["root_multiplicity"] == (len(bases) if offset == 0 else 0),
+                   "wrong multiplicity")
+            points += exact_points(doc, coefficients)
+            terms += len(coefficients)
+            cases += 1
+    return {"contexts": len(contexts), "certificates": cases,
+            "exact_rational_points": points, "expanded_support_entries": terms}
+
+
+def rejected(call):
+    try:
+        call()
+    except (ValueError, TypeError):
+        return
+    raise ValueError("invalid certificate was accepted")
+
+
+def negative_cases(example):
+    mutations = []
+    for key, value in (("bases", [2, 3, 5]), ("bases", [True, 3]),
+                       ("bases", [1, 3]), ("bases", [2] * 10),
+                       ("bases", [64, 64]), ("p", 0), ("p", 2),
+                       ("q", 17), ("scale", 0), ("scale", True),
+                       ("offset", -1), ("offset", 1)):
+        candidate = copy.deepcopy(example)
+        candidate["certificate"][key] = value
+        if value == [64, 64]:
+            candidate["certificate"]["q"] = 16
+        mutations.append(candidate)
+    for side, kind, key, value in (("new", "targets", "5", 12),
+                                    ("old", "targets", "5", 12),
+                                    ("new", "paid", "36", 2),
+                                    ("old", "paid", "4", True),
+                                    ("old", "paid", "04", 3),
+                                    ("new", "paid", "1000000001", 1),
+                                    ("new", "paid", "2", 10**60 + 1)):
+        candidate = copy.deepcopy(example)
+        candidate[side][kind][key] = value
+        mutations.append(candidate)
+    candidate = copy.deepcopy(example)
+    candidate["new"]["contract"]["model"] = "changed model"
+    mutations.append(candidate)
+    candidate = copy.deepcopy(example)
+    candidate["certificate"]["untrusted_claim"] = "positive"
+    mutations.append(candidate)
+    for candidate in mutations:
+        rejected(lambda: envelope.check(candidate))
+    for raw in (b'{"x":1,"x":2}', b'{"x":1.0}', b'{"x":NaN}', b' ' * (1024**2 + 1)):
+        rejected(lambda: envelope.decode(raw))
+    ensure(prod(Fraction(a)**0 - a for a in (2, 3, 5)) < 0, "odd-factor control fails")
+    return len(mutations) + 5
+
+
+def cli_case():
+    path = ROOT / "EXAMPLE.json"
+    result = subprocess.run([sys.executable, "-I", "-W", "error", "-B",
+                             str(ROOT / "envelope.py"), str(path)],
+                            check=True, capture_output=True, text=True, timeout=15)
+    parsed = json.loads(result.stdout)
+    ensure(parsed["input_sha256"] == hashlib.sha256(path.read_bytes()).hexdigest(),
+           "CLI input hash differs")
+    ensure(parsed["minimum"] == 0 and parsed["root_multiplicity"] == 2, "wrong CLI envelope")
+    return parsed
+
+
+def main():
+    example, digest = envelope.load(ROOT / "EXAMPLE.json")
+    ensure(envelope.check(example)["support_size"] == 4, "example support differs")
+    stats = positive_cases()
+    stats["rejection_controls"] = negative_cases(example)
+    stats["example_input_sha256"] = digest
+    stats["cli"] = cli_case()
+    names = ("envelope.py", "verify.py", "PROOF.md", "README.md", "TASK.json",
+             "SOURCES.json", "VERIFY.json", "EXAMPLE.json")
+    stats["package_sha256"] = {name: hashlib.sha256((ROOT / name).read_bytes()).hexdigest()
+                               for name in names}
+    print(json.dumps(stats, indent=2, sort_keys=True))
+    print("PASS_MIXED_RANK_TOUCHING_ENVELOPE")
+
+
+if __name__ == "__main__":
+    main()