Remove three endpoint reversals from physical convolution (no new κ)

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.

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.

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"
+    }
+  ]
+}