Research: verify the complete PR2979 native/helper boundary

research/rank7-complete-native-boundary/PROOF.md

@@ -0,0 +1,105 @@
+# Complete finite source/native boundary
+
+## Statement and scope
+
+Fix the two literal PR2979 words pinned in SOURCES.json, the emitted programs
+and recipes authenticated by their retained native receipt, and either the
+forward or inverse-transpose orientation. Assume physical rational scalar
+operations, COPY/CLEAR in the declared common charts, and fresh zero allocation
+with the stated lifetime contract.
+
+Every native event in the complete emitted stream realizes the source-bound
+chart operator, including its global phase. In normalized source coordinates,
+each of the 408 original dirty helpers ends at its own arbitrary input, with
+no dependence on the other original inputs. Every one of the 91 private arrays
+is zero immediately before its actual free. These statements hold for arbitrary
+source, target and dirty-helper arrays.
+
+The statement is a finite conditional macro/native refinement. A restored
+normalized helper is not automatically a physical identity on its entire array.
+Its physical entrance/terminal frames and the supplied residual Fourier child
+remain charged. The result supplies no physical backing, allocation fit,
+precision, all-size implementation or new exponent.
+
+## Eventwise native realization
+
+The retained PR3038 source decoder reconstructs the whole source schedule,
+including rational operations, both center paths, ordered charts, warps,
+private lifetimes and wrapper positions. It independently decodes the emitted
+program, checks every source metadata field it consumes and requires equality
+of the complete event sequences. No dependency pruning occurs in this audit.
+
+For every native event, the retained native selector assigns its literal
+child, warp, ordinary adapter or residual-wrapper class. A class is checked
+against the exact serialized recipe selected by that event. The separate
+Gaussian-integer kernel compares all 512 basis columns with the source-derived
+reference, including global phase. Equality on a basis implies equality on every
+array. Cached equality uses the entire candidate circuit, reference circuit,
+selected record and orientation. A local frame number is not a global key.
+The receipt retains every event association and every exact identity digest.
+
+For a residual with entrance E and terminal U, the reference is T_U T_E^-1.
+Both inverse wrappers are included in the checked sandwich, whose factor is
+the coordinate Fourier transform on dim(U)-dim(E) axes. The inverse-transpose
+orientation conjugates the complete chronological circuit. It does not reverse
+execution order or replace inverse transpose with adjoint.
+
+Induction over the complete event sequence now gives the source macro's
+normalized semantics, subject to the stated physical scalar and allocation
+contracts. Common-chart incidence and nested center paths are checked by the
+source decoder. Native identities do not implement an unpriced scalar or
+physical allocator.
+
+## Helper and private observations
+
+The new forward observer assigns an independent formal input to every original
+live role and zero to each private allocation. It propagates exact rational
+linear combinations over the free algebra of signed warp words. Only adjacent
+inverse warp symbols cancel. ADD, SCALE, COPY and CLEAR have their literal
+semantics. Each actual private free requires the zero row before deletion.
+At the end, every helper row must be exactly its own input.
+
+This is stronger than testing a collection of numerical arrays. A formal
+identity remains an identity after substituting arbitrary arrays and the
+actual native warp operators. It uses no accidental commuting relations.
+The source decoder/native selector and the forward algebra arithmetic are
+credited reused tools. Their existing independence is reused, not newly claimed.
+
+A second, retained algorithm pulls each helper output covector backwards
+through the original source word. It swaps and negates directed shears for
+inverse transpose and retains noncommutative operator order. The projected row
+on the 632 original inputs must be the corresponding helper basis row. Terms
+from private entrances are retained in the receipt but those entrances are
+zero by the allocation premise. This source check is separate from the emitted
+forward observer. It does not replace the native phase checks.
+
+## Added coverage and failure witnesses
+
+PR3038 checks the helper249/private953 cone. PR3238 adds every actual private
+free. This audit takes every event in the complete stream and every original
+dirty-helper output. Exact class-set subtraction against the two pinned prior
+receipts identifies the additional native classes and their event occurrences.
+The previous classes are checked again along with the added classes.
+Here RESULT.prior_delta.new_native_events counts occurrences of added classes,
+not the total newly included native events. The latter also includes new
+occurrences of old classes. These coverage deltas are relative to PR3238; the
+group-A and group-B direct-path audits already cover selected identities.
+
+For each orientation, a literal helper ADD outside the prior expanded cone has
+its coefficient sign flipped. All 91 private frees and helper249 still pass
+under the retained observer. The complete helper-output check rejects it.
+For example, changing the sign at inverse-transpose event 21,886 gives
+helper287 the row x287-2*x286.
+Taking x286 nonzero and x287 zero witnesses failure while the old roots pass. A
+separate fault changes the global phase of a newly covered native child recipe;
+the all-column comparison rejects it. These mutants are failure controls, not
+reported faults in the original construction.
+
+## Remaining obligations
+
+The intended source/target endpoint identities, their application, physical
+scalar/COPY/CLEAR implementations, storage and movement, the actual owner fill,
+precision/prefix/tape costs, both supplier caps, outer coupling and all-size
+compiler/analytic premises remain separate. No selected result is modified.
+This proof is an exact finite argument backed by Python replay; independent
+human and formal proof-kernel review are unclaimed.

research/rank7-complete-native-boundary/README.md

@@ -0,0 +1,112 @@
+# Complete PR2979 source/native boundary
+
+This finite audit checks both complete emitted native streams and all 408
+arbitrary dirty-helper outputs of the original PR2979 construction, in both
+orientations. It extends PR3038's single endpoint cone and PR3238's all-private
+free cone. The source word, allocation and paid costs are unchanged. No new
+supplier, kappa or selected-frontier change is claimed.
+
+The precise statement and composition argument are in [PROOF.md](PROOF.md).
+[SOURCES.json](SOURCES.json) pins every consumed input to canonical main
+`6f100d4bb5083f8c35d96fd95a539811c62f245c`, priority revision 6. The original
+construction is PR2979 at `be191346391661f4d35fc0d1508d0a6029572576`.
+
+## Added coverage
+
+Each complete source stream has 22,748 events. Every native event is selected
+from that complete stream, without dependency pruning. Both orientations have
+3,481 classes per provider. Against PR3238's exact class union, that adds 833
+forward classes and 314 inverse-transpose classes. Those new classes cover
+998 and 317 event occurrences. In total, native event coverage increases from
+3,717/4,537 to 5,125 in each orientation, adding 1,408 forward and 588
+inverse-transpose event occurrences. This also includes new occurrences of
+previously checked classes. Existing classes are replayed too. These increments
+are relative to PR3238, not claims that every individual identity is new.
+The group-A and group-B direct-path audits already cover selected identities.
+
+The new forward observer checks all 408 final helper rows and every actual
+private free over exact rational free-warp expressions. A separate retained
+backward source-covector algorithm checks every original helper output.
+Native classes are checked on all 512 address columns, including global phase.
+The residual Fourier factors, all 91 private families and the full local
+paid profile remain charged.
+
+A literal helper ADD outside the prior expanded cone can have its sign flipped
+while all earlier private-free and helper249 roots still pass. The complete
+helper check rejects that mutant. A global-phase fault in a newly covered
+native class also rejects. At inverse-transpose event 21,886, the helper ADD
+sign change leaves helper287 equal to x287-2*x286 while all older roots pass.
+These are semantic failure controls, not defects reported in the original
+word. Exact indices, rows and class/event associations
+are retained in the two compressed RESULT files.
+
+The source decoder, native selector, exact Gaussian kernel, forward arithmetic
+and backward covector machinery are credited reused checking tools. This is a
+coverage extension using those independent implementations, not a claim to
+have independently reimplemented them.
+
+## Reproduce
+
+Use Python 3.12 with `numpy==2.3.5`, which the unchanged producer requires.
+The new proof calculations and exact kernel use the standard library. Run
+commands sequentially with an external session-owned temporary directory:
+
+```sh
+mkdir -p "$RUN_ROOT/scratch"
+TMPDIR="$RUN_ROOT/scratch" python3.12 -Werror -B scripts/research_package.py \
+  --package research/rank7-complete-native-boundary
+```
+
+The registered hook runs eight behavioral groups, then a fresh source/native
+replay for each provider. Direct replay is:
+
+```sh
+TMPDIR="$RUN_ROOT/scratch" python3.12 -I -O -Werror -B \
+  research/rank7-complete-native-boundary/verify.py --provider base
+TMPDIR="$RUN_ROOT/scratch" python3.12 -I -O -Werror -B \
+  research/rank7-complete-native-boundary/verify.py --provider extra
+```
+
+Each command authenticates inputs before executing retained code, generates
+fresh recipes, checks source/event and retained artifact equality, executes
+semantic controls and compares the complete deterministic receipt. It prints
+`PASS_COMPLETE_SOURCE_NATIVE_BOUNDARY provider=base` or `provider=extra`.
+`--emit` prints a fresh uncompressed receipt. `--artifacts DIR` reuses supplied
+producer artifacts but still authenticates and checks all identities; that mode
+does not claim a fresh producer execution. Replay needs no network or Git.
+
+## Limits
+
+The theorem is conditional on physical rational scalar, COPY/CLEAR and
+fresh-zero allocation contracts. Normalized restoration includes paid native
+residual Fourier children; it is not a physical identity on every helper's
+whole array. Actual backing and owner geometry, movement, storage,
+precision/prefix/tape, the complete intended source/target application,
+both supplier caps, outer coupling and all-size/compiler/analytic obligations
+are separate. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+The next useful step is to join a newly covered helper endpoint and its
+recursive residual to the actual owner placement and paid physical scalar
+implementation. This determines whether the checked local operator fits the
+complete invoice. Unknown physical and precision costs block admission.
+Another native-class census of this fixed word is unnecessary.
+
+## Credit
+
+Nick Petalas. Apache-2.0, following the repository license. Frozen predecessor
+sources and their notices remain unchanged.
+
+Marius-Paul Dumitrean supplied PR2979 and PR2942. ToikY supplied PR3038's
+source/native machinery and Sagar Thakrar supplied its separate exact
+Gaussian-integer kernel. commdata2338 supplied PR3238's forward free-algebra
+arithmetic and all-private-free coverage. Nick Petalas supplied
+PR2993/3006/3008/3014 and the backward covector engine. The group-A and group-B
+native/interface audits are credited complementary checks. Retain Jeremy
+Kothe's frame/native/cleanup and rewrite credit, Mason Hale and Jeremy
+Diviney's extraction lineage, icekylinx's native compiler, Ross Richardson's
+packing/invoice audits, and Tekalign, Yiyang Lu, Dugongue, Cinna Davis,
+DreamingOfClouds, Douglas Colkitt and the source packages' geometry lineage.
+
+[Canonical scoped claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-19009367).

research/rank7-complete-native-boundary/SOURCES.json

@@ -0,0 +1,138 @@
+{
+  "schema_version": 1,
+  "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c",
+  "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/frontier1094-recipes-exact-seed76/clifford.py",
+      "usage": "input",
+      "git_blob": "6f1e6a38febde7eb7a7341d317522e6650d84408",
+      "sha256": "d5e42ddabd141b7bfbd70fe13908f3c3a06aeccebeab90623596bfb1988b97fb"
+    },
+    {
+      "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/evidence/FULL-NATIVE-RECEIPT.json",
+      "usage": "input",
+      "git_blob": "87ac21d0878479877bb75961b3c054843711d4d4",
+      "sha256": "6d27c89d5e3a2c7f28387e4b20c462b0dff6c9fa92aacdde715d4b29cc286d41"
+    },
+    {
+      "path": "research/rank7-peer-private-free-audit/RESULT-base.json",
+      "usage": "input",
+      "git_blob": "3a7bd808ad6d25ed69a3a773a3fe6f39ffbac195",
+      "sha256": "adb6b7de5dd70db6c44174c5e8dcd98f56a9a3fcaea86cddbe413f8f5eb6fb40"
+    },
+    {
+      "path": "research/rank7-peer-private-free-audit/RESULT-extra.json",
+      "usage": "input",
+      "git_blob": "30ef75fd1e032dd18a570e81263e7c3e43bc7274",
+      "sha256": "5d41601ed7dff21f7b9a6e2c0ae5c7ee099f0462330ee61e6d2defbeb828ab73"
+    },
+    {
+      "path": "research/rank7-peer-private-free-audit/lifetimes.py",
+      "usage": "input",
+      "git_blob": "aa60e87471293b7c0b6e5b9dee6ce9303f58916b",
+      "sha256": "51a93c571ccfc697d890940552b35f5c76161b059b451fb0cc83221e8faa201c"
+    },
+    {
+      "path": "research/rank7-v45-native-cone-seed78/RESULT-base.json",
+      "usage": "input",
+      "git_blob": "9f78923a15b9dc13fbf5d78b7c94a75a3f7083ad",
+      "sha256": "5cea9b1f2c51b07d62a225100ca2abbcb710943f2d88aaedab0619d214297b40"
+    },
+    {
+      "path": "research/rank7-v45-native-cone-seed78/RESULT-extra.json",
+      "usage": "input",
+      "git_blob": "a2a293d5157846a80068bace94ce26e647b54a80",
+      "sha256": "86b999e314f5d66ce7db7171b1cda9e78c2e5b69bd7f51bee189cac963c3b958"
+    },
+    {
+      "path": "research/rank7-v45-native-cone-seed78/audit.py",
+      "usage": "input",
+      "git_blob": "8841684e69da3beac4c5461630f9b549807f1bb7",
+      "sha256": "175d0e7bb67b3a4c48080c2189451a798f747d8ae486af949528acc59e404ed3"
+    },
+    {
+      "path": "research/rank7-v45-native-cone-seed78/native.py",
+      "usage": "input",
+      "git_blob": "1a86a5649bdf5a409eac6f583cd2962a0f61c7e8",
+      "sha256": "3598214e804a042006d2343801bfbf94eaf4d4ff10810bb41081b94d53865171"
+    },
+    {
+      "path": "research/rank7-v45-native-cone-seed78/source.py",
+      "usage": "input",
+      "git_blob": "dbe5c740991f399e7070bfe31431aad87b05f266",
+      "sha256": "879357b502b007ca7d8b17e4cc542750a5b9d9702bbae000bb3880c0179d6834"
+    },
+    {
+      "path": "research/rank7-v45-native-cone-seed78/support.py",
+      "usage": "input",
+      "git_blob": "26f8526137ab404009ac06c02816b538bf42beaa",
+      "sha256": "ef58c76411c62a9baf263ab1a275e056de8dd2fec8f7d50d0cebb60765af373e"
+    },
+    {
+      "path": "research/rank7-v45-native-endpoint/endpoints.py",
+      "usage": "input",
+      "git_blob": "79c2495d2e0208ecf4d6f0a53f5f108a54217a47",
+      "sha256": "d5e8b8bf640cc6283141065995ade7f475b7ab3116ea01ce682765b5f84405c0"
+    },
+    {
+      "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_adapters.py",
+      "usage": "input",
+      "git_blob": "82beaa9c1d13bcd5f79d0a5e10e8a10733eac347",
+      "sha256": "c5907050a9a7fa36d4fcba3ad4fe440d1bec2063360c095013891785ba65c3ce"
+    },
+    {
+      "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_emit.py",
+      "usage": "input",
+      "git_blob": "6d47f63ab7a533941b3881bbfd3ae4dac5f76932",
+      "sha256": "99b59a6fa3feda86785e4225157dcb1a6169d256cec4f5e0acc9cea7a701df76"
+    },
+    {
+      "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_gauss.py",
+      "usage": "input",
+      "git_blob": "1ff29dfb244e2114de8e586a450ae9fb70308d58",
+      "sha256": "0884b14d6d77cde419a3c773ad9b21d0d18de1e6e20e6b6d5add458ed32ba4cb"
+    },
+    {
+      "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_phases.py",
+      "usage": "input",
+      "git_blob": "99f351785ebca5fbf3336bedcd7b48bac9c255e5",
+      "sha256": "9d1a620e26715f4c42fd0347ecc14ef5a4a9031867869b64e8bae4d8526a821e"
+    },
+    {
+      "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/bw_transport.py",
+      "usage": "input",
+      "git_blob": "08248542b18864c94a5ac050c8669f68519838e1",
+      "sha256": "9818e08b819310b40f1441b89be8c4369584a5b3fa5dfe9b86b1df9a7f5d6a76"
+    },
+    {
+      "path": "research/two-sided-helper-extraction/vendor/fastnative/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py",
+      "usage": "input",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
+    }
+  ]
+}