Save eight further ADDs in the translated Gaussian reader (no κ)

research/translated-reader-step/PROOF.md

@@ -0,0 +1,124 @@
+# The further rational reader shear
+
+This scoped proof and construction were produced by Nick Petalas. Apache-2.0.
+
+## Inputs and new operation
+
+Work over the commutative ring R = Q[C2^9], with tau_g tau_h = tau_(g xor h).
+Use the actual rank-30 factorization supplied by Ali Romman's PR5646, after
+Nick Petalas's PR6677 translated basis. Write J for its 112 by 30 scatter and
+L for its 30 by 112 gather. The cited input contract gives LJ = 0 and the
+reader response JL. These premises and the native source application are not
+audit claims of this package. Source manifests pin their exact input bytes.
+
+Indices are zero based. Let
+
+```text
+A = I_30 - (1/5) E_(0,1),       A^-1 = I_30 + (1/5) E_(0,1).
+```
+
+Since E_(0,1)^2 = 0, these are inverses over R. Define L' = AL and
+J' = JA^-1. This changes exactly the gather row and scatter column
+
+```text
+L'_0 = L_0 - (1/5)L_1,         J'_1 = J_1 + (1/5)J_0.
+```
+
+Every other row or column is unchanged. Thus
+
+```text
+J'L' = J A^-1 A L = JL,
+L'J' = A L J A^-1 = 0.
+```
+
+This proves the exact operator identity in the group algebra. It remains true
+under every representation by nine commuting involutions, in particular the
+supplied positive-column tensor representations. The basis is absorbed into
+the factors; no additional runtime A or A^-1 pass is presumed free.
+
+## Complete dirty-bank endpoint
+
+For arbitrary data x0 and arbitrary dirty bank z0, run the four shears
+
+```text
+z += L'x
+x += J'z
+z -= L'x
+x -= J'z
+```
+
+After the first two, z1 = z0 + L'x0 and
+x1 = x0 + J'z0 + J'L'x0. The third gives
+
+```text
+z2 = z0 + L'x0 - L'(x0 + J'z0 + J'L'x0) = z0,
+```
+
+because L'J' = 0. The last gives x2 = x1 - J'z0 = (I+JL)x0.
+Every dirty value is restored, and the data response is identical to the cited
+input word. This argument assumes no clean scratch, discarded bank, fresh
+centre, or free COPY/CLEAR operation. It concerns this recoder; it does not
+remove the native section's separately required bank or implementation costs.
+
+## Exact enumerated invoice
+
+The finite factor construction gives the following complete counts.
+
+| Quantity | Cited translated input | New factors |
+|---|---:|---:|
+| Scatter coefficients | 220 | 228 |
+| Gather coefficients | 9,940 | 9,928 |
+| Four-shear coefficient ADDs | 20,320 | 20,312 |
+| Nonidentity translation applications | 20,320 | 20,312 |
+| Axis-translation units | 91,924 | 91,852 |
+| Common denominator | 960 | 4,800 |
+| Maximum absolute coefficient | 9/8 | 9/8 |
+| Scatter absolute row-sum bound | 43/16 | 43/16 |
+| Gather absolute row-sum bound | 72 | 72 |
+
+The new gather row has twelve fewer terms. The new scatter column has eight
+more. Each factor appears twice, so the net saving is 2(12-8) = 8 ADDs.
+Every group element is charged for each coefficient occurrence. Pricing
+its direct axis decomposition by popcount(g), the complete translation-weight
+histograms for weights zero through nine are
+
+```text
+input: [0, 852, 0, 7048, 0, 8776, 0, 3374, 0, 270]
+new:   [0, 844, 0, 7076, 0, 8752, 0, 3370, 0, 270].
+```
+
+Their weighted sums differ by 72 units. A backend restoring the source layout
+after every coefficient ADD would use two route passes, with invoices 183,848
+and 183,704. These are declared logical routing units, not physical tape time.
+Coefficient multiplication and address access are not priced as free.
+
+At denominator 4,800 the largest absolute numerator is 5,400. No new odd prime
+appears, but the common denominator has one more factor of five. The same
+factor-norm bounds give the conservative prefix/suffix bound
+
+```text
+B = ((1+72)(1+43/16))^2 = (4307/16)^2.
+```
+
+A gather or partial coefficient pass has stacked infinity norm at most 73;
+a scatter or partial pass at most 59/16. Every prefix and suffix of the
+four-shear word, or its signed inverse, contains at most two of each.
+This bounds the exact logical maps uniformly in payload volume. It does not
+price rational arithmetic interiors or rounded precision.
+
+## What the certificate establishes
+
+The verifier reconstructs the cited factors only to apply this new step.
+It compares the entire two-mode product J0 L0 + J1 L1 before and after,
+with all 14,320 nonzero baseline coefficients and any possible new positions,
+checks the inverse operation and every untouched vector, and enumerates all
+metrics above. A separate literal four-shear executor checks one dense payload
+and a nonzero dirty bank on all 512 addresses. Eight rejecting controls detect
+specific algebraic and input faults. No predecessor scientific suite is run.
+
+The input identities are cited premises; the elementary basis identity and
+the arbitrary-input endpoint above prove the new universal implication.
+Finite execution corroborates the concrete factor expansion and instruction
+ordering. The contribution is one new explicit factor pair, with no claim to
+an optimum, new kappa, physical supplier, admission or complete multiplication
+theorem. A complete arithmetic and physical caller remains unproved.

research/translated-reader-step/README.md

@@ -0,0 +1,120 @@
+# Eight fewer ADDs in the translated Gaussian reader
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: finite explicit factor construction with a scoped algebraic proof.
+After the translated reader basis of [PR6677](https://github.com/CrocSwap/integer-mult-bounds/pull/6677),
+one new rational shear, in zero-based mode indices,
+
+```text
+L0 -= (1/5) L1,          J1 += (1/5) J0,
+```
+
+reduces the complete four-shear bill from 20,320 to **20,312 coefficient
+ADDs**. Every factor translation is charged. The axis-by-axis translation
+invoice falls from 91,924 to 91,852 units. Thirty arbitrary dirty borrowed
+fields are still exactly restored. The maximum absolute coefficient and
+factor norm bounds stay at 9/8, 43/16 and 72.
+
+The common coefficient denominator rises from 960 to **4,800**. The saving
+is in coefficient instructions and the declared translation invoice; a
+complete physical or arithmetic saving is unproved. No new kappa, productive
+helper credit, admitted supplier or selected-frontier change is claimed.
+
+The question is Ali Romman's [PR5646](https://github.com/CrocSwap/integer-mult-bounds/pull/5646)
+broader-basis question. The new step is this further rational shear after
+PR6677, not a replay or audit of its construction. [PROOF.md](PROOF.md)
+gives the factor identity and the arbitrary-input dirty-bank argument.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/translated-reader-step/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/translated-reader-step/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/translated-reader-step
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/translated-reader-step --check-source-history
+```
+
+Another CPython 3.12 executable can replace the local interpreter. The direct
+checker prints `PASS_TRANSLATED_READER_STEP` in a generated JSON receipt
+bound to all package files. It writes nothing. The registered runner prints
+`PASS_REGISTERED_RESEARCH_PACKAGE`; the publication check prints
+`PASS_RESEARCH_COMMIT_BYTES`.
+
+The new checks compare the entire changed-pair product in Q[C2^9], including
+all 14,320 nonzero baseline coefficients and any possible new positions.
+They check the inverse basis, every untouched factor vector, all coefficient,
+translation, denominator and magnitude metrics, and one literal dense
+512-address four-shear execution. That execution compares all 57,344 data
+coordinates and restores all 15,360 dirty-bank coordinates. Eight controls
+reject omitted factor updates, a wrong sign or translation, invalid shifts,
+inexact coefficients and a missing mode. The written proof supplies the
+universal input and representation quantifiers; the payload is corroboration.
+
+## Scope and credit
+
+Canonical base is `e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8,
+selected #7000. The `complex-new-helper-inventory` card changes scope to an
+ordinary reader-interface side result. Its new productive-helper and complete
+physical-invoice gates are unmet. All five selected assumptions remain.
+[TASK.json](TASK.json) records the exact card and changed scope.
+
+Ali Romman / PR5646 supplies the actual factors, constant dyadic basis and
+broader-basis question. Nick Petalas / PR6677 supplies the translated input
+basis and the reconstruction and word code adapted here; PR5919 supplies
+the earlier rational escape and factor-reconstruction lineage. David Ganz /
+Dugongue / PR5634 supplies the reader substitution and four-shear identity;
+Ali Romman / PR5640 supplies the borrowed-space contract. Centre-code-services,
+reciprocal-native-responses, native-centre-capture, centre-metric-encoders,
+PR3133, PR3148, PR2588, PR2226 and their individual native, numerical and
+compiler contributors retain their attribution. Their files and credit lines
+are unchanged. The source identities and null-product premise are cited inputs,
+not new verification claims. Independent human and formal proof-kernel review
+are unclaimed.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539321)
+followed live PR/account lists, recent handoffs, active Discussions, reservation
+checks and main/merged searches for the actual Gaussian reader and general
+translated bases. The cached local note search covers 194 of 10,178 HEAD
+records; explicit main-tree searches supplement that sparse inventory.
+Unpublished work and arbitrary historical diffs remain outside coverage.
+Discovery stopped at the first verified new step. No local or global optimum
+is asserted.
+
+## Open next questions
+
+- Does the eight-ADD saving survive a complete rational arithmetic and physical
+  routing bill? Start with both factor pairs in the same priced kernel,
+  charging multiplication, rounding, source-layout return, storage and returned
+  ownership. The full caller and arithmetic backend are missing.
+- Can a further basis improve a fixed complete physical objective? Define that
+  objective before another cancellation search. This witness supplies no optimum;
+  physical prices and a consumer contract remain the blockers.
+
+Structured relevance, first steps and blockers are in TASK.json.
+
+## Implementation bounds and limits
+
+The fixed reconstruction uses 112 ports, 30 modes and 512 addresses, ten supplied
+constant basis operations, one cited translated operation and one new rational
+operation. Kernel vectors contain at most 57,344 entries; decoded source files
+have a 16 MiB bound. Literal states contain at most 142 arrays of 512 entries,
+with one exact integer scale per shear. Functions stay below sixty physical
+lines. New code uses no recursion, network, subprocess, dynamic evaluation or
+mutable shared research state. Explicit exception checks remain active under
+optimization. Warning-strict normal/optimized execution and AST compilation
+supply the available diagnostics; no separate type/lint analyzer is claimed.
+
+Power of Ten rule 3 has a managed-runtime deviation. Python allocates integers,
+Fractions, lists and dictionaries dynamically. Fixed source bytes, dimensions,
+operations and fixture counts bound the mathematical data, but no fixed pool
+or byte-exact heap bound is claimed. A future variable-size arithmetic backend
+must provide its own capacity and cleanup contract.
+
+Native source correctness, the section's own thirty-field bank, arithmetic
+interiors, tape movement, whole-caller precision, stock, owned erasure, uniform
+compilation and outer use remain separate obligations. Selected cold replay,
+predecessor scientific suites, Lean, Docker and a materialized rounded multiplier
+are unrun. This package proves no complete multiplication theorem.

research/translated-reader-step/SOURCES.json

@@ -0,0 +1,78 @@
+{
+  "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/actual-gaussian-reader-tariff/BASIS.json",
+      "usage": "input",
+      "git_blob": "31923652cded9b0a131b84535536c43c83a01a66",
+      "sha256": "b21900ee6c5de7c7e5e77e99254f960c35a5f10a55972e27bad68ea9961278e5"
+    },
+    {
+      "path": "research/actual-gaussian-reader-tariff/README.md",
+      "usage": "provenance",
+      "git_blob": "e5d49d12040e9f9079d73e6e5c93683e86f88db0",
+      "sha256": "32dc7b3e3262842eae8d18b800bf19d81890d163874e1db95de7f0375a238dd8"
+    },
+    {
+      "path": "research/actual-gaussian-reader-tariff/inputs/reader.md",
+      "usage": "provenance",
+      "git_blob": "3be2e5ecd836a3b9501be914d131f1ca580bd716",
+      "sha256": "028568bdcd33cf7daf7e9a754b5c686854d0825ca6a41d3c7362b13a9962b751"
+    },
+    {
+      "path": "research/actual-gaussian-reader-tariff/inputs/tariff.md",
+      "usage": "provenance",
+      "git_blob": "df12205db8e6a49f0d7a7e08887a987391598e9e",
+      "sha256": "d84745ac51a83fbe56f3a3e88e63884cb2f97018f3ee374e7c520982789bd516"
+    },
+    {
+      "path": "research/centre-code-services/frozen/lanes/history-encoding/independent-skeleton-20261018/fresh-three-child/FRESH-THREE-CHILD-PROGRAMS.json.gz",
+      "usage": "input",
+      "git_blob": "f552c66d6124c1fd84eacf4003638c82363bee81",
+      "sha256": "afc3aad86eb9b6da3027d3ac57eac1a2a766729dca0608e70e36d0554c8afc96"
+    },
+    {
+      "path": "research/centre-code-services/frozen/lanes/new-core-transfer-20261017/low-displacement-20261020/run-normal/RESPONSE-PROGRAM.json",
+      "usage": "input",
+      "git_blob": "bcf3dd1d992257c2f933e6c1a0a3c3a27238f904",
+      "sha256": "5832788135e16c2427f8c746f251501621684a02ef88b0a14322056653dc2d7c"
+    },
+    {
+      "path": "research/centre-code-services/frozen/root/RANK30-PHASE-SECTION-BLOCKS-20261020.json.gz",
+      "usage": "input",
+      "git_blob": "3695574aa24d06fd2d3b3a8ea923bfc3c3d0201a",
+      "sha256": "742c2a1907c61be01aa9a2f80df095ad21ad9608a43b38f7fb2ef7ee7ef6d994"
+    },
+    {
+      "path": "research/translated-reader-basis/README.md",
+      "usage": "provenance",
+      "git_blob": "59a40f25ff94eda8921f3048d33f70c91a2bcb6c",
+      "sha256": "070d89d13143b5172cf4b4d814924d0ed2d8cdbd4c498e51f118c2dcf31e59aa"
+    },
+    {
+      "path": "research/translated-reader-basis/kernels.py",
+      "usage": "provenance",
+      "git_blob": "9285ab65dc4503e9fe354efec84ca70ad7037b03",
+      "sha256": "e58ecfeface4b366640401c7a59dee3df4308e03bebefc755ca829880ffd1f75"
+    },
+    {
+      "path": "research/translated-reader-basis/word.py",
+      "usage": "provenance",
+      "git_blob": "bc29344f47fdf9ef0aff4c5c322bd2f4cc571f95",
+      "sha256": "1b61850677ad55784fde8200de00f82d5545042c3659d5574e7fafb623a19657"
+    }
+  ]
+}