Mister-Meeseeks · Oct 24, 2026 · Oct 24, 2026 · Oct 24, 2026
diff --git a/research/native-coupled-inverse/ORIGINS.json b/research/native-coupled-inverse/ORIGINS.json
@@ -0,0 +1,56 @@
+{
+  "head": "3348fccea855082786d5f0fc5558b73d4974e745",
+  "repository": "CrocSwap/integer-mult-bounds",
+  "pr": 5402,
+  "archive_sha256": "530fe35e8e8abdcf9c6207168c7e8586c56b2fbe491c6c67046bea83343809cc",
+  "files": [
+    {
+      "file": "verify.py",
+      "path": "research/native-rank8-helper-provider/verify.py",
+      "git_blob": "b62af49c87864ad9337f3964b2515ba53de85d4f",
+      "sha256": "121d87787c0f76bd530b6e1682704a311e96dfb33d787bea2ba29a1d0e5ee23e"
+    },
+    {
+      "file": "README.md",
+      "path": "research/native-rank8-helper-provider/README.md",
+      "git_blob": "92d0d7e523dbf90c67b7244de4c87cc74c0d3b61",
+      "sha256": "0d86590c471a498f3b735397d42bbaf4d5e89c33b75ddbd48dbf972192ab351f"
+    },
+    {
+      "file": "PROOF.md",
+      "path": "research/native-rank8-helper-provider/PROOF.md",
+      "git_blob": "5cbfc4fd02dce926c3d235f1549bdb2035dea088",
+      "sha256": "2d59282f3b5e9fb848d0099ce91729fa433162e6975f877a441e2ab4f57a29c5"
+    },
+    {
+      "file": "ATTRIBUTION.md",
+      "path": "research/native-rank8-helper-provider/ATTRIBUTION.md",
+      "git_blob": "efe3acb566448caeb4a340235bb50234808ff728",
+      "sha256": "29756f86ebad2a957d8073bea173306f00e7d957828a5bab9f7832faf5815543"
+    },
+    {
+      "file": "SOURCES.json",
+      "path": "research/native-rank8-helper-provider/SOURCES.json",
+      "git_blob": "dd77397ca519f0c15799b4f90a489af3d6a2cb0f",
+      "sha256": "f16756004bd3100e4993b250181c4c8d15c31b0a1478b627091dd900e1103888"
+    },
+    {
+      "file": "WITNESS.json",
+      "path": "research/native-rank8-helper-provider/WITNESS.json",
+      "git_blob": "19665f9eac2238d709758e0296eb6016e71b2b1a",
+      "sha256": "24599011da06325e1012619b2b84a4dd3aceb90ab42d3caaf6414879e7d16591"
+    },
+    {
+      "file": "PROVIDER.json",
+      "path": "research/native-rank8-helper-provider/PROVIDER.json",
+      "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455",
+      "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65"
+    },
+    {
+      "file": "WORD.json.gz",
+      "path": "research/native-rank8-helper-provider/WORD.json.gz",
+      "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e",
+      "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc"
+    }
+  ]
+}
diff --git a/research/native-coupled-inverse/PROOF.md b/research/native-coupled-inverse/PROOF.md
@@ -0,0 +1,165 @@
+# A native inverse with the same paid Gaussian profile
+
+This construction inverts the coupled provider from
+[PR #5402](https://github.com/CrocSwap/integer-mult-bounds/pull/5402), at
+`3348fccea855082786d5f0fc5558b73d4974e745`. It preserves all 632 original
+input directions. Nine temporary fields can start with arbitrary values and
+finish zero. No new Gaussian child is needed. The inverse needs additional
+ordinary operations, which are counted below.
+
+This is an enabling construction. It gives no new kappa, complete caller,
+autonomous credit for the eight coupled outputs, or selected-result change.
+The physical source implementation and its interpretation at every positive
+fiber width remain inherited premises. The source replay is run again.
+
+## Exact physical map
+
+Use the source notation. Q is the central Gaussian, D is the product on the
+eight other axes, and R = DQ. W and Z are the specified ordinary maps between
+112 main fields and eight mode fields. They satisfy ZW = 14I, WZ = I - C,
+RW = WR, and RZ = ZR, with the appropriate domain on each side. Do not commute
+W or Z through D or Q separately.
+
+The source map is
+
+```text
+X = D x - R y + R W h
+Y = D y
+H = D(h - Z y).
+```
+
+Its inverse is
+
+```text
+y = D^-1 Y
+h = D^-1 H + Z D^-1 Y
+x = D^-1 X + Q C D^-1 Y - Q W D^-1 H.
+```
+
+The first two equations give y and h. Substitution in the X equation gives
+the third equation, since C = I - WZ. This derivation retains operator order.
+It proves the map is invertible; it does not alone give a native schedule.
+The schedule below supplies that missing implementation. The other 400 fields
+undergo the inverses of their original autonomous helper maps.
+
+## Remove the unused center accumulator
+
+The changed source word has no paid operation on C0. Its live center uses have
+this form, in the same chart:
+
+```text
+CLEAR C0
+COPY C0, Ck
+ADD Lr, C0, -1
+CLEAR C0
+```
+
+Replace the live ADD by `ADD Lr, Ck, -1`. Delete all scalar writes to C0.
+Before each replaced center, the old accumulation in C0 is erased without a
+read. In total, 176 ADDs, eight COPYs and 24 CLEARs are removed. The eight
+source sites and their cache fields are in RESULT.json. One entry CLEAR keeps
+the unused C0 field zero under the retained nine-field temporary interface.
+
+The source interpreter checks every endpoint row, every persistent/cache
+exit chart, and every paid call before and after this change. The final chart
+of the unused zero C0 field is immaterial; no original field is excluded.
+
+The remaining word consists of invertible ADDs, nonzero SCALEs, native maps,
+paid children, eight initial cache CLEAR/COPY pairs, and eight retags of
+identically zero persistent fields. Each retained cache is read but not
+changed until the final whole-field swap.
+
+## Reverse the complete word
+
+Reverse the physical output boundary first. Clear the nine temporary fields.
+Undo each final whole-field swap, including its chart. Apply the inverse cache
+normalizer and its inverse scalar. The original persistent mode field is now
+zero, while the cache contains the corresponding independent output input.
+Apply the inverse output helper basis, then run the reduced native word in
+reverse order:
+
+- Negate an ADD coefficient and invert a nonzero SCALE coefficient.
+- Invert a native map and reverse its chart transition.
+- Invert a paid child and reverse its chart transition. Keep its rank.
+- Reverse a zero retag only after its row is proved zero.
+- Replace a cache COPY by subtraction of its restored source field.
+- At an initial cache CLEAR, verify that its row is zero and do no operation.
+
+Finally invert the input helper basis and the physical input boundaries.
+All eight inverse COPY operations return their cache rows to zero. Clear
+the eight owned cache returns after this check. C0 stays zero. The verifier starts with 641 distinct formal input columns, erases only
+owned entry dirt, and checks both compositions against the identity on the
+632 original columns. It also checks the inverse endpoint against a separate
+closed formula in the source scalar coordinates:
+
+```text
+y = Y
+h = H + M^T Y
+x = X + (I - M M^T/4) Y - M H/4.
+```
+
+Here M has 112 rows and eight columns. The source file stores its transpose.
+The physical boundary maps convert this formula to the ordered physical
+inverse above. All 464 boundary adjoints are checked with both signed
+Clifford tableaux and absolute phase. Source adapter and phase annotations
+retain their physical interpretation in reverse order; they are not new
+scalar row operations. Internal native maps use their actual inverses.
+
+For a positive rank-r Gaussian child G, `G^-1 = X G`, where X translates the
+r active bits. Thus a descending child needs one rank-r positive call and at
+most one additional ordinary translation. The verifier checks the exact phase
+identity for ranks 1 through 9. Tensoring this identity gives the same result
+at every positive fiber width. Scalar coefficients in the owner program are
+applied once; the program does not tensor a sum over owners.
+
+Every other operation is reversed literally. The free-group row proof holds
+for each evaluation of the native maps by invertible operators. This proves
+the all-width inverse within the inherited native implementation model.
+No formal proof kernel or independent human review is claimed.
+
+## Complete local bill and limits
+
+Both directions use the paid profile
+`{1:2193, 2:412, 3:510, 4:127, 5:40}`: 3,282 child calls and rank mass 5,255.
+The 400 autonomous helper jobs retain inverse Gaussian ranks
+`{4:28, 7:7, 8:47, 9:318}`. The remaining eight fields are coupled; they get
+no autonomous target credit.
+
+| Explicit operation | Reduced forward | Inverse |
+|---|---:|---:|
+| ADD | 17,741 | 17,749 |
+| SCALE | 1,204 | 1,204 |
+| COPY | 8 | 0 |
+| CLEAR | 17 | 17 |
+| Whole-field SWAP | 8 | 8 |
+| Physical boundary monomial maps | 464 | 464 |
+| Additional child-inverse translations | 0 | at most 3,282 |
+
+The CLEAR count includes eight terminal owned clears in each direction.
+They act on certified zeros in the exact model.
+
+The native word's 240 internal warp records remain. Its 448 adapter and ten
+phase annotations retain their source semantics. RESULT.json records their
+full census. The table does not turn these inherited operations into zero
+work and does not give a complete machine/compiler tariff.
+
+A direct product of scalar operator-norm bounds gives an inverse suffix bound
+of `2^18812`. Gaussian and monomial maps have norm one. A local schedule with
+m errors of norm at most epsilon therefore has output error at most
+`m * 2^18812 * epsilon`. This is a conservative fixed-template bound.
+The complete caller, recursive error allocation, movement, storage, compiler,
+BIT supplier and outer recovery still need explicit funding. In particular,
+unchanged Gaussian counts do not imply unchanged ordinary/compiler costs.
+
+## Verification and next use
+
+The registered verifier runs the frozen predecessor replay, reconstructs the
+changed word, checks both all-column compositions and the separate inverse
+formula, and checks owned cleanup, charts, exact paid counts, boundary phases
+and inverse child phases. Mutations of inverse COPY sign, reverse zero-retag
+input and boundary phase must fail.
+
+The next use is one chronological caller that retains useful progress in the
+eight mode fields. Its full invoice must include every helper transfer and
+all additional queries. A local inverse, a favorable cost estimate or a
+finite failed control search does not establish that caller.
diff --git a/research/native-coupled-inverse/README.md b/research/native-coupled-inverse/README.md
@@ -0,0 +1,79 @@
+# Invert the eight-mode coupled native provider
+
+This package gives an exact native inverse of
+[PR #5402](https://github.com/CrocSwap/integer-mult-bounds/pull/5402) at
+`3348fccea855082786d5f0fc5558b73d4974e745`. All 632 original input directions
+are retained and all nine owned fields return zero. The inverse uses the same
+paid profile: `{1:2193,2:412,3:510,4:127,5:40}`. It adds no Gaussian child.
+
+The construction removes the unused C0 accumulator, reverses the remaining
+native operations, and uncomputes the eight retained copies by subtraction.
+The complete physical boundary is reversed with its exact phase. Positive
+Gaussian implementations of the inverse children need at most 3,282 additional
+ordinary bit translations. These operations are explicit costs.
+
+**This does not increase kappa.** The eight mode outputs remain coupled.
+A profitable complete caller, full compiler/precision bill and outer admission
+remain open. Reversing a source operation also reverses its D factor; it does
+not supply an independent fresh-D call by itself. The selected frontier is
+unchanged.
+
+[PROOF.md](PROOF.md) gives the ordered physical inverse, all-width argument,
+chronological schedule and local bill. [RESULT.json](RESULT.json) records the
+exact replay receipt. The verifier runs the pinned predecessor replay, checks
+both compositions on all original columns, checks a separate inverse formula,
+and rejects changes to COPY sign, zero-retag input and boundary phase.
+It checks 464 boundary adjoints and the phase-correct inverse-child identity
+for ranks 1 through 9. No independent human or formal-kernel review is claimed.
+
+## Reproduce
+
+Python 3.12 and its standard library suffice for mathematical replay.
+The optional source-history preflight also needs full Git history. From the
+repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/native-coupled-inverse
+python3.12 -I -O -B research/native-coupled-inverse/verify.py
+python3.12 -B scripts/check_research_commit.py --package research/native-coupled-inverse --check-source-history
+```
+
+Expected final token: `PASS_SAME_PAID_NATIVE_TWO_SIDED_INVERSE`.
+The default verifier is read-only. `--emit` writes RESULT.json for authors.
+[VALIDATION.md](VALIDATION.md) records executed checks and unrun obligations.
+
+## Sources and credit
+
+Dillon supplies the coupled provider, its all-input basis and physical boundary
+in [PR #5402](https://github.com/CrocSwap/integer-mult-bounds/pull/5402).
+The [source proof](https://github.com/CrocSwap/integer-mult-bounds/blob/3348fccea855082786d5f0fc5558b73d4974e745/research/native-rank8-helper-provider/PROOF.md)
+and [attribution](https://github.com/CrocSwap/integer-mult-bounds/blob/3348fccea855082786d5f0fc5558b73d4974e745/research/native-rank8-helper-provider/ATTRIBUTION.md)
+remain part of the review. SOURCE.zip contains the exact source files needed
+to replay that pending construction without a network or an unmerged Git
+object. ORIGINS.json records their source paths, Git blobs and byte hashes.
+The archive retains the original README, proof and attribution. It is unpacked
+only to a private temporary directory. No predecessor code is changed.
+
+Ali Romman's [PR #5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383)
+supplies the eight cached-center identities consumed by that provider.
+Cao Yifan supplies the actual native word, Dugongue supplies the center-free
+code, and Cinna Davis supplies the retained-cache/helper/controller lineage.
+Retain zxv's native and Clifford work, Jacob Alan Sussman's mixed-target
+recursion, Ryanson Jonathan's controller checks and the full source notices.
+Yiyang's [PR #4966](https://github.com/CrocSwap/integer-mult-bounds/pull/4966)
+already constructs owned-center inverses for the original word by recomputation.
+This result uses the new retained-cache interface and its eight zero outputs;
+it does not claim the first native inverse or the general idea of uncomputation.
+
+Canonical base: `1ec1119972c9aefe42525172d07b332fcff81cb4`, priority revision 7.
+The [caller claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19156336)
+takes Dillon's released handoff. The broader breakthrough goal is not complete.
+New inverse construction, proof and checks prepared for Ali Romman with
+substantial OpenAI Codex assistance. No subagents. Apache-2.0.
+
+## Open next questions
+
+Use the exact inverse to close one chronological caller that preserves useful
+progress in the eight mode fields. First give every original endpoint and the
+full paid/ordinary invoice. Only then run compiler, precision and outer
+admission. [TASK.json](TASK.json) records this question and its open obligations.