Supplier-boundary audit: all 36 selected frontier1094 residual wrappers exact with global phase, by two kernels (no new kappa)

research/frontier1094-residual-wrappers-seed62/README.md

@@ -0,0 +1,146 @@
+# The selected frontier1094 word's 36 residual wrappers are exact
+
+**Supplier-boundary audit: an independent, byte-bound check. No new κ, and no existing check is changed.**
+
+- Track: 60–74 (adversarial audit), assignment seed 62, drawn with the OS CSPRNG via Python `secrets`.
+- Card: `supplier-boundary-audit`, with the scope **refined** in [TASK.json](TASK.json).
+- Base: `179089e4`. The selected record frontier1094 is unchanged.
+
+## The obligation and where its acceptance came from
+
+Lemma A's exact part (`research/e8-lemma-a-lean`, `research/e8-lemma-g-lean/PROOF.md` §4) concerns every helper that enters at a nonzero frame E or ends below FULL at a hyperplane U. Each such helper needs a stored wrapper (L, R) with
+
+`L ∘ (C_[w] ⊗ I) ∘ R = T_end ∘ T_E⁻¹`,  w = dim end − dim E,
+
+where end is FULL, or U for a hyperplane end. For the selected gauge44 provider these are the 36 records in `RESIDUAL-ADAPTERS.json`, raw sha256 `383f40aa`.
+
+The selected chain binds the bytes of that file, but not their exactness:
+- **The bytes are pinned.** Both the owner audit's `source_artifacts` and the certificate's fresh invoice (`input_sha256.fresh_invoice` → `PREFIX-AND-INVOICE.json` → `providers.gauge44.artifacts`) pin it.
+- **The chain's own audit checks structure only.** `gauge44-slots-t16/code/audit_allcold.py` (lines 56–61) checks only each wrapper's `frame`, `terminal`, `vectors`, `terminal_vectors` and ranks.
+- **Exactness is established only by the producer's own code.** `hpe_adapters_local.py` generates the wrappers and decodes them again with the same `clifford_exact` primitives, then writes `WRAPPER-CHECKS.json` (`PASS_RESIDUAL_WRAPPERS_ARE_EXACT`, sha256 `0ae753d6`).
+  - The fresh invoice pins that receipt's bytes, but no chain code reads its status or content.
+  - The cold replay re-runs the same producer, for example `gauge44-slots/construction/slots/verify_slots.py:103`.
+- **#1781 (ours) left these records out** of its independent check. It covered the 2,896 child records and the 224 endpoint adapters.
+
+## What this package checks
+
+### Binding
+- It reuses the merged #1781 binding, which our package imports with its digests pinned. The chain runs: selected record → frontier1094 certificate → capsule → owner audit → gauge44 word and programs.
+- `RESIDUAL-ADAPTERS.json` must match the owner audit's own digest.
+- The `split-centres` decoy, which has the same basename, differs by digest.
+- The certificate's fresh invoice pins both `RESIDUAL-ADAPTERS.json` and `WRAPPER-CHECKS.json`.
+- The global8 twin is byte-identical. This is informational only.
+
+### Inventory
+- **The keys.** The 36 keys are exactly the word's entering helpers ending at FULL (key = start) together with its hyperplane-ending helpers (key = start:final). That gives:
+  - 22 FULL-ended records;
+  - 12 cold hyperplane-end records (`0:U`);
+  - 2 entering hyperplane-end records (`2:999` and `3:998`).
+- **The records.** Every record's frames, vectors and ranks match the word, and all 72 monomials are well formed.
+- **The program events.** In both programs, every residual event is a `pre` or a `post`. Each of the 240 wrapped helpers has exactly one of each, with the right key. Its first event is the `pre` and its last is the `post`. Our open #1964, from another session, checks this placement as part of Lemma G's H1. Each orientation has 480 events, with widths {4: 112, 5: 64, 7: 60, 8: 244}.
+- **Record fields.** Every record has exactly its expected field set.
+
+### Two kernels
+- **Kernel B** ([closed_form.py](closed_form.py), new, standard library only) computes amplitudes directly from closed forms:
+  - the frame operator from its closed formula;
+  - the monomial records from their closed forms;
+  - F_w from the √X product.
+
+  It works on sparse exact columns and evaluates no gate list.
+- **Kernel A** is #1781's packed Gaussian-integer evaluator (`clifford.py`).
+
+Both must find every identity exact on all 512 columns, with the global phase included.
+
+### Calibration of kernel B
+Before any record is judged, kernel B must pass three checks:
+- **Frame operator.** Kernel B must reproduce #702's 14 frame-kernel digests and #1415's three operator digests of T_U ∘ T_E⁻¹. These cover frames of rank 1, 4 and 8 and the conjugate transpose.
+- **Monomials and F_w.** On every column, kernel B's monomial and F_w must equal kernel A's: for 10 record monomials, and for F_w with w = 1, 4, 8 and 9. Without this check, those two conventions would be anchored only by the records under test.
+- **Lean pairs.** Records `3:998` and `2:999` must be field-for-field equal to Exact.lean's pair 2 and pair 3. For `2:999`, #1611 had already shown this for this word.
+
+## Results ([RESULT.json](RESULT.json))
+
+| | Records | Exact (kernel B) | Exact (kernel A) | K (C gates per identity) |
+|---|---|---|---|---|
+| FULL-ended | 22 | 22 | 22 | 9 |
+| Cold hyperplane-end `0:U` | 12 | 12 | 12 | 4 (8 records), 8 (4 records) |
+| Entering hyperplane-end | 2 | 2 | 2 | 8 |
+
+All 36 wrappers are exact.
+
+### Controls
+Each mutation below is rejected on every record it applies to:
+- global phase +1;
+- input character (`linear_Z4 += 2`);
+- a CZ term in Q;
+- an offset translation;
+- swapped wrappers;
+- width −1 and width +1;
+- a transposed matrix (36/36 each);
+- hyperplane-end records evaluated against FULL (14/14);
+- a FULL-ended wrapper reused for a hyperplane end (2/2);
+- another basis of the same span (2/2, while the same rows reordered pass);
+- kernel B's own phase and width mutants (8/8).
+
+The tests also reject the decoy, a flipped archive byte, a dropped `pre` event, an event read with the wrong key, and a wrong record vector. [test_package.py](test_package.py) has 17 tests.
+
+## Overlap
+
+Prior coverage, checked against the repository:
+- **The Lean pairs.** `2:999` and `3:998` are the Exact.lean pairs (#593, with #1415's semantic binding). #1611 tied `2:999` to pair 3 for this word.
+- **The cold rank-4 records.** The eight records `0:124`…`0:327` are byte-identical to records in earlier provider files. One example is `research/complex-sw4-frame8-validation`; the `community-k492-audit` copies match up to the terminal frame id. #702 checked that family's cold wrappers by amplitudes, for PR626.
+- **The four cold hyperplane-end records `0:1000`…`0:1003`.** They are hyperplane cases of #1697's audit of all 511 cold hyperplane terminals. That audit used wrappers its own run generated, not this word's stored bytes.
+- **What was producer-only.** The 22 FULL-ended entrance wrappers had only producer evidence.
+
+What this package adds: all 36 are now checked from the **selected** word's bound bytes, by two kernels, and tied to its programs.
+
+## What this does not show
+
+- **The executor bridge.** It does not show that the emitted program applies these records with exactly these semantics (Lemma G's H1 and the label bridge; see #1964).
+- **Other recipes.** The child and endpoint records are #1781's, and the identity adapters are not checked.
+- **Lean.** There is no Lean proof for the 34 records outside the Exact.lean pairs.
+- **κ.** There is no new κ.
+
+## Reproduce
+
+```sh
+python3 -I -B research/frontier1094-residual-wrappers-seed62/verify.py        # about 40 s; PASS_FRONTIER1094_RESIDUAL_WRAPPERS_EXACT
+python3 -I -B -m unittest discover -s research/frontier1094-residual-wrappers-seed62 -p test_package.py
+python3 scripts/research_package.py --package research/frontier1094-residual-wrappers-seed62 --check-only
+python3.12 scripts/research_package.py --package research/frontier1094-residual-wrappers-seed62
+```
+
+Requires standard-library Python 3.10 or later. It was run on Python 3.12.15 and 3.14.8 (macOS 26.5, arm64).
+
+## Open next questions
+
+1. **Does the emitted executor apply the child, endpoint and residual records with exactly these semantics?**
+   - Why it matters: record-level exactness, here and in #1781, still needs the bridge rec(A, B) = record circuit.
+   - First step: replay one helper's full event sequence (`pre` wrapper, climbs, `post` wrapper) through an independent statevector executor and compare the result with C_[w] ⊗ I.
+   - Blocked by: an independent executor for the emitted program format.
+2. **Should the chain check the exactness receipt's content, not just its bytes?**
+   - Why it matters: the fresh invoice pins `WRAPPER-CHECKS.json`, but nothing in the chain reads its status. This package's RESULT is an independent receipt that could be checked instead.
+   - First step: propose a status check, or this package's RESULT digest, at the next frontier1094 integration.
+   - Blocked by: a maintainer decision.
+3. **Can Lean's `Clifford.check` kernel-check the 36 packed identities for this instance?**
+   - Why it matters: two of them are already Lean-proved, so the rest would turn this replay into a formal result.
+   - First step: emit the 22 FULL-ended identities as Lean `check` terms and time `lake build`.
+   - Blocked by: a Lean toolchain, which is not installed here.
+
+## Credit
+
+- **Lean packages:** Lemma A (#516) and Lemma G (#509), both by DreamingOfClouds and formalizing #484.
+- **The producer of the residual wrappers and `WRAPPER-CHECKS.json`:** `hpe_adapters_local.py` (DreamingOfClouds, after PR #458 by chafreaky). It uses `clifford_exact.py` (icekylinx), whose exact phase lowering adapts PR425 (jacklightChen).
+- **`HyperplaneEnd/Exact.lean`:** jeremykothe2 (#593).
+- **Calibration sources:** #1415 (commdata2338) and #702 (BigCactusLabs).
+- **The packed kernel and binding:** our #1781.
+- **Related checks:**
+  - #1697 (navinor): all 511 cold hyperplane terminals;
+  - #1611 (bbMisk): binding helper 450's wrapper pair;
+  - #1964 (ours, open): Lemma G H1 extended labels.
+
+Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via Claude Code.
+- Parallel read-only scout and judge subagents selected the obligation and traced the producer-only evidence.
+- The closed-form kernel, the verifier and the controls were then written fresh.
+- A post-PR adversarial review corrected the supplier trace (the fresh invoice pins the receipt's bytes) and the overlap, and added the kernel cross-check and further controls (second commit).
+
+No claim was posted to Discussions. New material is Apache-2.0.

research/frontier1094-residual-wrappers-seed62/RESULT.json

@@ -0,0 +1,99 @@
+{
+ "binding": {
+  "archive": "research/community-frontier1094-audit/selected-replay.tar.gz",
+  "archive_sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6",
+  "canonical_word_gz_sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219",
+  "canonical_word_payload_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c",
+  "certificate": "research/community-frontier1094-audit/ASSEMBLY.json",
+  "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045",
+  "global8_twin_byte_identical": true,
+  "local_programs_gz_sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a",
+  "owner_audit_sha256": "30bafff060afcfb3644e951214d66cfaffe58242881c652e28003958b42127cc",
+  "recipes_sha256": "d0768f2164d5f64a2fdbec422f1cfde4e400818792f1904ca541958377243731",
+  "record_or_checkpoint": "certificates/selected-result.json or certificates/checkpoints/frontier1094.json",
+  "residual_adapters_sha256": "383f40aadd00a4ac700dfd0d4c22d6c6c0be9a9863116e4d69c7acd23bafae0c",
+  "review_sha256": "cb0e10a8b284f176526c17177e91186ce09aa3e88b4f6acc561051daa072b0d0",
+  "slot_pins_sha256": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2",
+  "template_sha256": "9c4c51425251389ee9a747c465814cd07c64812c15b7aeef704dad7d65395a74",
+  "wrapper_checks_in_owner_audit": false,
+  "wrapper_checks_pinned_by": "certificate input_sha256.fresh_invoice -> PREFIX-AND-INVOICE providers.gauge44.artifacts (bytes only; no chain code checks its status or content)",
+  "wrapper_checks_sha256": "0ae753d6fa6e922d8b8180da602828f6cb3f444fcd124d019acee74e145c0836"
+ },
+ "calibration": {
+  "kernel_B_vs_kernel_A": "kernel B monomials (10, all columns) and F_w (w = 1, 4, 8, 9) equal kernel A",
+  "lean_pairs": "records 3:998 and 2:999 equal Exact.lean pair 2 and pair 3 field by field",
+  "pr1415": "kernel B reproduces the three operator digests of T_U o T_E^-1 (frame operator at ranks 1 and 8, and its conjugate transpose)",
+  "pr702": "kernel B reproduces all 14 frame-kernel digests"
+ },
+ "controls": {
+  "cz_term": "rejected 36/36",
+  "frame_basis": "other basis rejected 2/2; reordered rows pass 2/2",
+  "full_wrapper_for_hyperplane_end": "rejected 2/2",
+  "global_phase": "rejected 36/36",
+  "hpe_record_against_full_end": "rejected 14/14",
+  "input_character": "rejected 36/36",
+  "kernel_B_mutants": "rejected 8/8",
+  "producer_wrapper_checks": {
+   "frames": 22,
+   "hyperplane_end_pairs": 14,
+   "status": "PASS_RESIDUAL_WRAPPERS_ARE_EXACT"
+  },
+  "swapped_wrappers": "rejected 36/36",
+  "translation": "rejected 36/36",
+  "transposed_matrix": "rejected 36/36",
+  "width_minus_one": "rejected 36/36",
+  "width_plus_one": "rejected 36/36"
+ },
+ "evaluation": {
+  "K_histogram": {
+   "4": 8,
+   "8": 6,
+   "9": 22
+  },
+  "columns": 512,
+  "global_phase_included": true,
+  "kernel_A_exact": 36,
+  "kernel_B_exact": 36,
+  "records": 36
+ },
+ "inventory": {
+  "events": {
+   "backward": {
+    "post": 240,
+    "pre": 240,
+    "widths": {
+     "4": 112,
+     "5": 64,
+     "7": 60,
+     "8": 244
+    },
+    "wrapped_helpers": 240
+   },
+   "forward": {
+    "post": 240,
+    "pre": 240,
+    "widths": {
+     "4": 112,
+     "5": 64,
+     "7": 60,
+     "8": 244
+    },
+    "wrapped_helpers": 240
+   }
+  },
+  "helper_classes": {
+   "cold_full": 240,
+   "cold_hpe": 48,
+   "enter_full": 162,
+   "enter_hpe": 30
+  },
+  "kinds": {
+   "cold_hpe": 12,
+   "enter_hpe": 2,
+   "full_end": 22
+  },
+  "records": 36
+ },
+ "scope": "Record level: all 36 residual wrappers of the selected gauge44 word satisfy L F_w R T_E = T_end on all 512 columns with global phase (Lemma A exact part); not the executor bridge, a Lean proof or a new kappa",
+ "status": "PASS_FRONTIER1094_RESIDUAL_WRAPPERS_EXACT"
+}

research/frontier1094-residual-wrappers-seed62/SOURCES.json

@@ -0,0 +1,102 @@
+{
+  "schema_version": 1,
+  "base_commit": "179089e4111a56a3bbf1f512410e7ef789380a71",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    },
+    {
+      "path": "docs/research/community-batch1099-integration.json",
+      "usage": "input",
+      "git_blob": "9d60e86c0e494d17bec5e28eda41b275c9ede64e",
+      "sha256": "684c50d1ac69863e1fcc0a34bf76c54bac576f6bbde79b3c67d8432a495c8c1c"
+    },
+    {
+      "path": "research/cold-wrapper-amplitude-audit/EXPECTED.json",
+      "usage": "input",
+      "git_blob": "64bb189e2e5c86da68f1b53bec8296a4220f583b",
+      "sha256": "64d9a891148c84bb6e5454ac6a02399a2abb3e553ee62f2719f8ed061eb8a501"
+    },
+    {
+      "path": "research/community-frontier1094-audit/ASSEMBLY.json",
+      "usage": "input",
+      "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0",
+      "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045"
+    },
+    {
+      "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json",
+      "usage": "input",
+      "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8",
+      "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b"
+    },
+    {
+      "path": "research/community-frontier1094-audit/selected-replay.tar.gz",
+      "usage": "input",
+      "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f",
+      "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6"
+    },
+    {
+      "path": "research/e8-lemma-a-lean/README.md",
+      "usage": "provenance",
+      "git_blob": "42355bfe904684da18f4ed1763dfcefb36eb36c8",
+      "sha256": "87a242f674783d6c553c450b7c5951f667f0f480316a557146449c5003c1d298"
+    },
+    {
+      "path": "research/e8-lemma-g-lean/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "6b24da0ab861902a6a3f65d9599bb9c0f964aa1c",
+      "sha256": "2a7d84a83d34495dcf46ff9241ee3d7ec18ffc7d49c5476ab15fe0834046f2a3"
+    },
+    {
+      "path": "research/frontier1094-recipes-exact-seed76/CASES.json",
+      "usage": "input",
+      "git_blob": "e508b1224dedb4be9424cac58c361825c5a79810",
+      "sha256": "012493aa8d71a5f4e91fd82dd828daaab993efa36189a13b71b5c88eac536863"
+    },
+    {
+      "path": "research/frontier1094-recipes-exact-seed76/clifford.py",
+      "usage": "input",
+      "git_blob": "6f1e6a38febde7eb7a7341d317522e6650d84408",
+      "sha256": "d5e42ddabd141b7bfbd70fe13908f3c3a06aeccebeab90623596bfb1988b97fb"
+    },
+    {
+      "path": "research/frontier1094-recipes-exact-seed76/verify.py",
+      "usage": "input",
+      "git_blob": "8775d15e7473ee0b11ec47a07bc0d9cf0834bdd4",
+      "sha256": "7f66d587b6f73451b2b35941efe3bdd9271c83a88d64982a426f51b8c19336ef"
+    },
+    {
+      "path": "research/gauge44-slots-t16/code/audit_allcold.py",
+      "usage": "provenance",
+      "git_blob": "923bf7b675ca09f4d2633e7e53f16a1b23b6d5bc",
+      "sha256": "1467a2acb654e62552c69fb9a7c4c85f70a02120881d222313865058ab71a6cc"
+    },
+    {
+      "path": "research/gauge44-slots-t16/construction/slots/SLOT-PINS-k8.json",
+      "usage": "input",
+      "git_blob": "2702c368f4de0b671577aee9a0e2df41c1b27658",
+      "sha256": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2"
+    },
+    {
+      "path": "research/hpe-lean-semantic-binding/RESULT.json",
+      "usage": "input",
+      "git_blob": "c9169b5d5d483fc66dcb1ca5c27f2c2fa7124288",
+      "sha256": "9c0b3f39d9ef68ed8484f29fd9cb5d57e931580a882157afb593fb28839cbfdf"
+    },
+    {
+      "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean",
+      "usage": "input",
+      "git_blob": "1af33a206a9ba6c4826b3a1516d104e770380869",
+      "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183"
+    }
+  ]
+}