test(research): independently audit the six restore skips

research/rank7-restore-substitution-audit/.gitattributes

@@ -0,0 +1,2 @@
+# Preserve exact predecessor bytes bound by VENDOR.json.
+vendor/** -text

research/rank7-restore-substitution-audit/ENGINEERING.md

@@ -0,0 +1,80 @@
+# Verification and engineering limits
+
+## Scope and principles
+
+Build the Lever led to a standalone deterministic checker instead of manual
+matrix arithmetic. Prove It Works led to literal preimage reconstruction,
+separate dirty-column and frame checks, semantic mutants and publication-byte
+comparison. No predecessor Python module is imported or executed.
+
+The audited object is the exact PR3042 head in VENDOR.json. Its original notices
+are retained. The checker does not modify that package, shared tooling, frozen
+inputs or the selected result. The maintained code is frames.py, verify.py and
+test_verify.py in this package only.
+
+## Power of Ten review
+
+1. All proof control flow is structured and nonrecursive. Failure propagates as
+   an exception before the final JSON is printed. Only the byte-mutation test
+   acquires a temporary directory, owned by a context manager on every exit.
+2. Source inventories have at most 32 entries; a scalar operator has at most
+   1,000 gates on at most 704 rows. Frame lists have at most nine generators,
+   each section at most 20,000 gates, and B has at most 704 warps. Cleanup has
+   at most 60,000 forward events. Source bytes are hash-checked before decoding;
+   compressed/JSON input is at most 3 MB and decoded input at most 8 MB. Other
+   loops traverse these pinned bounded arrays, two edits, two providers, 704
+   registers or fixed 512-vector subspaces. Registered commands have 120-second
+   timeouts each. Input-shape failures propagate rather than retrying.
+3. Deviation. CPython, Fraction and immutable JSON containers allocate during
+   execution; static allocation would require another implementation/runtime.
+   Scope is this bounded offline audit, not a service. The cache holds at most
+   4,096 subspaces, each containing at most 512 vectors. Sparse matrices contain
+   at most 704 squared rational entries and only the pinned dyadic coefficients
+   are used in the accepted artifact. No process concurrency is used. A future
+   unpinned-input service would need explicit coefficient-growth and allocator
+   limits before reusing this implementation.
+4. Functions remain below the repository-independent 60-line review limit.
+   check_variant is near that limit and owns one cohesive variant obligation.
+5. Proof checks use ordinary require calls and survive Python optimization.
+   They cover source pins, literal equality, arbitrary dirty rows, monotone
+   frames, derived cleanup, widths, actual skipped registers and complete cost.
+6. Mutable rows and frame histories are local to a single calculation. The
+   only cache is the bounded pure span function. Tests temporarily patch the
+   package path only inside a context manager to test real byte corruption.
+7. Every proof return contributes to the receipt or an equality check. Invalid
+   gate kinds, zero denominators, dirty-state differences, illegal frames and
+   stale bookkeeping fail. Test temporary writes and copies propagate errors.
+8. There is no exec, evaluation, generated code or production registration.
+   Deviation. Standard unittest discovery and mocking use runtime dispatch;
+   scope is the fixed test class and the one context-managed path substitution.
+   Thirteen named behavioral groups exercise that bounded mapping.
+9. Proof calls target ordinary functions directly. Dictionaries contain scalar
+   rows or explicit histories rather than chains of callbacks. The test-only
+   unittest dispatch deviation in rule 8 applies here as well. No pointer or
+   unsafe memory operations are used.
+10. The verification run uses warnings-as-errors, normal and optimized receipt
+    equality, source compilation and Ruff's E/F/B/UP/C4/SIM/PIE/PGH/RUF checks
+    with a 100-column line limit. The registered replay runs the proof and all
+    behavioral controls. Lint is a documented local check, not a new shared CI
+    dependency.
+
+## Commands
+
+From the repository root, with RUN a fresh session-owned external directory:
+
+```sh
+python3.12 -W error -B research/rank7-restore-substitution-audit/verify.py > "$RUN/result.json"
+python3.12 -W error -O -B research/rank7-restore-substitution-audit/verify.py > "$RUN/optimized.json"
+cmp "$RUN/result.json" "$RUN/optimized.json"
+TMPDIR="$RUN" python3.12 -W error -B research/rank7-restore-substitution-audit/test_verify.py
+ruff check --no-cache --config line-length=100 \
+  --select E,F,B,UP,C4,SIM,PIE,PGH,RUF research/rank7-restore-substitution-audit/*.py
+python3.12 -B scripts/research_package.py --package research/rank7-restore-substitution-audit
+python3.12 -B scripts/check_research_commit.py --package research/rank7-restore-substitution-audit
+```
+
+Direct verification emits only stdout. Test scratch uses the operating system's
+temporary-directory API and is removed on normal exceptions and success; setting
+TMPDIR keeps it inside RUN on this POSIX host. The registered launcher isolates
+bytecode-cache reads. Direct -B execution does not provide that isolation.
+No full native, geometry, selected cold replay, Lean or Docker run was performed.

research/rank7-restore-substitution-audit/README.md

@@ -0,0 +1,181 @@
+# Independent audit of the two literal restore substitutions
+
+This package independently proves the two PR3042 restore identities and recounts
+their frame costs without importing any predecessor code. Both providers pass.
+The total paid-profile saving is correct. The literal edits differ from the
+public description inspected during this session.
+
+The source is dcharb78's [PR3042][3042], exact head
+`84cc406ad91ec53fff329a11a445d7effe564a77`, on Marius-Paul Dumitrean's
+[PR2979][2979] words. Jeremy Kothe's [PR3015][3015] supplied the declared-edit
+interface and first restore skip. Canonical main is
+`d8e0f83f00191df62174b641e9fff055c357f641`, priority revision 6.
+
+## Result and description correction
+
+For each provider, the actual source-addressed edits have these effects.
+
+| Literal edit | Original gates | Replacement gates | Registers skipping rank 8 | Local delta |
+|---|---:|---:|---|---|
+| `R1_E42`, restore `[162:188]` | 26 | 33 | 22, 40, 54, 63 | `-8 H1 + 4 H2` |
+| `R2_E7`, restore `[190:203]` | 13 | 15 | 5, 73 | `-4 H1 + 2 H2` |
+| Combined | 39 | 48 | All six | `-12 H1 + 6 H2` |
+
+The inspected PR body instead describes 29 and 14 replacement gates, with three
+skips per block and register 22 assigned to the second block. The
+[description snapshot](evidence/DESCRIPTION-SNAPSHOT.json) preserves the relevant
+quotes and observation time. This is a description correction, not a
+counterexample to the final word or its total saving. The immutable literal
+lists and independently recounted isolated edits establish the table above.
+
+In particular, the first literal edit already contains the temporary aggregation
+`X40 -= 2 X54` at their common rank-seven frame. It does not implement the
+public body's described carrier-369/carrier-450 construction. Downstream work
+should consume the pinned lists rather than reconstructing that narrative.
+
+The combined local profile is
+
+```text
+PR2979   {1:2445, 2:706, 3:232, 4:108, 5:18, 8:8}
+PR3042   {1:2433, 2:712, 3:232, 4:108, 5:18, 8:8}
+```
+
+Each changed register replaces its final `7 -> 8 -> 9` itinerary with a direct
+`7 -> 9` transition. No other register's jump histogram changes. The audit
+checks every literal A/B/restore frame, the A and B warp boundaries, the center cuts
+and all final endpoints. The emitted evidence contains the changed registers'
+complete transition histories, not just their sums.
+
+## Exact substitution proof
+
+Let every register hold an independent arbitrary dirty value in a vector space
+over the rationals. An ADD replaces row `t` by `row(t) + c row(s)`. A SCALE
+multiplies its row by its exact rational coefficient. For each hunk, the checker
+starts with the identity matrix on the union of its touched registers and
+computes every row before and after substitution. The matrices agree exactly.
+Untouched rows remain identity, so this is equality on all 704 input columns,
+not merely on target outputs or on a sampled reachable state.
+
+The verifier also checks the complete restore operator and reconstructs the
+literal final restore from the two nonoverlapping original-address preimages.
+All other word sections except report and inverse cleanup are unchanged.
+Therefore the hunk identities substitute into the inherited word for arbitrary
+intermediate register values. They preserve the full scalar operator, its
+inverse and its dual, even when preceding operations are symbolic linear
+operators. This implication does not require a fresh replay of those preceding
+operations.
+
+Cleanup is checked separately as the inverse reverse of the actual forward
+body, with the same injective renaming of the 91 restored helpers into their
+private buffer registers. The larger replacement adds nine restore gates and
+nine cleanup gates. The audit does not call those physical operations free.
+The native/program cost of their implementation remains a separate obligation.
+
+`frames.py` independently represents each binary frame by its full set of at
+most 512 vectors. It uses set containment and cardinalities, not the inherited
+Gaussian-elimination routine. The ordered 408 helper widths are unchanged in
+both providers, with inventory `{4:26, 5:2, 6:16, 7:52, 8:99, 9:213}`.
+The private-buffer namespace is unchanged; all 91 buffers remain charged.
+
+## Complete bill implication
+
+The literal T74 fill, order and dispatch are byte-identical to PR2979's inputs.
+[VENDOR.json](VENDOR.json) binds their PR3042 hashes, while
+[SOURCES.json](SOURCES.json) binds the working predecessor bytes. Together with
+unchanged ordered widths and unchanged call boundaries, this preserves the
+baseline geometry problem and idle bill. Baseline legality is a premise here;
+this audit does not rerun the geometric owner checker.
+
+There are 666 calls. Replacing their local profiles in the original complete
+profile reconstructs the shipped PR3042 profile exactly:
+
+```text
+delta = -7992 rank-one children + 3996 rank-two children
+profile = {1:1637688, 2:474192, 3:159468, 4:71928,
+           5:13716, 8:5328, 48:28190}
+rank mass = 4816512 = 74 * 65088
+physical stock = 66304 + 408 + 8 + 91 + 2 = 66813
+```
+
+For `Hr(b) = r (73/r)^b`, the per-call difference is
+
+```text
+6 H2(b) - 12 H1(b) = 12 * 73^b * (2^(-b) - 1) < 0, for every b > 0.
+```
+
+Both constructions have the same complete-moment normalization and idle bill.
+Thus the complete recursive moment strictly improves at every positive saving,
+conditional on the inherited boundary and baseline allocation. This proof uses
+no floating-point decision and needs no new numerical root calculation.
+It does not certify the reported numerical kappa, bit-side cap or outer transfer.
+No new kappa or selected-frontier change is claimed.
+
+## Reproduce
+
+Only Python's standard library is needed. The registered commands check pins,
+both providers and semantic failure controls in about two seconds locally.
+They do not generate words or logs in the checkout.
+
+```sh
+python3.12 -B scripts/research_package.py \
+  --package research/rank7-restore-substitution-audit
+```
+
+To compare the deterministic result with the retained evidence, write outside
+the checkout:
+
+```sh
+python3.12 -B research/rank7-restore-substitution-audit/verify.py > "$RUN/result.json"
+cmp "$RUN/result.json" research/rank7-restore-substitution-audit/evidence/RESULT.json
+```
+
+Thirteen behavioral groups cover positive words, every hunk's dropped gate and
+wrong coefficient, arbitrary dirty source restoration, exact preimages,
+unlisted changes, illegal/dependent frames, stale and incomplete cleanup,
+stale profiles, an unpaid child and changed source bytes. Optimized execution
+produces the same receipt because proof checks do not use removable assertions.
+See [ENGINEERING.md](ENGINEERING.md) for diagnostics and resource limits.
+
+The initial bounded construction probe combined E45 sources 70/71/72. Their
+joined preceding frame already equals the consumer frame, and the tested
+rewrites retained the paid histogram. That probe is not a general exclusion;
+no unsuccessful candidate is proposed as an improvement.
+
+## Limits
+
+This is a code-disjoint finite scalar/frame audit, not independent human or
+formal-kernel review. PR3042's author already supplies forward/dual free-operator
+audits and full-release receipts. The new coverage is the standalone rational
+substitution proof, independently enumerated frame itineraries, isolated-edit
+attribution correction and unchanged-boundary invoice implication.
+
+Native Clifford phases, arbitrary-size compilation, physical backing and
+movement, prefix/magnitude and precision/tape costs, recursive callers, analytic
+transfer and universal block-energy assumptions are not verified here. Physical
+stock arithmetic alone does not establish those contracts. The current selected
+record remains unchanged. The live T740 composition claim is separate.
+
+## Open next questions
+
+1. Independently replay PR3042's exact native/admission/outer chain before
+   adoption. Start with its declared full reproduction command and fresh
+   external outputs; compare actual word and invoice hashes. This needs a
+   separate compute budget and scientific review of inherited hypotheses.
+2. Correct the mutable source description to match its literal edits, or publish
+   a separately bound realization of the described alternative. This matters
+   because downstream composition needs the actual gate chronology and extra
+   scalar work. The table above and the pinned lists give the first check.
+
+## Credit
+
+Nick Petalas contributed this independent audit and description correction.
+Credit dcharb78 for PR3042's two literal rewrites, Jeremy Kothe for PR3015's edit
+interface and first restore rewrite, and Marius-Paul Dumitrean for PR2979's words
+and allocation. The unchanged [credits](vendor/CREDITS.md) and
+[notice](vendor/NOTICE) retain Mason Hale, Jeremy Diviney, Yiyang Lu, Tekalign,
+Ross Richardson, Dugongue, icekylinx, themilkman216 and the geometry/native/owner
+lineage. Apache-2.0. Development used substantial automated assistance.
+
+[3042]: https://github.com/CrocSwap/integer-mult-bounds/pull/3042
+[3015]: https://github.com/CrocSwap/integer-mult-bounds/pull/3015
+[2979]: https://github.com/CrocSwap/integer-mult-bounds/pull/2979

research/rank7-restore-substitution-audit/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641",
+  "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"
+    },
+    {
+      "path": "research/rank7-joint-endframes/data/WORD-base.json.gz",
+      "usage": "input",
+      "git_blob": "d9aa96a93fea5f7395e7783aef0bc117c0a0ae89",
+      "sha256": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d"
+    },
+    {
+      "path": "research/rank7-joint-endframes/data/WORD-extra.json.gz",
+      "usage": "input",
+      "git_blob": "74f6cb64595c21f7726ae77e69437868620bdcee",
+      "sha256": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7"
+    },
+    {
+      "path": "research/rank7-joint-endframes/allocation/PROFILE.json",
+      "usage": "input",
+      "git_blob": "46a83eeda67ab67cccbffe8b7ad8e44368b40ea7",
+      "sha256": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf"
+    },
+    {
+      "path": "research/rank7-joint-endframes/allocation/FILL.json.gz",
+      "usage": "input",
+      "git_blob": "8d4fd644d60ba2c98106dc770803b647afdf0963",
+      "sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39"
+    },
+    {
+      "path": "research/rank7-joint-endframes/allocation/ORDER.json",
+      "usage": "input",
+      "git_blob": "7409c4df1092241729739596c7648bda504e6aad",
+      "sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1"
+    },
+    {
+      "path": "research/rank7-joint-endframes/allocation/DISPATCH.json",
+      "usage": "input",
+      "git_blob": "9544fee4e6ee1f202cee22bfaeaf229ee3b2515e",
+      "sha256": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c"
+    }
+  ]
+}