diff --git a/research/many-axis-prime-supply/.gitattributes b/research/many-axis-prime-supply/.gitattributes
new file mode 100644
index 0000000000..e022399ddb
--- /dev/null
+++ b/research/many-axis-prime-supply/.gitattributes
@@ -0,0 +1 @@
+source/** -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol
diff --git a/research/many-axis-prime-supply/INDEPENDENT.md b/research/many-axis-prime-supply/INDEPENDENT.md
new file mode 100644
index 0000000000..b9ff18ee1e
--- /dev/null
+++ b/research/many-axis-prime-supply/INDEPENDENT.md
@@ -0,0 +1,143 @@
+# Independent review of the many-axis prime-supply port
+
+Scope: mathematical and uniform-setup review only. No repository edits,
+publication, selected-frontier claim, production-sized prime search or formal
+proof-kernel review.
+
+## Source binding
+
+Canonical main: 20ecf2891d80b5acf18d980b2164fb44ea7faa90.
+Tensor PR3935 head: 240597ed313fc2854c0462b23c89dc3bae72aaf5.
+`research/physical-gaussian-tensor/tensor_plan.py` has
+`dimensions=axes+1=D` and `d=dimensions+1=D+1`.
+Its `production_axis` requires, for gap g=t-s,
+
+    4*d*g > s, (2*d-1)*g < s.
+
+Thus the required strict gap interval is
+`t/(4*d+1) < g < t/(2*d)`.
+Target lengths are `t=2^ell` or `2^(ell-1)` and the final axis has the first
+length. The repeated 7x7 finite fixture is not a CRT prime-supply witness.
+
+Primary analytic source independently consulted:
+Fiori, Kadiri and Swidinsky, *Sharper bounds for the error term in the Prime
+Number Theorem*, arXiv:2206.12557v2 (17 May 2023), Corollary 22:
+https://arxiv.org/pdf/2206.12557v2 . Corollary22 gives exponent0.84768363; using0.8476 is a safe weakening.
+The resulting pi-minus-Li error is
+`9.2211*x*sqrt(log x)*exp(-0.8476*sqrt(log x))` for every x>=2.
+
+## Interior interval and prime count
+
+For each target t use
+
+    a=t*(1-1/(3*d)), b=t*(1-1/(4*d)), interval (a,b].
+
+Every selected prime satisfies the strict source ratios. This alone does not
+supply the independent source period guard. Write H for the actual
+`target_halo` field and K=H+2w. Add the explicit condition
+`K<=2^(ell-3)` (the sufficient executable bit-length check
+`K.bit_length()<=ell-3` avoids forming that power). Then for both targets,
+`s>a>=5*2^(ell-1)/6>2^(ell-2)>=2K`, which discharges the third
+`production_axis` predicate. Polynomial H,w eventually meet this condition
+under the retained growth laws; a p cutoff needs their fixed constants.
+None of `production_common` is inferred from this prime lemma. The length is
+`t/(12*d)`. Write `y=log(t)`.
+For the stated large domain, endpoint logs lie in [y/2,y], hence the sum of
+the two FKS endpoint errors is at most
+`20*t*sqrt(y)*exp(-sqrt(y)/2)`.
+The Li increment is at least `(b-a)/y=t/(12*d*y)`.
+It follows that the interval contains at least D primes whenever
+
+    480*d*y^(3/2)*exp(-sqrt(y)/2) <= 1,
+    t >= 24*d*D*y.
+
+Neither an integrality nor an open-endpoint term is missing: pi(b)-pi(a)
+counts exactly the integers in (a,b], including b if prime.
+
+## Uniform sufficient threshold
+
+Suppose ell>=2^32, 2<=d<=ell^334, D=d-1, and
+`t in {2^(ell-1),2^ell}`. Then ell/4 <= y <= ell.
+The function `y^(3/2)*exp(-sqrt(y)/2)` decreases for y>36. Therefore the
+first left side is at most `480*z^671*exp(-z/4)`, z=sqrt(ell)>=65536.
+At z=65536 its logarithm is less than
+
+    7+671*16-16384 = -5641.
+
+Here log480<7 follows already from e>5/2 and (5/2)^7>480; log2<1.
+The logarithmic derivative `671/z-1/4` is negative throughout this range.
+
+For the second condition, dD<=ell^668 and y<=ell. It suffices that
+`ell/4 >= log24+669*log(ell)`.
+At ell=2^32 the right side is below `5+669*32=21413`, while the left side
+is 2^30; the difference increases because `1/4-669/ell>0`.
+Thus both sufficient conditions hold uniformly.
+
+## Distinctness, ordering and product budget
+
+All these primes exceed 2, so they are odd. The intervals at t=r/2 and t=r
+are disjoint. Enumerating ascending distinct primes in each therefore gives
+pairwise-coprime lengths across both groups. Two monotone source tables plus
+one scan of the target flags suffice to assign primes in original axis order;
+the final axis is assigned from the r table.
+
+For every selected length s/t>1-1/(3d). Bernoulli's inequality gives
+
+    S/T > (1-1/(3d))^D >= 1-D/(3d) > 2/3,
+
+so `T/S<3/2<2`. No floating logarithmic estimate is needed here.
+
+## New-regime distinction and predecessor credit
+
+The source08 selector and CinnaDavis's `prime-source-selector-transfer` already
+provide an all-size selection argument on the domain `log(t)>8d`. Chafik's
+PR1786 already uses the same general strategy of explicit PNT error bounds for
+fine intervals. Trial division itself is inherited. This review claims none of
+those general ideas as new.
+
+The changed source binding matters: at ell=2^32 and d=ell^333, the new
+`d<=ell^334` criterion holds, while `log(t)<=ell<8d` contradicts the old lemma's
+premise. The independent checker represents this enormous dimension only by
+an integer power/bit-length certificate; it creates no prime-sized target or
+axis-length list. Under the retained D=Theta(p^.997), ell=Theta(p^.003) family,
+`D+1<=ell^334` holds eventually, whereas log(t)/d tends to zero.
+
+## Conservative uniform setup bill and limits
+
+Trial division is inherited from source08, not a new algorithm. A deliberately
+loose fixed-tape implementation can examine all candidate integers below r in
+the two intervals and trial-divide by every divisor below the candidate.
+There are O(r^2) divisions, each performed by binary scans in O(ell^2) steps.
+Encoded candidate/divisor counters and rational endpoint preparation have
+polynomial overhead; repeated buffers are cleared after each division.
+At most D ascending primes from each of the two bands suffice.
+Two sequential tables of at most D primes need O(D*ell) output/backing cells.
+The flags-to-axis assignment uses monotone cursors, not numerical random access.
+
+For the explicit large domain, log2(d)<=334*log2(ell)=O(ell), so endpoint
+arithmetic and candidate/divisor/count buffers all have O(ell) bits. Ordinary
+binary long division uses O(ell^2) reads/writes/unit moves on fixed many tapes.
+The two tables and final output require O(D*ell) cells and linear total scans.
+Consequently setup is O(r^2*ell^2+D*ell) steps and O(D*ell+ell) visited cells,
+including cleared scratch backing. Each candidate and divisor is an encoded
+counter, not a host control integer. Ascending enumeration supplies distinct
+primes without retaining rejected candidates or a growing recursion stack.
+
+The head contract is: borrowed encoded inputs and flag stream return unchanged
+at LEFT+1, the declared source/flag outputs return at LEFT+1, and temporary
+working bodies are erased with their heads at LEFT+1. Rewinding and erasing
+O(ell) arithmetic buffers after each test is absorbed into O(ell^2); the final
+sequential table clearing/rewind costs O(D*ell). No dirtied register is treated
+as free. This is a written fixed-tape implementation argument; the small host
+reference is not an executed literal encoded implementation.
+
+In particular the setup bound is `r^2*poly(ell,D)` steps and
+`poly(ell,D)` visited cells. Under the retained caller laws ell=Theta(p^.003),
+D=Theta(p^.997), and V>=2^(c*p) for fixed c>0, this setup is `2^o(p)=o(V)`.
+An explicit p cutoff requires the fixed constants in those Theta statements;
+the (ell,d) threshold above is already explicit and directly checkable.
+
+Remaining obligations: full caller/source08 integration, all non-prime Gaussian
+and routing premises, native supplier execution, production tensor precision,
+CRT/integer recovery, physical reserve and any selected-frontier admission.
+This review establishes no new kappa and no independent human/formal acceptance.
diff --git a/research/many-axis-prime-supply/LICENSE b/research/many-axis-prime-supply/LICENSE
new file mode 100644
index 0000000000..261eeb9e9f
--- /dev/null
+++ b/research/many-axis-prime-supply/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/research/many-axis-prime-supply/NOTICE.md b/research/many-axis-prime-supply/NOTICE.md
new file mode 100644
index 0000000000..2b63b0479e
--- /dev/null
+++ b/research/many-axis-prime-supply/NOTICE.md
@@ -0,0 +1,11 @@
+# Attribution and source notice
+
+New source-bound proof, host reference and controls: ToikY, with substantial OpenAI Codex assistance, including separate AI proof/test contexts. Apache-2.0; no independent human or formal-kernel acceptance is asserted.
+
+Byte-exact source exports retain their original content and credits. Jose Manuel (`jmbarrancoml`) owns PR3935's tensor implementation/interface; Tekalign (`tekuuu`) owns PR4024's encoded CRT converter and proof. Their exported READMEs retain the manuscript, RaD/hipotures, Chafik Boukhalfa, eumemic, icekylinx, Hanson Sun, Artus Krohn-Grimberghe, Mason Hale, Douglas Colkitt and other nested predecessor acknowledgements. Only the complete production-axis method is extracted for a host semantic check; their full runtimes/archives are not copied or executed here.
+
+The canonical source08 assembly belongs to the retained OpenAI manuscript / Douglas Colkitt repository lineage under Apache-2.0. The original upstream repository is https://github.com/openai/math, commit adc7f1241b42e322a6451854ab7e4b4c146bf78a. This package exports the exact canonical-main build section, without changing it. Retain the repository and upstream notices when incorporating the larger source chain.
+
+Credit Cinna Davis for the old-domain prime-source selector transfer; Chafik Boukhalfa/chafreaky PR1786 for earlier explicit PNT fine-prime supply; JosieElliston for its transfer audit; Harvey–van der Hoeven and source08 for prime-interval/trial-division construction; Agarwal and Cooley for CRT Fourier algebra. Trial division and the general PNT strategy are inherited, not new inventions.
+
+Andrew Fiori, Habiba Kadiri and Joshua Swidinsky, arXiv:2206.12557v2 Corollary22, supply the imported analytic estimate. Tim Trudgian's earlier explicit estimates are part of the credited predecessor method. No paper text is vendored and no external analytic theorem is reproved by these finite checks. This is not an official OpenAI release or endorsement.
diff --git a/research/many-axis-prime-supply/PROOF.md b/research/many-axis-prime-supply/PROOF.md
new file mode 100644
index 0000000000..1046c7493c
--- /dev/null
+++ b/research/many-axis-prime-supply/PROOF.md
@@ -0,0 +1,233 @@
+# Prime source supply for the newer many-axis tensor caller
+
+ToikY, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Scope and the source obligation
+
+PR4024, head `e99297be6749518a1b5b85cd129ecaf204d26c63`, supplies the
+encoded CRT address conversion but explicitly assumes pairwise-coprime odd
+source lengths. Its numerical tensor dependency is PR3935, head
+`240597ed313fc2854c0462b23c89dc3bae72aaf5`. This package supplies those lengths
+for the newer many-axis asymptotic caller, subject to an explicit sufficient
+cutoff and period condition. It supplies no numerical tensor composition,
+integer recovery, native execution, complete supplier or new kappa.
+
+The actual PR3935 `TensorPlan` has `dimensions=axes+1` resampled scalar axes.
+Call this number `D`; its internal `d` is `D+1`. Its target lengths are
+`t_i in {2^ell,2^(ell-1)}`, with the final axis always `2^ell`. In
+`TensorPlan.production_axis`, putting `g=t-s`, the exact ratio predicates are
+
+```
+4d*g > s,              (2d-1)*g < s.
+```
+
+Equivalently, `t/(4d+1)<g<t/(2d)`. The same method also requires
+`s>2*(target_halo+2*w)`. The source method is authenticated before its complete
+AST is extracted and checked with an integer-semantic Count adapter. The
+source imports and numerical engine are not executed. This is a host reference
+check of the exact method, not execution of its encoded Count implementation.
+
+The old prime-length argument in canonical source08,
+`upstream/build/sections/08-assembly.tex`, uses Harvey--van der Hoeven's
+prime-interval lemma with a condition of the form `log(t)>8d`. Its old small
+dimension exponent makes that condition eventual. Under the newer laws
+`D=Theta(p^.997)` and `ell=Theta(p^.003)`, `log(t)/d` instead tends to zero.
+This is a change of admissible parameter regime, not a counterexample to the
+old lemma. We replace that particular source-supply argument; the existing
+CRT algebra, trial-division idea and tensor cost results retain predecessor
+credit.
+
+## Explicit prime-supply statement
+
+Let integer `ell>=2^32`, `D>=1`, `d=D+1<=ell^334`, and let every target
+`t` be `2^ell` or `2^(ell-1)`. For each of the two target sizes use the
+interior interval
+
+```
+I(t,d) = (a,b],
+a = t*(1-1/(3d)),       b = t*(1-1/(4d)).
+```
+
+Each interval contains at least D primes. The intervals for the two target
+sizes are disjoint. Choose as many increasing primes from each as its target
+flags require, then merge the two lists in the original flag order. This gives
+D distinct odd primes `s_i` and therefore pairwise coprimality. For every axis,
+
+```
+t/(4d) <= t-s < t/(3d).
+```
+
+These inequalities lie strictly inside the actual source ratio predicates:
+`t/(4d)>t/(4d+1)` and `t/(3d)<t/(2d)`.
+Writing `S=product(s_i)` and `T=product(t_i)`, Bernoulli gives
+
+```
+S/T > (1-1/(3d))^D >= 1-D/(3d) > 2/3,
+```
+
+so `T/S<3/2<2`. No numerical approximation or search heuristic establishes
+these ratio or coprimality conclusions.
+
+For the complete source method, additionally assume
+
+```
+K = target_halo+2*w <= 2^(ell-3).
+```
+
+Since `d>=2`, each selected prime is greater than
+`(5/6)*2^(ell-1)>2^(ell-2)>=2K`. Hence the period predicate also holds.
+This is a separate sufficient condition; prime abundance alone does not admit
+an arbitrarily large halo. In the retained newer caller, halo and `w` are
+polynomial in p, whereas `2^ell` exceeds every fixed polynomial. This condition
+is therefore eventual under those caller premises. Unrelated
+`production_common` Gaussian, precision, separation, native and global
+admissions remain outside this length-supply result.
+
+## Imported analytic input and effective cutoff
+
+We use Fiori, Kadiri and Swidinsky, *Sharper bounds for the error term in the
+Prime Number Theorem*, [arXiv:2206.12557v2](https://arxiv.org/pdf/2206.12557v2),
+Corollary 22. Their explicit unconditional theorem implies the following
+slightly weakened estimate, valid for every real `x>=2`:
+
+```
+|pi(x)-Li(x)| <= 9.2211*x*sqrt(log(x))*exp(-.8476*sqrt(log(x))).
+```
+
+Here `Li(x)=integral_2^x dt/log(t)`. The decay coefficient `.8476` is a
+deliberate weakening of the corollary's more precise coefficient. This analytic
+theorem is an imported mathematical input. The finite verifier does not
+reprove its zeta-function analysis or claim formal-kernel verification.
+
+Put `y=log(t)`. For `d>=2,t>=4`, both endpoints are between `sqrt(t)` and t.
+Because `9.2211<10` and `.8476/sqrt(2)>1/2`, the sum of their two prime-counting
+error bounds is at most `20*t*sqrt(y)*exp(-sqrt(y)/2)`. Also
+
+```
+Li(b)-Li(a) >= (b-a)/log(t) = t/(12*d*y).
+```
+
+Consequently
+
+```
+pi(b)-pi(a) >= t/(12*d*y) - 20*t*sqrt(y)*exp(-sqrt(y)/2).
+```
+
+The following two effective inequalities suffice for at least D primes:
+
+```
+480*d*y^(3/2)*exp(-sqrt(y)/2) <= 1,
+t >= 24*d*D*y.
+```
+
+We now establish both uniformly without constructing a giant target integer.
+For `ell>=2`, the two target sizes satisfy `ell/4<=y<=ell`, using
+`1/2<log(2)<1`. Thus the first left side is at most
+
+```
+480*ell^(335.5)*exp(-sqrt(ell)/4)
+   = 480*z^671*exp(-z/4),       z=sqrt(ell).
+```
+
+For `ell>=2^32`, `z>=z0=2^16`. At that endpoint, its logarithm is less than
+`7+671*16-2^14 = -5641`, since `log(480)<7` and `log(z0)<16`.
+The derivative of `log(480)+671*log(z)-z/4` is negative for `z>=z0`, because
+`4*671<z0`. The first inequality follows for the entire domain.
+
+For the second, `24*d*D*y<=24*ell^669`, while `t>=exp(ell/4)`.
+At `ell0=2^32`,
+
+```
+log(24*ell0^669) < 5+669*32 = 21413 < ell0/4 = 1073741824.
+```
+
+The derivative of `ell/4-669*log(ell)-5` is positive in that domain, because
+`4*669<ell0`. This proves the second inequality uniformly. All constants in
+these threshold comparisons are checked by small exact integers/rationals.
+The verifier never forms `2^(2^32)` or runs an astronomical prime search.
+
+Finally, the newer growth laws imply
+`d=O(ell^(997/3))`, and `997/3<334`. Thus `d<=ell^334` holds eventually,
+including fixed constants in those growth laws. The cutoff is deliberately
+conservative; no near-optimal or practically useful prime-search threshold is
+claimed.
+
+## Uniform construction and complete setup bill
+
+This section describes a uniform fixed-tape algorithm. It is a proof of
+constructibility and a conservative bill; the finite program in this package
+is explicitly a host-integer reference rather than that machine.
+
+Compute encoded integer endpoints
+
+```
+lo = t-ceil(t/(3d))+1,          hi = t-ceil(t/(4d)).
+```
+
+They enumerate exactly `(a,b]`, including nonintegral endpoints correctly.
+For each target size, scan candidate integers from lo through hi in increasing
+order. Test primality by division by every integer from 2 through candidate-1;
+reject as soon as one remainder is zero. This deliberately simple test is
+correct and avoids an unpriced primality oracle. Stop when the required quota
+is reached. The proved prime count guarantees successful completion above the
+cutoff. Below it the finite reference may reject insufficient intervals; it
+does not manufacture a repeated or composite length.
+
+All candidates, divisors and remainders have `O(ell)` bits. The dimension and
+quota counters fit the same bound in the admitted domain; the source flags
+are a packed stream, not D separate runtime tapes. Binary schoolbook division
+uses a fixed number of scratch words and `O(ell^2)` symbol operations including
+the scan/return costs. Two target intervals contain at most `2r` candidates,
+where `r=2^ell`; each has fewer than r divisors. Their complete conservative
+search cost is therefore
+
+```
+O(r^2*ell^2).
+```
+
+The two selected-prime tables use `O(D*ell)` cells. A monotone cursor in each
+table, while scanning the original flags, emits the source words in the
+original axis order; the final full-axis flag remains implicit exactly as in
+`TensorPlan`. No random access or per-axis tape is needed. Endpoint setup,
+quota counting, list copies, erasure and restoration cost
+`O(poly(ell,log(d))+D*ell)` in addition to the search. A fixed inventory of
+arithmetic, table and output tapes suffices, with `O(D*ell+ell)` visited
+backing for this producer. The caller must consume and clear its distinct
+owned output before reuse; borrowed flag and parameter heads are restored.
+No source-meter constant or literal fixed-tape execution is claimed.
+
+Computing the total source product and CRT metadata uses `O(D*ell)`-bit
+integers, hence polynomial setup in p under `D*ell=Theta(p)`. With the newer
+`ell=Theta(p^.003)` law, the entire setup above, including conservative table
+management, is `2^O(ell)*poly(p)=2^o(p)`. The actual caller volume
+`V=C*T*R`, with `log2(T)=Theta(p)` and `C,R>=1`, is at least `2^(c*p)` for a
+fixed positive c. Thus setup is `o(V)` and fits the retained conversion
+allowance. This does not price the unchanged router/native operations or
+turn their conditional universal premises into verification results.
+
+## Evidence and controls
+
+The five finite cases include both target widths, nonmonotone flags, repeated
+target sizes and source-order reconstruction. Every returned prime is checked
+by the host trial-division reference, full source method, exact rational band,
+distinctness and complete product ratio. The emitted source words have exactly
+ell little-endian bits per axis; the flags omit the final implicit one.
+An independent checker uses a separate Eratosthenes sieve and independently
+reconstructs the complete bytes and source predicates. These small examples
+corroborate the implementation and source binding; their existence does not
+prove the imported analytic input or the large-cutoff theorem.
+
+Negative controls cover insufficient supply, nonliteral flags, a missing final
+full axis, an attempted giant finite run, strict source ratio failures, period
+failure and a composite. Separate boundary tests exercise explicit supplied
+values, source authentication, receipts and read-only exports. Exact validation
+receipts distinguish host execution from the written uniform algorithm.
+
+Credit the source08 authors and Harvey--van der Hoeven for prior prime-interval
+and trial-division construction; CinnaDavis's prime-selector transfer and
+Chafik Boukhalfa/PR1786 and its audit for prior selector/prime-supply work;
+Fiori--Kadiri--Swidinsky for the analytic estimate; Jose Manuel/PR3935 for the
+actual production predicates and newer caller; and Tekalign/PR4024 for the
+explicit unresolved CRT source premise and encoded layout. Source README
+credits and frozen bytes are retained. This result closes that stated length
+premise, not the numerical recovery, full multiplication or selected frontier.
diff --git a/research/many-axis-prime-supply/README.md b/research/many-axis-prime-supply/README.md
new file mode 100644
index 0000000000..f3f736734a
--- /dev/null
+++ b/research/many-axis-prime-supply/README.md
@@ -0,0 +1,36 @@
+# Prime supply for the actual many-axis tensor caller
+
+This supplies the odd, pairwise-coprime source lengths explicitly left open by [PR4024](https://github.com/CrocSwap/integer-mult-bounds/pull/4024), bound to [PR3935](https://github.com/CrocSwap/integer-mult-bounds/pull/3935)'s actual `TensorPlan.production_axis`. It repairs one parameter-regime implication; no new κ or complete supplier is claimed.
+
+Let D be the actual scalar-axis count, d=D+1, and targets be 2^ell or 2^(ell−1), with the final axis full. For **ell≥2^32, 2≤d≤ell^334** and **target_halo+2w≤2^(ell−3)**, choose distinct primes from each interior interval `(t(1−1/(3d)), t(1−1/(4d))]`. Each interval contains at least D primes; every chosen length meets the complete source ratio/period guards, and the full product ratio satisfies **T/S<3/2<2**.
+
+[PROOF.md](PROOF.md) derives the effective sufficient domain from Fiori–Kadiri–Swidinsky [Corollary22](https://arxiv.org/pdf/2206.12557v2), an imported analytic theorem. It proves a conservative uniform fixed-tape trial-division/list construction with `O(r² ell²+D ell)` steps and `O(D ell+ell)` visited backing for the source-length producer, r=2^ell, including sequential output and scratch/head restoration. Under the retained D=Theta(p^.997), ell=Theta(p^.003), V≥2^(cp) laws this setup is 2^o(p)=o(V). An explicit p cutoff needs the fixed growth/halo constants. The (ell,d) cutoff is intentionally enormous, not a practical search target.
+
+The old source08/Cinna Davis selector uses `log(t)>8d`, valid eventually in its original small-dimension family. It does not directly cover this newer family, where log(t)/d→0. Chafik's PR1786 and JosieElliston's audit already use explicit PNT error bounds for fine intervals; the new result is the exact newer-caller binding, guard-safe band, explicit sufficient domain and complete ordering/product/setup argument.
+
+## Evidence and boundary
+
+The executed program is a **host-integer finite reference**, `encoded_execution=false`. It authenticates five retained files before extracting the complete source `production_axis` AST and checking it with a semantic Count adapter. It does not import or run the predecessor numerical engine or encoded arithmetic runtime. The fixed-tape algorithm and its bill are written constructions, not literal encoded executions.
+
+Five small coprime cases cover both target scales, repeated scales, nonmonotone flags and final-axis ordering. An independent checker imports no primary executable and reconstructs primes with Eratosthenes, exact predicates, product and emitted source/flag hashes. The primary includes8 internal controls; the separate suite checks50 expected rejections and5 positives. See [RESULT.json](RESULT.json), [INDEPENDENT.md](INDEPENDENT.md) and the executable checks. These corroborate the finite reference and symbolic inequalities; they do not reprove the imported analytic theorem or execute giant primes.
+
+Unrelated `production_common` Gaussian/precision/separation policies, numerical tensor composition, native premises, CRT integer recovery and final normalization, complete physical reserve/stock, supplier integration and frontier admission remain open. The repeated7×7 predecessor fixture remains conformance evidence and is not repurposed as coprime production supply.
+
+## Reproduce
+
+Python3.12, standard library; no network, Git, external inputs or package writes are required at replay. All5 source exports are local and pinned by byte size, SHA256 and Git blob in [SOURCES.json](SOURCES.json) and [SOURCE-PINS.json](SOURCE-PINS.json).
+
+```sh
+python3.12 -B scripts/research_package.py --package research/many-axis-prime-supply
+```
+
+From a Git-free package export, run `verify.py`, `independent.py`, and `test_verify.py` with Python3.12 and `-B`. The default independent command checks the colocated complete primary receipt. All commands also work with `-O`. The huge threshold is checked symbolically without forming 2^(2^32) or an axis list of that size. [TASK.json](TASK.json) records the changed task scope, overlap coverage, cutoff and remaining questions. The historical selected-record/catalogue pins are provenance, not runtime inputs.
+
+## Open next questions
+
+1. Lower and admit the written sequential prime producer at the actual encoded `TensorPlan`/CRT interface. First review the full source/head/output contracts and period premise; literal production implementation and complete caller integration are blockers.
+2. Complete numerical tensor composition and integer recovery under the actual policies. Coordinate with Jose Manuel's [Discussion3664 clarification](https://github.com/CrocSwap/integer-mult-bounds/discussions/3664#discussioncomment-19036660), retaining the total gamma and both final S factors. Prime supply alone does not discharge those obligations.
+
+## Credit
+
+ToikY prepared this source binding, proof and checks with substantial OpenAI Codex assistance and separate AI review contexts. Credit Jose Manuel/jmbarrancoml, Tekalign/tekuuu, Cinna Davis, Chafik Boukhalfa, JosieElliston, Fiori–Kadiri–Swidinsky, source08/OpenAI manuscript/Douglas Colkitt, Harvey–van der Hoeven and Agarwal–Cooley. Frozen exported READMEs retain the deeper lineage. [NOTICE.md](NOTICE.md) and [LICENSE](LICENSE) preserve attribution and Apache-2.0 terms.
diff --git a/research/many-axis-prime-supply/RESULT.json b/research/many-axis-prime-supply/RESULT.json
new file mode 100644
index 0000000000..923d67d8e5
--- /dev/null
+++ b/research/many-axis-prime-supply/RESULT.json
@@ -0,0 +1,207 @@
+{
+  "cases": [
+    {
+      "D": 1,
+      "S": 223,
+      "T": 256,
+      "address_bits": 8,
+      "d": 2,
+      "ell": 8,
+      "encoded_execution": false,
+      "flag_bit_length": 0,
+      "flag_bits_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855",
+      "flags": [
+        1
+      ],
+      "primes": [
+        223
+      ],
+      "production_tensor_execution": false,
+      "source_bit_length": 8,
+      "source_bits_sha256": "6aa472d266dc1bd49066a0bfab2308ecaceb2f6cb25d16d71a93a5ff196a82c2",
+      "source_guard_adapter": "host-integer Count semantics; complete authenticated AST method",
+      "source_guard_checks": 1,
+      "target_halo": 16,
+      "targets": [
+        256
+      ],
+      "w": 2
+    },
+    {
+      "D": 3,
+      "S": 26621083873,
+      "T": 34359738368,
+      "address_bits": 35,
+      "d": 4,
+      "ell": 12,
+      "encoded_execution": false,
+      "flag_bit_length": 2,
+      "flag_bits_sha256": "b413f47d13ee2fe6c845b2ee141af81de858df4ec549a58b7970bb96645bc8d2",
+      "flags": [
+        0,
+        1,
+        1
+      ],
+      "primes": [
+        1879,
+        3761,
+        3767
+      ],
+      "production_tensor_execution": false,
+      "source_bit_length": 36,
+      "source_bits_sha256": "596904c4b724e18460fe15f5bd058f04ab3acbac6a032ce9adb06d56a52db249",
+      "source_guard_adapter": "host-integer Count semantics; complete authenticated AST method",
+      "source_guard_checks": 3,
+      "target_halo": 16,
+      "targets": [
+        2048,
+        4096,
+        4096
+      ],
+      "w": 2
+    },
+    {
+      "D": 4,
+      "S": 27429511315202641,
+      "T": 36028797018963968,
+      "address_bits": 55,
+      "d": 5,
+      "ell": 14,
+      "encoded_execution": false,
+      "flag_bit_length": 3,
+      "flag_bits_sha256": "85f90dfea1d8027e1463e5ca971a250110a20df0119d204a74220bc63516d15b",
+      "flags": [
+        1,
+        0,
+        1,
+        1
+      ],
+      "primes": [
+        15299,
+        7649,
+        15307,
+        15313
+      ],
+      "production_tensor_execution": false,
+      "source_bit_length": 56,
+      "source_bits_sha256": "d9fee5cbcb717a1fcf0ded07f6d08e7f8b7ee38c0ff5d5c2013f07f83df5c33a",
+      "source_guard_adapter": "host-integer Count semantics; complete authenticated AST method",
+      "source_guard_checks": 4,
+      "target_halo": 16,
+      "targets": [
+        16384,
+        8192,
+        16384,
+        16384
+      ],
+      "w": 2
+    },
+    {
+      "D": 6,
+      "S": 1823994740588505902039923,
+      "T": 2417851639229258349412352,
+      "address_bits": 81,
+      "d": 7,
+      "ell": 14,
+      "encoded_execution": false,
+      "flag_bit_length": 5,
+      "flag_bits_sha256": "01e246b58d8e782fc96881c090d833eefa37e804cb308aeae0f7471c9ef1ea1a",
+      "flags": [
+        0,
+        1,
+        0,
+        1,
+        0,
+        1
+      ],
+      "primes": [
+        7817,
+        15607,
+        7823,
+        15619,
+        7829,
+        15629
+      ],
+      "production_tensor_execution": false,
+      "source_bit_length": 84,
+      "source_bits_sha256": "000088c72e4aa19b77230557e1b7af048dbe0de5b9ba2cf963472aa04de30ac2",
+      "source_guard_adapter": "host-integer Count semantics; complete authenticated AST method",
+      "source_guard_checks": 6,
+      "target_halo": 16,
+      "targets": [
+        8192,
+        16384,
+        8192,
+        16384,
+        8192,
+        16384
+      ],
+      "w": 2
+    },
+    {
+      "D": 7,
+      "S": 29793443698968829367437279271,
+      "T": 39614081257132168796771975168,
+      "address_bits": 95,
+      "d": 8,
+      "ell": 14,
+      "encoded_execution": false,
+      "flag_bit_length": 6,
+      "flag_bits_sha256": "cadb8048d389403a76d11dc0bbd99cb34b0b79245cd53ab5bab530bc7240d423",
+      "flags": [
+        1,
+        0,
+        0,
+        1,
+        1,
+        0,
+        1
+      ],
+      "primes": [
+        15727,
+        7853,
+        7867,
+        15731,
+        15733,
+        7873,
+        15737
+      ],
+      "production_tensor_execution": false,
+      "source_bit_length": 98,
+      "source_bits_sha256": "0e02fc5f360c28732858cc4f9befd97a14b2cb75a25755bf7b8f0b4c7e1feb77",
+      "source_guard_adapter": "host-integer Count semantics; complete authenticated AST method",
+      "source_guard_checks": 7,
+      "target_halo": 16,
+      "targets": [
+        16384,
+        8192,
+        8192,
+        16384,
+        16384,
+        8192,
+        16384
+      ],
+      "w": 2
+    }
+  ],
+  "encoded_execution": false,
+  "full_multiplication_theorem": false,
+  "mode": "host-reference",
+  "new_kappa": false,
+  "schema_version": 1,
+  "semantic_controls": 8,
+  "threshold": {
+    "FKS_reference": "arXiv:2206.12557v2 Corollary22; weaker decay coefficient0.8476",
+    "analytic_input_imported": true,
+    "analytic_input_reproved": false,
+    "dimension_power": 334,
+    "ell0": 4294967296,
+    "error_exponential_lower": 16384,
+    "error_log_upper": 10743,
+    "giant_power_constructed": false,
+    "period_premise": "K=target_halo+2*w <= 2^(ell-3); separate from prime abundance",
+    "volume_exponential_lower": 1073741824,
+    "volume_log_upper": 21413,
+    "z0": 65536
+  }
+}
diff --git a/research/many-axis-prime-supply/SOURCE-PINS.json b/research/many-axis-prime-supply/SOURCE-PINS.json
new file mode 100644
index 0000000000..224661262a
--- /dev/null
+++ b/research/many-axis-prime-supply/SOURCE-PINS.json
@@ -0,0 +1,27 @@
+{
+  "PR3935-README.md": {
+    "bytes": 6383,
+    "git_blob": "2b665e76b4e86421bbea53b2252df8e81c91b290",
+    "sha256": "7a7f218579ae4ff192bd4b7fdf00ba008117f6d6fbcb3a70e2d021be5bf8a209"
+  },
+  "PR3935-tensor_plan.py": {
+    "bytes": 12079,
+    "git_blob": "239caba2d2ccf2640c36d377949df3fb6a920cf0",
+    "sha256": "474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3"
+  },
+  "PR4024-PROOF.md": {
+    "bytes": 11035,
+    "git_blob": "479a2b727b67b88efc8bdc64bde340a1c0d95ec3",
+    "sha256": "7b141475955cc372c5936118ff16e8748b589b93de2d26b76da28feec9b45de4"
+  },
+  "PR4024-README.md": {
+    "bytes": 5356,
+    "git_blob": "63648c961b96c6c76c305471b102e26d6b861d1b",
+    "sha256": "2f179858402d1eac28b1da46139fa3198a625375532cc2c53a01c1ffc565281b"
+  },
+  "source08-assembly.tex": {
+    "bytes": 46444,
+    "git_blob": "337810a1d9a58a2ecf14123420923c039ba322a6",
+    "sha256": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a"
+  }
+}
diff --git a/research/many-axis-prime-supply/SOURCES.json b/research/many-axis-prime-supply/SOURCES.json
new file mode 100644
index 0000000000..c95069c3dd
--- /dev/null
+++ b/research/many-axis-prime-supply/SOURCES.json
@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ],
+  "source_exports": [
+    {
+      "path": "research/many-axis-prime-supply/source/PR3935-README.md",
+      "origin_repository": "CrocSwap/integer-mult-bounds",
+      "origin_commit": "240597ed313fc2854c0462b23c89dc3bae72aaf5",
+      "origin_path": "research/physical-gaussian-tensor/README.md",
+      "bytes": 6383,
+      "git_blob": "2b665e76b4e86421bbea53b2252df8e81c91b290",
+      "sha256": "7a7f218579ae4ff192bd4b7fdf00ba008117f6d6fbcb3a70e2d021be5bf8a209",
+      "usage": "Byte-exact local source export; complete production_axis AST is the only extracted executable. README/proof/source08 bind scope and credit; full predecessor numerical runtimes not imported."
+    },
+    {
+      "path": "research/many-axis-prime-supply/source/PR3935-tensor_plan.py",
+      "origin_repository": "CrocSwap/integer-mult-bounds",
+      "origin_commit": "240597ed313fc2854c0462b23c89dc3bae72aaf5",
+      "origin_path": "research/physical-gaussian-tensor/tensor_plan.py",
+      "bytes": 12079,
+      "git_blob": "239caba2d2ccf2640c36d377949df3fb6a920cf0",
+      "sha256": "474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3",
+      "usage": "Byte-exact local source export; complete production_axis AST is the only extracted executable. README/proof/source08 bind scope and credit; full predecessor numerical runtimes not imported."
+    },
+    {
+      "path": "research/many-axis-prime-supply/source/PR4024-PROOF.md",
+      "origin_repository": "CrocSwap/integer-mult-bounds",
+      "origin_commit": "e99297be6749518a1b5b85cd129ecaf204d26c63",
+      "origin_path": "research/crt-address-streams/PROOF.md",
+      "bytes": 11035,
+      "git_blob": "479a2b727b67b88efc8bdc64bde340a1c0d95ec3",
+      "sha256": "7b141475955cc372c5936118ff16e8748b589b93de2d26b76da28feec9b45de4",
+      "usage": "Byte-exact local source export; complete production_axis AST is the only extracted executable. README/proof/source08 bind scope and credit; full predecessor numerical runtimes not imported."
+    },
+    {
+      "path": "research/many-axis-prime-supply/source/PR4024-README.md",
+      "origin_repository": "CrocSwap/integer-mult-bounds",
+      "origin_commit": "e99297be6749518a1b5b85cd129ecaf204d26c63",
+      "origin_path": "research/crt-address-streams/README.md",
+      "bytes": 5356,
+      "git_blob": "63648c961b96c6c76c305471b102e26d6b861d1b",
+      "sha256": "2f179858402d1eac28b1da46139fa3198a625375532cc2c53a01c1ffc565281b",
+      "usage": "Byte-exact local source export; complete production_axis AST is the only extracted executable. README/proof/source08 bind scope and credit; full predecessor numerical runtimes not imported."
+    },
+    {
+      "path": "research/many-axis-prime-supply/source/source08-assembly.tex",
+      "origin_repository": "CrocSwap/integer-mult-bounds",
+      "origin_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+      "origin_path": "upstream/build/sections/08-assembly.tex",
+      "bytes": 46444,
+      "git_blob": "337810a1d9a58a2ecf14123420923c039ba322a6",
+      "sha256": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a",
+      "usage": "Byte-exact local source export; complete production_axis AST is the only extracted executable. README/proof/source08 bind scope and credit; full predecessor numerical runtimes not imported."
+    }
+  ],
+  "source_export_contract": "Runtime source bytes are package-local and authenticated by both primary and independent checks. Foreign pending PR commits are provenance, not Git ancestry dependencies. The primary extracts only the complete production_axis method and uses a host semantic Count adapter; encoded_execution=false.",
+  "analytic_input": {
+    "title": "Sharper bounds for the error term in the Prime Number Theorem",
+    "authors": [
+      "Andrew Fiori",
+      "Habiba Kadiri",
+      "Joshua Swidinsky"
+    ],
+    "url": "https://arxiv.org/pdf/2206.12557v2",
+    "location": "Corollary22",
+    "usage": "Imported established analytic theorem; weaker decay0.8476. Not downloaded at replay, reproved or formalized by the finite checker."
+  },
+  "predecessor_results": [
+    {
+      "package": "research/prime-source-selector-transfer",
+      "credit": "Cinna Davis: old-source all-size selector transfer and trial-division setup; old log(t)>8d domain retained."
+    },
+    {
+      "pr": 1786,
+      "head": "c52345caa318fc6b1b6e2659c57d746317a72823",
+      "credit": "Chafik Boukhalfa/chafreaky: explicit PNT fine-interval supply strategy; no claim of inventing that method."
+    },
+    {
+      "package": "research/pr1786-fine-prime-transfer-audit",
+      "credit": "JosieElliston: independent prior fine-prime transfer audit."
+    },
+    {
+      "pr": 3935,
+      "head": "240597ed313fc2854c0462b23c89dc3bae72aaf5",
+      "credit": "Jose Manuel/jmbarrancoml: actual many-axis tensor interface and production guard."
+    },
+    {
+      "pr": 4024,
+      "head": "e99297be6749518a1b5b85cd129ecaf204d26c63",
+      "credit": "Tekalign/tekuuu: encoded CRT converter and explicit remaining source premise."
+    }
+  ]
+}
diff --git a/research/many-axis-prime-supply/TASK.json b/research/many-axis-prime-supply/TASK.json
new file mode 100644
index 0000000000..4fd1241eeb
--- /dev/null
+++ b/research/many-axis-prime-supply/TASK.json
@@ -0,0 +1,102 @@
+{
+  "schema_version": 1,
+  "task_id": "supplier-boundary-audit",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "supplier-boundary-audit",
+    "question": "Does one selected supplier obligation follow from its actual source-bound checks?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/owner-boundary-audit/README.md",
+      "research/scatter-export-parity-audit/README.md"
+    ],
+    "methods": [
+      "Trace one hypothesis through the source, checker and complete caller.",
+      "Construct one semantically invalid but superficially well-formed fixture and test rejection."
+    ],
+    "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #2977 reported duplicate-scatter counterexample and its opt-in repair. The archive is not a production fix or an independently validated selected-result failure; the selected generator emits unique rows.",
+      "scope": "Source-binding orientation only; does not replay or validate the reported bug."
+    },
+    "first_experiment": "First check whether the scatter repair has been adopted. If still open, independently reproduce #2977 symbolic-versus-exported parity on the tiny duplicate fixture, compare the selected unique-row positive control, and define either enforced uniqueness or consistent multiplicity semantics. A bounded guard-adoption patch must preserve valid inputs and test the actual exported action. Stop after this obligation; no full historical replay or frontier change follows from the mutant alone.",
+    "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.",
+    "allowed_variations": [
+      "Audit one named current condition using a new semantic counterexample."
+    ],
+    "scope_change_triggers": [
+      "Reporting the historical timing-only diagnostic as a new current acceptance bug.",
+      "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary."
+    ],
+    "overlap_terms": [
+      "owner boundary",
+      "bridge omission",
+      "hosting",
+      "2977",
+      "scatter export",
+      "duplicate index",
+      "parity semantics"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Discharge the actual PR4024/PR3935 many-axis odd coprime source-length premise with an explicit sufficient prime-supply/period domain, written uniform setup bill, and source-bound finite host reference.",
+  "scope_change_reason": "Handoff-first inspection found the explicit remaining PR4024 prime-supply premise. The old source08/Cinna selector premise log(t)>8d does not port to the newer D=Theta(p^.997), ell=Theta(p^.003) family. Use the named supplier-boundary card as changed provenance; no reroll or selected-construction bug claim. The prescribed research_baseline.py was attempted but its inventory check is blocked by sparse omission of research/community-frontier1094-audit/ASSEMBLY.json. No full selected replay is claimed.",
+  "bottleneck_link": "Supplies one explicit source premise needed by the pending encoded CRT converter and numerical tensor caller. It is a proof/input repair for that conditional lane; it does not admit the selected supplier or change kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Freeze one source-bound length-supply proof, exact finite host reference and independent controls. Stop on overlap, invalid source predicates, failed prime-count or setup budget. No numerical recovery, large native execution or unrelated optimization. Science cutoff2026-10-19T10:50:26Z; final15minutes reserved for verification/handoff.",
+  "outcome": "partial",
+  "evidence": "PROOF.md and INDEPENDENT.md establish the explicit conditional analytic statement and written uniform construction. RESULT.json records five bounded host-reference cases and8 internal controls; test_verify.py adds50 expected rejections and5 positives. These do not reprove imported analytic theorems or execute an encoded producer.",
+  "author": "ToikY",
+  "ai_assistance": "Substantial OpenAI Codex assistance in source analysis, proof, reference implementation, testing and separate AI review contexts. No independent human or formal-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Can this source-length producer be connected to the actual encoded TensorPlan and CRT caller?",
+      "why_it_matters": "The finite program here uses host integers and a semantic Count adapter; the uniform fixed-tape construction/bill is written.",
+      "first_step": "Review the exact period and prime-count hypotheses, lower the sequential prime queues to actual encoded Count streams, and compare full metadata/head/cleanup contracts with pinned TensorPlan and Converter.run_plan.",
+      "blocked_by": "No literal encoded prime producer or full numerical composition is executed here."
+    },
+    {
+      "question": "Can the numerical tensor sandwich and integer recovery be completed under the actual caller policies?",
+      "why_it_matters": "Pairwise coprime lengths alone do not price or validate numerical error, final normalization, physical reserve or a supplier.",
+      "first_step": "Coordinate with Jose Manuel Discussion3664; bind all production_common policies, actual gamma and both final S factors at the pinned source interface.",
+      "blocked_by": "Numerical/native analytic premises, precision and recovery, complete physical caller/stock and supplier admission remain separate."
+    }
+  ],
+  "selection": {
+    "method": "handoff-first; named supplier-boundary-audit card retained as changed provenance",
+    "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+    "priority_revision": 6,
+    "entry_checked_at_utc": "2026-10-19T10:06:22Z",
+    "entry_open_pr_bodies_including_drafts": 729,
+    "pagination": "seven100-record pages plus29-recordpage8 and empty9;729unique",
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/4024#issuecomment-6264858503",
+    "live_coordination": [
+      "Discussions1166,1163,active board before card",
+      "Discussion3664 clarification19036660: prospective numerical recovery distinct; repeated7x7 is not CRT production supply"
+    ],
+    "pre_selection": {
+      "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+      "checked_at_utc": "2026-10-19T10:14:00Z",
+      "source4024_head": "e99297be6749518a1b5b85cd129ecaf204d26c63",
+      "decision": "Continue one new-regime source prime premise, not prior generic prime-selection or repeated small tensor conformance."
+    },
+    "coverage_limit": "All729 open PR bodies including drafts at entry, helper report, targeted retained source-selector/fine-prime packages and bounded live threads. Broader Discussions, arbitrary code and closed work partial; absence of match is not novelty proof.",
+    "pre_submission": {
+      "checked_at_utc": "2026-10-19T10:23:09.584045+00:00",
+      "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+      "priority_revision": 6,
+      "source4024_head": "e99297be6749518a1b5b85cd129ecaf204d26c63",
+      "source3935_head": "240597ed313fc2854c0462b23c89dc3bae72aaf5",
+      "latest_number": 4028,
+      "discussions": "Live1166 reloaded, newest19037308; source4024 only own active claim; Discussion3664 numerical recovery distinct.",
+      "decision": "Main/guidance/selected/source pins unchanged; no competing prime-supply claim in inspected latest100 delta. Continue frozen baseline; broader coverage remains partial."
+    }
+  }
+}
diff --git a/research/many-axis-prime-supply/VERIFY.json b/research/many-axis-prime-supply/VERIFY.json
new file mode 100644
index 0000000000..8deea8ee29
--- /dev/null
+++ b/research/many-axis-prime-supply/VERIFY.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Five exact host-reference cases, authenticated complete source-guard AST, symbolic cutoff and8 internal rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Independent sieve/ratio/period/byte reconstruction of colocated RESULT.json, all5 source pins and separate symbolic-threshold proof; no primary code imported."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "50 semantic/integrity expected rejections and5 positive controls, source and receipt preservation; no imported analytic theorem or encoded-execution claim."
+    }
+  ]
+}
diff --git a/research/many-axis-prime-supply/independent.py b/research/many-axis-prime-supply/independent.py
new file mode 100644
index 0000000000..4764ed7c67
--- /dev/null
+++ b/research/many-axis-prime-supply/independent.py
@@ -0,0 +1,149 @@
+#!/usr/bin/env python3
+"""Independent many-axis prime-supply review; imports no primary executable.
+
+FKS Corollary22 is an external analytic premise, not established by a finite
+check. New work: ToikY with substantial OpenAI Codex assistance, Apache-2.0.
+"""
+from __future__ import annotations
+import argparse
+from fractions import Fraction
+import hashlib
+import json
+from math import gcd
+from pathlib import Path
+
+
+HERE=Path(__file__).resolve().parent
+PINS={'PR3935-README.md': (6383, '7a7f218579ae4ff192bd4b7fdf00ba008117f6d6fbcb3a70e2d021be5bf8a209', '2b665e76b4e86421bbea53b2252df8e81c91b290'), 'PR3935-tensor_plan.py': (12079, '474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3', '239caba2d2ccf2640c36d377949df3fb6a920cf0'), 'PR4024-PROOF.md': (11035, '7b141475955cc372c5936118ff16e8748b589b93de2d26b76da28feec9b45de4', '479a2b727b67b88efc8bdc64bde340a1c0d95ec3'), 'PR4024-README.md': (5356, '2f179858402d1eac28b1da46139fa3198a625375532cc2c53a01c1ffc565281b', '63648c961b96c6c76c305471b102e26d6b861d1b'), 'source08-assembly.tex': (46444, '763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a', '337810a1d9a58a2ecf14123420923c039ba322a6')}
+
+def authenticate():
+    for name,(length,sha,blob) in PINS.items():
+        path=HERE/'source'/name
+        need(not path.is_symlink(),'independent source symlink')
+        raw=path.read_bytes()
+        need(len(raw)==length and hashlib.sha256(raw).hexdigest()==sha,'independent source SHA: '+name)
+        need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==blob,'independent source Git blob: '+name)
+
+def need(test,message):
+    if not test:raise ValueError(message)
+
+
+def period_sufficient(ell,K):
+    need(type(ell) is int and type(K) is int and ell>=3 and K>=0,'symbolic period domain')
+    return K.bit_length()<=ell-3
+
+def symbolic_threshold():
+    """Tiny integers/rationals only; never form 2**(2**32)."""
+    ell0=1<<32;z0=1<<16
+    need(z0*z0==ell0,'threshold square')
+    need(Fraction(5,2)**7>480,'log480<7 from e>5/2')
+    need(2**5>24,'log24<5 from e>2')
+    need(Fraction(8476,10000)**2>Fraction(1,2),'FKS weakened exponential')
+    need(2*Fraction(92211,10000)<20,'two FKS error constants')
+    first=z0//4-7-671*16;second=ell0//4-5-669*32
+    need(first>0 and z0>4*671,'first uniform threshold and derivative')
+    need(second>0 and ell0>4*669,'second uniform threshold and derivative')
+    example_d=ell0**333
+    need(2<=example_d<=ell0**334 and ell0<8*example_d,'new domain example fails old logt>8d premise')
+    need(period_sufficient(ell0,ell0**10),'symbolic polynomial period example')
+    return dict(ell0=ell0,dimension_exponent=334,sqrt_ell0=z0,
+                new_regime_example={'ell':ell0,'d_power':333,'d_bit_length':example_d.bit_length(),'old_logt_gt_8d_fails':True,'no_target_power_or_axis_list_materialized':True},
+                first_log_margin_lower=first,second_log_margin_lower=second,
+                first_derivative_margin=z0-4*671,second_derivative_margin=ell0-4*669)
+
+
+def sieve(limit):
+    """Independent small-fixture Eratosthenes oracle, not trial division."""
+    need(type(limit) is int and 2<=limit<=1<<20,'finite sieve bound')
+    prime=bytearray(b'\1')*(limit+1);prime[:2]=b'\0\0';p=2
+    while p*p<=limit:
+        if prime[p]:
+            start=p*p;prime[start:limit+1:p]=b'\0'*(((limit-start)//p)+1)
+        p+=1
+    return prime
+
+
+def interval(t,d):
+    return Fraction(t*(3*d-1),3*d),Fraction(t*(4*d-1),4*d)
+
+
+def oracle(ell,flags,target_halo=16,w=2):
+    need(type(ell) is int and 3<=ell<=20,'small finite ell')
+    need(type(flags) in (tuple,list) and flags and all(type(f) is int and f in (0,1) for f in flags),'complete finite flag grammar')
+    need(flags[-1]==1,'final target axis is r')
+    need(type(target_halo) is int and target_halo>=0 and type(w) is int and w>=0,'period parameters')
+    D=len(flags);d=D+1;r=1<<ell;prime=sieve(r);pools={}
+    for flag in (0,1):
+        t=r if flag else r//2;a,b=interval(t,d)
+        lo=a.numerator//a.denominator+1;hi=b.numerator//b.denominator
+        pools[flag]=[n for n in range(lo,hi+1) if prime[n]]
+    used={0:0,1:0};lengths=[];targets=[]
+    for flag in flags:
+        need(used[flag]<len(pools[flag]),'insufficient primes in small fixture; not production theorem')
+        lengths.append(pools[flag][used[flag]]);used[flag]+=1;targets.append(r if flag else r//2)
+    for s,t in zip(lengths,targets):
+        gap=t-s
+        need(s>2 and s%2==1 and prime[s],'odd prime source axis')
+        need(4*d*gap>s and (2*d-1)*gap<s,'literal source ratio predicates')
+        need(s>2*(target_halo+2*w),'literal source period predicate')
+        need(0<s<t<2*s,'literal near-one source predicate')
+    need(len(set(lengths))==D,'all actual source lengths distinct')
+    need(all(gcd(a,b)==1 for i,a in enumerate(lengths) for b in lengths[:i]),'pairwise coprime')
+    need(all(gcd(s,r)==1 for s in lengths),'coprime to power-of-two target')
+    S=T=1
+    for s,t in zip(lengths,targets):S*=s;T*=t
+    need(3*S>2*T,'source/target product ratio exceeds2/3')
+    need(Fraction(1)-Fraction(D,3*d)>Fraction(2,3),'Bernoulli lower bound')
+    source_bits=bytes((s>>bit)&1 for s in lengths for bit in range(ell))
+    flag_bits=bytes(flags[:-1])
+    return dict(ell=ell,D=D,d=d,flags=list(flags),targets=targets,primes=lengths,
+                source_bits_sha256=hashlib.sha256(source_bits).hexdigest(),
+                flag_bits_sha256=hashlib.sha256(flag_bits).hexdigest(),S=S,T=T,
+                source_bit_length=D*ell,flag_bit_length=D-1,source_guard_checks=D,
+                encoded_execution=False,production_tensor_execution=False,
+                address_bits=sum(ell if f else ell-1 for f in flags),
+                band_prime_counts={str(k):len(v) for k,v in pools.items()})
+
+
+def no_duplicates(pairs):
+    out={}
+    for key,value in pairs:
+        need(key not in out,'duplicate receipt key')
+        out[key]=value
+    return out
+
+
+def check_receipt(path):
+    receipt=json.loads(path.read_text(),object_pairs_hook=no_duplicates)
+    need(type(receipt) is dict and type(receipt.get('schema_version')) is int and receipt['schema_version']==1,'receipt schema')
+    need(receipt.get('mode')=='host-reference' and receipt.get('encoded_execution') is False,'host-reference scope')
+    need(type(receipt.get('cases')) is list and receipt['cases'],'nonempty finite cases')
+    for row in receipt['cases']:
+        expected=oracle(row['ell'],row['flags'],row.get('target_halo',16),row.get('w',2))
+        for key,value in expected.items():
+            if key=='band_prime_counts':continue
+            need(key in row and type(row[key]) is type(value) and row[key]==value,'independent exact field: '+key)
+    threshold=receipt['threshold']
+    exact={'ell0':1<<32,'dimension_power':334,'z0':1<<16,'error_log_upper':10743,
+           'error_exponential_lower':16384,'volume_log_upper':21413,'volume_exponential_lower':1<<30,
+           'analytic_input_imported':True,'analytic_input_reproved':False,'giant_power_constructed':False}
+    for key,value in exact.items():
+        need(key in threshold and type(threshold[key]) is type(value) and threshold[key]==value,'independent symbolic threshold field: '+key)
+    return len(receipt['cases'])
+
+
+def audit():
+    configs=((8,[1]),(12,[0,1,1]),(14,[1,0,1,1]),(14,[0,1,0,1,0,1]))
+    return {'threshold':symbolic_threshold(),'cases':[oracle(ell,flags) for ell,flags in configs]}
+
+
+if __name__=='__main__':
+    parser=argparse.ArgumentParser();parser.add_argument('--receipt',type=Path,default=HERE/'RESULT.json');parser.add_argument('--self-test',action='store_true');args=parser.parse_args()
+    try:
+        result=audit()
+        if args.self_test:count=len(result['cases'])
+        else:
+            authenticate();count=check_receipt(args.receipt)
+        print('PASS_INDEPENDENT_MANY_AXIS_PRIME_SUPPLY cases='+str(count)+' external_FKS_premise no_production_prime_search')
+    except Exception as error:
+        raise SystemExit('FAIL_INDEPENDENT_MANY_AXIS_PRIME_SUPPLY '+str(error))
diff --git a/research/many-axis-prime-supply/source/PR3935-README.md b/research/many-axis-prime-supply/source/PR3935-README.md
new file mode 100644
index 0000000000..2b665e76b4
--- /dev/null
+++ b/research/many-axis-prime-supply/source/PR3935-README.md
@@ -0,0 +1,114 @@
+# Complete physical Gaussian tensor transform
+
+I connect the retained Gaussian expansion, complete chirp and principal-core
+compression into one source-box transform. I include fixed-cut padding, four
+canonical full-support gathers/scatters, short mixed-radix moves, periodic
+halos, original-axis coefficient pages, source-core assembly and exact
+normalization restoration. The caller preserves its borrowed data and pages
+and restores a fixed inventory of owned tapes.
+
+Under the stated production and inherited transfer contracts, I derive
+
+\[
+\|\widetilde{\mathscr F}x-RF_{\boldsymbol s}x\|_\infty
+<2^\gamma(Dp^2+4\sqrt2M+22+2D)2^{-p},\qquad
+\gamma=D(2u+\lceil\log_2(32p)\rceil+1).
+\]
+
+I use `D=d-1` actual resampled axes and retain the source's `R F_s`
+convention. With the caller-family growth laws and complete charges in
+[PROOF.md](PROOF.md), I obtain the conditional `O(V p^.99827619697 log p)`
+bound, plus fixed native compilation. I retain the exact B1/sparse/Fourier
+premises, polynomial coefficient setup and the production locality domain.
+I leave the selected frontier unchanged.
+
+For the explicit finite case I generated the actual p48/P80 catalogue for
+two source7/target8 axes. I compared the complete49-input,64-middle,
+49-output forward path against a separate natural-coordinate staged model.
+All4900 output bits matched, with12 nonzero restored outputs. I also checked
+changed-axis rejection, the half-disk entrance, positive reuse after failure
+and protected output. The opposite-direction consumer also matched its
+complete staged reference. [EVIDENCE.md](EVIDENCE.md) separates those author
+checks from the final committed-export and hosted receipts.
+
+The finite parameters use reduced halos and establish staged conformance.
+They do not meet the production locality domain or establish the production
+Fourier-error guarantee. I have not executed the production-prime supplier,
+implemented the CRT/integer recovery boundary, or obtained independent human
+or formal-kernel review.
+
+## Verification boundary
+
+I retain the actual generated coefficient return as an immutable archive.
+The producer check regenerates it and compares the entire packet byte for
+byte. The numerical checks authenticate that packet before passing it to
+the actual tensor consumer. I split the checks at this existing public page
+port after a combined attempt reached600 seconds; I keep both setup and
+consumer costs in the verification budget. See [CATALOGUE.md](CATALOGUE.md)
+for parameters, hashes, provenance and invalidation.
+
+The checker in `tensor_model.py` uses natural coordinates, reads the emitted
+factors and preserves rounding after each axis. It makes no physical
+numerical calls. The physical implementation uses encoded metadata and
+payload tapes under sealed constructors and a no-decoding harness.
+
+I also check dense-support permutations, unequal mixed-radix fields, seams,
+overlaps, core assembly, production policy metadata and arithmetic boundaries.
+[ARITHMETIC.md](ARITHMETIC.md) describes the exact fixed-digit leaves,
+streamed setup division, encoded small-order radicals and guarded
+scalar-width adaptation. I also use bounded loops for signed records up to
+4096 bits, preserving the wider-record fallback. I retain
+the general-order producer and asymptotic word bounds. The p48 metadata
+specialization proves three exact fixed inequalities and changes no numerical
+coefficient or child result.
+
+For the six registered checks, use:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/physical-gaussian-tensor
+```
+
+I bound each command by at most 400 seconds and their declared total by 1200
+seconds. I record measured stages in [EVIDENCE.md](EVIDENCE.md) and exact
+publication receipts in the linked investigation; runtime depends on the host.
+
+## Implementation map
+
+| Files | Responsibility |
+| --- | --- |
+| `tensor_router.py`, `tensor_gather.py` | Complete support, capped physical batches and canonical global order |
+| `tensor_moves.py`, `tensor_windows.py` | One short field at a time, periodic halos and original source-core assembly |
+| `tensor_plan.py`, `tensor_catalogue.py` | Encoded common policy, original-axis geometry and actual coefficient production |
+| `tensor_lines.py`, `tensor_engine.py` | Complete numerical line groups and the full source-box schedule |
+| `tensor_word.py`, `tensor_counts.py`, `tensor_division.py`, `tensor_twiddles.py`, `tensor_arithmetic.py`, `tensor_records.py` | Explicit exact arithmetic and record adaptations with fixed tape bounds |
+| `tensor_sources.py`, `tensor_fixture.py`, `tensor_model.py` | Authenticated sources, declared finite fixture and separate checker reference |
+
+## Open next questions
+
+1. **Implement the CRT entrance and integer return.** The source-transform
+   endpoint alone does not complete integer multiplication. Start with one
+   complete arithmetic field conversion and recovery interval, retaining
+   both final `S` factors from source08 and the actual total `gamma`.
+2. **Review the source and physical correspondence.** Check the old-H page
+   provenance, tensor locality order, nonlinear-rounding telescoping and
+   complete catalogue bill against the pinned sources. Author checks and
+   model-assisted source analysis do not provide independent review.
+3. **Discharge or execute the retained native premises.** The finite checker
+   uses literal q2 children. The production native constructor performs
+   prime-sized initialization. A practical production witness or a separate
+   validated refinement remains outside this package.
+
+## Credit
+
+Jose Manuel (`jmbarrancoml`) contributed this implementation and proof with
+substantial OpenAI Codex assistance, including source-analysis agents.
+I retain the Gaussian, chirp, word and routing lineage from PR3878, PR3851,
+PR3787, PR3763, PR3709 and PR3640 through complete authenticated exports.
+I credit Dugongue's PR3877 row-mass bound and the separate PR3910 local norm
+audit by `1337isnot1337`, without extending their stated review scope.
+
+I retain the RaD project/hipotures, Chafik Boukhalfa, eumemic, icekylinx,
+Hanson Sun, Artus Krohn-Grimberghe, Mason Hale, Harvey–van der Hoeven,
+the OpenAI manuscript contributors, Douglas Colkitt and the nested source
+notices. I use standard schoolbook, Karatsuba, FFT and digit-pair square-root
+algorithms; I do not claim their invention. New work follows Apache-2.0.
diff --git a/research/many-axis-prime-supply/source/PR3935-tensor_plan.py b/research/many-axis-prime-supply/source/PR3935-tensor_plan.py
new file mode 100644
index 0000000000..239caba2d2
--- /dev/null
+++ b/research/many-axis-prime-supply/source/PR3935-tensor_plan.py
@@ -0,0 +1,249 @@
+"""Encoded global tensor shape, common Gaussian policy and restoration guard."""
+from tensor_sources import active
+active()
+from cardinal_counts import Count, positive
+from compact_counts import read_fixed, write_fixed
+from encoded import compare, subtract
+from expansion_geometry import ProductionBlock
+from expansion_records import Fields
+from gaussian_rationals import read_count, write_count
+from ring_words import power_two
+from router_metadata import ceiling_log, indices, owned
+from twiddle_setup import quotient
+from words import BLANK, need
+
+
+def band(precision, u):
+    with owned(Count(precision)) as (numerator,):
+        numerator.multiply_small(16)
+        with owned(quotient(numerator, u, True)) as (target,):
+            root = Count.literal(0)
+            try:
+                while True:
+                    with owned(Count.product(root, root)) as (square,):
+                        if compare(square, target) >= 0:
+                            break
+                    root.increment()
+                root.increment()
+                root.increment()
+                return root
+            except BaseException:
+                root.close()
+                raise
+
+
+class Policy(Fields):
+    def __init__(self, p, alpha):
+        super().__init__()
+        try:
+            self.keep("block", ProductionBlock(p, alpha))
+            for name in ("P", "sigma", "radius"):
+                self.keep(name, Count(getattr(self.block, name)))
+            with owned(Count.product(p, p)) as (square,):
+                self.keep("halo", Count.product(square, p))
+                self.halo.multiply_small(4096)
+                with owned(Count.product(square, square)) as (fourth,):
+                    with owned(Count.product(fourth, fourth)) as (eighth,):
+                        self.keep("inner_bits", ceiling_log(eighth))
+            self.keep("expansion_capacity", power_two(self.inner_bits))
+            self.keep("w", band(p, self.block.u))
+        except BaseException:
+            self.close()
+            raise
+
+
+class TensorHeader(Fields):
+    names = ("version", "mode", "p", "ell", "axes", "alpha", "inner_bits", "P",
+             "sigma", "radius", "expansion_capacity", "halo", "w")
+
+    def __init__(self, page):
+        super().__init__()
+        try:
+            for name in self.names:
+                self.keep(name, read_count(page))
+            with owned(Count.literal(1)) as (one,):
+                need(compare(self.version, one) == 0 and compare(self.mode, one) <= 0,
+                     "tensor catalogue version and production mode")
+        except BaseException:
+            self.close()
+            raise
+
+    @classmethod
+    def dump(cls, plan, page):
+        for name in cls.names:
+            write_count(getattr(plan, name), page)
+
+
+class AxisRow(Fields):
+    names = ("s", "t", "width", "tiles")
+
+    def __init__(self, source):
+        super().__init__()
+        try:
+            for name in self.names:
+                self.keep(name, read_count(source))
+        except BaseException:
+            self.close()
+            raise
+
+
+class TensorPlan(Fields):
+    """Common policy plus the complete source words and target-axis flags."""
+    def __init__(self, sources, flags, axes, ell, p, alpha, inner_bits, P, sigma,
+                 radius, expansion_capacity, halo, w, factory, production=False):
+        super().__init__()
+        self.sources = self.flags = self.axis_rows = None
+        try:
+            need(type(production) is bool, "compiled tensor production policy")
+            self.keep("version", Count.literal(1))
+            self.keep("mode", Count.literal(int(production)))
+            for name, value in (("p", p), ("ell", ell), ("axes", axes), ("alpha", alpha),
+                                ("inner_bits", inner_bits), ("P", P), ("sigma", sigma),
+                                ("radius", radius), ("expansion_capacity", expansion_capacity),
+                                ("halo", halo), ("w", w)):
+                self.keep(name, Count(value))
+                if name != "sigma":
+                    positive(value)
+            with owned(Count.literal(16), Count.literal(2)) as (sixteen, two):
+                need(compare(p, sixteen) >= 0 and compare(ell, two) >= 0 and compare(ell, p) < 0,
+                     "complete tensor chirp precision and exponent")
+                need(compare(alpha, two) >= 0, "complete tensor integer alpha")
+            need(compare(P, p) >= 0, "tensor work grid covers target grid")
+            self.keep("dimensions", Count(axes))
+            self.dimensions.increment()
+            self.keep("d", Count(self.dimensions))
+            self.d.increment()
+            self.keep("L", power_two(inner_bits))
+            self.keep("u", Count.product(alpha, alpha))
+            self.keep("target_halo", Count(halo))
+            self.target_halo.multiply_small(2)
+            self.target_halo.add(self.L)
+            with owned(Count(p)) as (scaled,):
+                scaled.multiply_small(32)
+                self.keep("j", ceiling_log(scaled))
+            with owned(Count(self.u)) as (scale,):
+                scale.multiply_small(2)
+                scale.add(self.j)
+                scale.increment()
+                self.keep("gamma", Count.product(self.dimensions, scale))
+            self.keep("component_bits", Count(p))
+            self.component_bits.increment()
+            self.component_bits.increment()
+            self.keep("record_bits", Count(self.component_bits))
+            self.record_bits.multiply_small(2)
+            self.keep("source_product", Count.literal(1))
+            self.keep("address_bits", Count.literal(0))
+            self.sources, self.flags, self.axis_rows = factory(), factory(), factory()
+            sources.rewind()
+            flags.rewind()
+            for index in indices(self.dimensions):
+                flag = 1 if compare(index, axes) == 0 else flags.read()
+                need(flag in (0, 1), "complete tensor target flags")
+                if compare(index, axes) < 0:
+                    self.flags.append(flag)
+                    flags.step(1)
+                with owned(Count.literal(1)) as (one,):
+                    with owned(Count(ell) if flag else subtract(ell, one)) as (width,):
+                        need(compare(width, inner_bits) > 0, "at least two complete target tiles per axis")
+                        with owned(read_fixed(sources, ell)) as (s,):
+                            positive(s)
+                            need(s.read() == 1, "odd original tensor source axis")
+                            with owned(power_two(width), Count(s)) as (t, twice_s):
+                                twice_s.multiply_small(2)
+                                need(compare(s, t) < 0 and compare(t, twice_s) < 0, "near-one original tensor axis")
+                                with owned(subtract(width, inner_bits)) as (coarse_width,):
+                                    with owned(power_two(coarse_width)) as (tiles,):
+                                        for value in (s, t, width, tiles):
+                                            write_count(value, self.axis_rows)
+                                write_fixed(s, self.sources, ell)
+                                following = Count.product(self.source_product, s)
+                                self.source_product.close()
+                                self.fields["source_product"] = following
+                                self.address_bits.add(width)
+                                if production:
+                                    self.production_axis(s, t)
+            need(sources.read() == flags.read() == BLANK, "complete tensor source words and flags")
+            for tape in (self.sources, self.flags, self.axis_rows):
+                tape.rewind()
+            self.keep("target_product", power_two(self.address_bits))
+            self.keep("outer_bits", subtract(self.address_bits, ell))
+            with owned(Count.literal(13)) as (margin,):
+                with owned(Count(self.outer_bits)) as (minimum,):
+                    minimum.add(margin)
+                    need(compare(p, minimum) >= 0, "complete chirp p-A margin")
+            self.keep("inner_address_bits", Count.product(self.dimensions, inner_bits))
+            self.keep("coarse_address_bits", subtract(self.address_bits, self.inner_address_bits))
+            self.keep("coarse_product", power_two(self.coarse_address_bits))
+            if production:
+                self.production_common()
+        except BaseException:
+            self.close()
+            raise
+        finally:
+            sources.rewind()
+            flags.rewind()
+
+    def production_axis(self, s, t):
+        with owned(subtract(t, s)) as (gap,):
+            with owned(Count.product(self.d, gap)) as (lower,):
+                lower.multiply_small(4)
+                need(compare(lower, s) > 0, "production tensor strict lower ratio")
+            with owned(Count(self.d), Count.literal(1)) as (twice_d, one):
+                twice_d.multiply_small(2)
+                with owned(subtract(twice_d, one)) as (factor,):
+                    with owned(Count.product(factor, gap)) as (upper,):
+                        need(compare(upper, s) < 0, "production tensor strict upper ratio")
+        with owned(Count(self.target_halo), Count(self.w)) as (required, bands):
+            bands.multiply_small(2)
+            required.add(bands)
+            required.multiply_small(2)
+            need(compare(s, required) > 0, "production tensor period exceeds paired halo")
+
+    def production_common(self):
+        with owned(Policy(self.p, self.alpha)) as (expected,):
+            for name in ("P", "sigma", "radius", "inner_bits", "expansion_capacity", "halo", "w"):
+                need(compare(getattr(self, name), getattr(expected, name)) == 0,
+                     "exact production tensor Gaussian policy")
+        with owned(Count(self.p)) as (eight_p,):
+            eight_p.multiply_small(8)
+            with owned(ceiling_log(eight_p)) as (minimum,):
+                need(compare(self.u, minimum) >= 0, "production tensor logarithmic concentration")
+        with owned(Count.product(self.u, self.d), Count(self.w)) as (weighted, separated):
+            separated.multiply_small(4)
+            separated.increment()
+            separated.increment()
+            need(compare(weighted, self.p) <= 0 and compare(self.d, separated) > 0,
+                 "production tensor similarity and cell separation")
+        with owned(Count.product(self.d, self.halo)) as (needed,):
+            needed.multiply_small(64)
+            need(compare(self.L, needed) >= 0, "production tensor source-padding room")
+        # F <= 2^A*(D*p^2+32+2D). This guard bounds the restored
+        # approximation error by 1/256 before narrowing to the disk format.
+        with owned(Count.product(self.p, self.p)) as (square,):
+            with owned(Count.product(self.dimensions, square), Count(self.dimensions), Count.literal(32)) as (bound, twice_d, constant):
+                twice_d.multiply_small(2)
+                bound.add(twice_d)
+                bound.add(constant)
+                with owned(ceiling_log(bound), Count(self.gamma), Count.literal(8)) as (logarithm, required, guard):
+                    required.add(self.outer_bits)
+                    required.add(logarithm)
+                    required.add(guard)
+                    need(compare(self.p, required) >= 0, "production restored tensor error margin")
+
+    def axis(self, index):
+        self.axis_rows.rewind()
+        try:
+            need(compare(index, self.dimensions) < 0, "existing tensor axis")
+            for _ in indices(index):
+                with owned(AxisRow(self.axis_rows)):
+                    pass
+            return AxisRow(self.axis_rows)
+        finally:
+            self.axis_rows.rewind()
+
+    def close(self):
+        for tape in (self.sources, self.flags, self.axis_rows):
+            if tape is not None:
+                tape.clear()
+        self.sources = self.flags = self.axis_rows = None
+        super().close()
diff --git a/research/many-axis-prime-supply/source/PR4024-PROOF.md b/research/many-axis-prime-supply/source/PR4024-PROOF.md
new file mode 100644
index 0000000000..479a2b727b
--- /dev/null
+++ b/research/many-axis-prime-supply/source/PR4024-PROOF.md
@@ -0,0 +1,178 @@
+# Encoded coefficient-address conversion
+
+Tekalign (tekuuu), with substantial OpenAI Codex assistance. Apache-2.0.
+Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`.
+
+## Statement and exact interface
+
+Let D≥1, pairwise coprime odd integers s_i≥3, and powers of two t_i>s_i
+be given on canonical little-endian Count tapes. Put S=∏s_i, T=∏t_i,
+n=log₂T, P_i=∏_{j<i}s_j and μ_i=P_i⁻¹ mod s_i. A payload contains C≥1
+rows, each of S consecutive opaque R≥1-bit records. Borrowed ports stand at
+their left origin. Forward conversion moves record k to the natural tensor
+address with digits b_i=μ_i k mod s_i; the final axis is contiguous. Inverse
+conversion moves that record back to ordinary coefficient k. All R bits of
+every record and every row are carried together. Output is a distinct owned
+port, which the consumer must clear and erase before reuse. The implementation
+restores borrowed bytes/heads and empties its scratch and routing descendants
+on successful return. Checked malformed metadata/payload exits also clean their
+owned scratch. This is not an interrupted-child recovery protocol.
+
+`Converter.run_plan` accepts the actual, unchanged PR3935 `TensorPlan`, compiled
+at `240597ed313fc2854c0462b23c89dc3bae72aaf5`. It extracts its packed axis rows
+and checks its source product, padded product and address width against the
+computed shape. The default record width is exactly `plan.record_bits`.
+This is a typed layout bridge, not a call of the numerical tensor engine.
+A TensorPlan need not have coprime source lengths; the new adapter rejects such
+a plan. The executable typed witness has s=(3,5), t=(4,8), p=16 and is explicitly
+nonproduction. Its 15 source records and 32 padded records match the real plan.
+
+## Algebra and padded extension
+
+This algebra is inherited from source08 (lines 216–283), following
+Agarwal–Cooley; the new result is the encoded implementation and its complete
+routing bill. The map x↦∏x_i^μ_i is a cyclic-group isomorphism because each μ_i
+is a unit and the s_i are coprime. Therefore it preserves cyclic convolution.
+Writing k=Σa_iP_i, its i-th coordinate is
+
+    b_i = a_i + μ_i Σ_{j<i} a_j P_j (mod s_i).
+
+Terms with j>i vanish modulo s_i; μ_iP_i=1. Forward updates run in descending
+i, so lower coordinates are still original. Inverse updates run in ascending
+i and subtract the same expression from already recovered lower coordinates.
+
+On the full padded box, use offset zero whenever a lower control is invalid.
+For a valid lower prefix, rotate only [0,s_i), fixing [s_i,t_i). Each step is
+a bijection preserving the valid box and its complement, including arbitrary
+nonzero payloads on invalid prefixes and target tails. Consequently initially
+zero padding stays zero. Cropping checks every discarded bit is zero; it does
+not silently throw away nonzero information.
+
+The offset producer enumerates physical lower prefixes in natural axis order
+(the last lower axis varies fastest), using a single packed address tape.
+Its integer arithmetic forms Σa_jP_j and multiplies by μ_i before taking its
+residue. No metadata cardinality is decoded into a host integer. Modular inverse
+uses the binary extended-gcd invariants u≡ax, v≡ay mod m, 0≤x,y<m for odd m.
+Even operands halve, adding m before halving an odd coefficient; odd differences
+subtract modulo m. Each subtraction followed by halving reduces the positive
+operands. A unit reaches 1. A nonunit reaches equal operands greater than 1
+and rejects. Computing inverses for every prefix checks precisely the needed
+coprimality, rather than assuming primality of the supplied s_i.
+
+## Physical composition
+
+Ordinary k order is colexicographic a order. Padding first enumerates the full
+colex box. A single full-support router then reverses the order of the axis
+fields, retaining little-endian bit order inside each field. It moves old bit
+position P+j to n-P-width+j. The descriptor is sorted by old position and uses
+the unchanged fixed-width `router_metadata.write_pair` codec. The inverse
+map is separately compiled and sorted: unequal field widths do not in general
+give an involution on bit positions.
+
+In natural padded order, each controlled shift splits its target into the
+first s_i-offset positions, the remaining offset positions, and the invalid
+tail. A first sequential pass writes three bucket tapes. A second emits the
+second, first and invalid buckets in that order, carrying each complete
+spectator suffix as a block. Inverse splits at offset instead. It prepares
+actual encoded offsets; there is no free shift or address oracle.
+
+The actual tensor interface is compact, so a complete conversion is:
+
+* forward: colex compact → colex padded → global field permutation →
+  descending triangular shifts → natural compact;
+* inverse: natural compact → natural padded → ascending inverse shifts →
+  inverse global permutation → colex compact.
+
+Thus each conversion pays one global router call, D shifts and **two** padding
+passes. Integer multiplication would use three conversions (two forward inputs
+and one inverse output), hence **three**, not two, global router calls. The final
+S² normalization, rounding/carry recovery and integer wrapper are not supplied.
+
+## Time invoice, including setup and restoration
+
+Write V=CTR and r_min=min t_i. With n=Θ(p), R=Θ(p), the complete conditional
+invoice per conversion is
+
+    O(V p^β log^(1+τ)p + D V + CT(n+R)
+      + C D T poly(n)/r_min + poly(p)) + fixed native compilation F_q + source setup F_src,
+
+where τ=332353/332929 and β=41544341/41616125. The polynomial degrees are fixed,
+independent of D,C and the input values. F_q is charged once to a fixed compiled
+native instance; it is not silently reconstructed at each conversion. F_src
+pays authentication, copying and extraction of the fixed pinned local source
+artifacts once per cold cohort, with their fixed storage retained separately.
+Network transport is a replay prerequisite, not a numerical tape operation.
+
+The first term is the full-support PR3935 router theorem at the exact source
+pin above (PROOF.md, “four canonical gathers”). It includes factorization into
+two involutions, sorted batches, all unchanged spectators, interval/reservoir
+selection, metadata, child recompilation and restoration. Its polynomial setup
+is retained, then absorbed only under its stated n=Θ(p) caller hypothesis.
+We inherit its B1/sparse endpoint, all-size/compiler, universal cost and bounded
+fallback premises. We neither certify those premises here nor execute its
+production-sized selected native program in the q=2 literal fixtures.
+
+Each shear pays O(V) movement, including bucket copying/erasure, full suffixes,
+row-offset copying and counter restoration. The copied offset has O(log t_i)
+length, at most a constant times the t_i target records it controls. There are
+B_i=∏_{j<i}t_j≤T/t_i prefixes. Packed metadata lookup and binary arithmetic cost
+a fixed polynomial in n per prefix, so total offset preparation is bounded by
+D T poly(n)/r_min; the displayed C factor safely includes row replication and
+row-extent setup. Shape compilation, modular inverses and descriptor compilation
+cost poly(n). Canonical binary countdowns have amortized ripple cost; fixed-role
+Count products and their explicit rewinds are charged. Logarithmic C/R setup
+is dominated by the full packet bill, since C,R≥1 and T=2^n.
+
+Padding uses a packed (s_i,width_i) page, never a fresh scan of the full six-field
+plan for each digit. Extracting all address fields, comparing bounds and returning
+the heads costs O(n) per address. Handling the opaque record costs O(R).
+Both scans therefore cost O(CT(n+R)); when n,R=Θ(p), this is O(V). Final compact
+output copies and all successful erasures add O(V+poly(n)).
+
+For the *conditional* newer caller laws D=Θ(p^(997/1000)), ell=Θ(p^(3/1000)),
+t_i∈{2^ell,2^(ell-1)}, n=Θ(p), R=Θ(p), r_min exceeds every fixed polynomial.
+Thus offset preparation is o(V), and .997 < β < Φ=.99827619697. The router's
+extra factor log^τ p is absorbed by the strictly positive gap Φ-β. The complete
+conversion is consequently O(V p^Φ log p). Three conversions obey the same
+order, but their constant and F_q/setup costs remain paid. These inequalities
+are conditional cost comparisons, not a new κ or a complete multiplication
+algorithm. The pairwise coprime lengths are explicit inputs: no claim is made
+that an old prime-generation cutoff proves their existence under newer laws.
+Source08's adjacent-swap *upper bound* O(V D²(1+ell^τ)) does not certify this
+allowance under these laws; it is not a lower bound or an impossibility theorem.
+
+## Fixed roles and backing
+
+The wrapper has 192 scratch roles and one protected output, allocated before
+entry; all numerical execution runs under sealed constructors. There are no
+D-sized host lists of runtime tapes. Axis metadata occupies O(Dn)≤O(n²) cells
+on two packed tapes. Buckets, current data, offset copies and output occupy
+O(V+n²) live cells. The finite maximum wrapper lease count is reported as an
+observation, not an all-parameter role proof. A lexically fixed inventory bounds
+simultaneous roles: shape/page ≤6, one six-field axis plus enclosing counters
+≤16, prefix preparation plus its nested axis/arithmetic ≤64, or shear/copy
+≤32, descriptor/padding ≤32, and conversion staging ≤16; even their conservative
+sum is <192. Nested arithmetic uses fixed tuples of Counts, independent of D.
+The child has its own fixed inventories, retained from its authenticated source.
+
+`Tape.clear()` erases cells but does not shrink its Python bytearray. For a
+sequence of calls, each fixed wrapper role therefore retains its largest past
+extent. Wrapper *backing* is O(max_history(V+n²)), not merely current live space.
+Add the inherited child high-water backing (including polynomial planning) and
+fixed native storage and fixed source/extraction storage separately. This is not a quantified production memory
+coefficient or a claim that all retained native backing is O(current V).
+
+## Verification scope and unresolved work
+
+The replay checks every coefficient column simultaneously as independent opaque
+basis bits, forward and inverse, on four complete shapes (including unequal
+widths and three axes), and compares directly to kμ_i mod s_i. It checks every
+padded prefix, separate descriptor directions against the unchanged codec,
+nonzero invalid shear geometry, the actual typed TensorPlan, 2,176 unit/nonunit
+inverse cases, source and receipt integrity, protected outputs, malformed inputs,
+zero-padding checks, aliases, dirty prior work and wrong-algebra/order controls.
+It checks exact exponent arithmetic independently. These are finite implementation
+checks alongside the scoped argument above, not formal verification of the
+all-size multiplication theorem. Native compilation/execution at production q,
+the inherited router theorem assumptions, prime supply, actual numerical tensor
+composition and final integer recovery remain distinct obligations.
diff --git a/research/many-axis-prime-supply/source/PR4024-README.md b/research/many-axis-prime-supply/source/PR4024-README.md
new file mode 100644
index 0000000000..63648c961b
--- /dev/null
+++ b/research/many-axis-prime-supply/source/PR4024-README.md
@@ -0,0 +1,96 @@
+# Encoded CRT address conversion for the physical tensor
+
+This package implements the CRT coefficient-order entrance and exit left open
+by Jose Manuel's [PR3935](https://github.com/CrocSwap/integer-mult-bounds/pull/3935),
+pinned at `240597ed313fc2854c0462b23c89dc3bae72aaf5`. It preserves source08's
+triangular CRT algebra and substitutes one **paid full-support router** for a
+quadratic sequence of adjacent-axis exchanges. Both directions include the
+two padding/cropping scans required by the actual compact tensor interface,
+all encoded offsets, complete spectator records, copies and cleanup.
+
+Under the pinned router premises and the explicit newer many-axis caller laws,
+the complete conditional conversion bill fits `O(V p^Φ log p)`,
+Φ=.99827619697. [PROOF.md](PROOF.md) states the full invoice and backing bound.
+Integer multiplication requires **three** conversions; its numerical tensor,
+prime supply, final normalization and integer recovery remain separate.
+There is **no new κ claim**, production-sized native execution or formal proof
+of the complete multiplication theorem.
+
+The implementation uses canonical Count tapes and a fixed 192-role wrapper.
+`Converter.run_plan` accepts the actual PR3935 `TensorPlan` and verifies its
+products and address width. Coprimality is checked rather than inferred from
+the type; the predecessor's repeated-(7,7) fixture is not a CRT witness.
+
+## Reproduce
+
+Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`; Python 3.12, standard library.
+From the repository root:
+
+```sh
+python3.12 scripts/research_package.py --package research/crt-address-streams
+```
+
+The registered command explicitly downloads about 38.5 MB of **pinned external
+predecessor sources** into temporary storage. Every size, SHA256 and Git blob
+is checked; no GitHub credentials are needed. Network availability is required
+for that command. The exact files and source commit are in
+[NETWORK-SOURCES.json](NETWORK-SOURCES.json). This avoids duplicating large
+frozen predecessor archives in the PR. Only declared source files enter a private import tree, with a fresh bytecode
+namespace; unpinned siblings and cached bytecode in an offline tree are ignored.
+The predecessor loader independently
+checks the complete embedded exports, receipts and source-specific notices.
+
+For an already downloaded, authenticated tree with paths matching that manifest:
+
+```sh
+python3.12 -B research/crt-address-streams/verify.py --source-root /path/to/dependencies
+```
+
+Expected: `PASS_CRT_ADDRESS_STREAMS ...`. Direct replay also works from a Git-free
+source export. Neither mode writes into the package or modifies predecessors.
+Dependency source authentication/setup is outside the numerical macro and is
+explicitly disclosed; it is not free runtime arithmetic.
+
+## Evidence and limits
+
+[EXPECTED.json](EXPECTED.json) records deterministic replay coverage: every basis
+column for four complete shapes, both descriptor/conversion directions, all
+padded lower prefixes, arbitrary nonzero invalid shear cells, 2,176 independent
+unit/nonunit inverse cases, the actual compact typed-plan fixture, failure
+controls and exact cost-gap arithmetic. The wrapper peak in these fixtures is
+39 scratch leases. Finite observations do not replace the all-parameter role,
+cost or router assumptions. Python backing retains past high-water lengths;
+the proof distinguishes that from current live space.
+
+Wrong offsets, wrong shift direction and wrong field permutation are checked
+against the direct `k μ_i mod s_i` oracle. Malformed extents/metadata, nonzero
+padding, dirty prior work, internal-port aliases and unconsumed outputs reject.
+The tests use the unchanged full router with its q=2 **literal** native fixture;
+they do not execute the enormous production native instance or establish its
+universal cost premise.
+
+## Open next questions
+
+The two structured questions in [TASK.json](TASK.json) are actual numerical
+tensor composition and final integer normalization/rounding. Each names its
+first experiment and inherited blockers. Neither is discharged by this layout
+contribution. Pairwise coprime near-one lengths under the newer asymptotic laws
+also remain an explicit source premise, rather than an assertion about an old
+prime-generation cutoff.
+
+## Credit and license
+
+Prepared by Tekalign (tekuuu), with substantial OpenAI Codex assistance in design,
+code, proof and verification. New work is Apache-2.0. CRT algebra follows
+Agarwal and Cooley and the retained source08 construction; the full router and
+physical tensor interface are Jose Manuel (`jmbarrancoml`)'s PR3935, building on
+PR3619 and the predecessors pinned within its complete exports, including the original
+OpenAI manuscript, RaD/hipotures reports and Douglas Colkitt's retained work. Those sources,
+licenses and notices are unchanged. This contribution adds the actual encoded
+layout composition and full conditional cost/backing argument; it does not
+claim the predecessor's algebra or routing theorem as new work.
+
+Jose Manuel's concurrent [interface clarification](https://github.com/CrocSwap/integer-mult-bounds/discussions/3664#discussioncomment-19036660)
+confirms the direction convention, actual scalar-axis notation and the two final
+S factors for the eventual numerical sandwich. Its prospective recovery work is
+separate; this package pins the published tensor head above.
diff --git a/research/many-axis-prime-supply/source/source08-assembly.tex b/research/many-axis-prime-supply/source/source08-assembly.tex
new file mode 100644
index 0000000000..337810a1d9
--- /dev/null
+++ b/research/many-axis-prime-supply/source/source08-assembly.tex
@@ -0,0 +1,1007 @@
+\section{Exact integer multiplication and its cost}
+\label{sec:assembly}
+
+We now use the preceding algorithms to multiply two $n$-bit integers.
+An equal-width address swap on logical bit volume $V$ costs
+$O(Vu^\tau)$ for width $u$.  A completed parallel normalized butterfly
+layer costs $O(Vd^{\lambda'})$ and has coefficient error less than
+$\sqrt2\,2^{-p}$.  The ordered Gaussian resampling maps are
+contractions; their disk-grid approximations have error less than
+$p^2 2^{-p}$ and cost $O(tp^{3/2+\delta}\alpha)$ on a line of length
+$t$.  Address permutations and intermediate dyadic arithmetic are
+exact.  We choose compatible parameters for these procedures, recover
+the integer coefficients from their approximations, and account for the
+remaining tape operations.
+
+\subsection{A fixed rational choice}
+
+The two motif exponents were fixed in \eqref{eq:explicit-motif-exponents}.
+Take the following fixed rational numbers:
+\begin{equation}\label{eq:fixed-parameters}
+\begin{gathered}
+ \tau=\sigma=1-2^{-50},\qquad \beta=\frac12,\qquad \delta=\frac1{16},\\
+ \lambda=1-2^{-52},\qquad c=2^{-56},\qquad
+ \lambda'=1-2^{-54},\\
+ C_1=20,\qquad \epsilon=2^{-75},\qquad \kappa=2^{-182}.
+\end{gathered}
+\end{equation}
+These constants are deliberately conservative; no optimization is claimed.
+
+The layer conditions hold with room to spare:
+\[
+ \max\{\tau,\sigma\}<\lambda<1,\qquad
+ \tau(1+c/\beta)<1-31\cdot2^{-55}<\lambda,
+\]
+and
+\[
+ \sigma+\beta(1-\sigma)=1-2^{-51}<\lambda<\lambda'<1.
+\]
+The strict final inequality absorbs the logarithmic number of groups in
+a base-$m$ partition.  The dimension exponent also satisfies
+\[
+\begin{gathered}
+ \epsilon<\frac1{12},\quad \epsilon C_1<1,\quad
+ \epsilon(2-\tau)<1-\tau,\quad
+ \frac34+\delta+\frac32\epsilon<1,\\
+ \epsilon(1+c)<1,\qquad \epsilon+\delta<1.
+\end{gathered}
+\]
+
+\subsection{Input and transform sizes}
+
+The input is the promised string $x\#y$, with both operands written
+most significant bit first.  In one left-to-right pass, copy $x$ and
+$y$ to two fixed work tapes and count the bits of $x$ with a binary
+counter.  The promise gives both operands this counted length $n$.
+The counter bound in Section~\ref{sec:streams} and the two sequential
+copies give cost $O(n)$, including all leading zeroes.  The work-copy
+heads finish just after the least significant bits, ready to move
+leftward when the digits are formed.
+
+\subsubsection{The padded box and working precision}
+
+After obtaining $n$, compute the size parameters below with the
+separate setup costs stated in this subsection.  For sufficiently
+large $n$, put
+\[
+ b=\lceil\log_2n\rceil,\quad p=6b,\quad d=\lfloor b^\epsilon\rfloor,
+ \quad K=\lfloor d^c\rfloor.
+\]
+Take the power of two $T$ in $[4n/b,8n/b)$, and let
+$r=2^{\lceil(\log_2T)/d\rceil}$ and $\ell=\log_2r$.  Choose
+$d\ell-\log_2T$ of the $d$ axis lengths to be $r/2$ and the others to
+be $r$.  This gives
+\[
+ t_i\in\{r/2,r\},\qquad \prod_i t_i=T,\qquad t_d=r.
+\]
+Indeed $d\ell-\log_2T$ is an integer in $[0,d)$, so at least one axis
+has length $r$; choose it as the last axis.
+These definitions give
+\begin{equation}\label{eq:sizes}
+ Tp=\Theta(n),\quad d=\Theta(p^\epsilon),\quad
+ K=\Theta(p^{\epsilon c}),\quad
+ \ell=\Theta(p^{1-\epsilon}),\quad r=2^{\Theta(p^{1-\epsilon})}.
+\end{equation}
+The comparison constants can be fixed for every input length at once.
+For sufficiently large $b$, the bounds on $n,T$ give
+$b/2\leq\log_2T\leq b$. Since $p=6b$, $d=\lfloor b^\epsilon\rfloor$
+and $d\leq b$, they imply
+\[
+ \frac1{12}p^\epsilon\leq d\leq p^\epsilon,
+ \qquad \frac{p}{12d}\leq\ell\leq\frac{p}{3d}.
+\]
+Thus we fix $a_d=a_r=1/12$, $b_d=1$, $b_r=1/3$, and $C_\ell=1$
+in the layer and transform interfaces. Their pointwise bounds cover every
+computed pair $(d,r)$, including all choices arising at the same $p$.
+These bounds also give that $r$ exceeds every fixed power of $p$,
+$K/\log p\to\infty$, and
+$\ell/K\to\infty$.  There are eventually enough axes for the
+$O(\log d)$ reserved row axes and enough bits for all work blocks.
+
+Set
+\[
+ \alpha=\left\lceil(12d^2b)^{1/4}\right\rceil,
+ \qquad \gamma=2d\alpha^2,\qquad \eta=\frac1{4d}.
+\]
+The ceiling does not affect the needed bounds: for $A\ge1$,
+$\lceil A\rceil\le2A$, and hence
+\begin{equation}\label{eq:gamma}
+ \alpha\le2(12d^2b)^{1/4},\qquad
+ \gamma<28d^2\sqrt b\le28b^{1/2+2\epsilon}\le28b^{2/3}.
+\end{equation}
+It follows that $2\le\alpha<\sqrt p$ eventually and $\gamma=o(b)$.
+For example $b\ge2^{24}$ implies $\gamma\le b/4$.
+
+\subsubsection{Prime source lengths}
+
+The distinct prime lengths $s_i$ must be close to the powers of two
+$t_i$: their product must occupy a fixed fraction of the padded box,
+while each ratio $t_i/s_i$ must leave enough separation for resampling.
+We verify both requirements for the parameters just chosen.
+
+The prime-interval result
+\cite[Lemma~5.1]{HarveyHoeven2021}, based on explicit estimates of
+Rosser and Schoenfeld~\cite{RosserSchoenfeld1962}, gives the following
+bound: for
+$0<\eta<1/4$ and $x>e^{2/\eta}$, the interval
+\[
+ (1-2\eta)x<q\leq(1-\eta)x
+\]
+contains at least $\eta x/(2\log x)$ primes. Here $\log$ is the natural
+logarithm. The size bounds in \eqref{eq:sizes} give
+$d=\Theta(p^\epsilon)$ and $\log r=\Theta(p/d)$.
+For large $n$ we have $d\geq2$, so
+$0<\eta<1/4$, and
+\[
+ \frac{\log(r/2)}d=\Theta(p^{1-2\epsilon})\longrightarrow\infty.
+\]
+Thus both $x=r/2$ and $x=r$ satisfy $\log x>8d=2/\eta$.
+For either choice, the stated lower bound for the number of primes is
+$x/(8d\log x)$ and exceeds $d$:
+indeed, $\log x=\Theta(p^{1-\epsilon})$, whereas
+$\log(8d^2\log x)=O(\log p)=o(\log x)$, so $x>8d^2\log x$ eventually.
+The two intervals are disjoint because
+$(1-\eta)r/2<(1-2\eta)r$ for $\eta<1/4$, and both intervals lie above
+$2$. We may therefore choose distinct odd primes satisfying
+\[
+ (1-2\eta)t_i<s_i\leq(1-\eta)t_i.
+\]
+Every $\gcd(s_i,t_i)$ equals one because $t_i$ is a power of two.
+Put $S=\prod_i s_i$. Multiplying the lower bounds on $s_i$ and
+applying strict Bernoulli inequality gives
+\[
+ \frac ST>
+ \left(1-\frac1{2d}\right)^d>\frac12
+ \qquad(d\geq2).
+\]
+Together with $s_i<t_i$, this gives $T/2<S<T$.
+Writing $\theta_i=t_i/s_i-1$, the upper bound on $s_i$ gives
+$\theta_i\geq\eta/(1-\eta)>\eta$. Therefore
+\[
+ \alpha^4\theta_i>\frac{12d^2b}{4d}=3db\geq6b=p.
+\]
+The choice of $\alpha$ gives
+$\alpha=\Theta(p^{1/4+\epsilon/2})$, and \eqref{eq:gamma} already
+ensures $2\leq\alpha<\sqrt p$ for large $n$. We also have
+$t_i\leq r\leq T<8n/b<2^{6b}=2^p$.
+Thus every hypothesis of Lemma~\ref{lem:no-sort-resampling} holds for
+all sufficiently large input lengths. The superpolynomial growth of $r$
+established above also supplies the setup condition in
+Lemma~\ref{lem:tensor-resampling}.
+
+The machine finds these primes by scanning the two intervals
+deterministically and testing each candidate by trial division through
+its square root. Testing every candidate would visit $O(r)$ candidates
+and at most $O(\sqrt r)$ trial divisors per candidate. Elementary
+division on $O(\log r)$-bit integers and management of a list of at most
+$d$ selected primes give the conservative bound
+$O(dr^{3/2}\operatorname{poly}(p))$. Its logarithm is
+\[
+ O(\log p+\log r)=O(\log p+p/d)=o(p).
+\]
+Since $p=6\lceil\log_2 n\rceil=\Theta(\log n)$, the search takes
+$n^{o(1)}=o(n)$ time.
+All remaining scalar setup, including comparisons for fixed rational
+powers, modular inverses,
+prime products and shape descriptors, has cost polynomial in $p$.
+For example, $d=\lfloor b^{2^{-75}}\rfloor$ is found by binary search
+using exact comparisons $d^{2^{75}}\le b$; the exponent is fixed.
+The same procedure computes $K$ and all other fixed rational powers.
+All primes and length parameters are therefore generated by the machine;
+they are not advice.
+
+\subsubsection{The radix-digit polynomials}
+
+Write the two inputs as polynomials in $2^b$, each with
+$q=\lceil n/b\rceil$ nonnegative digits.  Their product has degree at most
+\[
+ 2q-2<2n/b\le T/2<S.
+\]
+Thus convolution modulo $x^S-1$ has no nonzero wraparound.  Every product
+coefficient obeys
+\begin{equation}\label{eq:capacity}
+ 0\le c_j\le q(2^b-1)^2<2^{3b},
+\end{equation}
+since $q\le n\le2^b$.
+
+\subsection{An explicit cyclic-convolution layout}
+
+To use the source tensor, we first place the ordinary coefficient stream
+in its tensor order. Agarwal and Cooley used the Chinese remainder
+theorem to convert one cyclic convolution into multidimensional cyclic
+convolution~\cite{AgarwalCooley1977}. The following map uses that
+algebraic split, with coordinate powers that make the change of order a
+sequence of controlled cyclic shifts.
+
+Let $s_1,\ldots,s_d$ be the pairwise coprime
+source lengths, let $S=\prod_i s_i$, and put
+\[
+ P_i=\prod_{j<i}s_j,\qquad \mu_i=P_i^{-1}\pmod{s_i}.
+\]
+Here $P_i$ denotes an integer prefix product, not a Fourier-coordinate
+permutation.  The assignment
+\[
+ \Phi:\mathbb C[x]/(x^S-1)\longrightarrow
+ \mathbb C[x_1,\ldots,x_d]/(x_1^{s_1}-1,\ldots,x_d^{s_d}-1),
+ \qquad x\longmapsto\prod_i x_i^{\mu_i}
+\]
+respects $x^S=1$, so it defines an algebra map.  The target monomial
+group has size $S$, and the image of $x$ has order $S$, because each
+$\mu_i$ is a unit and the $s_i$ are pairwise coprime.  Its powers
+therefore run through all target basis monomials exactly once.  Hence
+$\Phi$ is an isomorphism and preserves cyclic convolution.
+
+Every ordinary coefficient index has a unique mixed-radix expression
+\[
+ k=\sum_{j=1}^d a_jP_j,\qquad 0\le a_j<s_j.
+\]
+The coordinate of $\Phi(x^k)$ in axis $i$ is
+\begin{equation}\label{eq:triangular-crt}
+ b_i=a_i+\mu_i\sum_{j<i}a_jP_j\pmod{s_i}.
+\end{equation}
+Indeed terms with $j>i$ are divisible by $s_i$, and $\mu_iP_i=1$ modulo
+$s_i$.  Numerical order of $k$ is lexicographic order of
+$(a_d,\ldots,a_1)$.  Insert the padding in one nested scan of the full
+box $\prod_i[0,t_i)$ in this lexicographic order, with $a_d$ the
+outermost counter and $a_1$ the innermost.  At an address satisfying
+$a_i<s_i$ for every $i$, copy the next original coefficient record;
+at every other address, write a zero record.  The valid addresses
+occur in the original coefficient order, so each record is copied to
+its intended mixed-radix address.  To delete the padding after the
+inverse axis reorder, use the same enumeration, copying the record at
+each valid address and skipping the record at each invalid address.
+
+Store the nested binary counters consecutively on a fixed work tape.
+Their total width is $\sum_i\log_2t_i=\log_2T=O(p)$, and the stored
+bounds $s_i$ also have total width $O(p)$.  At each of the $T$
+addresses, updating the counters, testing validity, and handling the
+$O(p)$-bit record therefore cost $O(p)$ steps, including counter-head
+returns.  Each insertion or deletion scan costs $O(Tp)$.
+
+Now reorder the complete padded axes to $(a_1,\ldots,a_d)$.  In this
+physical order, the coordinates with
+indices below $i$ precede coordinate $i$.  Update the targets in the
+order $i=d,d-1,\ldots,1$ using \eqref{eq:triangular-crt}.  When target
+$i$ is updated, none of its lower-index controls has yet changed, so
+the offset is computed from the original digits $a_j$ required by the
+formula.
+
+To specify the action on padded addresses, let
+\[
+ \mathcal P=\prod_i[0,t_i),\qquad \mathcal V=\prod_i[0,s_i)
+\]
+be sets of integer addresses.  On a fixed control prefix, rotate the
+valid target interval $[0,s_i)$ by the offset in
+\eqref{eq:triangular-crt} and fix $[s_i,t_i)$.  If any lower-index
+control is invalid, use the identity.  This defines a bijection of
+$\mathcal P$: for fixed controls and spectators it is a cyclic
+permutation of the valid target interval and the identity elsewhere.
+Each step preserves $\mathcal V$ and its complement.  Consequently
+zero padding remains zero after every step.  An inverse is explicit:
+process $i=1,\ldots,d$, subtracting the same expression formed from the
+already recovered lower coordinates; then undo the axis reorder and
+perform the deletion scan just described.
+
+Each triangular update is a prefix-controlled cyclic shift.  The
+controls precede its target in the current physical order.  For each
+prefix, prepare the offset, split the valid target interval into its
+two consecutive pieces, and merge those pieces in the opposite order.
+Every target position carries its full spectator suffix as a block;
+the invalid interval is copied unchanged.  There are at most $T/t_i$
+control prefixes for target $i$.  For any fixed setup degree $C$, all
+offsets therefore cost $O(dTp^C/r)=o(Tp)$ to prepare, since
+$t_i\ge r/2$ and $r$ exceeds every fixed power of $p$.
+
+The axis widths are $\ell$ or $\ell-1$.  To exchange two adjacent axes
+of unequal width, move the longer axis's leading bit outside their
+equal-width pair, swap that pair by the proved chunk-swap procedure,
+and put the leading bit at its new position.  This adds a fixed number
+of linear passes to the equal-width swap cost.  Reversing all axes
+uses $O(d^2)$ such moves.  Therefore the map $\Phi$, its inverse, and
+their padding operations cost
+\[
+ O\bigl(Tp\,d^2(1+\ell^\tau)\bigr).
+\]
+This construction describes payload movement from address $a$ to its
+new address.  It is distinct from the operator convention
+$(R_cz)_j=z_{cj}$ used for Fourier dilations, which moves a payload
+from address $j$ to $c^{-1}j$.
+
+\subsection{Complex convolution by a coefficient twist}
+
+The power-of-two complex convolution used in the chirp identity is
+obtained from the synthetic convolution by a coefficient twist.
+Put $\mathcal R=\mathcal R_r=\mathbb C[y]/(y^r+1)$ and
+$\zeta=e^{\pi i/r}$.  The map
+\[
+ \Theta:\mathbb C[x_d]/(x_d^r-1)\longrightarrow\mathcal R,
+ \qquad x_d\longmapsto\zeta y
+\]
+is well defined, since $(\zeta y)^r=(-1)(-1)=1$.  On the bases
+$(x_d^k)_{0\le k<r}$ and $(y^k)_{0\le k<r}$ it is diagonal,
+multiplying coefficient $k$ by the nonzero number $\zeta^k$.  It is therefore an
+isomorphism, with inverse multiplying that coefficient by
+$\zeta^{-k}$.  Both exact maps preserve the coefficient sup norm.
+For an explicit check on the wrap, write $k+l=j+hr$, where
+$h\in\{0,1\}$.  A product term after twisting and negacyclic reduction
+has factor
+\[
+ \zeta^{k+l}(-1)^h=\zeta^j(\zeta^r)^h(-1)^h=\zeta^j.
+\]
+Untwisting therefore recovers the cyclic coefficient with the correct
+sign.  We next specify how this linewise map meets the ring-convolution
+interface.  Put $M=\prod_{i<d}t_i=T/r$.  For a complex array $f$ on
+$\prod_{i=1}^d\mathbb Z/t_i\mathbb Z$, with $t_d=r$, define
+\[
+ (\iota f)_{\boldsymbol j}
+   =\sum_{k=0}^{r-1}f_{\boldsymbol j,k}y^k,
+ \qquad
+ \boldsymbol j\in\prod_{i<d}\mathbb Z/t_i\mathbb Z.
+\]
+This identifies the scalar tensor with an array of $M$ records in
+$\mathcal R$. As maps of values, $\iota$ and $\iota^{-1}$ preserve norms
+and grids. Write
+$(D_\pm f)_{\boldsymbol j,k}=\zeta^{\pm k}f_{\boldsymbol j,k}$.
+The linewise extension of $\Theta$ is $\iota D_+$, with inverse
+$D_-\iota^{-1}$.  Consequently, with $\mathcal M_r$ from
+Section~\ref{sec:exact-ring-products}, normalized complex cyclic
+convolution is
+\[
+ \mathcal M_{\mathbb C}(f,g)
+   :=D_-\iota^{-1}
+       \mathcal M_r(\iota D_+f,\iota D_+g)
+    =\frac{f*g}{T}.
+\]
+Here $\mathcal M_r$ convolves the first $d-1$ axes over $\mathcal R$,
+whereas $*$ on the right convolves all $d$ scalar axes.  The division
+by $T$ is already part of $\mathcal M_r$.  The maps $D_\pm$ and
+$\iota^{\pm1}$ are isometries, so $\mathcal M_{\mathbb C}$ is also a
+bilinear contraction.
+
+\subsubsection{Computed complex convolution}
+
+For the tape representation, use the scalar format of
+Section~\ref{sec:resampling}, with $w_{\rm c}=p+2$ bits per component.
+For $p\geq2$, this satisfies $p+2\leq w_{\rm c}\leq2p$, so fix $C_w=2$
+and instantiate the synthetic component width as $w=w_{\rm c}$.
+Both representations then concatenate exactly the same real and
+imaginary words in the same coefficient order: the last coordinate is
+already the contiguous polynomial suffix. Hence $\iota$ and
+$\iota^{-1}$ change only the shape descriptor and require no payload
+movement when these component formats agree.
+
+For the synthetic transform calls, the machine writes the header
+\[
+ \mathcal T=\Gamma(p)\Gamma(d)\Gamma(r)\Gamma(K)\Gamma(w_{\rm c})
+       \prod_{i=1}^{d-1}\Gamma(t_i).
+\]
+For each normalized polynomial product it supplies
+$\Gamma(p)\Gamma(r)\Gamma(w_{\rm c})$. These are precisely the headers
+of Lemmas~\ref{lem:synthetic-transform-cost} and
+\ref{lem:signed-ring-product}, formed from the computed parameters.
+Their lengths are $O(p)$; forming the transform header costs
+$\operatorname{poly}(p)=o(Tp)$, and copying a product header for each of
+the $M=T/r$ polynomial records costs $O(Mp)=O(Tp)$.
+
+For $0\le k<r$, obtain disk-grid approximations
+$\widetilde\theta_k^+$ and $\widetilde\theta_k^-$ to $\zeta^k$ and
+$\zeta^{-k}$, each with error less than $2\,2^{-p}$.  The exponential
+routine uses denominator $2r$ and costs $O(p^{1+\delta})$ per factor.
+Write $\widetilde{\mathcal M}_r$ for the procedure in
+Proposition~\ref{prop:synthetic-convolution}.  For disk-grid inputs
+$f,g$, one of norm at most $.7$, the computed complex convolution is the
+following sequence,
+with the twist arrays repeated on every last-coordinate line:
+\[
+ \begin{aligned}
+ f'&=Q_p(\widetilde\theta^+\mathbin{\cdot}f),\\
+ g'&=Q_p(\widetilde\theta^+\mathbin{\cdot}g),\\
+ h'&=\widetilde{\mathcal M}_r(\iota f',\iota g'),\\
+ \widetilde{\mathcal M}_{\mathbb C}(f,g)
+   &=Q_p\!\left(\widetilde\theta^-\mathbin{\cdot}
+                    \iota^{-1}h'\right).
+ \end{aligned}
+\]
+Each phase product is computed exactly as a dyadic product before
+$Q_p$ truncates its two components. The factors and disk operands have
+numerators of magnitude at most $2^p$; four signed integer products and
+their sums therefore use $O(p)$ bits. Truncation shifts the absolute
+component numerators right by $p$ places and restores their signs, then
+writes the resulting disk-grid value in the $w_{\rm c}$-bit component
+format. It costs $O(p^{1+\delta})$ per coefficient. Generating every
+factor anew therefore still gives total
+twist cost $O(Tp^{1+\delta})$. The precision calculation below proves
+that these calls return disk-grid arrays.
+
+At the $h'$ step, Proposition~\ref{prop:synthetic-convolution} returns
+its computed grid numerators after the exact scale $M$, in the known width
+$w_M=w_{\rm c}+\log_2M$. The disk margin proved below gives
+$\|h'\|<.701$ in every use here, so each component numerator has
+magnitude at most $2^p$. Before applying $\iota^{-1}$, scan each
+$w_M$-bit word and remove only leading sign-extension bits, writing the
+same integer in $w_{\rm c}$ bits. The retained sign bit agrees with every
+removed bit by that magnitude bound. This exact normalization costs
+$O(Tw_M)=O(Tp)$ and supplies the matching scalar format for the output
+untwist; it introduces no numerical truncation.
+
+\subsection{Chirp and source-transform procedures}
+
+We next use the complex convolution to evaluate the middle factor
+$QF_{\boldsymbol t}$ in \eqref{eq:no-sort-tensor}, and then compose it
+with the Gaussian maps. For the chirp array $a$ in
+\eqref{eq:permuted-chirp}, the phase numerator
+at tensor address $j$ is computed modulo $2r$ as
+\[
+ -\sum_i s_i j_i^2(r/t_i)\pmod{2r}.
+\]
+All integers have $O(p)$ bits and $r/t_i\in\{1,2\}$.  Scan the stored
+axis descriptors and compute the $d$ squares and products with the
+previously established integer multiplier.  Additions, reductions
+modulo a power of two, and restarting local counters cost $O(p)$ per
+term; multiplication costs $O(p\log p)=O(p^{1+\delta})$.  Exponential
+evaluation then has the same $O(p^{1+\delta})$ bound.  Thus chirp
+construction costs $O(Td p^{1+\delta})$ in total.  In particular, this
+cost includes the scan of the axis descriptors at every coefficient.
+
+Let $\widetilde a$ be the resulting disk-grid array, so
+$\|\widetilde a-a\|_\infty<2\,2^{-p}$.  For a disk-grid target tensor
+$x$ of norm at most $.6$, the computed chirp transform forms the arrays
+\[
+ \begin{aligned}
+ x_0&=Q_p(\overline{\widetilde a}\mathbin{\cdot}x),\\
+ y_0&=\widetilde{\mathcal M}_{\mathbb C}(\widetilde a,x_0),\\
+ \widetilde{\mathscr C}(x)
+     &=Q_p(\overline{\widetilde a}\mathbin{\cdot}y_0).
+ \end{aligned}
+\]
+Thus $\widetilde a$ is the convolution kernel and $x_0$ is the data
+operand after the first endpoint phase.  Replacing the approximations
+by exact phases and exact convolution gives
+$\overline a\mathbin{\cdot}\mathcal M_{\mathbb C}
+(a,\overline a\mathbin{\cdot}x)=QF_{\boldsymbol t}x$ by
+\eqref{eq:permuted-chirp}.  Below we show that $\|x\|_\infty\le.6$
+implies $\|x_0\|_\infty\le.6$, which supplies the smaller operand
+required by the computed convolution.
+
+\subsubsection{The source transform}
+
+For a source disk-grid tensor of norm at most $.5$, write
+$\widetilde{\mathscr F}$ for the following procedure: apply the linewise
+approximation to $\mathcal A$, apply the
+computed chirp transform $\widetilde{\mathscr C}$, apply the linewise
+approximation to $\mathcal B_0$, and multiply the grid numerators
+exactly by $2^\gamma$.  Its exact counterpart is
+\[
+ \mathscr F=2^\gamma\mathcal B_0QF_{\boldsymbol t}\mathcal A
+            =RF_{\boldsymbol s}.
+\]
+Here an exact counterpart replaces every numerical subroutine by the
+exact map it approximates and omits truncations.  The source arrays are
+stored in the padded power-of-two box, with zeros outside the valid
+source coordinates.
+The compressed scalar output uses $w_{\rm c}$-bit components. Appending
+$\gamma$ zero bits to each word gives the exact scaled numerator in the
+known signed width $w_{\rm c}+\gamma$. For the stated input norm, the
+disk estimate below proves that every scaled coordinate still belongs to
+$\mathbb D_p$. Its component numerators therefore have magnitude at most
+$2^p$, so a scan removes only leading sign-extension bits and returns
+the same integers in $w_{\rm c}$ bits. This scan costs
+$O(T(w_{\rm c}+\gamma))=O(Tp)$ and leaves the padded zero records zero.
+Define the opposite-sign procedure by
+\[
+ \widetilde{\mathscr F}^{+}(z)
+   =\overline{\widetilde{\mathscr F}(\overline z)};
+\]
+its exact counterpart is $RF_{\boldsymbol s}^{+}$ by
+Lemma~\ref{lem:chirp-permutation}.
+
+\subsection{The multiplication algorithm}
+
+The source-transform procedures now supply the three transforms needed
+for the radix-digit convolution. Read each stored operand backward from
+its least significant end in groups of $b$ bits. This produces the radix-$2^b$ digits
+$a_0,\ldots,a_{q-1}$ in increasing coefficient order.  Buffer each
+group on a fixed work tape and read it back most significant bit first,
+reversing its least-significant-first input order; pad the final short
+group with leading zeroes.
+For digit $a_j$, write the exact grid numerator
+$a_j2^{p-b-2}$ in a signed $w_{\rm c}$-bit real word, followed by a zero
+$w_{\rm c}$-bit imaginary word. This exponent is nonnegative
+because $p=6b$, and the represented value is exactly $a_j2^{-b-2}$.
+Append $S-q$ zero coefficient records.  Buffering and ordering the
+groups costs $O(n)$, including the one partial group's padding, and
+writing the $S$ records costs $O(Sp)$.
+Together with the initial count and copies, this input conversion
+costs $O(n+Sp)=O(Tp)$; all $n$ input bits, including leading zeroes,
+are retained before the final group is padded.
+
+With these streams prepared, perform the following operations.
+\begin{enumerate}
+\item Apply the coefficient-address map $\Phi$, with its padded layout, to obtain
+source arrays $u,v$.  Their coefficients are exact $p$-bit grid
+values of norm less than $1/4$.
+\item Compute $\widetilde{\mathscr F}(u)$ and
+$\widetilde{\mathscr F}(v)$.
+\item Multiply corresponding complex coefficients exactly and truncate
+each real and imaginary part toward zero to $p$ fractional bits, writing
+the result in the common $w_{\rm c}$-bit component format.
+Denote the resulting source array by $z$.
+\item Compute $\widetilde{\mathscr F}^{+}(z)$ and multiply its grid
+numerators exactly by $S$, retaining the denominator $2^p$ and writing
+each component in signed width $w_{\rm c}+b$. Denote the represented
+dyadic array by $\widetilde w$.
+\item Multiply the grid numerators of $\widetilde w$ exactly by
+$2^{2b+4}S$, again retaining the denominator $2^p$, and write each
+component in signed width $w_{\rm c}+4b+4$. Round the represented real
+values to the nearest integers. At each valid address, write the rounded
+coefficient in one signed $(3b+1)$-bit word, most significant bit first;
+at every padded address,
+write a zero word of that width. Supply this local payload width to
+$\Phi^{-1}$ and apply it, including removal of the address padding, to
+restore the ordinary coefficient order.
+\item Propagate radix-$2^b$ carries in increasing coefficient order.
+Write the resulting bits from least to most significant on a work tape,
+then reverse that stream and output exactly $2n$ bits in
+most-significant-first order.
+\end{enumerate}
+
+The two occurrences of $S$ in this algorithm undo different
+normalizations.  By \eqref{eq:source-permutation-cancel}, the exact
+counterpart after the three transforms is $(u*v)/S^2$, so after the
+first scale it is $w=(u*v)/S$.  The second scale gives
+$2^{2b+4}(u*v)$, whose inverse image under $\Phi$ is the original
+integer coefficient convolution.  The next subsection verifies the
+disk bounds needed by every call and proves that the final error is
+less than $1/2$; it also justifies the rounding, carries, and output
+length.
+
+\subsection{Precision and exact recovery}
+
+Proposition~\ref{prop:simultaneous-layer} uses
+$C_1=20$, so $\epsilon C_1<1$ makes its coefficient width $O(p)$.
+Lemma~\ref{lem:synthetic-transform-cost} therefore applies to every
+synthetic transform here, with error less than
+$\sqrt2\ell\,2^{-p}<L2^{-p}$, where $L=\log_2T$, for all
+sufficiently large $n$.
+
+\subsubsection{Scales and disk margins}
+
+Put $h_p=2^{-p}$, and use the coefficient sup norm throughout this
+subsection.  An error of $a$ will mean absolute error less than $ah_p$.
+A linear contraction propagates an input error without increasing it.
+For a bilinear contraction $\mathcal M$, replacing its operands gives
+\[
+ \|\mathcal M(f',g')-\mathcal M(f,g)\|
+ \le \|f'-f\|\,\|g'\|+\|f\|\,\|g'-g\|.
+\]
+When all four operands are in the disk, their two errors therefore add.
+
+We also need the norm as well as the error of a computed phase product.
+Let $e$ be a unit phase, let $\widetilde e$ be a disk-grid approximation
+with $|\widetilde e-e|<2h_p$, and let $x$ be a disk operand.  The
+truncation bound in \eqref{eq:transform-truncate} gives
+\[
+ \|Q_p(\widetilde e x)-ex\|
+   <(2\|x\|+\sqrt2)h_p<4h_p,
+ \qquad
+ \|Q_p(\widetilde e x)\|\le\|x\|.
+\]
+The second inequality follows from $|\widetilde e|\le1$ and the fact
+that $Q_p$ does not increase the norm.  It preserves every smaller
+operand norm through a twist or an endpoint phase multiplication.
+The same bounds hold coordinatewise for arrays of phases.
+
+For disk-grid ring arrays $f,g$, put $M=T/r$.  Two normalized synthetic
+forwards, pointwise polynomial multiplication divided by $r$, and the
+normalized opposite transform give $(f*g)/(rM^2)$.  The exact
+multiplication by $M$ in Proposition~\ref{prop:synthetic-convolution}
+then gives $\mathcal M_r(f,g)=(f*g)/T$.  Before that multiplication,
+the three transform errors and the polynomial-product truncation total
+less than $3L+2$.  Thus the error of the returned normalized
+convolution is bounded by
+\[
+ E_{\rm ring}:=M(3L+2)<5TL.
+\]
+If one operand has norm at most $.7$, bilinear contraction gives
+$\|\mathcal M_r(f,g)\|\le.7$.  Its computed grid output consequently
+has norm less than $.7+5TLh_p<.701$ for large $n$.  This proves the
+disk margin after the scale $M$, without clipping the output.
+
+Consider now $\widetilde{\mathcal M}_{\mathbb C}(f,g)$ for disk grid
+operands, one of norm at most $.7$.  Its two computed input twists
+$f',g'$ are disk grid arrays, and the smaller one still has norm at
+most $.7$ by the phase inequality.  The identification $\iota$
+preserves these bounds.  The preceding ring margin therefore gives
+$\|h'\|<.701$.  Neither $\iota^{-1}$ nor the computed output untwist
+increases this norm.  In particular,
+$\widetilde{\mathcal M}_{\mathbb C}(f,g)$ is a disk grid array.
+
+To compare it with $\mathcal M_{\mathbb C}(f,g)$, insert the exact
+normalized $\mathcal M_r$ at $\iota f'$ and $\iota g'$.
+Its bilinear contraction bound propagates the two input twist errors,
+each less than $4$.  Its approximation contributes $E_{\rm ring}$,
+and the output untwist contributes less than $4$.  All these
+comparisons are at the normalized $\mathcal M_r$ interface, after its
+factor $M$.  They give
+\[
+ \|\widetilde{\mathcal M}_{\mathbb C}(f,g)
+            -\mathcal M_{\mathbb C}(f,g)\|
+ <(E_{\rm ring}+4+4+4)h_p<6TLh_p.
+\]
+
+For a disk-grid chirp input $x$ with $\|x\|\le.6$, the previously
+defined data operand $x_0=Q_p(\overline{\widetilde a}\cdot x)$ has
+norm at most $.6$.  The kernel $\widetilde a$ is a disk grid array.
+Thus this pair satisfies the smaller-operand condition just proved:
+$\|y_0\|<.701$, and the last endpoint multiplication gives
+$\|\widetilde{\mathscr C}(x)\|<.701$.  In particular, the chirp output
+is a legal disk-grid input to the compression maps.
+
+For its error, the exact operands $a$ and $\overline a\cdot x$ are in
+the disk because every entry of $a$ has modulus one.  The kernel
+approximation contributes less than $2$ and
+the first endpoint multiplication contributes less than $4$ when
+inserted into the exact bilinear contraction
+$\mathcal M_{\mathbb C}$.  The computed convolution contributes less
+than $6TL$, and the last endpoint multiplication less than $4$.
+Equation~\eqref{eq:permuted-chirp} identifies the exact result, so
+\[
+ \|\widetilde{\mathscr C}(x)-QF_{\boldsymbol t}x\|
+ <(6TL+2+4+4)h_p<8TLh_p.
+\]
+
+Finally let the input to a source transform have norm at most $.5$.
+The computed expansion has error less than $dp^2$ and norm less than
+$.5+dp^2h_p<.51$.  It is therefore a permitted chirp input.  The
+chirp output is in the disk by the preceding argument, so each
+compression call is defined and returns another disk-grid array.
+Insert the exact contractions $\mathcal A$, $QF_{\boldsymbol t}$,
+and $\mathcal B_0$ at the computed inputs.  The error before the
+source scale is less than $2dp^2+8TL$.  Multiplication by
+$2^\gamma$ therefore gives error less than
+$2^\gamma(2dp^2+8TL)h_p$, which is bounded by $E_sh_p$ with
+\begin{equation}\label{eq:source-error}
+ E_s=9\,2^\gamma TL,
+\end{equation}
+because $2dp^2<TL$ eventually.  The exact source transform
+$RF_{\boldsymbol s}$ is a contraction, so the scaled approximation
+has norm at most $.5+E_sh_p<.501$.  Its exact numerator scaling
+therefore also leaves a disk-grid output without clipping.
+Conjugation preserves the grid and norm, so the opposite procedure
+has the same error and disk guarantee.
+All these margins may be enforced by one fixed cutoff.  For example,
+$b\ge2^{24}$, together with the other eventual construction conditions,
+makes $dp^2h_p$, $8TLh_p$, $E_sh_p$ and
+$28\,2^\gamma T^2Lh_p$ smaller than $10^{-3}$.
+
+\subsubsection{The final integer coefficients}
+
+The scaled radix digits in $u,v$ are exact $p$-bit grid values of norm
+strictly less than $1/4$.  Put
+\[
+ \begin{aligned}
+ U&=RF_{\boldsymbol s}u,&\qquad V_1&=RF_{\boldsymbol s}v,\\
+ \widetilde U&=\widetilde{\mathscr F}(u),&
+ \widetilde V_1&=\widetilde{\mathscr F}(v).
+ \end{aligned}
+\]
+The exact arrays have norm less than $1/4$, and the computed arrays
+have norm less than $1/4+E_sh_p<.26$.  Hence
+$z=Q_p(\widetilde U\cdot\widetilde V_1)$ has norm at most
+$.26^2<.5$.  To estimate its error, write
+\[
+ \widetilde U\cdot\widetilde V_1-U\cdot V_1
+ =(\widetilde U-U)\cdot\widetilde V_1
+       +U\cdot(\widetilde V_1-V_1).
+\]
+The factors $\widetilde V_1$ and $U$ are in the disk.  The two terms
+have total norm less than $2E_sh_p$, and truncation adds less than $2h_p$.
+Thus $\|z-U\cdot V_1\|<(2E_s+2)h_p$.
+
+Let $G:=RF_{\boldsymbol s}^+$ be the exact opposite contraction.
+Lemma~\ref{lem:chirp-permutation}, applied to
+$U=RF_{\boldsymbol s}u$ and $V_1=RF_{\boldsymbol s}v$, gives
+\[
+ G(U\cdot V_1)=(u*v)/S^2.
+\]
+The computed opposite transform may be applied to $z$ because
+$\|z\|<.5$. Insert $G$ at that computed input:
+\[
+ \begin{aligned}
+ \|\widetilde{\mathscr F}^{+}(z)-G(U\cdot V_1)\|
+ &\le \|\widetilde{\mathscr F}^{+}(z)-Gz\|\\
+ &\qquad+\|G(z-U\cdot V_1)\|\\
+ &<(3E_s+2)h_p.
+ \end{aligned}
+\]
+The first exact numerator multiplication by $S$ gives
+$\widetilde w$, approximating $w=(u*v)/S$ with error less than
+$E_wh_p$, where
+\[
+ E_w:=S(3E_s+2)<28\,2^\gamma T^2L.
+\]
+Each coefficient of $w$ is an average of $S$ products of coefficients
+of $u$ and $v$, so $\|w\|<1/16$.  The earlier cutoff therefore gives
+\[
+ \|\widetilde w\|<1/16+E_wh_p<1/16+10^{-3}<1.
+\]
+This proves the disk bound for the computed first scaled result.
+
+In tensor order, the unscaled integer coefficient array is
+$2^{2b+4}S w$.  This second occurrence of $S$ reverses the
+normalization still present in $w$, and $2^{2b+4}$ reverses the two
+input scales.  Both multiplications act exactly on grid numerators.
+Since $S\le T<2^b$ and $L<b$ eventually, the final absolute error is less than
+\begin{equation}\label{eq:final-error}
+ 2^{2b+4}S\cdot28\,2^\gamma T^2L\cdot2^{-6b}
+ <448b\,2^{-b+\gamma}
+ \le448b\,2^{-3b/4}<\frac12.
+\end{equation}
+The true coefficients are real integers.  If $H_j$ is the real
+numerator after the second scaling, its represented value is
+$H_j/2^p$.  The strict error below $1/2$ makes the nearest integer to
+that value the unique correct coefficient.
+
+These exact operations use known fixed record widths. If $N$ is a
+signed $w_0$-bit integer, then $-2^{w_0-1}\leq N<2^{w_0-1}$. Since
+$0<S<2^b$, its product satisfies
+$-2^{w_0+b-1}<SN<2^{w_0+b-1}$ and therefore fits in signed width $w_0+b$.
+The first product by $S$ starts at width $w_{\rm c}$ and is written in
+width $w_{\rm c}+b$. The next product by $S$ is written in width
+$w_{\rm c}+2b$; appending $2b+4$ least significant zero bits then gives
+the exact second scale in width $w_{\rm c}+4b+4$. Each complex record
+still places its most-significant-bit-first real word before its imaginary
+word. The known widths determine every boundary in the next scan and are
+$O(p)$ because $p=6b$.
+
+The established integer multiplier performs the two products by $S$ in
+$O(p\log p)$ time per entry. To serialize each exact signed product at
+its stated width, zero-pad its magnitude and complement and increment
+for a negative sign. The proved bounds ensure that no significant bit is
+discarded. These conversions and the power-of-two shift use linear scans.
+To round $H_j/2^p$, recover the real magnitude, inspect its low $p$ bits,
+and apply the rounding carry with the sign restored. The strict error
+bound makes the result the correct nonnegative coefficient, and
+\eqref{eq:capacity} puts it in $[0,2^{3b})$. It therefore fits in one
+signed $(3b+1)$-bit two's-complement word, written most significant bit
+first. Scan the padded box in the
+physical axis order recorded by its shape descriptor, using the same
+$O(p)$-bit nested counters and validity tests as above. Consume the
+imaginary word and write this real coefficient word at each valid address,
+with an all-zero
+word at each padded address. This serialization costs $O(Tp)$ in total.
+It keeps the tensor address order and supplies payload width $3b+1$ to
+the local descriptors for $\Phi^{-1}$, so the address routine receives a
+stream of known fixed-length records.
+
+Lemma~\ref{lem:signed-ring-product} proves exact signed packing,
+centered extraction and negacyclic reduction. Its only numerical error
+is the stated truncation after division by $r$, already included above.
+Undo the coefficient-address isomorphism $\Phi$ before propagating
+radix carries.
+
+To propagate carries, let $Q_0=2^b$.  The recovered ordinary
+coefficients are the $c_j$ in \eqref{eq:capacity}; they are zero for
+$2q-2<j<S$.  With $q=\lceil n/b\rceil$ as
+above, use the recurrence for $0\le j<S$:
+\[
+ k_0=0,\qquad d_j=(c_j+k_j)\bmod Q_0,\qquad
+ k_{j+1}=\left\lfloor\frac{c_j+k_j}{Q_0}\right\rfloor.
+\]
+The carries satisfy $0\le k_j\le q(Q_0-1)<Q_0^2$.  If this holds at
+$j$, then
+\[
+ c_j+k_j\le q(Q_0-1)^2+q(Q_0-1)=qQ_0(Q_0-1),
+\]
+which proves the next carry bound.  The defining relation
+$c_j+k_j=d_j+Q_0k_{j+1}$ also gives the exact invariant
+\[
+ \sum_{h<j}c_hQ_0^h
+   =\sum_{h<j}d_hQ_0^h+k_jQ_0^j.
+\]
+It holds for $j=0$, and the defining relation proves its next instance.
+The unprocessed terms are multiples of $Q_0^j$, so the identity fixes
+the first $j$ radix digits of the full product.  The value $k_j$ is
+the carry from the processed coefficients into the remaining positions.
+
+After $\Phi^{-1}$ the coefficients occur in increasing ordinary index,
+so this carry scan proceeds from least to most significant.  Carry
+storage and work per coefficient are $O(b)$ bits and steps.  Write
+each digit's bits from low to high on a work tape, and drain the final
+$O(b)$-bit carry in the same order.  Copy the completed stream backward
+once to obtain most-significant-first order.  The stream has length
+$O(Sb)=O(Tp)$, including chunk padding and the final carry, so this
+reversal is a charged linear tape pass.  The exact product is less
+than $2^{2n}$; all bits above position $2n-1$ are therefore zero.
+Remove only those zero padding bits and retain leading zeros as needed
+to produce exactly $2n$ bits.  Zero inputs obey the same invariant and
+output rule.
+
+\subsection{The complete time bound}
+
+For the cost calculation put $V=Tp=\Theta(n)$. The fixed-width coefficient
+formats use $\Theta(p)$ bits per coefficient, so a full padded array has
+$\Theta(V)$ stored bits. Table~\ref{tab:costs} lists costs after division
+by $V$; a fixed number of repeated transforms and convolutions is
+included in its constants.
+\begin{table}[ht]
+\centering
+\small
+\begin{tabular}{@{}>{\raggedright\arraybackslash}p{.40\linewidth}ll@{}}
+\toprule
+Operation & Normalized cost & Power of $p$\\
+\midrule
+Prefix-slot moves and individual butterfly rounds & $dK$ & $\epsilon(1+c)$\\
+Chunk exchanges for transform layout & $pK^{\tau-1}$ & $1-\epsilon c(1-\tau)$\\
+Simultaneous butterfly rounds & $\ell d^{\lambda'}$ & $1-\epsilon(1-\lambda')$\\
+CRT and axis layouts & $d^2(1+\ell^\tau)$ & $\tau+\epsilon(2-\tau)$\\
+Gaussian line maps & $dp^{1/2+\delta}\alpha$ & $3/4+\delta+3\epsilon/2$\\
+Chirps, twists and scalar products & $dp^\delta$ & $\epsilon+\delta$\\
+Packed polynomial products & $\log(rp)$ & $1-\epsilon$\\
+Final scaling and rounding & $p^\delta$ & absorbed above\\
+Input, padding, carries and output & $1$ & absorbed above\\
+\bottomrule
+\end{tabular}
+\caption{Costs divided by $Tp$; each coefficient
+representation has $O(p)$ bits.}\label{tab:costs}
+\end{table}
+
+The seven dominant powers in Table~\ref{tab:costs} have the following
+margins below one:
+\begin{equation}\label{eq:margin-list}
+\begin{split}
+ g_1&=1-\epsilon(1+c),\qquad
+ g_2=\epsilon c(1-\tau),\qquad
+ g_3=\epsilon(1-\lambda'),\\
+ g_4&=1-\tau-\epsilon(2-\tau),\qquad
+ g_5=1/4-\delta-3\epsilon/2,\\
+ g_6&=1-\delta-\epsilon,\qquad g_7=\epsilon.
+\end{split}
+\end{equation}
+Direct substitution gives
+\[
+ g_1>\frac12,\quad g_2=2^{-181},\quad g_3=2^{-129},\quad
+ g_4>2^{-51},\quad g_5>\frac18,\quad g_6>\frac12,\quad g_7=2^{-75}.
+\]
+Thus $\min_i g_i=2^{-181}=2\kappa$.  This explicit slack will cover
+any remaining fixed power of $\log p$.
+
+Here $d^2$ is absorbed by $d^2\ell^\tau$, and
+$\log(rp)=O(p^{1-\epsilon}+\log p)=O(p^{1-\epsilon})$.
+The first three rows are the terms in
+\eqref{eq:synthetic-transform-cost}. The prefix-slot moves and
+individual butterfly rounds in Lemma~\ref{lem:synthetic-transform-cost}
+use $O(dK)$ linear scans. Its positional layout uses $O(p/K)$ exchanges
+of width-$K$ chunks, because $d\ell=O(p)$. Each exchange costs
+$O(VK^\tau)$ by Lemma~\ref{lem:chunk-swap}, so the normalized total is
+\[
+ O(p/K)\,K^\tau=O(pK^{\tau-1}).
+\]
+For the at most $\ell$ simultaneous rounds,
+Proposition~\ref{prop:simultaneous-layer} supplies $O(Vd^{\lambda'})$
+per round. Its bound already includes the binary basis changes,
+deterministic repair, row padding and removal, all base-$m$ groups,
+and fixed-tape cleanup.
+
+Axis exposure and restoration require $O(d^2)$ adjacent axis moves.
+Each costs $O(V(1+\ell^\tau))$: peel a single excess bit when widths
+differ by one, exchange their equal-width parts, and restore the bit.
+The $d$ CRT rotations copy valid and invalid intervals in $O(dV)$ time.
+Their offset setup was bounded above by $O(dTp^C/r)=o(Tp)$,
+using at most $T/t_i$ control prefixes for target $i$.
+
+For Gaussian resampling, axis $i$ has at most $T/t_i$ processed lines.
+The line-machine costs therefore sum to
+\[
+ \sum_{i=1}^d\frac{T}{t_i}
+       O(t_i p^{3/2+\delta}\alpha)
+ =O(dTp^{3/2+\delta}\alpha).
+\]
+Dividing by $V=Tp$ gives the fifth row.  The factor
+$\alpha=\Theta(p^{1/4+\epsilon/2})$ explains its displayed power of $p$.
+
+Chirp numerators have $O(p)$ bits and can be computed modulo $2r$ as
+sums of $d$ terms $s_i j_i^2(r/t_i)$.  Computing their squares and
+products with the previously established $O(N\log(2N))$ multiplier
+on $N$-bit inputs,
+then generating the exponentials, costs $O(dp^{1+\delta})$ per entry.
+The smaller twist and scalar pointwise-product costs fit the same row:
+they use a fixed number of exact products on $O(p)$-bit component
+numerators, followed by linear truncation scans.  The two final products
+by $S$ also cost $O(p\log p)$ per entry, so their normalized cost is
+$O(\log p)=O(p^\delta)$ as listed separately.  There are $T/r$
+polynomial records in each pointwise ring product.  Four integer
+products on $O(rp)$ bits per record therefore cost
+$O(Tp\log(rp))$ in total.  Signed packing, centered extraction,
+negacyclic wrapping, and copying are linear stream passes.  These calls
+use the previously established multiplier on records of length
+$O(rp)=o(n)$; they do not call the improved algorithm being constructed.
+The exact source scaling by $2^\gamma$ is a shift of $O(p)$-bit
+numerators by $\gamma=O(p)$ places, so it is a linear scan per entry
+and fits the final-scaling row. The scalar-format adapters and the exact
+removal of sign-extension bits after the ring and source scales also use
+linear scans of their $O(p)$-bit components, within the listed scan costs.
+
+\paragraph{Setup and exceptional streams across all calls.}
+We next separate setup at recursion nodes from work repeated for every
+polynomial record or every Gaussian line.  Here a visit means a node
+of the layer or address-layout recursions, or one of their round and
+group invocations.  The internal recursion of the established integer
+multiplier and the iterations of the quoted Gaussian algorithms are
+already included in their separately charged running times.
+The layer and address-layout recursions have constant branching and
+depth $O(\log p)$, and the number of their rounds and base-$m$ groups
+is polynomial in $p$.  Choose a fixed exponent $A$ so that their
+total number of visits is at most $p^A$, and a fixed $C$ bounding
+descriptor setup performed once per visit by $p^C$ steps.  This setup then
+costs at most $p^{A+C}=o(Tp)$.
+
+At a layer or synthetic-transform visit that processes polynomial
+records, there are at most $O(T/r)$ such records, including the
+bounded row padding.  Every relevant child keeps the whole
+length-$r$ polynomial suffix.  Consequently $O(p^C)$ descriptor or
+address work per record, over these visits, costs at most
+$O(Tp^{A+C}/r)=o(Tp)$.  Setup before each Gaussian line call has a
+different count:
+there are at most $2dT/r$ lines per tensor map and only a fixed number
+of such maps, so $O(p^C)$ setup per line costs
+$O(dTp^C/r)=o(Tp)$.  These estimates all use that $r$ exceeds every
+fixed power of $p$.
+
+The general address-swap subroutine also covers one-bit payloads,
+where no polynomial suffix is available. For root volume $V_0$ and
+current child volume $V_j$, the descriptor estimate in the proof of
+Proposition~\ref{prop:power-interchange} gives
+$(\log(2V_0))^{O(1)}=O(V_j)$. It uses the invariant that both original
+chunk ranges remain present in every child, and therefore includes
+polynomial descriptor work even for a one-bit payload.
+Elementary counter updates use local length copies, so they do not
+rescan a growing descriptor for each data bit.  The chirp computation
+does scan the axis descriptors at every coefficient; its
+$O(Tdp^{1+\delta})$ cost was included in the chirp row.
+
+For one packed change of basis, let $V_{\rm call}$ be its current
+logical volume.  The bad-address fraction is
+$O(d2^{-K})$, independently of the payload.  Each polynomial record
+has $\Theta(rp)$ payload bits, and an exceptional record adds an
+$O(p)$-bit destination key.  Thus the compact exceptional stream has
+length
+\[
+ O\!\left(\frac{V_{\rm call}}{rp}\,d2^{-K}(rp+p)\right)
+   =O(V_{\rm call}d2^{-K}).
+\]
+Stable bit sorting makes $O(p)$ scans of this stream, for one-call
+cost $O(V_{\rm call}dp2^{-K})$.  Extraction and reinsertion use a
+constant number of scans of the full current volume; those scans are
+already in the node overhead.  Since there are at most $p^A$ visits,
+each of volume $O(V)$, the compact sorting costs sum to at most
+\[
+ O\!\left(dp2^{-K}\sum_{\rm calls}V_{\rm call}\right)
+   =O(Vp^{A'}2^{-K})=o(V)
+\]
+for another fixed exponent $A'$.  Here $d=O(p^\epsilon)$ and
+$K=\Theta(p^{\epsilon c})$ with $\epsilon c>0$.  Predicate and key
+arithmetic is the polynomial work per record counted above.  This is
+a deterministic worst-case bound.
+
+Finally, all role, arithmetic, and stack tapes form fixed finite
+families.  A child parks and restores only its parent's streams, with
+the stack head at the active top; copying and cleanup are charged to
+that logical volume.  No operation repeatedly scans parked ancestors.
+Growing axis lists and call states are stored data, not extra tapes or
+alphabet symbols.  Global setup and prime search cost $o(V)$, as
+proved earlier.
+
+Each of the seven displayed powers is at most $1-2\kappa$ by
+\eqref{eq:margin-list}.  Any fixed power of $\log p$ is at most $p^\kappa$
+eventually.  The complete large-input bound is consequently
+\[
+ O(Tp\,p^{1-\kappa})=O(n(\log n)^{1-\kappa}).
+\]
+Fix one cutoff beyond all the size, precision, margin and layout
+conditions, and use schoolbook multiplication below it.  The finitely
+many smaller lengths are included by enlarging the implicit constant.
+With $\lg n=\max\{\lceil\log_2n\rceil,1\}$, the resulting single
+fixed-alphabet, fixed-tape deterministic machine has worst-case time
+$O(n(\lg n)^{1-\kappa})$ for every input length and produces precisely
+the required $2n$-bit product.
diff --git a/research/many-axis-prime-supply/test_verify.py b/research/many-axis-prime-supply/test_verify.py
new file mode 100644
index 0000000000..4d0cf8d205
--- /dev/null
+++ b/research/many-axis-prime-supply/test_verify.py
@@ -0,0 +1,253 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Bounded API and CLI controls for the many-axis prime-supply package.
+
+Exercises host-reference construction and the authenticated production predicate
+adapter. It does not establish the external analytic prime estimate, formalize
+the uniform tape construction, or claim encoded execution.
+"""
+from copy import deepcopy
+import hashlib
+import importlib.util
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+
+
+class TestFailure(Exception):
+    pass
+
+
+def need(ok, message):
+    if not ok:
+        raise TestFailure(message)
+
+
+def tree_bytes(root):
+    return {str(path.relative_to(root)): hashlib.sha256(path.read_bytes()).hexdigest()
+            for path in root.rglob('*') if path.is_file()}
+
+
+def load_subject(root):
+    spec = importlib.util.spec_from_file_location('many_axis_prime_subject', root / 'verify.py')
+    subject = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(subject)
+    return subject
+
+
+def run_cli(root):
+    command = [sys.executable, '-I', '-B']
+    if not __debug__:
+        command.append('-O')
+    return subprocess.run(command + [str(root / 'verify.py')], cwd=root,
+                          capture_output=True, text=True)
+
+
+class Controls:
+    def __init__(self):
+        self.rejected = []
+
+    def rejects(self, name, action):
+        try:
+            action()
+        except ValueError:
+            self.rejected.append(name)
+            return
+        except Exception as error:
+            raise TestFailure(name + ' crashed with ' + type(error).__name__ + ': ' + str(error)) from error
+        raise TestFailure(name + ' was accepted')
+
+    def cli_rejects(self, name, root, contains=None):
+        result = run_cli(root)
+        need(result.returncode != 0, name + ' CLI accepted the altered fixture')
+        need('FAIL' in result.stderr, name + ' CLI did not report an explicit validation failure: ' + result.stderr[-500:])
+        if contains is not None:
+            need(contains in result.stderr, name + ' failed through the wrong validation path: ' + result.stderr[-500:])
+        self.rejected.append(name)
+
+
+def writable_copy(source, destination):
+    shutil.copytree(source, destination, copy_function=shutil.copyfile)
+    for path in destination.rglob('*'):
+        path.chmod(0o755 if path.is_dir() else 0o644)
+    destination.chmod(0o755)
+
+
+def main():
+    import argparse
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--package', type=Path, default=Path(__file__).resolve().parent)
+    args = parser.parse_args()
+    root = args.package.resolve()
+    before = tree_bytes(root)
+    subject = load_subject(root)
+    controls = Controls()
+    positives = []
+    guard = subject.source_guard()
+    need(guard.__code__.co_filename == 'authenticated TensorPlan.production_axis',
+         'guard was not compiled from the authenticated selected source method')
+    fixture = subject.supplies(12, (0, 1, 1), guard=guard)
+    primes = list(fixture['primes'])
+    need(fixture['D'] == 3 and fixture['d'] == 4 and fixture['source_guard_checks'] == 3,
+         'actual source dimension d=D+1 was not used for all axes')
+    need(fixture['source_bit_length'] == 36 and fixture['flag_bit_length'] == 2,
+         'source words or implicit final full-axis flag count changed')
+    need(3 * fixture['S'] > 2 * fixture['T'] and fixture['S'] < fixture['T'],
+         'source product does not occupy the claimed target-volume fraction')
+    need(fixture['encoded_execution'] is False and fixture['production_tensor_execution'] is False,
+         'host reference incorrectly claimed encoded execution')
+    positives.append('D=3 mixed-axis source words, final-axis flags, volume and authenticated source guard')
+
+    def explicit_control(name, change_primes=None, flags=(0, 1, 1)):
+        supplied = primes.copy()
+        if change_primes is not None:
+            change_primes(supplied)
+        controls.rejects(name, lambda: subject.validate_supplied(12, flags, supplied, guard=guard))
+
+    explicit_control('same-target duplicate primes', lambda p: p.__setitem__(2, p[1]))
+    explicit_control('mixed-target duplicate primes', lambda p: p.__setitem__(0, p[1]))
+    explicit_control('in-band odd composite 1881', lambda p: p.__setitem__(0, 1881))
+    explicit_control('in-band even source 1880', lambda p: p.__setitem__(0, 1880))
+    explicit_control('power-of-two source length', lambda p: p.__setitem__(0, 1024))
+    explicit_control('source prime two', lambda p: p.__setitem__(0, 2))
+    explicit_control('boolean source prime', lambda p: p.__setitem__(0, True))
+    explicit_control('floating source prime', lambda p: p.__setitem__(0, float(p[0])))
+    explicit_control('source axis order swapped', lambda p: p.__setitem__(slice(0, 2), [p[1], p[0]]))
+    explicit_control('source flag order swapped', flags=(1, 0, 1))
+    explicit_control('missing source axis', lambda p: p.pop())
+    explicit_control('extra source axis', lambda p: p.append(p[-1]))
+    explicit_control('missing final full target axis', flags=(0, 1, 0))
+    explicit_control('boolean target flag', flags=(0, True, 1))
+    explicit_control('target flag outside literal alphabet', flags=(0, 2, 1))
+
+    for name, ell, flags in (
+        ('boolean fixture exponent', True, (1,)),
+        ('fixture exponent below domain', 2, (1,)),
+        ('giant symbolic threshold sent to bounded constructor', subject.ELL0, (1,)),
+        ('empty target flag stream', 12, ()),
+    ):
+        controls.rejects(name, lambda ell=ell, flags=flags: subject.supplies(ell, flags, guard=guard))
+    controls.rejects('boolean target halo', lambda: subject.supplies(12, (0, 1, 1), True, 2, guard))
+    controls.rejects('negative target halo', lambda: subject.supplies(12, (0, 1, 1), -1, 2, guard))
+    controls.rejects('boolean period width', lambda: subject.supplies(12, (0, 1, 1), 16, False, guard))
+    controls.rejects('boolean prime quota', lambda: subject.prime_queue(4096, 4, True))
+    controls.rejects('boolean interval dimension', lambda: subject.interval(4096, True))
+    controls.rejects('insufficient finite supply is not asymptotic admission',
+                     lambda: subject.supplies(4, (0, 1, 1), guard=guard))
+
+    # Equality must fail the literal source's strict predicates. These isolate
+    # lower, upper and period comparisons with the other numeric guards slack.
+    controls.rejects('strict lower source ratio at equality',
+                     lambda: subject.check_source_axis(8, 9, 2, 0, 0, guard))
+    controls.rejects('strict upper source ratio at equality',
+                     lambda: subject.check_source_axis(3, 4, 2, 0, 0, guard))
+    controls.rejects('strict source period at equality',
+                     lambda: subject.check_source_axis(14, 16, 2, 3, 2, guard))
+    need(subject.check_source_axis(1913, 2048, 4, guard=guard), 'valid d=D+1 source guard failed')
+    controls.rejects('using D instead of D+1 fails an actual source ratio',
+                     lambda: subject.check_source_axis(1913, 2048, 3, guard=guard))
+
+    for name, args in (
+        ('boolean source dimension before ownership allocation', (1913, 2048, True, 16, 2)),
+        ('negative source period before ownership allocation', (1913, 2048, 4, 16, -1)),
+    ):
+        controls.rejects(name, lambda args=args: subject.check_source_axis(*args, guard=guard))
+        need(not subject.Natural.live, 'invalid operand leaked modeled ownership')
+
+    def corrupt_dimension(model, _s, _t):
+        model.d.value += 1
+
+    controls.rejects('modeled borrowed dimension changed by guard',
+                     lambda: subject.check_source_axis(1913, 2048, 4, guard=corrupt_dimension))
+    need(not subject.Natural.live, 'rejected guard left modeled scratch live')
+    positives.append('literal strict source predicates and modeled ownership restoration')
+
+    reordered = subject.supplies(12, (1, 0, 1), guard=guard)
+    need(reordered['S'] == fixture['S'] and reordered['T'] == fixture['T']
+         and reordered['flag_bits_sha256'] != fixture['flag_bits_sha256']
+         and reordered['source_bits_sha256'] != fixture['source_bits_sha256'],
+         'axis order was collapsed to unordered products')
+    positives.append('ordered flag/source streams distinguish equal-product axis orders')
+
+    threshold = subject.threshold_certificate()
+    need(type(threshold['ell0']) is int and threshold['ell0'] == 1 << 32
+         and threshold['dimension_power'] == 334 and threshold['giant_power_constructed'] is False,
+         'symbolic threshold domain or no-giant-power scope changed')
+    ell = threshold['ell0']
+    maximal_d = ell ** threshold['dimension_power']
+    need(ell < 8 * maximal_d, 'new many-axis domain unexpectedly implies obsolete log(t)>8d shortcut')
+    need(threshold['analytic_input_imported'] is True and threshold['analytic_input_reproved'] is False,
+         'external analytic input was represented as a finite proof')
+    positives.append('symbolic cutoff without giant powers; obsolete HH shortcut fails at admitted maximal dimension')
+
+    # A fresh copied fixture can be writable even when the submitted export is
+    # read-only; no byte or permission of the package under test is changed.
+    with tempfile.TemporaryDirectory(prefix='many-axis-prime-negative-') as directory:
+        copied = Path(directory) / 'package'
+        writable_copy(root, copied)
+        baseline = run_cli(copied)
+        need(baseline.returncode == 0 and 'PASS_MANY_AXIS_PRIME_SUPPLY' in baseline.stdout,
+             'unaltered copied CLI fixture failed: ' + baseline.stderr[-500:])
+        positives.append('unaltered complete typed CLI receipt accepted')
+
+        source_path = copied / 'source/PR3935-tensor_plan.py'
+        source_bytes = source_path.read_bytes()
+        source_path.write_bytes(source_bytes + b'\ninvalid python !\n')
+        controls.cli_rejects('source authentication precedes AST parsing', copied, 'source bytes:')
+        source_path.write_bytes(source_bytes)
+        sibling = Path(directory) / 'same-tensor-plan.py'
+        sibling.write_bytes(source_bytes)
+        source_path.unlink()
+        source_path.symlink_to(sibling)
+        controls.cli_rejects('source symlink substitution', copied, 'source symlink:')
+        source_path.unlink()
+        source_path.write_bytes(source_bytes)
+
+        receipt_path = copied / 'RESULT.json'
+        original_receipt = receipt_path.read_bytes()
+        receipt = json.loads(original_receipt)
+
+        def receipt_control(name, change):
+            forged = deepcopy(receipt)
+            change(forged)
+            receipt_path.write_text(json.dumps(forged) + '\n')
+            controls.cli_rejects(name, copied, 'complete typed receipt')
+
+        receipt_control('boolean root schema', lambda r: r.__setitem__('schema_version', True))
+        receipt_control('integer false encoded-execution flag', lambda r: r.__setitem__('encoded_execution', 0))
+        receipt_control('wrong D instead of D+1 receipt', lambda r: r['cases'][1].__setitem__('d', 3))
+        receipt_control('wrong spectator flag count', lambda r: r['cases'][1].__setitem__('flag_bit_length', 3))
+        receipt_control('missing encoded source-word volume', lambda r: r['cases'][1].__setitem__('source_bit_length', 24))
+        receipt_control('false full source product volume', lambda r: r['cases'][1].__setitem__('S', 1))
+        receipt_control('wrong axis flag order hash', lambda r: r['cases'][1].__setitem__('flag_bits_sha256', '0' * 64))
+        receipt_control('boolean symbolic cutoff', lambda r: r['threshold'].__setitem__('ell0', True))
+        receipt_control('clamped symbolic cutoff outside proved domain', lambda r: r['threshold'].__setitem__('ell0', 20))
+        receipt_control('changed symbolic dimension domain', lambda r: r['threshold'].__setitem__('dimension_power', 335))
+        receipt_control('obsolete log-t-greater-than-8d analytic premise',
+                        lambda r: r['threshold'].__setitem__('FKS_reference', 'HH log(t)>8d shortcut'))
+        receipt_control('external analytic premise misreported as reproved',
+                        lambda r: r['threshold'].__setitem__('analytic_input_reproved', True))
+        receipt_control('giant threshold power misreported as constructed',
+                        lambda r: r['threshold'].__setitem__('giant_power_constructed', True))
+        receipt_control('unsupported new kappa claim', lambda r: r.__setitem__('new_kappa', True))
+        receipt_control('unrecognized receipt key', lambda r: r.__setitem__('all_obligations_closed', True))
+        serialized = json.dumps(receipt)
+        receipt_path.write_text('{"schema_version":1,' + serialized[1:] + '\n')
+        controls.cli_rejects('duplicate receipt JSON key', copied, 'duplicate JSON key')
+        receipt_path.write_bytes(original_receipt)
+
+    need(tree_bytes(root) == before, 'the package under test changed')
+    print('PASS_MANY_AXIS_PRIME_SUPPLY_TESTS ' + json.dumps(
+        {'positive_controls': len(positives), 'expected_rejections': len(controls.rejected),
+         'positive_names': positives, 'rejection_names': controls.rejected,
+         'package_bytes_unchanged': True, 'optimized': not __debug__}, sort_keys=True))
+
+
+if __name__ == '__main__':
+    try:
+        main()
+    except TestFailure as error:
+        raise SystemExit('FAIL_MANY_AXIS_PRIME_SUPPLY_TESTS ' + str(error))
diff --git a/research/many-axis-prime-supply/verify.py b/research/many-axis-prime-supply/verify.py
new file mode 100644
index 0000000000..abb055e5c3
--- /dev/null
+++ b/research/many-axis-prime-supply/verify.py
@@ -0,0 +1,299 @@
+#!/usr/bin/env python3
+"""Source-bound prime supply for the newer many-axis tensor caller.
+
+The finite constructor and Count adapter are HOST-INTEGER REFERENCES.
+No encoded prime producer, production tensor, native or supplier is executed.
+The uniform fixed-tape construction and cost are written in PROOF.md.
+Apache-2.0. ToikY with substantial OpenAI Codex assistance.
+"""
+import argparse
+import ast
+from contextlib import contextmanager
+from fractions import Fraction
+import hashlib
+import json
+from pathlib import Path
+from types import SimpleNamespace
+
+HERE = Path(__file__).resolve().parent
+PINS = {
+ 'PR3935-tensor_plan.py': (12079,'474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3','239caba2d2ccf2640c36d377949df3fb6a920cf0'),
+ 'PR3935-README.md': (6383,'7a7f218579ae4ff192bd4b7fdf00ba008117f6d6fbcb3a70e2d021be5bf8a209','2b665e76b4e86421bbea53b2252df8e81c91b290'),
+ 'PR4024-PROOF.md': (11035,'7b141475955cc372c5936118ff16e8748b589b93de2d26b76da28feec9b45de4','479a2b727b67b88efc8bdc64bde340a1c0d95ec3'),
+ 'PR4024-README.md': (5356,'2f179858402d1eac28b1da46139fa3198a625375532cc2c53a01c1ffc565281b','63648c961b96c6c76c305471b102e26d6b861d1b'),
+ 'source08-assembly.tex': (46444,'763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a','337810a1d9a58a2ecf14123420923c039ba322a6'),
+}
+CASES = ((8,(1,)), (12,(0,1,1)), (14,(1,0,1,1)),
+         (14,(0,1,0,1,0,1)), (14,(1,0,0,1,1,0,1)))
+ELL0, DIMENSION_POWER = 1 << 32, 334
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def unique(pairs):
+    result = {}
+    for key, value in pairs:
+        need(key not in result, 'duplicate JSON key')
+        result[key] = value
+    return result
+
+
+def typed(value):
+    if isinstance(value, dict):
+        return ('dict', tuple((k,typed(v)) for k,v in sorted(value.items())))
+    if isinstance(value, list):
+        return ('list', tuple(map(typed,value)))
+    return type(value).__name__, value
+
+
+def authenticate():
+    for name,(length,sha,blob) in PINS.items():
+        path = HERE/'source'/name
+        need(not path.is_symlink(), 'source symlink: '+name)
+        raw = path.read_bytes()
+        need(len(raw)==length and hashlib.sha256(raw).hexdigest()==sha, 'source bytes: '+name)
+        need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==blob, 'source blob: '+name)
+
+
+class Natural:
+    """Host semantic adapter for the extracted guard; no tape execution claim."""
+    live = set()
+    def __init__(self,value):
+        value = value.value if isinstance(value,Natural) else value
+        need(type(value) is int and value>=0, 'nonnegative host Count model')
+        self.value,self.alive = value,True
+        Natural.live.add(self)
+    @classmethod
+    def literal(cls,value):
+        return cls(value)
+    @classmethod
+    def product(cls,a,b):
+        need(a.alive and b.alive, 'live modeled product inputs')
+        return cls(a.value*b.value)
+    def multiply_small(self,value):
+        need(self.alive and type(value) is int and value>=0, 'modeled small multiplication')
+        self.value *= value
+    def add(self,other):
+        need(self.alive and other.alive, 'live modeled ADD')
+        self.value += other.value
+    def close(self):
+        need(self.alive, 'single modeled ownership close')
+        self.alive = False
+        Natural.live.remove(self)
+
+
+def compare(a,b):
+    need(a.alive and b.alive, 'live modeled comparison')
+    return (a.value>b.value)-(a.value<b.value)
+
+
+def subtract(a,b):
+    need(a.alive and b.alive and a.value>=b.value, 'modeled exact subtraction')
+    return Natural(a.value-b.value)
+
+
+@contextmanager
+def owned(*values):
+    try:
+        yield values
+    finally:
+        for value in values:
+            value.close()
+
+
+def source_guard():
+    """Authenticate first, then compile ONLY the complete selected AST method."""
+    authenticate()
+    source = ast.parse((HERE/'source/PR3935-tensor_plan.py').read_bytes())
+    classes = [n for n in source.body if isinstance(n,ast.ClassDef) and n.name=='TensorPlan']
+    need(len(classes)==1, 'unique source TensorPlan')
+    methods = [n for n in classes[0].body if isinstance(n,ast.FunctionDef) and n.name=='production_axis']
+    need(len(methods)==1, 'unique complete source production_axis')
+    method = methods[0]
+    need([a.arg for a in method.args.args]==['self','s','t'] and not method.decorator_list,
+         'source guard API')
+    module = ast.fix_missing_locations(ast.Module(body=[method],type_ignores=[]))
+    namespace = {'Count':Natural,'owned':owned,'subtract':subtract,'compare':compare,'need':need,
+                 '__builtins__':{}}
+    exec(compile(module,'authenticated TensorPlan.production_axis','exec'),namespace)
+    return namespace['production_axis']
+
+
+def check_source_axis(s,t,d,target_halo=16,w=2,guard=None):
+    need(all(type(x) is int and x>=0 for x in (s,t,d,target_halo,w)),
+         'typed nonnegative source guard operands')
+    need(not Natural.live, 'clean host-model entry')
+    arguments = [Natural(x) for x in (s,t,d,target_halo,w)]
+    protected = set(arguments)
+    model = SimpleNamespace(d=arguments[2],target_halo=arguments[3],w=arguments[4])
+    before = [a.value for a in arguments]
+    try:
+        (source_guard() if guard is None else guard)(model,*arguments[:2])
+        need(Natural.live==protected and before==[a.value for a in arguments], 'source guard model preservation')
+    finally:
+        for argument in arguments:
+            argument.close()
+        need(not Natural.live, 'source guard modeled scratch restoration')
+    return True
+
+
+def primality_reference(n):
+    """Bounded HOST reference: deliberately use all smaller trial divisors."""
+    need(type(n) is int and n>=2, 'candidate domain')
+    for divisor in range(2,n):
+        if n % divisor == 0:
+            return False
+    return True
+
+
+def interval(t,d):
+    need(type(t) is int and type(d) is int and t>=4 and d>=2, 'interval domain')
+    # a=t-t/(3d), b=t-t/(4d); search the exact open/closed integer interval.
+    return t-(t+3*d-1)//(3*d)+1, t-(t+4*d-1)//(4*d)
+
+
+def prime_queue(t,d,quota):
+    low,high = interval(t,d)
+    need(type(quota) is int and quota>=0, 'prime quota')
+    result = []
+    if quota:
+        for candidate in range(low,high+1):
+            if candidate>2 and primality_reference(candidate):
+                result.append(candidate)
+                if len(result)==quota:
+                    break
+    need(len(result)==quota, 'finite interval has insufficient prime supply')
+    return result
+
+
+def supplies(ell,flags,target_halo=16,w=2,guard=None):
+    """Small host reference; symbolic theorem never calls this at ELL0."""
+    need(type(ell) is int and 3<=ell<=20, 'bounded host-reference fixture width')
+    need(isinstance(flags,(list,tuple)) and flags and
+         all(type(f) is int and f in (0,1) for f in flags) and flags[-1]==1,
+         'literal target flags with final full axis')
+    need(type(target_halo) is int and type(w) is int and target_halo>=0 and w>=0,
+         'finite guard auxiliary values')
+    D,d = len(flags),len(flags)+1
+    targets = [1 << (ell-1+flag) for flag in flags]
+    queues = [prime_queue(1 << (ell-1+flag),d,flags.count(flag)) for flag in (0,1)]
+    cursors,primes = [0,0],[]
+    for flag,t in zip(flags,targets):
+        s = queues[flag][cursors[flag]]
+        cursors[flag] += 1
+        primes.append(s)
+    return validate_supplied(ell,flags,primes,target_halo,w,guard)
+
+
+def validate_supplied(ell,flags,primes,target_halo=16,w=2,guard=None):
+    """Validate an explicit reference return at the actual source interface."""
+    need(type(ell) is int and 3<=ell<=20, 'bounded explicit supply width')
+    need(isinstance(flags,(list,tuple)) and flags and
+         all(type(f) is int and f in (0,1) for f in flags) and flags[-1]==1,
+         'literal explicit target flags')
+    need(isinstance(primes,(list,tuple)) and len(primes)==len(flags), 'one supplied prime per axis')
+    need(all(type(s) is int and s>2 and s%2==1 for s in primes), 'odd supplied prime domain')
+    need(type(target_halo) is int and type(w) is int and target_halo>=0 and w>=0,
+         'explicit guard auxiliary values')
+    D,d = len(flags),len(flags)+1
+    targets = [1 << (ell-1+flag) for flag in flags]
+    guard = source_guard() if guard is None else guard
+    S,T = 1,1
+    for s,t in zip(primes,targets):
+        need(primality_reference(s), 'supplied prime primality')
+        need(Fraction(3*d-1,3*d)*t < s <= Fraction(4*d-1,4*d)*t, 'exact interior band')
+        check_source_axis(s,t,d,target_halo,w,guard)
+        S,T = S*s,T*t
+    need(len(set(primes))==D and 3*S>2*T, 'distinct primes and full volume ratio')
+    source_bits = bytes((s>>bit)&1 for s in primes for bit in range(ell))
+    flag_bits = bytes(flags[:-1])
+    return {'ell':ell,'D':D,'d':d,'flags':list(flags),'targets':targets,'primes':primes,
+            'source_bits_sha256':hashlib.sha256(source_bits).hexdigest(),
+            'flag_bits_sha256':hashlib.sha256(flag_bits).hexdigest(),
+            'source_bit_length':len(source_bits),'flag_bit_length':len(flag_bits),
+            'S':S,'T':T,'address_bits':sum(ell-1+f for f in flags),
+            'target_halo':target_halo,'w':w,'source_guard_checks':D,
+            'source_guard_adapter':'host-integer Count semantics; complete authenticated AST method',
+            'encoded_execution':False,'production_tensor_execution':False}
+
+
+def threshold_certificate():
+    """Only small integer/rational log bounds; never form 2**ELL0."""
+    z0 = 1 << 16
+    need(z0*z0==ELL0, 'threshold square')
+    # y=log(t) lies between ell/4 and ell. d<=ell^334.
+    polynomial_power = 2*DIMENSION_POWER+3
+    first_log_bound = 7+polynomial_power*16
+    first_exponential_bound = z0//4
+    need(first_log_bound<first_exponential_bound and 4*polynomial_power<z0,
+         'uniform decreasing error comparison')
+    # t >= exp(ell/4), while 24*d*D*y <=24*ell^669.
+    volume_power = 2*DIMENSION_POWER+1
+    second_log_bound = 5+volume_power*32
+    need(second_log_bound<ELL0//4 and 4*volume_power<ELL0, 'uniform volume comparison')
+    need(Fraction(8476,10000)**2>Fraction(1,2) and Fraction(92211,10000)<10,
+         'weakened analytic constants')
+    return {'ell0':ELL0,'dimension_power':DIMENSION_POWER,'z0':z0,
+            'error_log_upper':first_log_bound,'error_exponential_lower':first_exponential_bound,
+            'volume_log_upper':second_log_bound,'volume_exponential_lower':ELL0//4,
+            'FKS_reference':'arXiv:2206.12557v2 Corollary22; weaker decay coefficient0.8476',
+            'period_premise':'K=target_halo+2*w <= 2^(ell-3); separate from prime abundance',
+            'analytic_input_imported':True,'analytic_input_reproved':False,
+            'giant_power_constructed':False}
+
+
+def controls(guard):
+    count = 0
+    def reject(call):
+        nonlocal count
+        try:
+            call()
+        except ValueError:
+            count += 1
+            return
+        raise ValueError('semantic negative control escaped')
+    reject(lambda:supplies(4,(0,1,1),guard=guard))
+    reject(lambda:supplies(12,(0,True,1),guard=guard))
+    reject(lambda:supplies(12,(1,0),guard=guard))
+    reject(lambda:supplies(ELL0,(1,),guard=guard))
+    reject(lambda:check_source_axis(1023,1024,4,guard=guard))
+    reject(lambda:check_source_axis(513,1024,4,guard=guard))
+    reject(lambda:check_source_axis(953,1024,4,target_halo=512,guard=guard))
+    reject(lambda:need(primality_reference(221),'composite must not be supplied'))
+    return count
+
+
+def compute():
+    guard = source_guard()
+    return {'schema_version':1,'mode':'host-reference','encoded_execution':False,
+            'cases':[supplies(ell,flags,guard=guard) for ell,flags in CASES],
+            'threshold':threshold_certificate(),'semantic_controls':controls(guard),
+            'new_kappa':False,'full_multiplication_theorem':False}
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--write',action='store_true')
+    args = parser.parse_args()
+    if args.write:
+        need(not (HERE/'RESULT.json').exists(),'refuse existing receipt overwrite')
+    result = compute()
+    if args.write:
+        (HERE/'RESULT.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n')
+    else:
+        expected = json.loads((HERE/'RESULT.json').read_bytes(),object_pairs_hook=unique)
+        need(typed(result)==typed(expected),'complete typed receipt')
+    print('PASS_MANY_AXIS_PRIME_SUPPLY cases='+str(len(result['cases']))
+          +' host_reference_only symbolic_effective_threshold no_full_supplier_no_new_kappa')
+
+
+if __name__=='__main__':
+    try:
+        main()
+    except Exception as error:
+        import sys
+        print('FAIL_MANY_AXIS_PRIME_SUPPLY '+str(error),file=sys.stderr)
+        raise SystemExit(1)