petalas · Nov 11, 2026
diff --git a/research/rounded-image-block-minimum/PROOF.md b/research/rounded-image-block-minimum/PROOF.md
@@ -0,0 +1,143 @@
+# The sharp block count for the rounded tensor image
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written proof with exact finite corroboration.
+
+## Contract and predecessors
+
+Use the original-coordinate layout of CubeJerry's
+[PR6995](https://github.com/CrocSwap/integer-mult-bounds/pull/6995).
+For an arbitrary positive number D of axes, let
+
+\[
+ t_i=2^{\ell_i},\qquad s_i<t_i<2s_i,\qquad
+ Q_i(j)=\left\lfloor {t_i j\over s_i}+{1\over2}\right\rfloor,
+ \quad 0\le j<s_i.
+\]
+
+Axis zero is fastest. Its target stride is one, and axis i has stride
+\(\prod_{k<i}t_k\). The selected address set is
+
+\[
+ E=\left\{\sum_{i=0}^{D-1}Q_i(j_i)\prod_{k<i}t_k:
+                  0\le j_i<s_i\right\},\qquad S=\prod_i s_i.
+\]
+
+The field is the linear interval of T=prod(t_i) records beginning at
+address zero. Its seam is fixed; a cyclic change of origin is not free.
+All records have the same framed length, and unselected hole contents
+are arbitrary. An admitted block copy appends every record in one
+nonempty contiguous source interval, in increasing order. The complete
+readout copies every selected record exactly once in increasing order
+and copies no hole. It does not copy a larger interval and filter it later.
+
+The monotone rounded image, its one-or-two coordinate steps and the
+physical extractor are predecessor work. Dugongue's
+[PR5566](https://github.com/CrocSwap/integer-mult-bounds/pull/5566),
+analysis A11.1, already decomposes the scalar rounded grid into Beatty
+runs and permits a cyclic relabeling to obtain exactly t-s complete runs.
+The new result is the exact fixed-seam tensor block count, including
+which carry boundaries join, and its optimality in the contract above.
+No scalar Beatty-run novelty is claimed.
+
+## The formula
+
+Put
+
+\[
+ d_i=t_i-s_i,\qquad
+ b_i=\begin{cases}1&3s_i>2t_i,\\0&3s_i<2t_i.\end{cases}
+\]
+
+Equality cannot occur because t_i is a power of two. Empty products
+below equal one. The sharp number of block copies is
+
+\[
+ \boxed{R=\sum_{k=0}^{D-1}d_k
+           \left(\prod_{i<k}b_i\right)
+           \left(\prod_{i>k}s_i\right)
+          +\prod_{i=0}^{D-1}b_i.}                         \tag{1}
+\]
+
+Equivalently, if S_i and R_i are the selected volume and run count for
+axes i through D-1, then
+
+\[
+ S_D=R_D=1,\qquad S_i=s_iS_{i+1},\qquad
+ R_i=d_iS_{i+1}+b_iR_{i+1}.                              \tag{2}
+\]
+
+Thus D backward steps evaluate the answer without constructing T or S
+individual records. This is an arithmetic-operation count for the formula,
+not a constant-time bit-arithmetic or physical tape claim.
+
+## Proof
+
+First consider one axis and omit its subscript. The source indices
+increase by one, and 1<t/s<2, so adjacent Q values differ by one or two.
+The initial value is zero. At the last source index,
+
+\[
+ Q(s-1)=t-\left\lceil {t\over s}-{1\over2}\right\rceil.
+\]
+
+This is t-1 when 3s>2t and t-2 when 3s<2t. Therefore b is exactly the
+indicator that the scalar image reaches its last target position t-1.
+There are Q(s-1)-(s-1)=d-1+b internal gaps of size two. Every such gap
+starts a new run, so the scalar image has d+b runs.
+
+Now treat the lowest remaining axis i as the fast axis and flatten all
+higher axes into their own target field. Write S_h and R_h for the
+selected volume and run count in that higher field. Each selected
+higher address contributes one translated fast-axis image with d_i+b_i
+runs. Two successive such images join exactly when their higher
+addresses differ by one and the fast image ends at t_i-1.
+
+To see that no other join is possible, let delta be the positive
+difference of those higher addresses. The next image's first address
+minus the preceding image's last address is
+
+\[
+ t_i\,\mathit{delta}-Q_i(s_i-1).
+\]
+
+It equals one precisely when delta=1 and b_i=1. The higher image has
+S_h-R_h adjacent selected pairs. Starting with the separate translated
+images and subtracting exactly their joins therefore gives
+
+\[
+ R_i=(d_i+b_i)S_h-b_i(S_h-R_h)=d_iS_h+b_iR_h.
+\]
+
+This proves (2), with the empty higher field represented by one
+selected point and one run. Expanding the finite recurrence proves (1).
+
+Finally, a contiguous interval that copies no hole lies entirely in one
+maximal selected run. Every run contains a selected record that must be
+copied, so every admitted readout needs at least R intervals. Copying the
+R maximal runs in order attains the lower bound and preserves arbitrary
+record values. This proves sharpness for every admitted packet. The
+unbounded statement follows from this argument, not finite extrapolation.
+
+## Fixed-seam example and scope
+
+For \((t_i,s_i)=((4,3),(8,7),(8,5))\), axis zero fastest,
+the endpoint flags are (1,1,0), and (1) gives
+
+\[
+ R=1\cdot7\cdot5+1\cdot5+3=43.
+\]
+
+The image has 105 records in a 256-record target field. This is a new
+layout invariant for that packet, not a recount of predecessor operation
+totals. In particular, multiplying scalar run counts is incorrect, and
+using the scalar cyclic count silently changes the prescribed seam.
+If the fast axis already has b_0=0, (2) becomes R=d_0 S_1;
+no carry into a slower axis can merge two fast images.
+
+The theorem does not lower the cost of scanning the full input. It does
+not implement a bulk-copy tape operation, change the producer's order,
+prove that arbitrary axis permutations are free, or price native calls,
+restoration, precision, storage or compiler work. It gives no new kappa,
+supplier admission or complete multiplication theorem. All five selected
+framework assumptions remain.
diff --git a/research/rounded-image-block-minimum/README.md b/research/rounded-image-block-minimum/README.md
@@ -0,0 +1,140 @@
+# Exact block minimum for the rounded tensor image
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written proof with exact finite corroboration.
+There is no new kappa or selected-frontier change.
+
+The original-coordinate rounded tensor image has an exact, sharp
+contiguous block-copy count. This adds a layout invariant to CubeJerry's
+[PR6995](https://github.com/CrocSwap/integer-mult-bounds/pull/6995),
+whose physical extractor and reported invoices are cited predecessor work,
+not replay targets. The question here is original local side work, not an
+answer to its production-caller handoff.
+
+For integer dyadic target periods `t_i=2^ell_i` and integer source periods
+`s_i<t_i<2s_i`, define
+
+```text
+Q_i(j) = floor(t_i*j/s_i + 1/2),  0 <= j < s_i
+d_i = t_i-s_i
+b_i = 1 if 3*s_i > 2*t_i, otherwise 0
+S_D = R_D = 1
+S_i = s_i*S_(i+1)
+R_i = d_i*S_(i+1) + b_i*R_(i+1)
+```
+
+Axis zero is fastest and the linear field begins at address zero. The
+minimum number of intervals that copy exactly the selected records in
+order, copying each once and copying no hole, is `R_0`. Formula (1) in
+[PROOF.md](PROOF.md) gives its closed finite sum. Each `b_i` states whether
+the scalar image touches its right target endpoint. The proof counts all
+and only the carry boundaries at which two blocks join. Copying maximal
+selected runs attains the lower bound for arbitrary record contents.
+
+For target/source pairs `(4,3), (8,7), (8,5)` the sharp answer is
+`1*7*5 + 1*5 + 3 = 43` blocks for 105 records in a 256-record target field.
+This is a theorem about the layout and the stated interval-copy contract.
+It is not a measured speedup or a native operation count.
+
+## Evidence and reproduction
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-image-block-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rounded-image-block-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-image-block-minimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-image-block-minimum --check-source-history --check-modes
+```
+
+Another host can substitute its CPython 3.12 path. Expected direct output
+is `PASS_ROUNDED_IMAGE_BLOCK_MINIMUM` in a generated JSON receipt bound to
+the six package files and three source texts. The verifier writes nothing
+and imports no predecessor executable. The registered runner also checks
+source Git blobs, pinned historical metadata and declared live inputs.
+No receipt is hand-written or committed.
+
+The census enumerates every ordered dyadic packet with `sum(ell_i)<=10`,
+including every admissible source period for each axis. That is 4,180
+packets, 3,270,652 target records, 1,831,047 selected records and 657,556
+maximal blocks. One engine literally rounds source coordinates. A second
+scans target coordinates and tests inverse half-open integer intervals.
+Their complete ordered images agree. Both the backward recurrence and
+the finite sum equal the literal run count. Executing the run intervals
+copies exactly the selected addresses and no hole in every packet.
+
+The named 256-record fixture additionally copies distinct nonzero record
+values and preserves its source. Nine invalid packets reject. Five
+boundary controls distinguish the fixed seam from a cyclic seam, a
+trailing hole, the two axis orders of a mixed packet, and a larger
+sixteen-axis formula evaluation. The last control does not enumerate its
+large volume. The universal claim rests on the written proof.
+
+## Limits and implementation
+
+The exact count applies to interval copies with the stated seam and order.
+It does not exclude a changed producer, paid reordering, copying holes
+followed by filtering, noncontiguous native reads or a different service.
+No bulk-copy tape operation or improved scan time is supplied. Source
+delivery, movement, restoration, stock, precision, native cost and compiler
+closure still require complete invoices. No selected cold replay, Lean,
+Docker, full Gaussian transform or multiplier is run. All five selected
+framework assumptions remain. Independent human and formal proof-kernel
+review are unclaimed.
+
+The formula evaluator permits at most sixteen axes with exponents at most
+64; these executable caps do not restrict the written theorem. The literal
+oracle enforces target volume at most 1,024. Its worklist has capacity
+5,000, checks full exhaustion, and checks its packet coverage by a separate
+composition-count recurrence. All loops have finite bounds; there is no
+recursion, subprocess, network access or dynamic module loading. Functions
+fit within sixty physical lines. Explicit checks remain enabled under `-O`.
+
+Power of Ten rule 3 has a managed-runtime deviation in `verify.py`.
+Python integers and collections allocate during computation. The sixteen
+axis caps bound formula integers to at most 1,024 bits for the full volume;
+the literal engines retain one packet of at most 1,024 addresses at a time.
+The worklist retains fewer than 5,000 packets of at most five axes. Source
+and package files are capped at 128 KiB each, and the manifest at eight
+source rows. Hashing and JSON parsing use ordinary bounded Python
+allocations; allocator internals are not instrumented. Warning-strict normal
+and optimized executions plus AST/function-size inspection provide the
+available diagnostics. Fixed-capacity storage would be a separate native
+implementation if a real caller uses this formula.
+
+## Open next questions
+
+- What is the minimum over axis permutations that a real producer can
+  legally deliver? Start with an adjacent-axis exchange inequality from
+  recurrence (2), then price the complete physical permutation. The legal
+  producer layout and its movement cost are blockers.
+- Can a native extractor exploit maximal blocks with a complete setup,
+  movement, copy and restoration invoice? Start with one literal producer
+  packet and an encoded block iterator. A bulk-copy service, source delivery
+  and ownership/precision/storage accounting remain blockers.
+
+The structured questions are in [TASK.json](TASK.json). Neither is reserved.
+
+## Sources and coordination
+
+Base main is `e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8,
+selected #7000. The cheap source-binding orientation passed. The
+complex-new-helper-inventory card is explicitly changed to this local
+layout side result; no helper supplier or selected assumption is completed.
+[SOURCES.json](SOURCES.json) pins the exact predecessor texts, task card
+and selected record. Frozen files and predecessor credit are unchanged.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541691)
+followed live open/account PR, active Discussion, main and merged
+general-form searches and local reservation checks. Those checks found
+the credited scalar Beatty result, not the tensor carry formula. Their
+coverage does not include every unpublished result or arbitrary unseen
+diff. No global literature-priority claim is made.
+
+Credit CubeJerry for #6995 and its original-q extraction boundary;
+Dugongue / David Ganz for #5566's scalar Beatty runs and fixed-seam warning;
+the canonical Gaussian and #3851 selection authors, the retained
+Tape/Count contributors, and the normalized-recovery predecessor for the
+inherited image and carrier. Elementary interval counting and tensor
+flattening are classical methods. Only the fixed-seam tensor count and
+its stated block-readout consequence are claimed as the new step.
diff --git a/research/rounded-image-block-minimum/SOURCES.json b/research/rounded-image-block-minimum/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/beatty-run-gaussian-inverse/analysis.md",
+      "usage": "input",
+      "git_blob": "e5cc397cd0baacd686cb8a075d636b9e595bdfae",
+      "sha256": "5c015de52b1867b07296c666bbe917c89ce508f6ca45dec909aceea0518b111a"
+    },
+    {
+      "path": "research/original-q-field-extraction/PROOF.md",
+      "usage": "input",
+      "git_blob": "fc340cc0ef832b4f75daf1ca8d04db60328e3654",
+      "sha256": "88343373c2dc09d0dd3f86b14ab8cd48834305e2cd36b9a91c57a831db1c0fd2"
+    },
+    {
+      "path": "research/original-q-field-extraction/README.md",
+      "usage": "input",
+      "git_blob": "80d7910c1521abc4169e982c5ae5f62565dec00e",
+      "sha256": "c86faeef49046baefeaaa1ff2ed72ffa0a6b56554092dda520139ff7f0e2200d"
+    }
+  ]
+}