diff --git a/research/real-imaginary-conjugation-tariff/CODE-BOUNDS.md b/research/real-imaginary-conjugation-tariff/CODE-BOUNDS.md
new file mode 100644
index 0000000000..cfb954a111
--- /dev/null
+++ b/research/real-imaginary-conjugation-tariff/CODE-BOUNDS.md
@@ -0,0 +1,42 @@
+# Executable bounds and inspection
+
+The retained artifact is one standard-library Python file. `compile_frames`
+is its public computational entry; the other matrix routines are internal to
+that entry or the fixed no-argument replay. The compiler validates both inputs,
+matching dimensions, exact rational types, coefficient sizes and orthogonality.
+Unsupported inputs fail with ValueError. Boolean and floating-point entries
+are rejected. Every mathematical check uses an explicit exception and remains
+active under optimized Python.
+
+There is no recursion. Compiler dimension is at most eight, reduction has at
+most eight iterations, and each iteration strictly decreases the independently
+checked displacement rank. There are at most 25 emitted instructions. Compiler
+matrix loops have at most eight iterations per dimension. Product outputs have
+at most 4,096 numerator/denominator bits. Reflection construction and elimination
+between those checks use a finite number of exact operations on bounded-size
+matrices; no claim of a practical public worst-case runtime is made.
+
+The replay has 2,921 fixed program fixtures, at most eight active-plus-dirty
+complex coordinates, real matrices at most 16-by-16, at most 25 instructions per
+fixture, and at most 16 elimination pivots. Its nonreal word corpus has exactly
+1+5+25+125+625 words, each of at most four steps. All other loops range over
+these finite dimensions, the 12 control cases, or the package's source files.
+The receipt inventories only package-local regular files. The replay writes
+nothing and owns no network connection, subprocess, random generator or lock.
+
+Power of Ten rule 3 deviation: CPython and Fraction allocate during operation.
+The fixed corpus, dimension limits and input/product bit guards bound live
+matrices; one program endpoint is retained at a time. There is no service loop,
+external state or retained history of the census. A native fixed-allocation
+implementation is a separate obligation. Python has no pointer arithmetic or
+preprocessor; the artifact uses direct named calls, no dynamic evaluation,
+code generation or callback dispatch. Ordinary exception propagation is the
+failure path. No shared repository implementation is changed.
+
+Functions are below 60 physical lines. The compiler checks nonzero normals,
+rational basis inverses, strict rank progress, exact termination and the tariff.
+The separate interpreter verifies full endpoint matrices, every prefix bound,
+returned dirty coordinates and an independent antilinear-rank calculation.
+Warning-strict normal and optimized runs, AST syntax/function-size inspection
+and tabnanny are the local diagnostics. No static type checker, native compiler
+or formal proof kernel is claimed. Registered replay repeats both strict modes.
diff --git a/research/real-imaginary-conjugation-tariff/PROOF.md b/research/real-imaginary-conjugation-tariff/PROOF.md
new file mode 100644
index 0000000000..6a1667a66b
--- /dev/null
+++ b/research/real-imaginary-conjugation-tariff/PROOF.md
@@ -0,0 +1,155 @@
+# Exact conjugation tariff for separate real and imaginary frames
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof. Finite rational checks corroborate the
+construction. Independent human and formal proof-kernel review are unclaimed.
+
+## Contract and theorem
+
+Fix a positive integer n and real orthogonal n-by-n matrices P,Q. The target is
+
+    T(x+iy) = Px + iQy,       x,y in R^n arbitrary.
+
+There may also be any finite number s of arbitrary dirty complex coordinates.
+The complete endpoint must be T direct-sum I_s, including all dirty returns.
+Intermediate mixing with those coordinates is permitted.
+
+A program is a fixed finite sequence with these operations:
+
+- Any invertible complex-linear map on C^(n+s), at zero price in this model.
+- Conjugation of one coordinate z_j, leaving every other coordinate unchanged,
+  at unit price.
+
+No other real-linear, nonlinear, approximate, branching or irreversible
+operation is free. In particular, simultaneous conjugation of an arbitrary
+block is not one unit-price call.
+
+**Theorem.** The minimum paid-call count is exactly
+
+    rank_R(P-Q).
+
+It is independent of s. If P,Q are rational, an attaining program uses rational
+real matrices as its complex-linear maps. It requires no square roots and no
+dirty coordinates. The upper construction has r paid calls and 2r+1 displayed
+linear instructions, where r=rank(P-Q); adjacent linear instructions may be
+combined. This instruction count gives no physical scalar-cost bound.
+
+This is an exact tariff in the declared relaxation, not a lower bound on all
+possible real-linear provider alphabets or an admitted native supplier.
+
+## Lower bound from the antilinear part
+
+Every real-linear map S on C^d has a unique expression
+
+    S(z)=A_S z+B_S conjugate(z).
+
+Define b(S)=rank_C(B_S). For two such maps,
+
+    B_(S R) = A_S B_R + B_S conjugate(A_R).
+
+Rank subadditivity and the rank bound for a product imply
+
+    b(S R) <= b(S)+b(R).
+
+A complex-linear map has b=0. Single-coordinate conjugation has B=e_j e_j^t,
+so b=1. Consequently, any program with k paid calls has b(endpoint)<=k,
+irrespective of the number of dirty coordinates or intermediate mixing.
+
+For the required endpoint,
+
+    A = diag((P+Q)/2, I_s),
+    B = diag((P-Q)/2, 0_s).
+
+Its antilinear rank is rank_C(P-Q)=rank_R(P-Q). This proves the lower bound
+and the dirty-workspace assertion. It also proves additivity for independent
+direct-sum targets in this model. The last statement follows from the one
+theorem by choosing block-diagonal P,Q, rather than from a separate search.
+
+## A rank-tight rational reflection factorization
+
+Set R=P^t Q. Then R is real orthogonal and rank(I-R)=rank(P-Q). We give the
+classical Euclidean Householder reduction explicitly to specify the compiler.
+
+For a nonzero real v put H_v=I-2vv^t/(v^t v). Suppose R is not identity.
+Choose a coordinate e_j with Re_j != e_j and put v=Re_j-e_j. Since R preserves
+length, H_v Re_j=e_j. If f is fixed by R, then
+
+    f^t v = f^t R e_j - f^t e_j = (R^t f)^t e_j - f^t e_j = 0.
+
+Thus H_v also fixes every old fixed vector, and H_v R fixes e_j in addition.
+The new fixed space has dimension at least one larger. Conversely,
+
+    I-H_v R = (I-R)+(I-H_v)R
+
+differs from I-R by a rank-one matrix. Its rank can decrease by at most one.
+It therefore decreases by exactly one. Repeating terminates after exactly
+r=rank(I-R) steps, with
+
+    H_(v_r) ... H_(v_1) R = I,
+    R = H_(v_1) ... H_(v_r).
+
+All v_j and H_(v_j) are rational when R is rational. Positive definiteness
+ensures every nonzero v_j has v_j^t v_j>0. No assertion about arbitrary
+indefinite forms is used.
+
+## One coordinate conjugation per imaginary reflection
+
+Let J_v act by J_v(x+iy)=x+iH_v y. Choose an index k with v_k != 0. Define
+a rational real matrix S with first column v and, for every j != k, another
+column
+
+    u_j=e_j-(v_j/v_k)e_k.
+
+The u_j form a basis of v-perp, so S is invertible. Explicit inverse
+coordinates of a vector a are
+
+    c_0=(v^t a)/(v^t v),
+    c_j=a_j-v_j c_0,       j != k.
+
+Write C_0 for conjugation of coordinate zero. It fixes the real parts of all
+coordinates and flips only the imaginary part of coordinate zero. Therefore
+
+    S C_0 S^-1 (x+iy) = x+i S diag(-1,1,...,1) S^-1 y = J_v(x+iy).
+
+The identity follows because the displayed real matrix negates v and fixes
+v-perp. Each J_v costs exactly one paid call. Apply J_(v_r),...,J_(v_1)
+chronologically, then the free real matrix P. The result is
+
+    x+iy -> x+iRy -> Px+iPRy = Px+iQy.
+
+This uses exactly r conjugations and attains the lower bound. Extending each
+operation by identity supplies every s without using its dirty contents.
+
+## Discriminating two-coordinate example
+
+Take P=I_2 and
+
+    Q = [ 3/5  -4/5 ] = H_(-1,2) H_(0,1).
+        [ 4/5   3/5 ]
+
+Then rank(I-Q)=2. Conjugating the imaginary coordinates in the two displayed
+reflection bases, in reverse order, attains two calls. One call is impossible
+even with arbitrary complex-linear mixing and exactly restored dirty space.
+The complete real target has positive determinant, so orientation alone does
+not give this exclusion. Ordinary real displacement rank is not the right
+tariff either: multiplication by i is a free complex-linear map with
+rank_R(T-I)=2 and zero paid calls.
+
+## Attribution and scope
+
+Real-linear complex decomposition, rank subadditivity and the
+Cartan-Dieudonne-Scherk reflection method are classical. See
+[Rodriguez-Andrade, Aragon-Gonzalez, Aragon and Verde-Star, 2010](https://arxiv.org/abs/1011.1027)
+for constructive reflection factorization and minimum-length context. The
+reflection theorem itself and the antilinear-rank principle are not claimed
+as new. The contribution is their exact combined tariff, the explicit rational
+conjugation compiler and its dirty-workspace interface in this research model.
+No general literature-priority claim is made.
+
+The matrices P,Q need not commute. Free frames may be arbitrary complex-linear
+maps, although the attaining compiler uses real rational ones. Arbitrary
+real-linear targets outside the separate orthogonal P,Q contract are not
+classified. Conjugation delivery, the actual scalar/basis invoice, native
+frames, independent productive targets, all-size supplier compilation,
+precision, stock, tape movement and the outer multiplier are not provided.
diff --git a/research/real-imaginary-conjugation-tariff/README.md b/research/real-imaginary-conjugation-tariff/README.md
new file mode 100644
index 0000000000..a1b79aa31f
--- /dev/null
+++ b/research/real-imaginary-conjugation-tariff/README.md
@@ -0,0 +1,138 @@
+# Exact conjugation tariff for separate real and imaginary frames
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. For every
+positive n and real orthogonal n-by-n P,Q, the exact number of single-coordinate
+conjugations required for
+
+```text
+T(x+iy) = Px+iQy
+```
+
+is **rank(P-Q)** when arbitrary invertible complex-linear frames are free.
+Any finite number of exactly restored arbitrary dirty complex coordinates
+leaves this minimum unchanged. For rational P,Q, an explicit attaining
+compiler uses rational real frames and no square roots.
+
+[PROOF.md](PROOF.md) proves the all-size statement, its dirty-workspace lower
+bound and the rational construction. [verify.py](verify.py) implements that
+construction and a separate full real-matrix interpreter. This is a changed
+provider alphabet, rather than a new native supplier or a kappa improvement.
+
+The lower bound records the rank of the antilinear part of the complete map.
+Each paid conjugation increases it by at most one, while every free frame has
+zero antilinear part. Classical rank-tight Householder factorization attains
+the resulting bound. Those ingredients are credited below; the new scoped
+contribution is their exact tariff and explicit rational interface here.
+
+For example, P=I and Q=[[3/5,-4/5],[4/5,3/5]] need exactly two conjugations,
+even with dirty workspace and arbitrary complex-linear mixing. This excludes
+one-call realification of that pair. Positive real determinant alone would
+not exclude it. Conversely, the free map z->iz has real displacement rank two
+but needs no conjugation, so ordinary displacement rank is not this tariff.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/real-imaginary-conjugation-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/real-imaginary-conjugation-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/real-imaginary-conjugation-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/real-imaginary-conjugation-tariff --check-source-history
+```
+
+Another CPython 3.12 path may replace the absolute interpreter. The direct
+commands print `PASS_REAL_IMAGINARY_CONJUGATION_TARIFF` inside generated JSON
+stdout receipts bound to every package file hash. They write no files. The
+registered and publication checks print `PASS_REGISTERED_RESEARCH_PACKAGE`
+and `PASS_RESEARCH_COMMIT_BYTES` respectively.
+
+The finite corpus contains:
+
+- All 2,372 ordered pairs of signed permutation matrices in dimensions one,
+  two and three, and all 384 dimension-four targets with P=I.
+- 162 parameterized rational fixtures in dimensions one through six, with
+  zero, one or two arbitrary dirty complex coordinates. These fixtures may
+  repeat a matrix pair; no distinct-pair count is claimed.
+- Three dimension/coefficient boundary fixtures, including dimension eight
+  and a reflection with 253-bit rational coefficients.
+- 124,532 full real endpoint entries across those 2,921 program fixtures,
+  covering 22,136 emitted instructions. Every prefix obeys its antilinear
+  call bound. A separate 64-entry fixture transiently mixes active data and
+  dirty coordinates using a nonreal complex-linear shear and restores them.
+- All 781 words of length zero through four over two conjugations and three
+  complex-linear generators. A separately evaluated 2-by-2 Gaussian
+  determinant agrees with the full real antilinear-rank oracle.
+- Twelve rejected cases: nine malformed or unsupported compiler inputs and
+  three actual endpoint corruptions, omitting a call, flipping a real part
+  instead of an imaginary part, and reversing instruction order.
+
+The rank oracles use independent elimination implementations. Complete real
+matrix identities establish arbitrary-input endpoints for each finite
+fixture; they do not extrapolate the theorem. Normal and optimized receipts
+must agree. The first complete local corpus ran in about five seconds on
+CPython 3.12.15, macOS 27.0.1 arm64. This is a replay duration, not a speedup.
+
+## Scope and current bottleneck
+
+The complex-new-helper-inventory card is explicitly changed to a real-linear
+interface side result. The selected source-binding positive control passed
+at canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+The selected record is PR6030, kappa 0.003125804; older values in priority prose
+do not replace that record. [TASK.json](TASK.json) retains the complete card.
+
+A different real/imaginary frame cannot be supplied by complex-linear frames
+alone when P differs from Q. The theorem gives the exact remaining conjugation
+resource in this generous relaxation. It supplies no actual P104 cut, productive
+target or favorable complete recursive bill. Free frames are an accounting
+assumption, not a claim that physical basis work is free. The rational compiler
+can use odd denominators. A native or dyadic installation needs its own
+coefficient, scalar, access, lifetime and restoration argument.
+
+The logical identity, exact call tariff and rational frame constructor are
+proved. Native conjugation delivery, physical basis costs, chronology, owned
+storage, independent Gaussian targets, precision/tape, stock, uniform supplier
+compilation and outer funding are unknown here. No selected cold replay,
+predecessor scientific replay, Lean, Docker, native realization or rounded
+multiplier was run. All five selected framework assumptions remain. Independent
+human and formal proof-kernel review are unclaimed.
+
+[The advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376836)
+preceded substantial work. Live open/account PRs, recent handoffs, active
+Discussions, local reservations, general-form and distinctive main README
+searches, and merged PR searches were checked. The broader cache covered 141
+of 8,917 local note records, so it was supplemented by main-tree searches.
+These checks do not cover unpublished work or arbitrary historical diffs.
+No contributor's package or scientific checker is imported by the result.
+
+## Open next questions
+
+1. Can one actual complex supplier use separate real and imaginary frames at
+   a favorable complete bill? First name its literal producer and consumer,
+   and charge every basis, conjugation, return and target change. No native
+   delivery or full signed invoice is supplied here.
+2. Which rational frame pairs admit an attaining program in a required
+   physical coefficient ring? Fix that ring and examine the displayed bases
+   for one reached pair. Rational frames may have odd denominators.
+
+Structured versions, first steps and blockers are in [TASK.json](TASK.json).
+The first exact tariff is shipped without classifying more general real-linear
+maps or expanding into physical supplier construction.
+
+## Credit and executable bounds
+
+Antilinear decomposition and rank subadditivity are classical. The
+Cartan-Dieudonne-Scherk reflection method is classical; see
+[Rodriguez-Andrade, Aragon-Gonzalez, Aragon and Verde-Star, 2010](https://arxiv.org/abs/1011.1027)
+for constructive factorization context. The needed positive-definite reduction
+is proved explicitly in PROOF.md. No external code or proof text is copied,
+and no general literature-priority claim is made. Repository predecessors and
+their credit lines are unchanged.
+
+The public compiler accepts dimensions one through eight and integer/Fraction
+entries of at most 256 bits. Matrix-product outputs are guarded at 4,096 bits;
+exceeding an executable bound raises an error, not a mathematical impossibility.
+The written rational construction has no such limits. [CODE-BOUNDS.md](CODE-BOUNDS.md)
+records loop bounds, allocation deviations and diagnostics.
diff --git a/research/real-imaginary-conjugation-tariff/SOURCES.json b/research/real-imaginary-conjugation-tariff/SOURCES.json
new file mode 100644
index 0000000000..9705005d87
--- /dev/null
+++ b/research/real-imaginary-conjugation-tariff/SOURCES.json
@@ -0,0 +1,31 @@
+{
+  "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"
+    }
+  ],
+  "external_background": [
+    {
+      "url": "https://arxiv.org/abs/1011.1027v1",
+      "title": "An algorithm for the Cartan-Dieudonne theorem on generalized scalar product spaces",
+      "authors": [
+        "M.A. Rodriguez-Andrade",
+        "G. Aragon-Gonzalez",
+        "J.L. Aragon",
+        "Luis Verde-Star"
+      ],
+      "role": "Classical constructive reflection-factorization background. No code or proof text imported; PROOF.md proves the needed positive-definite rank-tight reduction explicitly."
+    }
+  ]
+}
diff --git a/research/real-imaginary-conjugation-tariff/TASK.json b/research/real-imaginary-conjugation-tariff/TASK.json
new file mode 100644
index 0000000000..08b6af44bb
--- /dev/null
+++ b/research/real-imaginary-conjugation-tariff/TASK.json
@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?",
+    "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": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.",
+    "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": [
+      "productive helper",
+      "target refinement",
+      "5599",
+      "5614"
+    ],
+    "existing_checks": [
+      {
+        "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 single-coordinate conjugation tariff for separate real and imaginary orthogonal frames, including arbitrary restored dirty complex coordinates.",
+  "scope_change_reason": "An original real-linear interface question changes the complex-linear alphabet. The result prices its antilinear resource in an optimistic free-basis relaxation, rather than producing a physical helper supplier.",
+  "bottleneck_link": "Changed complex provider interfaces need explicit resources beyond complex-linear frame changes. This sharp tariff and rational compiler separate that resource from unpriced basis and native delivery costs.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first proved tariff and bounded exact endpoint corroboration. Do not extend to arbitrary real-linear targets or launch a physical supplier search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and the standalone normal/optimized verify.py full real-matrix replay, independent rank oracle, nonreal complex-frame words and rejected controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one actual complex supplier use separate real and imaginary frames at a favorable complete bill?",
+      "why_it_matters": "The abstract conjugation tariff does not establish a new productive target or a recursive saving.",
+      "first_step": "Name one source-bound producer/consumer and charge every displayed basis, conjugation, return and target change.",
+      "blocked_by": "No native delivery, coefficient-format, chronology or complete signed invoice is supplied."
+    },
+    {
+      "question": "Which rational frame pairs admit an attaining program in a required physical coefficient ring?",
+      "why_it_matters": "The square-root-free construction may still use odd denominators.",
+      "first_step": "Fix the actual allowed ring and analyze the displayed reflection bases for one reached P,Q pair.",
+      "blocked_by": "A rational basis is not automatically a legal dyadic or native basis."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376836",
+  "question_source": "original",
+  "predecessor_package": null,
+  "selected_kappa": "781451/250000000",
+  "upstream_checked_utc": "2026-11-03T15:00:15Z",
+  "environment": {
+    "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
+    "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+    "platform": "macOS-27.0.1-arm64-arm-64bit"
+  }
+}
diff --git a/research/real-imaginary-conjugation-tariff/VERIFY.json b/research/real-imaginary-conjugation-tariff/VERIFY.json
new file mode 100644
index 0000000000..9f708ba834
--- /dev/null
+++ b/research/real-imaginary-conjugation-tariff/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete signed-permutation and rational endpoint corpus; independent real/Gaussian rank checks; restored dirty coordinates; malformed-input and endpoint corruption controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete signed-permutation and rational endpoint corpus; independent real/Gaussian rank checks; restored dirty coordinates; malformed-input and endpoint corruption controls."
+    }
+  ]
+}
diff --git a/research/real-imaginary-conjugation-tariff/verify.py b/research/real-imaginary-conjugation-tariff/verify.py
new file mode 100644
index 0000000000..3e8eaf1fe6
--- /dev/null
+++ b/research/real-imaginary-conjugation-tariff/verify.py
@@ -0,0 +1,407 @@
+#!/usr/bin/env python3
+"""Exact rational conjugation compiler and finite corroboration. Apache-2.0."""
+
+from collections import Counter
+from fractions import Fraction as F
+from hashlib import sha256
+from itertools import permutations, product
+import json
+from pathlib import Path
+
+MAX_DIM = 8
+MAX_BITS = 256
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def eye(n):
+    return tuple(tuple(F(i == j) for j in range(n)) for i in range(n))
+
+
+def trans(a):
+    return tuple(zip(*a))
+
+
+def mul(a, b):
+    out = tuple(tuple(sum((x * y for x, y in zip(row, col)), F(0))
+                      for col in trans(b)) for row in a)
+    need(all(max(abs(x.numerator).bit_length(), x.denominator.bit_length())
+             <= 4096 for row in out for x in row), 'working bit bound')
+    return out
+
+
+def sub(a, b):
+    return tuple(tuple(x - y for x, y in zip(r, s)) for r, s in zip(a, b))
+
+
+def rank(a):
+    """Rational row elimination for the compiler's progress checks."""
+    work = [list(row) for row in a]
+    count = 0
+    for j in range(len(a[0])):
+        pivot = next((i for i in range(count, len(work)) if work[i][j]), None)
+        if pivot is None:
+            continue
+        work[count], work[pivot] = work[pivot], work[count]
+        d = work[count][j]
+        work[count] = [x / d for x in work[count]]
+        for i in range(count + 1, len(work)):
+            c = work[i][j]
+            work[i] = [x - c * y for x, y in zip(work[i], work[count])]
+        count += 1
+        if count == len(work):
+            break
+    return count
+
+
+def matrix(a):
+    """Validate the rational, square, bounded executable interface."""
+    need(isinstance(a, (tuple, list)) and 1 <= len(a) <= MAX_DIM, 'dimension')
+    n = len(a)
+    need(all(isinstance(row, (tuple, list)) and len(row) == n for row in a),
+         'square matrix')
+    need(all(type(x) in (int, F) for row in a for x in row), 'rational entries')
+    out = tuple(tuple(F(x) for x in row) for row in a)
+    need(all(max(abs(x.numerator).bit_length(), x.denominator.bit_length())
+             <= MAX_BITS for row in out for x in row), 'entry bit bound')
+    return out
+
+
+def reflection(v):
+    n = len(v)
+    norm = sum(x * x for x in v)
+    need(norm > 0, 'nonzero real reflection normal')
+    return tuple(tuple(F(i == j) - 2 * v[i] * v[j] / norm
+                       for j in range(n)) for i in range(n))
+
+
+def reflection_basis(v):
+    """Rational S,S^-1 with first column v and other columns in v-perp."""
+    n = len(v)
+    k = next((i for i in range(n) if v[i]), None)
+    need(k is not None, 'nonzero basis normal')
+    norm = sum(x * x for x in v)
+    other = [j for j in range(n) if j != k]
+    columns = [tuple(v)] + [tuple(F(i == j) - F(i == k) * v[j] / v[k]
+                                 for i in range(n)) for j in other]
+    inverse = [tuple(x / norm for x in v)]
+    inverse += [tuple(F(i == j) - v[j] * v[i] / norm for i in range(n))
+                for j in other]
+    s, si = trans(columns), tuple(inverse)
+    need(mul(s, si) == eye(n) == mul(si, s), 'rational basis inverse')
+    return s, si
+
+
+def normals(q):
+    """Return v_1,...,v_r with q=H(v_1)...H(v_r), r=rank(I-q)."""
+    n = len(q)
+    current = q
+    result = []
+    initial = rank(sub(eye(n), q))
+    for _ in range(n):
+        if current == eye(n):
+            break
+        j = next(j for j in range(n)
+                 if any(current[i][j] != F(i == j) for i in range(n)))
+        v = tuple(current[i][j] - F(i == j) for i in range(n))
+        before = rank(sub(eye(n), current))
+        current = mul(reflection(v), current)
+        need(rank(sub(eye(n), current)) == before - 1, 'rank drops once')
+        result.append(v)
+    need(current == eye(n) and len(result) == initial, 'reflection termination')
+    return tuple(result)
+
+
+def compile_frames(p, q):
+    """Chronological ('L', real matrix) / ('C', coordinate) instructions."""
+    p, q = matrix(p), matrix(q)
+    n = len(p)
+    need(len(q) == n, 'matching dimensions')
+    need(mul(trans(p), p) == eye(n), 'orthogonal P')
+    need(mul(trans(q), q) == eye(n), 'orthogonal Q')
+    result = []
+    for v in reversed(normals(mul(trans(p), q))):
+        s, si = reflection_basis(v)
+        result.extend((('L', si), ('C', 0), ('L', s)))
+    result.append(('L', p))
+    need(sum(op == 'C' for op, _ in result) == rank(sub(p, q)), 'tariff')
+    return tuple(result)
+
+
+def dense_rank(a):
+    """Independent full Gauss-Jordan oracle, without compiler rank calls."""
+    rows = [list(map(F, row)) for row in a]
+    pivot_row = 0
+    for col in range(len(rows[0])):
+        choices = [i for i in range(pivot_row, len(rows)) if rows[i][col]]
+        if not choices:
+            continue
+        i = choices[-1]
+        rows[i], rows[pivot_row] = rows[pivot_row], rows[i]
+        divisor = rows[pivot_row][col]
+        for j in range(col, len(rows[0])):
+            rows[pivot_row][j] /= divisor
+        for k in range(len(rows)):
+            if k != pivot_row:
+                c = rows[k][col]
+                for j in range(col, len(rows[0])):
+                    rows[k][j] -= c * rows[pivot_row][j]
+        pivot_row += 1
+        if pivot_row == len(rows):
+            break
+    return pivot_row
+
+
+def dense_product(a, b):
+    """Literal full real matrix product, without compiler arithmetic calls."""
+    n = len(a)
+    out = [[F(0) for _ in range(n)] for _ in range(n)]
+    for i in range(n):
+        for k in range(n):
+            if a[i][k]:
+                for j in range(n):
+                    out[i][j] += a[i][k] * b[k][j]
+    return tuple(tuple(row) for row in out)
+
+
+def real_linear(a, b=None):
+    """Realification of complex-linear a+i*b; b defaults to zero."""
+    n = len(a)
+    if b is None:
+        b = tuple((F(0),) * n for _ in range(n))
+    return tuple(tuple(a[i % n][j % n] if i // n == j // n
+                       else (-1 if i < n else 1) * b[i % n][j % n]
+                       for j in range(2 * n)) for i in range(2 * n))
+
+
+def anti_rank(a):
+    """Half the real rank of M+J M J, the full antilinear component."""
+    n = len(a) // 2
+    b = [[F(0)] * (2 * n) for _ in range(2 * n)]
+    for i in range(2 * n):
+        for j in range(2 * n):
+            sign = -1 if (i < n) == (j < n) else 1
+            b[i][j] = a[i][j] + sign * a[(i + n) % (2 * n)][(j + n) % (2 * n)]
+    r = dense_rank(b)
+    need(r % 2 == 0, 'even real antilinear rank')
+    return r // 2
+
+
+def full_step(instruction, n, spectators):
+    op, payload = instruction
+    d = n + spectators
+    if op == 'C':
+        need(type(payload) is int and 0 <= payload < n, 'conjugation coordinate')
+        return tuple(tuple(F(i == j) * (-1 if i == d + payload else 1)
+                           for j in range(2 * d)) for i in range(2 * d))
+    need(op == 'L', 'instruction opcode')
+    need(len(payload) == n and all(len(row) == n for row in payload),
+         'instruction matrix shape')
+    need(dense_rank(payload) == n, 'invertible linear step')
+    padded = tuple(tuple(payload[i][j] if i < n and j < n else F(i == j)
+                         for j in range(d)) for i in range(d))
+    return real_linear(padded)
+
+
+def target(p, q, spectators):
+    n, d = len(p), len(p) + spectators
+    out = [[F(0)] * (2 * d) for _ in range(2 * d)]
+    for i in range(d):
+        for j in range(d):
+            out[i][j] = p[i][j] if i < n and j < n else F(i == j)
+            out[i + d][j + d] = q[i][j] if i < n and j < n else F(i == j)
+    return tuple(tuple(row) for row in out)
+
+
+def replay(p, q, spectators=0):
+    program = compile_frames(p, q)
+    d = len(p) + spectators
+    state = eye(2 * d)
+    calls = 0
+    for instruction in program:
+        state = dense_product(full_step(instruction, len(p), spectators), state)
+        calls += instruction[0] == 'C'
+        need(anti_rank(state) <= calls, 'every prefix obeys call lower bound')
+    need(state == target(p, q, spectators), 'complete real endpoint')
+    need(calls == dense_rank(sub(p, q)), 'independent exact tariff')
+    need(anti_rank(state) == calls, 'endpoint lower bound attained')
+    return calls, len(program), (2 * d) ** 2
+
+
+def signed_permutations(n):
+    for permutation in permutations(range(n)):
+        for signs in product((-1, 1), repeat=n):
+            yield tuple(tuple(F(signs[i] if j == permutation[i] else 0)
+                              for j in range(n)) for i in range(n))
+
+
+def rational_fixtures(n):
+    """Fixed rational orthogonal products, including oblique frames."""
+    fixtures = [eye(n)]
+    for seed in range(1, 9):
+        a = eye(n)
+        for k in range(1, n + 1):
+            v = tuple(F(((i + 2) * (seed + k) + i * i) % 7 - 3)
+                      for i in range(n))
+            if not any(v):
+                v = (F(1),) + (F(0),) * (n - 1)
+            a = mul(reflection(v), a)
+        fixtures.append(a)
+    return tuple(fixtures)
+
+
+def census():
+    counts, histogram = Counter(), Counter()
+    for n in range(1, 4):
+        choices = tuple(signed_permutations(n))
+        for p, q in product(choices, repeat=2):
+            calls, instructions, entries = replay(p, q)
+            counts['ordered_signed_permutation_pairs'] += 1
+            counts['instructions'] += instructions
+            counts['full_endpoint_entries'] += entries
+            histogram[calls] += 1
+    for q in signed_permutations(4):
+        calls, instructions, entries = replay(eye(4), q)
+        counts['four_coordinate_targets'] += 1
+        counts['instructions'] += instructions
+        counts['full_endpoint_entries'] += entries
+        histogram[calls] += 1
+    for n in range(1, 7):
+        choices = rational_fixtures(n)
+        for p, q in zip(choices, reversed(choices)):
+            for spectators in (0, 1, 2):
+                calls, instructions, entries = replay(p, q, spectators)
+                counts['rational_dirty_fixtures'] += 1
+                counts['instructions'] += instructions
+                counts['full_endpoint_entries'] += entries
+                histogram[calls] += 1
+    large = reflection((F(1 << 126), F(1)))
+    boundary = ((eye(8), eye(8)),
+                (eye(8), tuple(tuple(-x for x in row) for row in eye(8))),
+                (eye(2), large))
+    for p, q in boundary:
+        calls, instructions, entries = replay(p, q)
+        counts['dimension_and_coefficient_boundary_fixtures'] += 1
+        counts['instructions'] += instructions
+        counts['full_endpoint_entries'] += entries
+        histogram[calls] += 1
+    return counts, histogram
+
+
+def mixed_dirty_fixture():
+    """Nonreal free mixing of dirty coordinates inside a paid-call block."""
+    p = eye(2)
+    q = ((F(3, 5), F(-4, 5)), (F(4, 5), F(3, 5)))
+    program = compile_frames(p, q)
+    state = eye(8)
+    calls = 0
+    for op, payload in program:
+        if op == 'C':
+            # z_1 += i*z_2 mixes active/dirty data and commutes with C_0.
+            a = eye(4)
+            b = tuple(tuple(F(i == 1 and j == 2) for j in range(4))
+                      for i in range(4))
+            w = real_linear(a, b)
+            wi = real_linear(a, tuple(tuple(-x for x in row) for row in b))
+            state = dense_product(w, state)
+            need(state[1][6] != 0, 'dirty data enters an active coordinate')
+            state = dense_product(full_step((op, payload), 2, 2), state)
+            state = dense_product(wi, state)
+            calls += 1
+        else:
+            state = dense_product(full_step((op, payload), 2, 2), state)
+    need(state == target(p, q, 2) and anti_rank(state) == calls == 2,
+         'mixed dirty endpoint')
+    return 64
+
+
+def small_complex_rank(a):
+    """Independent 2-by-2 Gaussian determinant from four real blocks."""
+    b = [[((a[i][j] - a[i + 2][j + 2]) / 2,
+           (a[i + 2][j] + a[i][j + 2]) / 2)
+          for j in range(2)] for i in range(2)]
+    if all(x == (0, 0) for row in b for x in row):
+        return 0
+    x, y, z, w = b[0][0], b[0][1], b[1][0], b[1][1]
+    det = (x[0] * w[0] - x[1] * w[1] - y[0] * z[0] + y[1] * z[1],
+           x[0] * w[1] + x[1] * w[0] - y[0] * z[1] - y[1] * z[0])
+    return 1 if det == (0, 0) else 2
+
+
+def complex_word_checks():
+    """Complete short words with nonreal complex-linear frames."""
+    zero = ((F(0), F(0)), (F(0), F(0)))
+    phase = real_linear(zero, eye(2))
+    shear = real_linear(eye(2), ((F(0), F(1)), (F(0), F(0))))
+    swap = real_linear(((F(0), F(1)), (F(1), F(0))))
+    generators = ((full_step(('C', 0), 2, 0), 1),
+                  (full_step(('C', 1), 2, 0), 1),
+                  (phase, 0), (shear, 0), (swap, 0))
+    count = 0
+    for length in range(5):
+        for indices in product(range(5), repeat=length):
+            state, calls = eye(4), 0
+            for index in indices:
+                g, c = generators[index]
+                state = dense_product(g, state)
+                calls += c
+            need(anti_rank(state) == small_complex_rank(state) <= calls,
+                 'independent Gaussian rank and word bound')
+            count += 1
+    return count
+
+
+def controls():
+    rejected = 0
+    bad_inputs = [([], []), ([[1, 0]], [[1]]), ([[True]], [[1]]),
+                  ([[F(1, 3)]], [[1]]), ([[1]], [[1, 0], [0, 1]]),
+                  ([[1 << 257]], [[1]]), ([[1]], [[0]]),
+                  (eye(9), eye(9)), ([[1.0]], [[1]])]
+    for p, q in bad_inputs:
+        try:
+            compile_frames(p, q)
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError('invalid compiler input accepted')
+    p, q = eye(2), ((F(3, 5), F(-4, 5)), (F(4, 5), F(3, 5)))
+    program = compile_frames(p, q)
+    for defect in ('omit_conjugation', 'flip_real', 'reverse_word'):
+        state = eye(4)
+        removed = False
+        for op, payload in reversed(program) if defect == 'reverse_word' else program:
+            if defect == 'omit_conjugation' and op == 'C' and not removed:
+                removed = True
+                continue
+            step = full_step((op, payload), 2, 0)
+            if defect == 'flip_real' and op == 'C':
+                step = tuple(tuple(F(i == j) * (-1 if i == payload else 1)
+                                   for j in range(4)) for i in range(4))
+            state = dense_product(step, state)
+        need(state != target(p, q, 0), 'endpoint corruption must be detected')
+        rejected += 1
+    zero, one = ((F(0),),), ((F(1),),)
+    need(anti_rank(real_linear(zero, one)) == 0, 'displacement is not tariff')
+    need(anti_rank(target(p, q, 0)) == 2, 'orientation alone is insufficient')
+    return rejected
+
+
+def main():
+    counts, histogram = census()
+    counts['mixed_dirty_endpoint_entries'] = mixed_dirty_fixture()
+    counts['nonreal_complex_frame_words'] = complex_word_checks()
+    counts['rejected_invalid_or_corrupt_cases'] = controls()
+    here = Path(__file__).resolve().parent
+    hashes = {p.name: sha256(p.read_bytes()).hexdigest()
+              for p in sorted(here.iterdir()) if p.is_file()}
+    print(json.dumps({'status': 'PASS_REAL_IMAGINARY_CONJUGATION_TARIFF',
+                      'counts': dict(sorted(counts.items())),
+                      'tariff_histogram': dict(sorted(histogram.items())),
+                      'source_sha256': hashes}, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()