diff --git a/research/reversal-free-convolution/PROOF.md b/research/reversal-free-convolution/PROOF.md
new file mode 100644
index 0000000000..eb7b7a93ad
--- /dev/null
+++ b/research/reversal-free-convolution/PROOF.md
@@ -0,0 +1,134 @@
+# Omit the three outer frequency reversals
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Contract and source premises
+
+Fix any parameters admitted by the complete convolution caller of Jose Manuel's
+PR3709, with its complete rounded Fourier endpoints from PR3640. Write
+`a_i` for the address-bit lengths, `A=sum_i a_i`, `M=2^A`, and `r=2^ell`.
+The coefficients belong to `C[X]/(X^r+1)`. All rows and coefficients within a
+record retain their original order. Let B permute the M address records in
+each outer row by reversing the bits within each axis. It fixes coefficients,
+real/imaginary components, and outer rows, and satisfies B^2=I.
+
+We use the predecessor endpoint and normalized-product theorems as premises.
+We do not reprove native suppliers, exact-grid refinement, the physical word
+multiplier, twiddle approximation, or the multiplication theorem.
+
+Let Q denote the predecessor's component truncation to the specified grid.
+Its complete natural-order forward and opposite endpoints are
+
+    F(x) = Q(W_minus x / M),
+    G(x) = Q(W_plus x / M).
+
+Section 2 of PR3640's PROOF gives the raw round endpoints
+`B W_minus/M` and `W_plus B/M`. Its execute method materializes B after forward
+rounds and before opposite rounds. Section 3 proves that the lifted grid is
+exact through all intermediate rounds. B permutes whole words without changing
+them. Removing the forward reversal therefore gives exactly
+
+    F_raw(x) = B F(x).
+
+Removing the opposite reversal gives exactly
+
+    G_raw(x) = G(B x).
+
+These statements include the actual endpoint truncations: Q(Bx)=B Q(x).
+They do not infer bitwise equality from an error estimate alone.
+
+The physical RingProduct returns the same rounded polynomial operation on
+each record. Define it as P(x,y). Its exact contract is
+`Q_p(x_j y_j/r)` separately at every record j. The same parameters and
+arithmetic apply at each record, so
+
+    P(Bx, By) = B P(x,y).
+
+This is equivariance under a permutation of complete polynomial records.
+It uses no multiplicativity of component truncation. It does not permit B
+to permute coefficients within a polynomial or different B on the two inputs.
+
+## Complete equality
+
+The changed caller uses the unchanged Convolution code with one private
+Fourier subclass whose reversal method does no routing. Its intermediate
+Fourier API deliberately has the raw convention above. No raw Fourier object
+is returned by the adapter factory. The externally returned complete caller
+retains the original natural-order convolution API.
+
+Let S be the final exact M scale and width expansion in that caller. Then
+
+    S G_raw(P(F_raw(x), F_raw(y)))
+      = S G(B P(B F(x), B F(y)))
+      = S G(B B P(F(x), F(y)))
+      = S G(P(F(x), F(y))).
+
+The equality is between complete rounded outputs, including their signed bit
+encoding and unchanged width `p+2+A`. It holds for every input satisfying the
+predecessor's disk-grid contract, every admitted row count, long/short axis
+pattern and precision. It is a scoped program-refinement theorem, conditional
+on those inherited contracts, rather than a claim that finite tests cover
+all parameters.
+
+The original reported error bound `4 sqrt(2) M 2^-p` from `(x*y)/(rM)` transfers
+by equality. The same final disk-margin obligation remains before narrowing.
+There is no new approximate arithmetic or guard allowance.
+
+## Ownership and exact routing reduction
+
+The skipped routine reads geometry and routes only the current owned payload.
+It leaves flags and encoded counts at their required origins. Its completed
+router and temporary descriptor are erased. Replacing it by the identity on
+the current owned packet leaves the same ownership state at the next stage,
+with fewer child invocations. Every retained root, product, grid conversion,
+output width port, input rewind and cleanup is the inherited implementation.
+The changed intermediate values obey the same coefficientwise disk and grid
+bounds because B is a permutation. Thus the retained preconditions hold at
+every subsequent call. Borrowed inputs and metadata remain preserved; all
+owned scratch and both protected return ports retain the original lifecycle.
+This argument does not erase arbitrary external dirt or introduce fresh state.
+
+For P_precision=p+A, the source batches complete coordinate transpositions at
+capacity
+
+    b = 2^floor(997 floor(log2(P_precision))/1000).
+
+One reversal emits exactly
+
+    E = sum_i floor(a_i/2)
+
+edges. The source's loop flushes each b edges and then the remainder. Hence
+there are exactly `ceil(E/b)` nonempty sparse-router invocations per reversal,
+with the convention ceil(0/b)=0. The three complete transforms use identical
+parameters. The new program therefore removes exactly
+
+    3 ceil(E/b)
+
+of these outer sparse-router invocations, their descriptor generation/sorting
+and materialized returns. All six root calls, three diagonal passes, three
+lifts, three truncations, one polynomial product and final M scale in the
+four-address fixture remain. No claim is made about router calls internal to
+a root or the polynomial product, a measured speedup, or a recursive supplier
+histogram change. For a_i=2 and p=3, E=1, b=2, so the reduction is exactly three
+outer routing invocations. When E=0 the stated routing reduction is zero.
+
+## Prior work and new scope
+
+Matching DIF/DIT frequency order is classical FFT practice. The upstream
+synthetic interface already has compatible raw endpoints. Androolloyd's
+PR673 includes bit-reversed-order convolution in an indexed-read exact
+reference. PR3709 also uses the same idea inside the polynomial product's
+own coefficient FFT. These are credited precedents, not new general algebra.
+
+PR3640's Open next question 2 asks for a complete product consumer retaining
+the alternative convention. PR3709 subsequently supplies the required
+physical record-local product, while its outer caller still uses three
+natural-order Fourier endpoints. The new result is the source-bound adapter
+for that actual fixed-tape caller, its bitwise refinement proof, exact batching
+reduction, and a finite nonidentity-B execution. This does not extend the
+indexed-read model by merely changing its group or target.
+
+Production GL64/O73 execution, complete Gaussian/CRT/recovery joins, supplier
+admission and all five selected framework assumptions remain outside this
+contribution. The selected frontier is unchanged.
diff --git a/research/reversal-free-convolution/README.md b/research/reversal-free-convolution/README.md
new file mode 100644
index 0000000000..c84dd00454
--- /dev/null
+++ b/research/reversal-free-convolution/README.md
@@ -0,0 +1,133 @@
+# Remove three outer routing calls from the physical convolution
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+The complete physical normalized convolution in Jose Manuel's
+[PR3709](https://github.com/CrocSwap/integer-mult-bounds/pull/3709) can omit
+its three materialized endpoint bit reversals. A small adapter keeps the same
+bit-reversed record convention across both forward transforms, the polynomial
+product and the opposite transform. The complete rounded output, widened
+return descriptor, final scale and borrowed-port contract are unchanged.
+
+The claim is a scoped program-refinement proof with finite corroboration.
+For axis bit lengths a_i and P=p+sum a_i, it removes exactly
+
+    3 ceil(sum_i floor(a_i/2) / 2^floor(.997 floor(log2 P)))
+
+outer sparse-router invocations, plus their descriptors and materialized
+returns. The four-address p=3 fixture removes exactly three. This is an exact
+operation reduction, not a measured runtime factor or a new kappa.
+
+[PROOF.md](PROOF.md) proves equality including the actual rounding, disk/grid
+preconditions and ownership state. [adapter.py](adapter.py) changes only the
+private Fourier reversal method supplied to the unchanged Convolution class.
+It is imported inside the source package's authenticated cohort. Its raw
+Fourier convention is internal to the complete convolution; a standalone
+natural-order transform must continue to use the original Fourier API.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/reversal-free-convolution/verify.py --mode algebra
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/reversal-free-convolution/verify.py --mode physical
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/reversal-free-convolution
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/reversal-free-convolution --check-source-history
+```
+
+Any CPython 3.12 executable can replace that local path. Checks print a generated
+JSON stdout receipt with status `PASS_REVERSAL_FREE_CONVOLUTION`, exact counts
+and SHA256 bindings for all package files. Normal verification writes no files
+in the checkout. The inherited authenticated loader uses temporary directories.
+No receipt is handwritten.
+
+The algebra mode checks 24 exact rounded packets with 4,248 output coefficients,
+record-product equivariance on 4,248 coefficients, six failing asymmetric
+omission patterns, 25 enumerated batching cases and five invalid geometries.
+The physical mode executes the changed complete caller on one length-four
+axis, ell=2, p=3 and 16 Gaussian coefficients. B exchanges records 1 and 2.
+A nonzero character input and an imaginary second input give a nonzero rounded
+output. The first physical replay passed in 298.24 seconds on macOS arm64,
+CPython 3.12.15. It returned 224 bits at width 7, with SHA256
+`ad81a1219dc838dd3cd05b2aa4fb93aa80b7dee0edc77c4e0fb3b149482da8e9`. The independent unfactored polynomial-Fourier and quadratic-product
+reference computes the original natural-order output. The check includes
+encoded-metadata preservation, scratch erasure and protected width-port
+rejection. Host-decoding guards remain active during the physical execution.
+
+## Scope and credit
+
+This answers Open next question 2 of Jose Manuel / jmbarrancoml's
+[PR3640](https://github.com/CrocSwap/integer-mult-bounds/pull/3640), using his
+later PR3709 record-local consumer. Their complete transform/product theorems
+and native, tape, exact-grid and arithmetic premises are cited dependencies.
+They are not re-audited deliverables. Frozen source notices and predecessor
+credit remain unchanged. Exact live inputs and historical task provenance are
+in [SOURCES.json](SOURCES.json).
+
+Compatible DIF/DIT order is classical. The retained upstream synthetic
+interface and androolloyd's indexed-read
+[PR673](https://github.com/CrocSwap/integer-mult-bounds/pull/673) already use
+bit-reversed-order convolution. PR3709 applies it inside its coefficient FFT.
+The new work applies the cancellation to the three still-paid outer reversals
+in this actual fixed-tape composition. It does not claim a new FFT identity.
+
+The base is canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority
+revision 8. The selected binding baseline passed after materializing its sparse
+inputs. Live open PRs, recent account contributions, the handoff discussion,
+merged PR bodies and main README terms were checked before the
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228351).
+The cached overlap scan covered 393 open PRs and 5,629 Discussion records;
+sparse local-note coverage was incomplete. Direct main Git searches supplemented
+it. No search proves novelty against unpublished work or arbitrary code diffs.
+The card scope changes from a selected assumption audit to this enabled
+physical consumer improvement; no selected assumption is discharged.
+
+The physical fixture uses the inherited direct/literal q2 child and reduced
+test guards. Production GL64/O73 execution, Lean, Docker, the selected cold
+replay and the full Gaussian/CRT/integer join were not run. All selected
+framework assumptions and predecessor admission limitations remain. The
+conditional asymptotic exponent and selected frontier are unchanged.
+
+## Open next questions
+
+- Bind this alternative intermediate convention to one complete physical
+  Gaussian or CRT caller. First replace its Convolution owner and prove all
+  input disk margins and output narrowing bounds at that call. The remaining
+  field-layout, precision and integer-recovery obligations block a full join.
+- Count the removed routing work for one production-sized encoded shape.
+  First obtain its exact axis lengths and b, then retain the supplier's full
+  cost ledger. A measured runtime factor needs a separately budgeted experiment;
+  this exact invocation reduction does not supply one.
+
+## Implementation limits
+
+The new adapter adds no payload state, recursion or data-dependent loop. The
+reference is bounded to three axes, six address bits, ell<=4 and two rows.
+Each exact transform has at most 2*64*64*16 coefficient terms; each local
+product has at most 2*64*16^2 terms. Batch examples use at most 64 axes of
+256 bits each. Input and output invariants use explicit exceptions under -O.
+The finite physical fixture is fixed and inherits the bounded encoded loops
+and temporary-owner cleanup of the cited source implementation.
+
+Power of Ten deviations: Python integers, Fraction and lists allocate during
+bounded verification; no fixed-allocation runtime claim is made for the new
+reference. The inherited physical engine uses its existing recursive Karatsuba
+multiplier and dynamic cohort imports; neither is newly implemented or claimed
+compliant here. The adapter uses one inherited method dispatch with a fixed
+concrete target. Warning-strict normal/optimized execution, AST inspection and
+package/source-history checks provide diagnostics; no separate type checker,
+linter or proof kernel was run. Frozen predecessors remain unchanged.
+
+The managed-runtime deviation is limited to `reference.py`, `checks.py` and
+`physical.py`: Python requires dynamic integers and containers. Enforced small
+reference geometry and fixed physical inputs bound live state; normal and
+optimized algebra checks exercise the bounds. A future native reference would
+need fixed-capacity arithmetic before claiming Rule 3. The frozen Karatsuba
+recursion and cohort loader are unchanged Rule 1/8 dependencies, scoped to the
+authenticated predecessor contract. Source SHA256 checks and the complete new
+physical execution are the compensating controls. Replacing those mechanisms
+requires a separately reviewed predecessor change, rather than a mutation of
+pinned evidence. No fixed-allocation or recursion-free physical backend claim
+is made. All new functions fit within 60 physical lines.
diff --git a/research/reversal-free-convolution/SOURCES.json b/research/reversal-free-convolution/SOURCES.json
new file mode 100644
index 0000000000..e05bddc495
--- /dev/null
+++ b/research/reversal-free-convolution/SOURCES.json
@@ -0,0 +1,96 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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"
+    },
+    {
+      "path": "research/physical-ring-product/PROOF.md",
+      "usage": "input",
+      "git_blob": "2bc9926799296bb348193e68e55aed60ec6ce96d",
+      "sha256": "a2e43fe5f77350958c2d7d66a50389e5ec6b439a7f9620e94862b969e88fb500"
+    },
+    {
+      "path": "research/physical-ring-product/README.md",
+      "usage": "input",
+      "git_blob": "823f72e1b26aa8c71c5bd7141c5f93b2d59847fe",
+      "sha256": "dc4769ad9d7f3179659e28dc02bacc2822931a9bb8daaf9ad67cd935c1bb7094"
+    },
+    {
+      "path": "research/physical-ring-product/convolution_engine.py",
+      "usage": "input",
+      "git_blob": "02e4dd8e612d5d782a7b260b817b25ffd54348a8",
+      "sha256": "3d9941f986ad27e8b7ae8f46df2dc3a9ae7a2b119a69195735a5c735dc5aba65"
+    },
+    {
+      "path": "research/physical-ring-product/fft_arithmetic.py",
+      "usage": "input",
+      "git_blob": "606bb6c5e32ca813c927fba1a45315aae3e7de52",
+      "sha256": "bf7deff44f15f3349fcec98d0e86a6d20820f49ca008892fef9456b3629509e0"
+    },
+    {
+      "path": "research/physical-ring-product/inputs/fourier-export.tar",
+      "usage": "input",
+      "git_blob": "6f7f9d59abdf5d98cbecde1583db61103c1cd973",
+      "sha256": "30e460df0428ea1ff72dba6528537e53aec62fcec5dc6077bf736afd5cbbc7e8"
+    },
+    {
+      "path": "research/physical-ring-product/product_plan.py",
+      "usage": "input",
+      "git_blob": "b67caa174ee955c7edb98e04269577db99c21270",
+      "sha256": "fc8b0cf1fa46f2bf5492572c0aefa8f5420539e5e8b6e315bdfef4d57b6a9ed0"
+    },
+    {
+      "path": "research/physical-ring-product/ring_engine.py",
+      "usage": "input",
+      "git_blob": "9eff11c51258b9af1f8cefbc105aecdbf4ddf6ef",
+      "sha256": "322e653fe43f41bf23f79782f625acf8ff21c77e4ae62983ae6457ce60d8d0fe"
+    },
+    {
+      "path": "research/physical-ring-product/ring_sources.py",
+      "usage": "input",
+      "git_blob": "40a4b21a6ffd89d20051fac8055998fac252f130",
+      "sha256": "82f469acd7f8960ab6b32698e5300a377eb3f18f015f1f129f84604181cac746"
+    },
+    {
+      "path": "research/physical-ring-product/ring_words.py",
+      "usage": "input",
+      "git_blob": "1cb44ce6d95a1e0f9d2c6f78ecd5c7a8e8b39ba9",
+      "sha256": "6bd18c8f78c94b8a0b97512b4f45c03f88b608e895d0f120296585976e1e8104"
+    },
+    {
+      "path": "research/physical-ring-product/twiddle_setup.py",
+      "usage": "input",
+      "git_blob": "f8cba98e816b8aca30dc7c95d3e64dd4fb995cc5",
+      "sha256": "549bc2dd0c08034e8144226f76080b06155c252da514713dc923157d16faf2d4"
+    },
+    {
+      "path": "research/physical-ring-product/word_product.py",
+      "usage": "input",
+      "git_blob": "67e09e91103535fd1eb0b2d7d6db1fdc13de07d2",
+      "sha256": "12020ed0571fa756c2d19942b6ccdd6dc5627fdaadb388051417a618c14417d6"
+    },
+    {
+      "path": "research/physical-synthetic-fourier/PROOF.md",
+      "usage": "input",
+      "git_blob": "aa3c20a49eac7ec7406cf3ee3bab827181aeba09",
+      "sha256": "b2a6da7501a04848d0a42930da91f15b6653fccf42ed7a018cf602fc12a1d4f7"
+    },
+    {
+      "path": "research/physical-synthetic-fourier/README.md",
+      "usage": "input",
+      "git_blob": "adcc2f5fcf7e92896d1b662fe331368b4e09a5fd",
+      "sha256": "8800ae50710cfe22f0c3d88cac824d6522b1fb2db2ad2dfd683b49a24d539922"
+    }
+  ]
+}
diff --git a/research/reversal-free-convolution/TASK.json b/research/reversal-free-convolution/TASK.json
new file mode 100644
index 0000000000..406680f8eb
--- /dev/null
+++ b/research/reversal-free-convolution/TASK.json
@@ -0,0 +1,108 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its 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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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 one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "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": "Source-bound physical consumer refinement of PR3709: remove three outer Fourier endpoint reversal routines by retaining the common bit-reversed frequency-record convention.",
+  "scope_change_reason": "The selected-assumption card is changed to PR3640 Open next question 2, enabled by the later complete physical record-local product. This constructs a cheaper actual consumer boundary and does not audit predecessors or discharge a selected assumption.",
+  "bottleneck_link": "A complete reusable product boundary can avoid repeated representation conversions. This is an ordinary physical routing improvement under unchanged supplier contracts, not a recursive profile or kappa gain.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified bitwise-equivalent complete caller refinement; do not extend it to a Gaussian/CRT join or chase a runtime factor.",
+  "outcome": "completed",
+  "evidence": "Scoped bitwise refinement and exact all-shape routing reduction proved in PROOF.md. Algebra mode passes 24 rounded packets and 4248 coefficients, six asymmetric omission controls, 25 batch cases and five invalid geometries. The complete nonidentity-B physical execution passed in 298.24 seconds on CPython 3.12.15/macOS arm64, returning 224 bits at width 7 with SHA256 ad81a1219dc838dd3cd05b2aa4fb93aa80b7dee0edc77c4e0fb3b149482da8e9. All six root calls, three diagonals and full product/scale remain, with zero outer reversals; borrowed ports, scratch erasure and protected width rejection pass. Registered final-tree verification and hosted CI are tracked separately.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a complete physical Gaussian or CRT caller use the cheaper intermediate convention?",
+      "why_it_matters": "The local routing reduction is not a complete multiplication join.",
+      "first_step": "Replace one actual Convolution owner and derive its disk margin, widened output and narrowing requirements.",
+      "blocked_by": "The inherited field layout, Gaussian/CRT precision and integer-recovery obligations."
+    },
+    {
+      "question": "What complete routing bill disappears for one production-sized encoded shape?",
+      "why_it_matters": "The exact invocation formula does not establish a measured runtime factor or a changed recursive histogram.",
+      "first_step": "Obtain the actual axis lengths and batch limit and apply the formula in the complete supplier ledger.",
+      "blocked_by": "A production caller and separately budgeted measurement if a runtime factor is wanted."
+    }
+  ],
+  "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228351",
+  "source_question": {
+    "source": "PR #3640",
+    "author": "jmbarrancoml",
+    "question": "Open next question 2: retain bit-reversed frequency order across both operands and the opposite transform.",
+    "enabling_predecessor": "PR #3709"
+  },
+  "claim_type": "scoped program-refinement proof with finite physical corroboration",
+  "framework_assumptions_discharged": [],
+  "environment": {
+    "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+    "executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "machine": "arm64"
+  },
+  "verification_limits": [
+    "One direct/literal q2 physical fixture with reduced source test guards.",
+    "No production GL64/O73, selected replay, proof kernel, measured speed factor or Gaussian/CRT/integer join."
+  ]
+}
diff --git a/research/reversal-free-convolution/VERIFY.json b/research/reversal-free-convolution/VERIFY.json
new file mode 100644
index 0000000000..01084ff671
--- /dev/null
+++ b/research/reversal-free-convolution/VERIFY.json
@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/physical-ring-product/PROOF.md",
+    "research/physical-ring-product/README.md",
+    "research/physical-ring-product/convolution_engine.py",
+    "research/physical-ring-product/fft_arithmetic.py",
+    "research/physical-ring-product/inputs/fourier-export.tar",
+    "research/physical-ring-product/product_plan.py",
+    "research/physical-ring-product/ring_engine.py",
+    "research/physical-ring-product/ring_sources.py",
+    "research/physical-ring-product/ring_words.py",
+    "research/physical-ring-product/twiddle_setup.py",
+    "research/physical-ring-product/word_product.py",
+    "research/physical-synthetic-fourier/PROOF.md",
+    "research/physical-synthetic-fourier/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py",
+        "--mode",
+        "algebra"
+      ],
+      "timeout_seconds": 30,
+      "checks": "24 exact rounded cases, six asymmetric omission counterexamples, 25 enumerated routing batches and five invalid geometries."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py",
+        "--mode",
+        "algebra"
+      ],
+      "timeout_seconds": 30,
+      "checks": "The same mathematical and boundary controls with Python assertions disabled."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py",
+        "--mode",
+        "physical"
+      ],
+      "timeout_seconds": 550,
+      "checks": "Changed complete fixed-tape convolution with nonidentity frequency reversal, exact original endpoint oracle, all borrowed ports, scratch erasure, protected width port and actual zero reversal count."
+    }
+  ]
+}
diff --git a/research/reversal-free-convolution/adapter.py b/research/reversal-free-convolution/adapter.py
new file mode 100644
index 0000000000..aafe18d7e7
--- /dev/null
+++ b/research/reversal-free-convolution/adapter.py
@@ -0,0 +1,25 @@
+"""Keep bit-reversed frequency records inside the physical convolution caller.
+
+Import only inside the authenticated physical-ring-product cohort. The private
+Fourier object has a changed intermediate contract; expose the complete caller.
+"""
+
+from convolution_engine import Convolution
+from fourier_engine import Fourier
+from fourier_plan import FourierPlan
+from words import need
+
+
+class _FrequencyFourier(Fourier):
+    """Forward returns B F_minus; opposite accepts B-ordered records."""
+
+    def reversal(self, plan):
+        need(isinstance(plan, FourierPlan), "compiled convolution frequency plan")
+        need(self.current is not None, "live convolution frequency packet")
+        # The same B cancels across both inputs and the record-local product.
+        # Keep the inherited zero reversal count: no sparse router is invoked.
+
+
+def convolution(layer):
+    """Return the original natural-order convolution ABI with fewer routers."""
+    return Convolution(_FrequencyFourier(layer))
diff --git a/research/reversal-free-convolution/checks.py b/research/reversal-free-convolution/checks.py
new file mode 100644
index 0000000000..2c0a462022
--- /dev/null
+++ b/research/reversal-free-convolution/checks.py
@@ -0,0 +1,90 @@
+"""Exact finite corroboration and asymmetric frequency-order controls."""
+
+from itertools import product as tuples
+from reference import changed, geometry, original, permute, product, require, routing_saving
+
+
+def packet(lengths, ell, rows, salt):
+    count, degree = geometry(lengths, ell, rows)
+    limit = 1 << ell
+    return [((3*i+salt) % (2*limit+1)-limit,
+             (5*i+2*salt) % (2*limit+1)-limit) for i in range(rows*count*degree)]
+
+
+def finite_cases():
+    cases = points = equivariance = 0
+    invalid = {mask: False for mask in tuples((False, True), repeat=3)
+               if mask not in ((False,)*3, (True,)*3)}
+    for ell in (2, 3):
+        for axes in (1, 2):
+            for lengths in tuples((ell-1, ell), repeat=axes):
+                for rows in (1, 2):
+                    p = ell+1
+                    first = packet(lengths, ell, rows, 1)
+                    second = packet(lengths, ell, rows, 3)
+                    # Add a common low-frequency component without leaving the disk.
+                    first = [(a+(1 << (ell-1)), b) for a, b in first]
+                    second = [(a+(1 << (ell-1)), b) for a, b in second]
+                    require(all(a*a+b*b <= 1 << (2*p) for a, b in first+second), "finite disk inputs")
+                    expected = original(first, second, lengths, ell, p, rows)
+                    require(changed(first, second, lengths, ell, p, rows) == expected,
+                            "all-three omission preserves complete rounded output")
+                    a = permute(first, lengths, ell, rows)
+                    b = permute(second, lengths, ell, rows)
+                    require(product(a, b, lengths, ell, p, rows)
+                            == permute(product(first, second, lengths, ell, p, rows), lengths, ell, rows),
+                            "rounded record-local product equivariance")
+                    require(permute(a, lengths, ell, rows) == first, "actual B is involutive")
+                    for mask in invalid:
+                        if not invalid[mask]:
+                            invalid[mask] = changed(first, second, lengths, ell, p, rows, mask) != expected
+                    cases += 1
+                    points += len(expected)
+                    equivariance += len(first)
+    # A length-four character makes B exchange two different nonzero modes.
+    first = character_packet()
+    expected = original(first, first, (2,), 2, 3, 1)
+    require(any(a or b for a, b in expected), "nonzero omission control")
+    for mask in invalid:
+        invalid[mask] = invalid[mask] or changed(first, first, (2,), 2, 3, 1, mask) != expected
+    require(all(invalid.values()), "every asymmetric omission has a concrete counterexample")
+    return {"rounded_cases": cases, "output_coefficients": points,
+            "product_equivariance_coefficients": equivariance,
+            "asymmetric_omission_counterexamples": len(invalid)}
+
+
+def character_packet():
+    result = []
+    for address in range(4):
+        record = [(0, 0)]*4
+        for coefficient in range(4):
+            wraps, target = divmod(coefficient+2*address, 4)
+            record[target] = (-7 if wraps % 2 else 7, 0)
+        result.extend(record)
+    return result
+
+
+def tariff_cases():
+    tariffs = 0
+    for widths in ((1,), (2,), (3, 2), (8,)*64, (256,)*64):
+        for p in (2, 3, 8, 128, 65536):
+            cap = 1 << (997*((p+sum(widths)).bit_length()-1)//1000)
+            edges = sum(width//2 for width in widths)
+            batches = sum(1 for _ in range(0, edges, cap))
+            require(routing_saving(widths, p) == 3*batches, "enumerated bounded support batches")
+            tariffs += 1
+    require(routing_saving((2,), 3) == 3 and routing_saving((1,), 3) == 0,
+            "strict and degenerate routing controls")
+    rejected = 0
+    for widths, p in (((), 3), ((0,), 3), ((257,), 3), ((2,), 1), ((2,), 65537)):
+        try:
+            routing_saving(widths, p)
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("invalid routing geometry accepted")
+    return {"batch_cases": tariffs, "invalid_geometry_rejections": rejected}
+
+
+def run():
+    return {**finite_cases(), **tariff_cases()}
diff --git a/research/reversal-free-convolution/physical.py b/research/reversal-free-convolution/physical.py
new file mode 100644
index 0000000000..2971a9feff
--- /dev/null
+++ b/research/reversal-free-convolution/physical.py
@@ -0,0 +1,116 @@
+"""Execute the changed fixed-tape caller on a genuinely nonidentity B."""
+
+from hashlib import sha256
+from reference import original, require
+
+
+def encode(values, width):
+    return bytes((value >> bit) & 1 for pair in values for value in pair for bit in range(width))
+
+
+def body(tape):
+    from words import BLANK
+    tape.rewind()
+    result = bytearray()
+    for _ in range(len(tape.cells)+1):
+        value = tape.read()
+        if value == BLANK:
+            tape.rewind()
+            return bytes(result)
+        require(value in (0, 1), "binary returned payload")
+        result.append(value)
+        tape.step(1)
+    raise ValueError("terminated payload")
+
+
+def make_tape(bits):
+    from records import Tape
+    result = Tape()
+    for bit in bits:
+        result.append(bit)
+    result.rewind()
+    return result
+
+
+def check_closed(owner):
+    from words import BLANK
+    owner.idle()
+    require(owner.closed and not owner.pool.live and owner.a is owner.b is owner.current is None,
+            "closed changed caller with no live payload")
+    for item in owner.pool.tapes:
+        require(item.head == 1 and all(value == BLANK for value in item.cells),
+                "erased changed-caller scratch at origin")
+    require(owner.fourier.closed and not owner.fourier.pool.live
+            and owner.fourier.current is None, "closed changed Fourier owner")
+
+
+def read_width(port):
+    from words import RIGHT
+    port.rewind()
+    value = 0
+    try:
+        for bit in range(32):
+            if port.read() == RIGHT:
+                return value
+            require(port.read() in (0, 1), "binary returned width")
+            value |= port.read() << bit
+            port.step(1)
+        raise ValueError("bounded returned width")
+    finally:
+        port.rewind()
+
+
+def run():
+    from adapter import convolution
+    from cardinal_counts import Count
+    from check_composed import fixture
+    from check_support import no_decode
+    from session import erase_marker
+    from words import BLANK
+    # Four addresses on one length-four axis. B exchanges records 1 and 2.
+    ell, p, rows, lengths = 2, 3, 1, (2,)
+    from checks import character_packet
+    first = character_packet()
+    second = [(0, a) for a, _ in first]
+    require(all(a*a+b*b <= 1 << (2*p) for a, b in first+second), "disk-grid fixture")
+    expected_values = [(a << 2, b << 2) for a, b in original(first, second, lengths, ell, p, rows)]
+    expected = encode(expected_values, p+4)
+    require(any(a or b for a, b in expected_values), "nonzero complete convolution fixture")
+    originals = encode(first, p+2), encode(second, p+2), bytes((1,))
+    inputs = tuple(make_tape(bits) for bits in originals)
+    counts = tuple(Count.literal(value) for value in (1, ell, p, rows))
+    saved = tuple((bytes(value.tape.cells), value.tape.head) for value in counts)
+    owner = convolution(fixture()[0])
+    try:
+        with no_decode():
+            output, width_port = owner.run(*inputs, *counts)
+        actual = body(output)
+        require(actual == expected, "changed physical caller equals original rounded convolution")
+        require(tuple(body(value) for value in inputs) == originals, "unchanged borrowed data and flags")
+        require(saved == tuple((bytes(value.tape.cells), value.tape.head) for value in counts),
+                "unchanged borrowed encoded metadata")
+        width = read_width(width_port)
+        require(width == p+4, "original widened width")
+        check_closed(owner)
+        require(owner.calls == dict(forward=2, product=1, opposite=1, scale=1), "full original composition")
+        require(owner.fourier.calls == dict(roots=6, diagonals=3, reversals=0, lifts=3, truncations=3),
+                "actual three reversals omitted with all arithmetic stages retained")
+        output.clear()
+        erase_marker(output)
+        try:
+            with no_decode():
+                owner.run(*inputs, *counts)
+        except ValueError as error:
+            require("consume both" in str(error), "protected width port still enforced")
+        else:
+            raise ValueError("unconsumed width port accepted")
+        width_port.clear()
+        erase_marker(width_port)
+        require(output.read() == width_port.read() == BLANK, "consumed output ports")
+        return {"gaussians": 16, "address_bits": 2, "ell": ell, "p": p, "rows": rows,
+                "output_width": width, "output_bits": len(actual), "sha256": sha256(actual).hexdigest(),
+                "fourier_calls": dict(owner.fourier.calls), "consumer_calls": dict(owner.calls),
+                "removed_sparse_router_calls": 3, "protected_width_control": True}
+    finally:
+        for count in counts:
+            count.close()
diff --git a/research/reversal-free-convolution/reference.py b/research/reversal-free-convolution/reference.py
new file mode 100644
index 0000000000..ce4cea2ad3
--- /dev/null
+++ b/research/reversal-free-convolution/reference.py
@@ -0,0 +1,115 @@
+"""Bounded exact reference for the changed rounded convolution boundary."""
+
+from fractions import Fraction
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def geometry(lengths, ell, rows):
+    require(type(ell) is int and 2 <= ell <= 4, "reference ell in 2..4")
+    require(type(rows) is int and 1 <= rows <= 2, "reference rows in 1..2")
+    require(1 <= len(lengths) <= 3 and all(v in (ell-1, ell) for v in lengths),
+            "reference long/short axes")
+    require(sum(lengths) <= 6, "reference at most 64 addresses")
+    return 1 << sum(lengths), 1 << ell
+
+
+def coordinates(value, lengths):
+    result = [0] * len(lengths)
+    for index in range(len(lengths)-1, -1, -1):
+        result[index] = value % (1 << lengths[index])
+        value >>= lengths[index]
+    return result
+
+
+def reverse_index(value, lengths):
+    result = 0
+    for coordinate, width in zip(coordinates(value, lengths), lengths):
+        reversed_value = 0
+        for bit in range(width):
+            reversed_value = (reversed_value << 1) | ((coordinate >> bit) & 1)
+        result = (result << width) | reversed_value
+    return result
+
+
+def permute(values, lengths, ell, rows):
+    count, degree = geometry(lengths, ell, rows)
+    require(len(values) == rows*count*degree, "complete permutation reference packet")
+    return [values[(row*count+reverse_index(index, lengths))*degree+coefficient]
+            for row in range(rows) for index in range(count) for coefficient in range(degree)]
+
+
+def transform(values, lengths, ell, rows, opposite=False):
+    count, degree = geometry(lengths, ell, rows)
+    require(len(values) == rows*count*degree, "complete transform reference packet")
+    result = []
+    for row in range(rows):
+        for target in range(count):
+            total = [[0, 0] for _ in range(degree)]
+            outgoing = coordinates(target, lengths)
+            for source in range(count):
+                incoming = coordinates(source, lengths)
+                phase = sum((2*degree >> width)*a*b
+                            for width, a, b in zip(lengths, outgoing, incoming))
+                phase = phase if opposite else -phase
+                for coefficient in range(degree):
+                    wraps, destination = divmod(coefficient+phase, degree)
+                    sign = -1 if wraps % 2 else 1
+                    a, b = values[(row*count+source)*degree+coefficient]
+                    total[destination][0] += sign*a
+                    total[destination][1] += sign*b
+            result.extend((int(Fraction(a, count)), int(Fraction(b, count)))
+                          for a, b in total)
+    return result
+
+
+def product(first, second, lengths, ell, p, rows):
+    count, degree = geometry(lengths, ell, rows)
+    require(type(p) is int and ell < p <= 16, "reference precision")
+    require(len(first) == len(second) == rows*count*degree, "complete product packet")
+    result = []
+    for record in range(rows*count):
+        total = [[0, 0] for _ in range(degree)]
+        for left in range(degree):
+            a, b = first[record*degree+left]
+            for right in range(degree):
+                c, d = second[record*degree+right]
+                wrap, target = divmod(left+right, degree)
+                sign = -1 if wrap else 1
+                total[target][0] += sign*(a*c-b*d)
+                total[target][1] += sign*(a*d+b*c)
+        result.extend((int(Fraction(a, (1 << p)*degree)),
+                       int(Fraction(b, (1 << p)*degree))) for a, b in total)
+    return result
+
+
+def original(first, second, lengths, ell, p, rows):
+    a = transform(first, lengths, ell, rows)
+    b = transform(second, lengths, ell, rows)
+    return transform(product(a, b, lengths, ell, p, rows), lengths, ell, rows, True)
+
+
+def changed(first, second, lengths, ell, p, rows, omissions=(True, True, True)):
+    a = transform(first, lengths, ell, rows)
+    b = transform(second, lengths, ell, rows)
+    if omissions[0]:
+        a = permute(a, lengths, ell, rows)
+    if omissions[1]:
+        b = permute(b, lengths, ell, rows)
+    multiplied = product(a, b, lengths, ell, p, rows)
+    if omissions[2]:
+        multiplied = permute(multiplied, lengths, ell, rows)
+    return transform(multiplied, lengths, ell, rows, True)
+
+
+def routing_saving(lengths, p):
+    require(1 <= len(lengths) <= 64 and all(type(v) is int and 1 <= v <= 256 for v in lengths),
+            "bounded routing geometry")
+    require(type(p) is int and 2 <= p <= 65536, "bounded routing precision")
+    exponent = 997*((p+sum(lengths)).bit_length()-1)//1000
+    cap = 1 << exponent
+    edges = sum(width//2 for width in lengths)
+    return 3*((edges+cap-1)//cap)
diff --git a/research/reversal-free-convolution/verify.py b/research/reversal-free-convolution/verify.py
new file mode 100644
index 0000000000..199944f995
--- /dev/null
+++ b/research/reversal-free-convolution/verify.py
@@ -0,0 +1,54 @@
+"""Read-only source-bound verification of the changed physical caller."""
+
+import argparse
+from hashlib import sha256
+import importlib
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+sys.path.insert(0, str(HERE))
+
+
+def authenticate():
+    sources = json.loads((HERE / "SOURCES.json").read_text())
+    for row in sources["files"]:
+        if row["usage"] == "input":
+            path = ROOT / row["path"]
+            if not path.is_file() or path.is_symlink() or sha256(path.read_bytes()).hexdigest() != row["sha256"]:
+                raise ValueError("pinned input: " + row["path"])
+
+
+def physical():
+    source = ROOT / "research/physical-ring-product"
+    sys.path.insert(0, str(source))
+    from ring_sources import opened
+    with opened():
+        # Frozen cohort loaders install their own paths. Keep the new adapter
+        # first, followed by the authenticated live product implementation.
+        sys.path.insert(0, str(source))
+        sys.path.insert(0, str(HERE))
+        module = importlib.import_module("physical")
+        return module.run()
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--mode", choices=("algebra", "physical"), required=True)
+    args = parser.parse_args()
+    authenticate()
+    if args.mode == "physical":
+        result = physical()
+    else:
+        from checks import run
+        result = run()
+    files = {str(path.relative_to(HERE)): sha256(path.read_bytes()).hexdigest()
+             for path in sorted(HERE.iterdir()) if path.is_file()}
+    print(json.dumps({"status": "PASS_REVERSAL_FREE_CONVOLUTION", "mode": args.mode,
+                      "result": result, "package_sha256": files}, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()