[petalas]

Summary

Scoped program-refinement proof with finite physical corroboration. The complete normalized convolution of Jose Manuel / jmbarrancoml's #3709 can omit the three endpoint reversal routines inherited from #3640, retaining bit-for-bit output equality and the same borrowed-port contract.

F_raw = B F
P(Bx, By) = B P(x, y)
G_raw(x) = G(Bx)

Thus the common frequency permutation cancels through the actual record-local polynomial consumer. For axis bit lengths a_i and P=p+sum a_i, this removes exactly 3 ceil(E/b) outer sparse-router invocations, where E=sum floor(a_i/2) and b=2^floor(997 floor(log2 P)/1000). The nonidentity-B four-address fixture removes three. There is no measured runtime factor, changed recursive supplier histogram, new kappa or selected-frontier change.

This answers #3640 Open next question 2 using #3709's later physical product. Compatible DIF/DIT ordering is classical and already appears in the upstream raw interface, androolloyd's indexed-read #673 integration and #3709's inner coefficient FFT. The new contribution is its executable refinement of this particular outer fixed-tape caller, the complete rounded-output/ownership argument and exact batching reduction. Predecessor theorems are cited dependencies, not re-audited deliverables. Produced by Nick Petalas.

Evidence

• Before: the source caller materializes B after each forward transform and before the opposite transform, with ceil(E/b) nonempty routing batches each. After: the new private Fourier adapter omits those three routines inside the unchanged complete Convolution caller.
• The changed physical caller returns the exact original natural-order oracle output: 224 bit symbols, width 7, SHA256 ad81a1219dc838dd3cd05b2aa4fb93aa80b7dee0edc77c4e0fb3b149482da8e9. It retains six roots, three diagonals, three lifts, three truncations, the polynomial product and final M scale, with zero outer reversals. Borrowed data/flags/counts, scratch erasure and protected width-port rejection pass.
• Exact algebra checks cover 24 rounded packets / 4,248 output coefficients, product equivariance on 4,248 coefficients, all six asymmetric omission counterexamples, 25 enumerated routing-batch cases and five invalid geometries. Normal and optimized modes pass.
• All three registered checks pass in 296.08 seconds total. Separately timed direct normal and optimized algebra checks each take 0.92 seconds; the direct physical check takes 298.24 seconds. These are validation durations, not a speed comparison. Environment: macOS 27.0.1 arm64, CPython 3.12.15, standard library.
• Metadata/pins, exact committed bytes, executable modes and source-history preflight pass at d1f912d9c431414c7ea639baab0415c7183958d7. The official export checks all 13 declared inputs. Read-only, empty-PATH, Git-free optimized algebra replay passes; deliberate source corruption rejects, and all 24 exported files retain their original bytes after the control.

From the repository root:

/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 -O -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 --check-modes

Any CPython 3.12 executable can replace the local path. Expected markers are PASS_REVERSAL_FREE_CONVOLUTION, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Direct checks generate stdout receipts bound to all package-file hashes. No receipt is handwritten. Exact live source pins and historical task provenance are in SOURCES.json.

Limitations

The proof assumes the retained complete Fourier and record-local product contracts, including their exact-grid/native/tape premises. The finite physical fixture uses the inherited direct/literal q2 child and reduced test guards. Production GL64/O73 execution, optimized full physical replay, Lean, Docker, the selected cold replay and the Gaussian/CRT/integer join were not run. No selected framework assumption is discharged. Independent human and formal proof-kernel review are unclaimed.

The raw Fourier convention is private to the complete convolution adapter. A standalone natural-order transform still requires the original Fourier API. The stated router count excludes routing internal to roots and the polynomial product.

Open next questions

• Bind the adapter to one complete physical Gaussian or CRT caller, first proving its input disk margin, output width/narrowing and complete field layout. The retained precision and integer-recovery obligations remain blockers.
• Instantiate the exact removed-routing formula on one production-sized encoded shape and retain its complete supplier ledger. A measured runtime factor requires a separate experiment.

Related open work

• Prove the exact input-dimension price of unequal Fourier reads #5946 determines maximal restricted-input dimensions for unequal Fourier read maps. It supplies an algebraic input-space contract, while this contribution keeps both operands unrestricted and implements a common internal frequency convention in the physical Execute complete synthetic Fourier transforms on physical tapes #3640/Implement exact physical normalized polynomial products and Fourier composition #3709 caller. No shared numerical value is compared.
• Prove a ten-product dyadic S3 convolution floor (no new κ) #6022 proves a characteristic-three bilinear-product floor for S3 convolution. It concerns a different group algebra and product-rank quantity; this PR removes record-permutation routing from the physical polynomial-Fourier caller and computes no S3 product floor.
• Reduce XOR tape travel by at least N-2 crossings (no new κ) #6028 reduces XOR-by-mask framed-record tape travel with one restored dirty scratch record. Its permutation, caller and transition-count objective differ from the three omitted outer frequency-reversal routines here. No same-instance cost is computed or disputed.
• Reuse CRT row ROM banks to save 15,420 retained cells (no new κ) #6018 reuses physical ROM banks across CRT row queries. It changes bank allocation and retained cells, whereas this PR changes the intermediate frequency convention. No ROM-bank storage quantity is computed here.

The completion refresh inspected the titles and bodies of all 15 other open account PRs created since the advance CLAIM: #6013 through #6023 and #6025 through #6028. None modifies the #3640/#3709 outer endpoint-reversal contract or computes a competing value for this fixture's three omitted outer routing calls. No additional scientific computations were run to compare those contributions. The advance CLAIM remains the canonical investigation pointer.

CI notes

Both hosted checks passed at exact head d1f912d9c431414c7ea639baab0415c7183958d7 in run 40592559504: plan in 4m32s and replay (research/reversal-free-convolution) in 7m29s. The completed checks were read once, and the run head matches the PR head.

All local checks listed above also passed. Hosted execution certifies the bounded registered checks, including normal/optimized algebra and the physical fixture; it is not independent human or formal proof-kernel acceptance of the all-parameter refinement theorem. No CI failure remains.

Merge danger

Door: two-way. Blast radius: isolated research package.