From f92601d6b6d4e71b0c643fd0af09ac9c3aea5455 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 23:10:56 +0530 Subject: [PATCH 1/2] Supplier-boundary audit: the selected frontier1094 word's 36 residual wrappers are exact (no new kappa) Lemma A's exact part for the selected gauge44 word rests on the producer's own WRAPPER-CHECKS.json (not pinned by the owner audit); the chain's audit checks only the wrappers' structural fields. This binds RESIDUAL-ADAPTERS.json through the owner audit, ties its 36 keys and 480 residual events per orientation to the word and programs, and checks every identity L F_w R T_E = T_end exactly on all 512 columns with global phase by two kernels: a new closed-form amplitude kernel (calibrated on #702 and #1415) and #1781's packed evaluator. Mutation controls are rejected on every record. --- .../README.md | 135 ++++++++ .../RESULT.json | 95 ++++++ .../SOURCES.json | 102 ++++++ .../TASK.json | 72 ++++ .../VERIFY.json | 48 +++ .../closed_form.py | 213 ++++++++++++ .../test_package.py | 130 ++++++++ .../verify.py | 312 ++++++++++++++++++ 8 files changed, 1107 insertions(+) create mode 100644 research/frontier1094-residual-wrappers-seed62/README.md create mode 100644 research/frontier1094-residual-wrappers-seed62/RESULT.json create mode 100644 research/frontier1094-residual-wrappers-seed62/SOURCES.json create mode 100644 research/frontier1094-residual-wrappers-seed62/TASK.json create mode 100644 research/frontier1094-residual-wrappers-seed62/VERIFY.json create mode 100644 research/frontier1094-residual-wrappers-seed62/closed_form.py create mode 100644 research/frontier1094-residual-wrappers-seed62/test_package.py create mode 100644 research/frontier1094-residual-wrappers-seed62/verify.py diff --git a/research/frontier1094-residual-wrappers-seed62/README.md b/research/frontier1094-residual-wrappers-seed62/README.md new file mode 100644 index 0000000000..bf9f90c955 --- /dev/null +++ b/research/frontier1094-residual-wrappers-seed62/README.md @@ -0,0 +1,135 @@ +# 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 that file through the owner audit's `source_artifacts`, but it does not check that the records are exact: +- **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 rests on a receipt the chain does not pin.** The only statement of exactness is the producer's own `WRAPPER-CHECKS.json` (`PASS_RESIDUAL_WRAPPERS_ARE_EXACT`, sha256 `0ae753d6`). The producer wrote it with its own Clifford code, and the owner audit does **not** pin it. +- **Later re-runs are not independent.** Re-runs such as #1646 and `selected-replay-fastpath` execute that same producer code. +- **#1781 (ours) left these records out** of its independent check. It covered the 2,896 child records and 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 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, each of the 240 wrapped helpers has exactly one `pre` and one `post` residual event, 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}. + +### 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 reproduce: +- #702's 14 frame-kernel digests; +- #1415's three operator digests of T_U ∘ T_E⁻¹, which exercise the adjoint. + +Separately, records `3:998` and `2:999` are field-for-field Exact.lean's pair 2 and pair 3. Their identities are Lean-proved. + +## 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; +- 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 15 tests. + +## Overlap + +- **Lean pairs.** `2:999` and `3:998` were already Lean-proved as Exact.lean pairs 3 and 2 (#593). Their semantic binding is #1415's. +- **Cold rank-4 records.** The eight cold rank-4 records `0:124`…`0:327` are byte-identical to records in earlier provider files, for example `research/community-k492-audit`. #702 checked the cold wrappers of that family by amplitudes, for PR626. +- **What is new.** The other 26 records (the 22 FULL-ended ones and `0:1000`…`0:1003`) had only producer evidence. All 36 are now checked for the **selected** word, from its bound bytes, by two kernels. + +## 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 `WRAPPER-CHECKS.json`, or this package's receipt, be bound by the owner audit?** + - Why it matters: the chain pins the records but not the producer's exactness receipt. + - First step: propose the binding at the next maintainer integration of frontier1094. + - 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 + +- **Lemma A and Lemma G Lean packages, and the HPE wrapper tool:** DreamingOfClouds (#484/#509), following PR #458 (chafreaky). +- **`HyperplaneEnd/Exact.lean`:** jeremykothe2 (#593). +- **Calibration sources:** #1415 (commdata2338) and #702 (BigCactusLabs). +- **The producer:** `phases_full.py`/`clifford_exact.py` (icekylinx, from PR425). +- **The packed kernel and binding:** our #1781. +- **Related checks:** #1697 (navinor; the cold hyperplane operators), #1611 (bbMisk; binding helper 450's wrapper pair), and #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. + +No claim was posted to Discussions. New material is Apache-2.0. diff --git a/research/frontier1094-residual-wrappers-seed62/RESULT.json b/research/frontier1094-residual-wrappers-seed62/RESULT.json new file mode 100644 index 0000000000..52f898c9f4 --- /dev/null +++ b/research/frontier1094-residual-wrappers-seed62/RESULT.json @@ -0,0 +1,95 @@ +{ + "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_pinned_by_owner_audit": false, + "wrapper_checks_sha256": "0ae753d6fa6e922d8b8180da602828f6cb3f444fcd124d019acee74e145c0836" + }, + "calibration": { + "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", + "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_off_by_one": "rejected 36/36" + }, + "evaluation": { + "K_histogram": { + "4": 8, + "8": 6, + "9": 22 + }, + "both_kernels": true, + "columns": 512, + "global_phase_included": true, + "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" +} diff --git a/research/frontier1094-residual-wrappers-seed62/SOURCES.json b/research/frontier1094-residual-wrappers-seed62/SOURCES.json new file mode 100644 index 0000000000..0e0aedf891 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/frontier1094-residual-wrappers-seed62/TASK.json b/research/frontier1094-residual-wrappers-seed62/TASK.json new file mode 100644 index 0000000000..196cbf6bde --- /dev/null +++ b/research/frontier1094-residual-wrappers-seed62/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 3, + "base_commit": "179089e4111a56a3bbf1f512410e7ef789380a71", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "refined", + "actual_scope": "One selected supplier obligation traced to its source-bound checks: Lemma A's exact part for the selected frontier1094 gauge44 word, i.e. the 36 stored residual wrappers (RESIDUAL-ADAPTERS.json) satisfy L o F_w o R o T_E = T_end exactly on all 512 columns with global phase, and are exactly the wrappers its programs use.", + "scope_change_reason": "Refined to the one obligation whose acceptance rests only on the producer's own check: the selected chain's audit (gauge44-slots-t16/code/audit_allcold.py) checks the wrappers' structural fields only, and their exactness comes from the producer's WRAPPER-CHECKS.json, which the owner audit does not pin. This was left open by our #1781.", + "bottleneck_link": "Side result on the selected record's soundness, no kappa change. Lemma A turns each entering or hyperplane-ending helper's residual into C_[w] (x) I through these wrappers; an error would leave ranks and the paid profile unchanged but break exact restoration. This gives the first independent, byte-bound check of all 36 for the selected word.", + "budget_minutes": 180, + "stop_rule": "Stop when all 36 records are exact under two calibrated kernels, the inventory ties them to the programs' residual events, and every mutation control is rejected.", + "outcome": "completed", + "evidence": "RESULT.json: RESIDUAL-ADAPTERS 383f40aa pinned by the owner audit (WRAPPER-CHECKS 0ae753d6 is not); 36 records (22 FULL-ended, 12 cold hyperplane-end, 2 entering hyperplane-end) = the word's keys; 240 pre + 240 post residual events per orientation, keys correct, pre first and post last; kernel B reproduces #702 (14) and #1415 (3); 2:999 and 3:998 are Exact.lean pairs 3 and 2; all 36 identities exact on 512 columns with global phase under both kernels (K histogram 4:8, 8:6, 9:22); controls rejected: phase, input character, CZ term, translation, swapped wrappers, width, transposed matrix (36/36 each), hyperplane-end records against FULL (14/14), FULL wrapper reused for a hyperplane end (2/2), frame basis (2/2, reordered rows pass), kernel B mutants (8/8). 15 tests pass.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents selected the obligation (both judges ranked it first) and traced the producer-only evidence; the closed-form kernel, verifier and controls were then written fresh, reusing our merged #1781 binding and packed kernel by import with pinned digests.", + "open_questions": [ + { + "question": "Does the emitted executor apply the records (child, endpoint and residual) with exactly these semantics?", + "why_it_matters": "Record-level exactness (#1781 and this package) still needs the bridge rec(A,B) = record circuit for the stream (H1, check_extended_labels, lg_phys.run).", + "first_step": "Replay one helper's full event sequence (pre wrapper, climbs, post wrapper) through an independent statevector executor and compare with C_[w] (x) I.", + "blocked_by": "An independent executor for the emitted program format." + }, + { + "question": "Should WRAPPER-CHECKS.json be bound by the owner audit like RESIDUAL-ADAPTERS.json?", + "why_it_matters": "The selected chain currently pins the records but not the producer's exactness receipt; this package now supplies an independent receipt.", + "first_step": "Propose adding this package's RESULT digest (or WRAPPER-CHECKS) to the frontier1094 integration record at the next maintainer integration.", + "blocked_by": "Maintainer decision." + }, + { + "question": "Can the 36 packed identities be kernel-checked by Lean's Clifford.check for this instance?", + "why_it_matters": "It would turn this independent replay into a formal result; two of the 36 (2:999, 3:998) are already Lean-proved as Exact.lean pairs.", + "first_step": "Emit the 22 FULL-ended identities as Lean check terms and time lake build.", + "blocked_by": "A Lean toolchain (not installed here)." + } + ] +} diff --git a/research/frontier1094-residual-wrappers-seed62/VERIFY.json b/research/frontier1094-residual-wrappers-seed62/VERIFY.json new file mode 100644 index 0000000000..295b823811 --- /dev/null +++ b/research/frontier1094-residual-wrappers-seed62/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/community-batch1099-integration.json", + "research/cold-wrapper-amplitude-audit/EXPECTED.json", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/frontier1094-recipes-exact-seed76/CASES.json", + "research/frontier1094-recipes-exact-seed76/clifford.py", + "research/frontier1094-recipes-exact-seed76/verify.py", + "research/gauge44-slots-t16/construction/slots/SLOT-PINS-k8.json", + "research/hpe-lean-semantic-binding/RESULT.json", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Merged #1781 binding (selected record -> frontier1094 certificate -> capsule -> owner audit -> gauge44 word and programs), RESIDUAL-ADAPTERS.json pinned by the owner audit (split-centres decoy rejected, global8 twin identical); inventory (36 keys = entering and hyperplane-ending helpers; frames, vectors, ranks; monomials; 240 pre + 240 post residual events per orientation with correct keys, pre first and post last); kernel B calibrated on #702's 14 frame kernels and #1415's three digests, records 2:999/3:998 = Exact.lean pairs 3/2; all 36 identities L F_w R T_E = T_end exact on 512 columns with global phase by kernel B (closed form) and kernel A (#1781 packed); mutation controls rejected on every record; RESULT.json byte-identical." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 300, + "checks": "Decoy adapters and a flipped archive byte rejected; inventory counts and three inventory negatives; kernel B reproduces #702 kernels and matches kernel A columns; both kernels accept samples and reject a phase mutant; Lean pairs; kernel B is stdlib-only; recorded controls." + } + ] +} diff --git a/research/frontier1094-residual-wrappers-seed62/closed_form.py b/research/frontier1094-residual-wrappers-seed62/closed_form.py new file mode 100644 index 0000000000..89f86104bb --- /dev/null +++ b/research/frontier1094-residual-wrappers-seed62/closed_form.py @@ -0,0 +1,213 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Kernel B: closed-form amplitudes on C^(2^9), sparse exact columns (standard library only; no repository imports). + +Conventions (as in #1781's README "Operator semantics"; bit i of an index is axis i, F2 matrices are lists of row +bitmasks, (Gx)_i = parity(G[i] & x)): + +- frame operator, closed form: for a frame U of r independent rows, extend U by unit vectors to a basis, let G have + those vectors as columns, h = G^-1, Q = I + h^T h, a = diag Q and q(x) = sum_{i in x} a_i + 2 sum_{i = 2^-r sum_{delta < 2^r} i^(q(y) - q(x)) (1+i)^(r - |delta|) (1-i)^|delta| |y>, y = G (h x XOR delta); + T_0 = I and T_FULL = F_9 (the 9-axis sqrt-X product). +- monomial record m: M |x> = i^(phase + q_m(x)) |G_m x XOR offset> with q_m from (quadratic_rows, linear_Z4). +- F_w: sqrt(X) on axes 0..w-1; on one axis, |b> -> ((1+i)|b> + (1-i)|b XOR 1>)/2. + +A column is a dict {y: (re, im)} of Gaussian-integer numerators over a common 2^e (the exponent is carried +separately). Nothing here evaluates a gate list: T_U, M and F_w are applied from their formulas. +""" +DIM = 512 +N_AXES = 9 +_UNIT = ((1, 0), (0, 1), (-1, 0), (0, -1)) # i^k + + +def _par(x): + return bin(x).count('1') & 1 + + +def _mul(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def _rank(rows): + piv = {} + for x in rows: + while x: + h = x.bit_length() - 1 + if h in piv: + x ^= piv[h] + else: + piv[h] = x + break + return len(piv) + + +def _apply(rows, x): + return sum(_par(r & x) << i for i, r in enumerate(rows)) + + +def _columns_to_rows(cols): + return [sum(((cols[j] >> i) & 1) << j for j in range(N_AXES)) for i in range(N_AXES)] + + +def _invert(rows): + """F2 inverse by solving G z = e_k for each k (exhaustive over the 512 vectors, independent of elimination).""" + image = {_apply(rows, z): z for z in range(DIM)} + if len(image) != DIM: + raise ValueError('singular') + cols = [image[1 << k] for k in range(N_AXES)] # column k of G^-1 + return _columns_to_rows(cols) + + +def _phase(Q, a, x): + lin = sum(a[i] for i in range(N_AXES) if (x >> i) & 1) + quad = sum(((Q[i] >> j) & 1) for i in range(N_AXES) for j in range(i + 1, N_AXES) if (x >> i) & 1 and (x >> j) & 1) + return (lin + 2 * quad) % 4 + + +_PARTS = {} + + +def frame_parts(U): + key = tuple(U) + if key not in _PARTS: + _PARTS[key] = _frame_parts(U) + return _PARTS[key] + + +def _frame_parts(U): + ext = [] + for x in list(U) + [1 << k for k in range(N_AXES)]: + if _rank(ext + [x]) > len(ext): + ext.append(x) + if len(ext) != N_AXES or ext[:len(U)] != list(U): + raise ValueError('frame rows not independent') + G = _columns_to_rows(ext) + h = _invert(G) + hc = [sum(((h[i] >> j) & 1) << i for i in range(N_AXES)) for j in range(N_AXES)] # columns of h + Q = [sum(_par(hc[i] & hc[j]) << j for j in range(N_AXES)) ^ (1 << i) for i in range(N_AXES)] + a = [(Q[i] >> i) & 1 for i in range(N_AXES)] + table = [_phase(Q, a, z) for z in range(DIM)] + return G, h, Q, a, table + + +def frame_column(U, x): + """column x of T_U: ({y: (re, im)}, exponent e) with amplitudes = numerators / 2^e.""" + r = len(U) + if r == 0: + return {x: (1, 0)}, 0 + if r == N_AXES: + G, h, q = None, None, lambda z: 0 + base = x + img = lambda z: z # noqa: E731 + else: + G, h, Q, a, table = frame_parts(U) + q = table.__getitem__ + base = _apply(h, x) + img = lambda z: _apply(G, z) # noqa: E731 + col = {} + qx = q(x) + for delta in range(1 << r): + k = bin(delta).count('1') + amp = (1, 0) + for _ in range(r - k): + amp = _mul(amp, (1, 1)) + for _ in range(k): + amp = _mul(amp, (1, -1)) + y = img(base ^ delta) + amp = _mul(amp, _UNIT[(q(y) - qx) % 4]) + col[y] = (col.get(y, (0, 0))[0] + amp[0], col.get(y, (0, 0))[1] + amp[1]) + return {y: v for y, v in col.items() if v != (0, 0)}, r + + +def frame_column_adjoint(U, x): + """column x of T_U^-1 = T_U^dagger (T_U is unitary): entry y is conj(T_U[x, y]).""" + r = len(U) + out = {} + for y in range(DIM): + col, e = frame_column(U, y) + if x in col: + re, im = col[x] + out[y] = (re, -im) + return out, r + + +def monomial_apply(m, col): + Q, a, G, b, p = m['quadratic_rows'], m['linear_Z4'], m['matrix_rows'], m['offset'], m['phase'] + out = {} + for y, v in col.items(): + z = _apply(G, y) ^ b + out[z] = _mul(v, _UNIT[(p + _phase(Q, a, y)) % 4]) + return out + + +def fourier_apply(w, col, e): + for axis in range(w): + bit = 1 << axis + out = {} + for y, v in col.items(): + for target, c in ((y, (1, 1)), (y ^ bit, (1, -1))): + t = _mul(v, c) + old = out.get(target, (0, 0)) + out[target] = (old[0] + t[0], old[1] + t[1]) + col = {y: v for y, v in out.items() if v != (0, 0)} + e += 1 + return col, e + + +def _scaled(col, e, E): + s = 1 << (E - e) + return {y: (v[0] * s, v[1] * s) for y, v in col.items()} + + +def wrapper_identity(E_rows, U_rows, left, right, w): + """L o F_w o R o T_E = T_U on every column, exactly (global phase included). Returns the first failing column or None.""" + for x in range(DIM): + col, e = frame_column(E_rows, x) + col = monomial_apply(right, col) + col, e = fourier_apply(w, col, e) + col = monomial_apply(left, col) + ref, f = frame_column(U_rows, x) + E = max(e, f) + if _scaled(col, e, E) != _scaled(ref, f, E): + return x + return None + + +def kernel_digest_702(U): + """#702's frame-kernel digest: numerators over 2^r, unreduced, columns x = 0..511, rows ascending.""" + import hashlib + import json + body = [] + for x in range(DIM): + col, _ = frame_column(U, x) + body.append([[y, col[y][0], col[y][1]] for y in sorted(col)]) + return hashlib.sha256(json.dumps(body, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def matrix_digest_1415(E_rows, U_rows): + """#1415's digest of T_U o T_E^-1: per column, reduce by 2 while all numerators are even.""" + import hashlib + import json + adj = [dict() for _ in range(DIM)] # T_E^dagger columns, built from T_E's columns + for y in range(DIM): + col, _ = frame_column(E_rows, y) + for x, (re, im) in col.items(): + adj[x][y] = (re, -im) + rE, rU = len(E_rows), len(U_rows) + h, dens, nonzero = hashlib.sha256(), set(), 0 + tcols = [frame_column(U_rows, z)[0] for z in range(DIM)] + for x in range(DIM): + out = {} + for z, v in adj[x].items(): + for y, u in tcols[z].items(): + t = _mul(u, v) + old = out.get(y, (0, 0)) + out[y] = (old[0] + t[0], old[1] + t[1]) + col = {y: v for y, v in out.items() if v != (0, 0)} + e = rE + rU + while e > 0 and all(re % 2 == 0 and im % 2 == 0 for re, im in col.values()): + col = {y: (re // 2, im // 2) for y, (re, im) in col.items()} + e -= 1 + dens.add(e) + nonzero += len(col) + h.update((json.dumps([e, [[y, col[y][0], col[y][1]] for y in sorted(col)]], sort_keys=True, separators=(',', ':')) + '\n').encode()) + return h.hexdigest(), sorted(dens), nonzero diff --git a/research/frontier1094-residual-wrappers-seed62/test_package.py b/research/frontier1094-residual-wrappers-seed62/test_package.py new file mode 100644 index 0000000000..4388a7a9f5 --- /dev/null +++ b/research/frontier1094-residual-wrappers-seed62/test_package.py @@ -0,0 +1,130 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Controls for the residual-wrapper audit (about 30 s). + +Run: python3 -I -B -m unittest discover -s research/frontier1094-residual-wrappers-seed62 -p test_package.py -v +""" +import ast +import copy +import json +import sys +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import closed_form as B # noqa: E402 +import verify as V # noqa: E402 + +R, A = V.load_1781() +DATA, ADAPTERS, CHECKS, BINDING = V.bind(R) +WORD, PROGRAMS = DATA['word'], DATA['programs'] +FRAMES = WORD['frames'] +REC = ADAPTERS['recipes'] +RESULT = json.loads((HERE / 'RESULT.json').read_text()) + + +def parts(k): + E, U = V.end_of(k) + return E, U, len(FRAMES[U]) - len(FRAMES[E]) + + +class Binding(unittest.TestCase): + def test_decoy_adapters_rejected(self): + with self.assertRaisesRegex(V.Reject, 'pinned by the owner audit'): + V.bind(R, member_overrides={'adapters': V.MEMBERS['decoy']}) + + def test_archive_byte_flip_rejected(self): + raw = bytearray((V.ROOT / R.CASES['archive']['path']).read_bytes()) + raw[-1] ^= 1 + with self.assertRaisesRegex(Exception, 'archive digest'): + V.bind(R, archive_bytes=bytes(raw)) + + def test_binding_recorded(self): + self.assertEqual(BINDING['residual_adapters_sha256'], RESULT['binding']['residual_adapters_sha256']) + self.assertFalse(BINDING['wrapper_checks_pinned_by_owner_audit']) + + +class Inventory(unittest.TestCase): + def test_counts(self): + inv = V.inventory(A, WORD, PROGRAMS, ADAPTERS) + self.assertEqual(inv, RESULT['inventory']) + self.assertEqual(inv['kinds'], {'cold_hpe': 12, 'enter_hpe': 2, 'full_end': 22}) + + def test_dropped_pre_event_rejected(self): + progs = copy.deepcopy(PROGRAMS) + i = next(n for n, e in enumerate(progs['forward']) if e[0] == 'residual_adapter' and e[1] == 'pre') + del progs['forward'][i] + with self.assertRaisesRegex(V.Reject, 'one pre and one post'): + V.inventory(A, WORD, progs, ADAPTERS) + + def test_wrong_event_key_rejected(self): + progs = copy.deepcopy(PROGRAMS) + i = next(n for n, e in enumerate(progs['forward']) if e[0] == 'residual_adapter' and len(e) == 5) + progs['forward'][i] = progs['forward'][i][:4] # a hyperplane-end event read as its FULL key + with self.assertRaisesRegex(V.Reject, 'residual event key'): + V.inventory(A, WORD, progs, ADAPTERS) + + def test_record_vector_mismatch_rejected(self): + bad = copy.deepcopy(ADAPTERS) + bad['recipes']['423']['vectors'] = [46] + with self.assertRaisesRegex(V.Reject, 'record frames 423'): + V.inventory(A, WORD, PROGRAMS, bad) + + +class Kernels(unittest.TestCase): + def test_kernel_b_reproduces_the_published_frame_kernels(self): + e = json.loads((V.ROOT / R.CASES['fixtures']['pr702']['path']).read_text())['identities'] + self.assertTrue(all(B.kernel_digest_702(i['frame']) == i['kernel_sha256'] for i in e[:4])) + + def test_kernel_b_matches_kernel_a_on_frame_columns(self): + for f in (2, 124, 423, 1000): + U = FRAMES[f] + k = A.c_gates(A.canonical_frame(U)) + cols = A.columns(A.run(A.canonical_frame(U), A.radix(k)), A.radix(k)) + for x in (0, 5, 300): + col, e = B.frame_column(U, x) + self.assertEqual(e, k) + self.assertEqual(col, cols.get(x, {})) + + def test_both_kernels_accept_samples_and_reject_a_phase_mutant(self): + for k in ('2', '0:124', '0:1000', '3:998'): + E, U, w = parts(k) + r = REC[k] + self.assertIsNone(B.wrapper_identity(FRAMES[E], FRAMES[U], r['left'], r['right'], w)) + bad = dict(r['left'], phase=(r['left']['phase'] + 1) % 4) + self.assertIsNotNone(B.wrapper_identity(FRAMES[E], FRAMES[U], bad, r['right'], w)) + self.assertFalse(A.same_operator(A.canonical_frame(FRAMES[E]) + A.monomial(r['right']) + A.fourier(w) + + A.monomial(bad), A.canonical_frame(FRAMES[U]))) + + def test_lean_pairs_are_records(self): + cal = V.calibrate(R, ADAPTERS) + self.assertEqual(cal, RESULT['calibration']) + + def test_kernel_b_imports_only_the_standard_library(self): + tree = ast.parse((HERE / 'closed_form.py').read_text()) + mods = {a.name.split('.')[0] for n in ast.walk(tree) if isinstance(n, ast.Import) for a in n.names} + mods |= {n.module.split('.')[0] for n in ast.walk(tree) if isinstance(n, ast.ImportFrom)} + self.assertLessEqual(mods, {'hashlib', 'json'}) + + +class Controls(unittest.TestCase): + def test_recorded_controls_all_reject(self): + for name, value in RESULT['controls'].items(): + if name == 'producer_wrapper_checks': + continue + self.assertTrue(value.startswith('rejected') or value.startswith('other basis rejected'), name) + + def test_hyperplane_end_record_fails_against_full(self): + k = '0:1000' + E, U, w = parts(k) + r = REC[k] + self.assertFalse(A.same_operator(A.canonical_frame(FRAMES[E]) + A.monomial(r['right']) + A.fourier(9) + + A.monomial(r['left']), A.canonical_frame(FRAMES[1]))) + + def test_result_reports_all_records_exact(self): + self.assertEqual(RESULT['evaluation']['records'], 36) + self.assertTrue(RESULT['evaluation']['both_kernels']) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/frontier1094-residual-wrappers-seed62/verify.py b/research/frontier1094-residual-wrappers-seed62/verify.py new file mode 100644 index 0000000000..4414e28294 --- /dev/null +++ b/research/frontier1094-residual-wrappers-seed62/verify.py @@ -0,0 +1,312 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Supplier-boundary audit: the selected frontier1094 word's 36 residual wrappers are exact (no new kappa). + +Usage: python3 -I -B research/frontier1094-residual-wrappers-seed62/verify.py [--write] + +Lemma A's exact part needs, for every helper that enters at a nonzero frame E or ends below FULL at U, a stored wrapper +(L, R) with L o (C_[w] (x) I) o R = T_end o T_E^-1, w = dim end - dim E (end = FULL, or U for a hyperplane end). For the +selected gauge44 provider these 36 records live in RESIDUAL-ADAPTERS.json. The selected chain's own audit +(gauge44-slots-t16/code/audit_allcold.py) checks only their structural fields; their exactness rests on the producer's +WRAPPER-CHECKS.json, which the owner audit does not pin. This script: + + B binds the records: the merged #1781 binding (selected record -> frontier1094 certificate -> capsule -> owner audit + -> gauge44 word and programs), then RESIDUAL-ADAPTERS.json against the owner audit's own digest; the split-centres + decoy is rejected by digest and the global8 twin is byte-identical (informational); + I inventory: the 36 keys are exactly the word's entering / hyperplane-ending helpers' (start) and (start:final); + every record's frames, vectors and ranks match the word; every monomial is well formed; in both programs every + wrapped helper has one pre and one post residual event, with the right key; + FX calibrates the new closed-form kernel B (closed_form.py) on #702's 14 frame kernels and #1415's three operator + digests, and checks that records 2:999 and 3:998 are Exact.lean's pair 3 and pair 2; + E evaluates all 36 identities L o F_w o R o T_E = T_end exactly on all 512 columns, global phase included, with + kernel B (closed-form sparse amplitudes) and kernel A (#1781's packed evaluator); both must pass; + C semantic controls: each mutation is rejected on every record it applies to. + +Expected last line: PASS_FRONTIER1094_RESIDUAL_WRAPPERS_EXACT +""" +import argparse +import copy +import gzip +import hashlib +import io +import json +import sys +import tarfile +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P1781 = ROOT / 'research/frontier1094-recipes-exact-seed76' +sys.path.insert(0, str(HERE)) +import closed_form as B # noqa: E402 + +PREFIX = 'candidate/strict/' +MEMBERS = dict(adapters='global/base/providers/gauge44/RESIDUAL-ADAPTERS.json', + checks='global/base/providers/gauge44/WRAPPER-CHECKS.json', + decoy='global/base/split-centres/RESIDUAL-ADAPTERS.json', + twin='global8/base/providers/gauge44/RESIDUAL-ADAPTERS.json', + audit='global/audit/OWNERS-AND-PROFILE.json') +ARTIFACT = 'providers/gauge44/RESIDUAL-ADAPTERS.json' + + +class Reject(Exception): + """A check failed; the argument is the label of the check.""" + + +def need(ok, label): + if not ok: + raise Reject(label) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def load_1781(): + """import the merged #1781 package (binding helpers and kernel A) after checking its pinned digests.""" + pins = {f['path']: f['sha256'] for f in json.loads((HERE / 'SOURCES.json').read_text())['files']} + for name in ('verify.py', 'clifford.py', 'CASES.json'): + rel = 'research/frontier1094-recipes-exact-seed76/' + name + need(sha((ROOT / rel).read_bytes()) == pins[rel], 'B #1781 file pinned: ' + name) + import importlib.util + sys.path.insert(0, str(P1781)) + import clifford as A + spec = importlib.util.spec_from_file_location('verify_1781', P1781 / 'verify.py') # unique name: no clash with this file + R = importlib.util.module_from_spec(spec) + spec.loader.exec_module(R) + return R, A + + +def bind(R, archive_bytes=None, member_overrides=None): + data, binding = R.load() + arc = R.CASES['archive'] + raw = archive_bytes if archive_bytes is not None else (ROOT / arc['path']).read_bytes() + need(sha(raw) == arc['sha256'], 'B1 archive digest') + members = dict(MEMBERS, **(member_overrides or {})) + with tarfile.open(fileobj=io.BytesIO(raw), mode='r:gz') as tar: + index = R.safe_members(tar) + got = {k: tar.extractfile(index[PREFIX + p]).read() for k, p in members.items()} + audit = R.strict_loads(got['audit']) + need(audit['source_artifacts'][ARTIFACT] == sha(got['adapters']), 'B residual adapters pinned by the owner audit') + need(sha(got['decoy']) != audit['source_artifacts'][ARTIFACT], 'B the split-centres decoy differs by digest') + adapters = R.strict_loads(got['adapters']) + checks = R.strict_loads(got['checks']) + binding.update(residual_adapters_sha256=sha(got['adapters']), wrapper_checks_sha256=sha(got['checks']), + wrapper_checks_pinned_by_owner_audit=any(k.endswith('WRAPPER-CHECKS.json') for k in audit['source_artifacts']), + global8_twin_byte_identical=got['twin'] == got['adapters']) + return data, adapters, checks, binding + + +def end_of(key): + if ':' in key: + e, u = key.split(':') + return int(e), int(u) + return int(key), 1 + + +def inventory(A, word, programs, adapters): + v, R_ = word['v'], word['R'] + n = 2 * v + R_ + frames = word['frames'] + need(adapters['status'] == 'RESIDUAL_ADAPTER_RECIPES' and set(adapters) == {'recipes', 'status'}, 'I record file shape') + rec = adapters['recipes'] + starts = {str(word['start'][r]) for r in range(2 * v, n) if word['start'][r] != 0 and word['final'][r] == 1} + ends = {'%d:%d' % (word['start'][r], word['final'][r]) for r in range(2 * v, n) if word['final'][r] != 1} + need(set(rec) == starts | ends, 'I the 36 keys are the word\'s entering and hyperplane-ending helpers') + for k, r in rec.items(): + E, U = end_of(k) + w = len(frames[U]) - len(frames[E]) + need(r['frame'] == E and r['vectors'] == frames[E] and r['rank'] == w and r['entrance_rank'] == len(frames[E]), 'I record frames ' + k) + if ':' in k: + need(r['terminal'] == U and r['terminal_vectors'] == frames[U] and r['terminal_rank'] == len(frames[U]), 'I record end ' + k) + need(A.well_formed(r['left']) and A.well_formed(r['right']), 'I monomials well formed ' + k) + classes = Counter() + for r in range(2 * v, n): + s, f = word['start'][r], word['final'][r] + classes['cold_full' if s == 0 and f == 1 else 'enter_full' if f == 1 else 'cold_hpe' if s == 0 else 'enter_hpe'] += 1 + events = {} + for o in ('forward', 'backward'): + prog = programs[o] + touches = {} + for i, e in enumerate(prog): + if e[0] in ('climb', 'adapter', 'residual_adapter'): + touches.setdefault(e[2], []).append(i) + elif e[0] == 'scalar': + for a in e[1][1:3]: + if isinstance(a, list) and a[0] == 'L': + touches.setdefault(a[1], []).append(i) + res = [e for e in prog if e[0] == 'residual_adapter'] + pre = Counter(e[2] for e in res if e[1] == 'pre') + post = Counter(e[2] for e in res if e[1] == 'post') + wrapped = {r for r in range(2 * v, n) if word['start'][r] != 0 or word['final'][r] != 1} + need(set(pre) == set(post) == wrapped and set(pre.values()) == set(post.values()) == {1}, 'I one pre and one post per wrapped helper: ' + o) + for e in res: + r = e[2] + key = str(e[3]) if len(e) == 4 else '%d:%d' % (e[3], e[4]) + want = str(word['start'][r]) if word['final'][r] == 1 else '%d:%d' % (word['start'][r], word['final'][r]) + need(key == want and key in rec, 'I residual event key: ' + o) + bad = 0 + for r in wrapped: + idx = sorted(set(touches.get(r, ()))) + bad += not (prog[idx[0]][:2] == ['residual_adapter', 'pre'] and prog[idx[-1]][:2] == ['residual_adapter', 'post']) + need(bad == 0, 'I pre first and post last for every wrapped helper: ' + o) + widths = Counter(rec[str(e[3]) if len(e) == 4 else '%d:%d' % (e[3], e[4])]['rank'] for e in res) + events[o] = dict(pre=sum(pre.values()), post=sum(post.values()), wrapped_helpers=len(wrapped), + widths={str(k): x for k, x in sorted(widths.items())}) + kinds = Counter('full_end' if ':' not in k else 'cold_hpe' if k.startswith('0:') else 'enter_hpe' for k in rec) + return dict(records=len(rec), kinds=dict(sorted(kinds.items())), helper_classes=dict(sorted(classes.items())), events=events) + + +def calibrate(R, adapters): + out = {} + e702 = json.loads((ROOT / R.CASES['fixtures']['pr702']['path']).read_text())['identities'] + need(sha((ROOT / R.CASES['fixtures']['pr702']['path']).read_bytes()) == R.CASES['fixtures']['pr702']['sha256'], 'FX #702 pinned') + need(all(B.kernel_digest_702(i['frame']) == i['kernel_sha256'] for i in e702), 'FX kernel B reproduces #702') + out['pr702'] = 'kernel B reproduces all %d frame-kernel digests' % len(e702) + f1415 = json.loads((ROOT / R.CASES['fixtures']['pr1415']['path']).read_text())['factorizations'] + need(sha((ROOT / R.CASES['fixtures']['pr1415']['path']).read_bytes()) == R.CASES['fixtures']['pr1415']['sha256'], 'FX #1415 pinned') + for f in f1415: + d, dens, nz = B.matrix_digest_1415(f['entrance'], f['terminal']) + need(d == f['left']['matrix_sha256'] and dens == f['left']['denominator_exponents'] and nz == f['left']['nonzero_entries'], + 'FX kernel B reproduces #1415 pair %d' % f['pair']) + out['pr1415'] = 'kernel B reproduces the three operator digests of T_U o T_E^-1' + pairs = R.lean_fixtures() + rec = adapters['recipes'] + for key, k in (('3:998', 2), ('2:999', 3)): + p = pairs[k - 1] + need(rec[key]['vectors'] == p['E'] and rec[key]['terminal_vectors'] == p['U'] and rec[key]['left'] == p['L'] + and rec[key]['right'] == p['R'], 'FX record %s is Exact.lean pair %d' % (key, k)) + out['lean_pairs'] = 'records 3:998 and 2:999 equal Exact.lean pair 2 and pair 3 field by field' + return out + + +def evaluate(A, word, adapters): + frames = word['frames'] + out = {} + Ks = Counter() + for k, r in sorted(adapters['recipes'].items()): + E, U = end_of(k) + w = len(frames[U]) - len(frames[E]) + need(B.wrapper_identity(frames[E], frames[U], r['left'], r['right'], w) is None, 'E kernel B ' + k) + lhs = A.canonical_frame(frames[E]) + A.monomial(r['right']) + A.fourier(w) + A.monomial(r['left']) + rhs = A.canonical_frame(frames[U]) + need(A.same_operator(lhs, rhs), 'E kernel A ' + k) + Ks[max(A.c_gates(lhs), A.c_gates(rhs))] += 1 + out[k] = 'EXACT' + return dict(records=len(out), columns=B.DIM, global_phase_included=True, both_kernels=True, + K_histogram={str(k): x for k, x in sorted(Ks.items())}) + + +def _mut(m, field, fn): + m = copy.deepcopy(m) + m[field] = fn(m[field]) + return m + + +def controls(A, word, adapters, checks): + frames = word['frames'] + rec = adapters['recipes'] + + def ok(E, U, left, right, w): + return A.same_operator(A.canonical_frame(frames[E]) + A.monomial(right) + A.fourier(w) + A.monomial(left), + A.canonical_frame(frames[U])) + + def cz(Q): + Q = list(Q) + Q[6] ^= 1 << 7 + Q[7] ^= 1 << 6 + return Q + muts = { + 'global_phase': lambda L, R_, w: (L, _mut(R_, 'phase', lambda p: (p + 1) % 4), w), + 'input_character': lambda L, R_, w: (L, _mut(R_, 'linear_Z4', lambda a: [(a[0] + 2) % 4] + a[1:]), w), + 'cz_term': lambda L, R_, w: (_mut(L, 'quadratic_rows', cz), R_, w), + 'translation': lambda L, R_, w: (L, _mut(R_, 'offset', lambda b: b ^ 256), w), + 'swapped_wrappers': lambda L, R_, w: (R_, L, w), + 'width_off_by_one': lambda L, R_, w: (L, R_, w - 1 if w > 1 else w + 1), + 'transposed_matrix': lambda L, R_, w: (_mut(L, 'matrix_rows', lambda G: [sum(((G[j] >> i) & 1) << j for j in range(9)) for i in range(9)]), R_, w), + } + out = {} + for name, fn in muts.items(): + rej = tot = 0 + for k, r in rec.items(): + E, U = end_of(k) + w = len(frames[U]) - len(frames[E]) + L, R_, w2 = fn(r['left'], r['right'], w) + if L == r['left'] and R_ == r['right'] and w2 == w: + continue + tot += 1 + rej += not ok(E, U, L, R_, w2) + need(rej == tot, 'C control not rejected: ' + name) + out[name] = 'rejected %d/%d' % (rej, tot) + # hyperplane-end records evaluated against a FULL end; FULL-ended wrappers reused for a hyperplane end + hpe = [k for k in rec if ':' in k] + rej = sum(not ok(end_of(k)[0], 1, rec[k]['left'], rec[k]['right'], 9 - len(frames[end_of(k)[0]])) for k in hpe) + need(rej == len(hpe), 'C hyperplane-end record against FULL') + out['hpe_record_against_full_end'] = 'rejected %d/%d' % (rej, len(hpe)) + swap = [k for k in hpe if end_of(k)[0] != 0 and str(end_of(k)[0]) in rec] + rej = sum(not ok(end_of(k)[0], end_of(k)[1], rec[str(end_of(k)[0])]['left'], rec[str(end_of(k)[0])]['right'], + len(frames[end_of(k)[1]]) - len(frames[end_of(k)[0]])) for k in swap) + need(rej == len(swap), 'C FULL-ended wrapper used for a hyperplane end') + out['full_wrapper_for_hyperplane_end'] = 'rejected %d/%d' % (rej, len(swap)) + # frame basis: same span, other basis -> rejected; reordered rows -> passes + rej = passed = 0 + for k in ('0:124', '0:1000'): # end frames of dimension 4 and 8 + E, U = end_of(k) + r = rec[k] + tgt = U + alt = list(frames) + Uv = frames[tgt] + alt[tgt] = [Uv[0] ^ Uv[1]] + Uv[1:] + rej += not A.same_operator(A.canonical_frame(alt[E]) + A.monomial(r['right']) + A.fourier(len(frames[U]) - len(frames[E])) + + A.monomial(r['left']), A.canonical_frame(alt[U])) + alt[tgt] = list(reversed(Uv)) + passed += A.same_operator(A.canonical_frame(alt[E]) + A.monomial(r['right']) + A.fourier(len(frames[U]) - len(frames[E])) + + A.monomial(r['left']), A.canonical_frame(alt[U])) + need(rej == 2 and passed == 2, 'C frame basis control') + out['frame_basis'] = 'other basis rejected 2/2; reordered rows pass 2/2' + # kernel B also rejects: phase and width mutants on four records + sample = ['2', '423', '0:124', '0:1000'] + rej = 0 + for k in sample: + E, U = end_of(k) + r = rec[k] + w = len(frames[U]) - len(frames[E]) + rej += B.wrapper_identity(frames[E], frames[U], r['left'], _mut(r['right'], 'phase', lambda p: (p + 1) % 4), w) is not None + rej += B.wrapper_identity(frames[E], frames[U], r['left'], r['right'], w - 1) is not None + need(rej == 2 * len(sample), 'C kernel B rejects phase and width mutants') + out['kernel_B_mutants'] = 'rejected %d/%d' % (rej, 2 * len(sample)) + out['producer_wrapper_checks'] = dict(status=checks['status'], frames=checks['frames'], + hyperplane_end_pairs=len(checks['hyperplane_end_pairs'])) + return out + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.split('\n\n')[0]) + ap.add_argument('--write', action='store_true') + a = ap.parse_args() + R, A = load_1781() + data, adapters, checks, binding = bind(R) + inv = inventory(A, data['word'], data['programs'], adapters) + cal = calibrate(R, adapters) + ev = evaluate(A, data['word'], adapters) + ctrl = controls(A, data['word'], adapters, checks) + result = dict(status='PASS_FRONTIER1094_RESIDUAL_WRAPPERS_EXACT', binding=binding, inventory=inv, calibration=cal, + evaluation=ev, controls=ctrl, + 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') + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + target = HERE / 'RESULT.json' + if a.write: + target.write_text(text) + else: + need(target.read_text() == text, 'RESULT.json reproduced byte for byte') + print('records %d (%s) events %s' % (inv['records'], inv['kinds'], {o: (x['pre'], x['post']) for o, x in inv['events'].items()})) + print('PASS_FRONTIER1094_RESIDUAL_WRAPPERS_EXACT') + + +if __name__ == '__main__': + try: + main() + except Reject as exc: + raise SystemExit('FAIL ' + str(exc)) From da1bc730b9963f3e53538964d16364d2076a4e5d Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 23:38:56 +0530 Subject: [PATCH 2/2] Correct the supplier trace and overlap; cross-check kernel B against kernel A - The certificate's fresh invoice pins WRAPPER-CHECKS.json's bytes (now bound and recorded); the gap is that no chain code reads its status, and exactness comes only from the producer's own generation and decoding (re-run in the cold replay, verify_slots.py:103). - Overlap: #1697 covers 0:1000..0:1003 as hyperplane cases, #1611 tied 2:999 to Exact.lean pair 3; only the 22 FULL-ended records were producer-only. Byte-identical example corrected. - Kernel B's monomial and F_w are checked against kernel A on every column before evaluation; RESULT records per-kernel counts; dead adjoint removed. - Controls: width -1 and +1; residual events must be pre/post only; exact record field sets. 17 tests. - Credits: Lemma A (#516), producer hpe_adapters_local.py (DreamingOfClouds), PR425 (jacklightChen). --- .../README.md | 53 +++++++++++------- .../RESULT.json | 12 ++-- .../TASK.json | 12 ++-- .../closed_form.py | 12 ---- .../test_package.py | 15 ++++- .../verify.py | 56 +++++++++++++++---- 6 files changed, 103 insertions(+), 57 deletions(-) diff --git a/research/frontier1094-residual-wrappers-seed62/README.md b/research/frontier1094-residual-wrappers-seed62/README.md index bf9f90c955..a6738634d7 100644 --- a/research/frontier1094-residual-wrappers-seed62/README.md +++ b/research/frontier1094-residual-wrappers-seed62/README.md @@ -14,11 +14,13 @@ Lemma A's exact part (`research/e8-lemma-a-lean`, `research/e8-lemma-g-lean/PROO 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 that file through the owner audit's `source_artifacts`, but it does not check that the records are exact: +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 rests on a receipt the chain does not pin.** The only statement of exactness is the producer's own `WRAPPER-CHECKS.json` (`PASS_RESIDUAL_WRAPPERS_ARE_EXACT`, sha256 `0ae753d6`). The producer wrote it with its own Clifford code, and the owner audit does **not** pin it. -- **Later re-runs are not independent.** Re-runs such as #1646 and `selected-replay-fastpath` execute that same producer code. -- **#1781 (ours) left these records out** of its independent check. It covered the 2,896 child records and 224 endpoint adapters. +- **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 @@ -26,6 +28,7 @@ The selected chain binds that file through the owner audit's `source_artifacts`, - 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 @@ -34,7 +37,8 @@ The selected chain binds that file through the owner audit's `source_artifacts`, - 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, each of the 240 wrapped helpers has exactly one `pre` and one `post` residual event, 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}. +- **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: @@ -48,11 +52,10 @@ The selected chain binds that file through the owner audit's `source_artifacts`, 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 reproduce: -- #702's 14 frame-kernel digests; -- #1415's three operator digests of T_U ∘ T_E⁻¹, which exercise the adjoint. - -Separately, records `3:998` and `2:999` are field-for-field Exact.lean's pair 2 and pair 3. Their identities are Lean-proved. +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)) @@ -71,20 +74,24 @@ Each mutation below is rejected on every record it applies to: - a CZ term in Q; - an offset translation; - swapped wrappers; -- width ±1; +- 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 15 tests. +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 -- **Lean pairs.** `2:999` and `3:998` were already Lean-proved as Exact.lean pairs 3 and 2 (#593). Their semantic binding is #1415's. -- **Cold rank-4 records.** The eight cold rank-4 records `0:124`…`0:327` are byte-identical to records in earlier provider files, for example `research/community-k492-audit`. #702 checked the cold wrappers of that family by amplitudes, for PR626. -- **What is new.** The other 26 records (the 22 FULL-ended ones and `0:1000`…`0:1003`) had only producer evidence. All 36 are now checked for the **selected** word, from its bound bytes, by two kernels. +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 @@ -110,9 +117,9 @@ Requires standard-library Python 3.10 or later. It was run on Python 3.12.15 and - 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 `WRAPPER-CHECKS.json`, or this package's receipt, be bound by the owner audit?** - - Why it matters: the chain pins the records but not the producer's exactness receipt. - - First step: propose the binding at the next maintainer integration of frontier1094. +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. @@ -121,15 +128,19 @@ Requires standard-library Python 3.10 or later. It was run on Python 3.12.15 and ## Credit -- **Lemma A and Lemma G Lean packages, and the HPE wrapper tool:** DreamingOfClouds (#484/#509), following PR #458 (chafreaky). +- **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 producer:** `phases_full.py`/`clifford_exact.py` (icekylinx, from PR425). - **The packed kernel and binding:** our #1781. -- **Related checks:** #1697 (navinor; the cold hyperplane operators), #1611 (bbMisk; binding helper 450's wrapper pair), and #1964 (ours, open; Lemma G H1 extended labels). +- **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. diff --git a/research/frontier1094-residual-wrappers-seed62/RESULT.json b/research/frontier1094-residual-wrappers-seed62/RESULT.json index 52f898c9f4..b9b1ddede3 100644 --- a/research/frontier1094-residual-wrappers-seed62/RESULT.json +++ b/research/frontier1094-residual-wrappers-seed62/RESULT.json @@ -15,12 +15,14 @@ "review_sha256": "cb0e10a8b284f176526c17177e91186ce09aa3e88b4f6acc561051daa072b0d0", "slot_pins_sha256": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2", "template_sha256": "9c4c51425251389ee9a747c465814cd07c64812c15b7aeef704dad7d65395a74", - "wrapper_checks_pinned_by_owner_audit": false, + "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", + "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": { @@ -39,7 +41,8 @@ "swapped_wrappers": "rejected 36/36", "translation": "rejected 36/36", "transposed_matrix": "rejected 36/36", - "width_off_by_one": "rejected 36/36" + "width_minus_one": "rejected 36/36", + "width_plus_one": "rejected 36/36" }, "evaluation": { "K_histogram": { @@ -47,9 +50,10 @@ "8": 6, "9": 22 }, - "both_kernels": true, "columns": 512, "global_phase_included": true, + "kernel_A_exact": 36, + "kernel_B_exact": 36, "records": 36 }, "inventory": { diff --git a/research/frontier1094-residual-wrappers-seed62/TASK.json b/research/frontier1094-residual-wrappers-seed62/TASK.json index 196cbf6bde..34668b106a 100644 --- a/research/frontier1094-residual-wrappers-seed62/TASK.json +++ b/research/frontier1094-residual-wrappers-seed62/TASK.json @@ -41,14 +41,14 @@ }, "scope_status": "refined", "actual_scope": "One selected supplier obligation traced to its source-bound checks: Lemma A's exact part for the selected frontier1094 gauge44 word, i.e. the 36 stored residual wrappers (RESIDUAL-ADAPTERS.json) satisfy L o F_w o R o T_E = T_end exactly on all 512 columns with global phase, and are exactly the wrappers its programs use.", - "scope_change_reason": "Refined to the one obligation whose acceptance rests only on the producer's own check: the selected chain's audit (gauge44-slots-t16/code/audit_allcold.py) checks the wrappers' structural fields only, and their exactness comes from the producer's WRAPPER-CHECKS.json, which the owner audit does not pin. This was left open by our #1781.", + "scope_change_reason": "Refined to the one obligation whose acceptance rests only on the producer's own check: the chain pins the wrappers' bytes (owner audit; fresh invoice), its audit (gauge44-slots-t16/code/audit_allcold.py) checks only their structural fields, and their exactness is established only by the producer's own generation-and-decoding (WRAPPER-CHECKS.json, byte-pinned by the fresh invoice but never read for status). Left open by our #1781.", "bottleneck_link": "Side result on the selected record's soundness, no kappa change. Lemma A turns each entering or hyperplane-ending helper's residual into C_[w] (x) I through these wrappers; an error would leave ranks and the paid profile unchanged but break exact restoration. This gives the first independent, byte-bound check of all 36 for the selected word.", "budget_minutes": 180, "stop_rule": "Stop when all 36 records are exact under two calibrated kernels, the inventory ties them to the programs' residual events, and every mutation control is rejected.", "outcome": "completed", - "evidence": "RESULT.json: RESIDUAL-ADAPTERS 383f40aa pinned by the owner audit (WRAPPER-CHECKS 0ae753d6 is not); 36 records (22 FULL-ended, 12 cold hyperplane-end, 2 entering hyperplane-end) = the word's keys; 240 pre + 240 post residual events per orientation, keys correct, pre first and post last; kernel B reproduces #702 (14) and #1415 (3); 2:999 and 3:998 are Exact.lean pairs 3 and 2; all 36 identities exact on 512 columns with global phase under both kernels (K histogram 4:8, 8:6, 9:22); controls rejected: phase, input character, CZ term, translation, swapped wrappers, width, transposed matrix (36/36 each), hyperplane-end records against FULL (14/14), FULL wrapper reused for a hyperplane end (2/2), frame basis (2/2, reordered rows pass), kernel B mutants (8/8). 15 tests pass.", + "evidence": "RESULT.json: RESIDUAL-ADAPTERS 383f40aa pinned by the owner audit and the certificate's fresh invoice (which also pins WRAPPER-CHECKS 0ae753d6); 36 records (22 FULL-ended, 12 cold hyperplane-end, 2 entering hyperplane-end) = the word's keys, exact field sets; 240 pre + 240 post residual events per orientation (no other kind), keys correct, pre first and post last; kernel B reproduces #702 (14) and #1415 (3) and equals kernel A on monomials and F_w; 2:999 and 3:998 are Exact.lean pairs 3 and 2; all 36 identities exact on 512 columns with global phase under both kernels (36/36 each; K histogram 4:8, 8:6, 9:22); controls rejected: phase, input character, CZ term, translation, swapped wrappers, width -1, width +1, transposed matrix (36/36 each), hyperplane-end records against FULL (14/14), FULL wrapper reused for a hyperplane end (2/2), frame basis (2/2, reordered rows pass), kernel B mutants (8/8). Prior coverage: 2 Lean pairs, 8 records of #702's family, 4 hyperplane cases of #1697; the 22 FULL-ended records were producer-only. 17 tests pass.", "author": "Sagar Thakrar (thakrarsagar)", - "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents selected the obligation (both judges ranked it first) and traced the producer-only evidence; the closed-form kernel, verifier and controls were then written fresh, reusing our merged #1781 binding and packed kernel by import with pinned digests.", + "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents selected the obligation (both judges ranked it first) and traced the producer-only evidence; the closed-form kernel, verifier and controls were then written fresh, reusing our merged #1781 binding and packed kernel by import with pinned digests. A post-PR adversarial review corrected the supplier trace (fresh-invoice pin), the overlap (#1697, #1611) and credits, and added the kernel B/A cross-check and further controls (second commit).", "open_questions": [ { "question": "Does the emitted executor apply the records (child, endpoint and residual) with exactly these semantics?", @@ -57,9 +57,9 @@ "blocked_by": "An independent executor for the emitted program format." }, { - "question": "Should WRAPPER-CHECKS.json be bound by the owner audit like RESIDUAL-ADAPTERS.json?", - "why_it_matters": "The selected chain currently pins the records but not the producer's exactness receipt; this package now supplies an independent receipt.", - "first_step": "Propose adding this package's RESULT digest (or WRAPPER-CHECKS) to the frontier1094 integration record at the next maintainer integration.", + "question": "Should the chain check the exactness receipt's content, not just its bytes?", + "why_it_matters": "The fresh invoice pins WRAPPER-CHECKS.json, but no chain code reads its status; this package's RESULT is an independent receipt.", + "first_step": "Propose a status check, or this package's RESULT digest, at the next frontier1094 integration.", "blocked_by": "Maintainer decision." }, { diff --git a/research/frontier1094-residual-wrappers-seed62/closed_form.py b/research/frontier1094-residual-wrappers-seed62/closed_form.py index 89f86104bb..65634a94ac 100644 --- a/research/frontier1094-residual-wrappers-seed62/closed_form.py +++ b/research/frontier1094-residual-wrappers-seed62/closed_form.py @@ -118,18 +118,6 @@ def frame_column(U, x): return {y: v for y, v in col.items() if v != (0, 0)}, r -def frame_column_adjoint(U, x): - """column x of T_U^-1 = T_U^dagger (T_U is unitary): entry y is conj(T_U[x, y]).""" - r = len(U) - out = {} - for y in range(DIM): - col, e = frame_column(U, y) - if x in col: - re, im = col[x] - out[y] = (re, -im) - return out, r - - def monomial_apply(m, col): Q, a, G, b, p = m['quadratic_rows'], m['linear_Z4'], m['matrix_rows'], m['offset'], m['phase'] out = {} diff --git a/research/frontier1094-residual-wrappers-seed62/test_package.py b/research/frontier1094-residual-wrappers-seed62/test_package.py index 4388a7a9f5..4e9b7b0e96 100644 --- a/research/frontier1094-residual-wrappers-seed62/test_package.py +++ b/research/frontier1094-residual-wrappers-seed62/test_package.py @@ -41,7 +41,12 @@ def test_archive_byte_flip_rejected(self): def test_binding_recorded(self): self.assertEqual(BINDING['residual_adapters_sha256'], RESULT['binding']['residual_adapters_sha256']) - self.assertFalse(BINDING['wrapper_checks_pinned_by_owner_audit']) + self.assertFalse(BINDING['wrapper_checks_in_owner_audit']) + self.assertIn('fresh_invoice', BINDING['wrapper_checks_pinned_by']) + + def test_invoice_pin_mismatch_rejected(self): + with self.assertRaisesRegex(V.Reject, 'pinned by the fresh invoice|bound by the certificate'): + V.bind(R, member_overrides={'invoice': V.MEMBERS['audit']}) class Inventory(unittest.TestCase): @@ -96,8 +101,12 @@ def test_both_kernels_accept_samples_and_reject_a_phase_mutant(self): self.assertFalse(A.same_operator(A.canonical_frame(FRAMES[E]) + A.monomial(r['right']) + A.fourier(w) + A.monomial(bad), A.canonical_frame(FRAMES[U]))) + def test_kernel_b_monomial_and_fourier_match_kernel_a(self): + self.assertIn('equal kernel A', V.cross_check(A, WORD, ADAPTERS)) + def test_lean_pairs_are_records(self): cal = V.calibrate(R, ADAPTERS) + cal['kernel_B_vs_kernel_A'] = V.cross_check(A, WORD, ADAPTERS) self.assertEqual(cal, RESULT['calibration']) def test_kernel_b_imports_only_the_standard_library(self): @@ -122,8 +131,8 @@ def test_hyperplane_end_record_fails_against_full(self): + A.monomial(r['left']), A.canonical_frame(FRAMES[1]))) def test_result_reports_all_records_exact(self): - self.assertEqual(RESULT['evaluation']['records'], 36) - self.assertTrue(RESULT['evaluation']['both_kernels']) + ev = RESULT['evaluation'] + self.assertEqual((ev['records'], ev['kernel_A_exact'], ev['kernel_B_exact']), (36, 36, 36)) if __name__ == '__main__': diff --git a/research/frontier1094-residual-wrappers-seed62/verify.py b/research/frontier1094-residual-wrappers-seed62/verify.py index 4414e28294..517dd57f04 100644 --- a/research/frontier1094-residual-wrappers-seed62/verify.py +++ b/research/frontier1094-residual-wrappers-seed62/verify.py @@ -46,7 +46,8 @@ checks='global/base/providers/gauge44/WRAPPER-CHECKS.json', decoy='global/base/split-centres/RESIDUAL-ADAPTERS.json', twin='global8/base/providers/gauge44/RESIDUAL-ADAPTERS.json', - audit='global/audit/OWNERS-AND-PROFILE.json') + audit='global/audit/OWNERS-AND-PROFILE.json', + invoice='global/audit/PREFIX-AND-INVOICE.json') ARTIFACT = 'providers/gauge44/RESIDUAL-ADAPTERS.json' @@ -90,10 +91,18 @@ def bind(R, archive_bytes=None, member_overrides=None): audit = R.strict_loads(got['audit']) need(audit['source_artifacts'][ARTIFACT] == sha(got['adapters']), 'B residual adapters pinned by the owner audit') need(sha(got['decoy']) != audit['source_artifacts'][ARTIFACT], 'B the split-centres decoy differs by digest') + # the certificate's fresh invoice pins every provider file's bytes, WRAPPER-CHECKS.json included + asm = R.strict_loads((ROOT / R.CASES['certificate']).read_bytes()) + need(sha(got['invoice']) == asm['input_sha256']['fresh_invoice'], 'B fresh invoice bound by the certificate') + inv_art = R.strict_loads(got['invoice'])['providers']['gauge44']['artifacts'] + need(inv_art['RESIDUAL-ADAPTERS.json'] == sha(got['adapters']), 'B residual adapters pinned by the fresh invoice') + need(inv_art['WRAPPER-CHECKS.json'] == sha(got['checks']), 'B wrapper checks pinned by the fresh invoice') adapters = R.strict_loads(got['adapters']) checks = R.strict_loads(got['checks']) binding.update(residual_adapters_sha256=sha(got['adapters']), wrapper_checks_sha256=sha(got['checks']), - wrapper_checks_pinned_by_owner_audit=any(k.endswith('WRAPPER-CHECKS.json') for k in audit['source_artifacts']), + 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_in_owner_audit=any(k.endswith('WRAPPER-CHECKS.json') for k in audit['source_artifacts']), global8_twin_byte_identical=got['twin'] == got['adapters']) return data, adapters, checks, binding @@ -111,6 +120,9 @@ def inventory(A, word, programs, adapters): frames = word['frames'] need(adapters['status'] == 'RESIDUAL_ADAPTER_RECIPES' and set(adapters) == {'recipes', 'status'}, 'I record file shape') rec = adapters['recipes'] + base = {'entrance_rank', 'frame', 'left', 'rank', 'right', 'vectors'} + for k, r in rec.items(): + need(set(r) == (base | {'terminal', 'terminal_rank', 'terminal_vectors'} if ':' in k else base), 'I record keys ' + k) starts = {str(word['start'][r]) for r in range(2 * v, n) if word['start'][r] != 0 and word['final'][r] == 1} ends = {'%d:%d' % (word['start'][r], word['final'][r]) for r in range(2 * v, n) if word['final'][r] != 1} need(set(rec) == starts | ends, 'I the 36 keys are the word\'s entering and hyperplane-ending helpers') @@ -137,10 +149,12 @@ def inventory(A, word, programs, adapters): if isinstance(a, list) and a[0] == 'L': touches.setdefault(a[1], []).append(i) res = [e for e in prog if e[0] == 'residual_adapter'] + need(all(e[1] in ('pre', 'post') and len(e) in (4, 5) for e in res), 'I residual events are pre or post: ' + o) pre = Counter(e[2] for e in res if e[1] == 'pre') post = Counter(e[2] for e in res if e[1] == 'post') wrapped = {r for r in range(2 * v, n) if word['start'][r] != 0 or word['final'][r] != 1} - need(set(pre) == set(post) == wrapped and set(pre.values()) == set(post.values()) == {1}, 'I one pre and one post per wrapped helper: ' + o) + need(set(pre) == set(post) == wrapped and set(pre.values()) == set(post.values()) == {1} + and len(res) == 2 * len(wrapped), 'I one pre and one post per wrapped helper: ' + o) for e in res: r = e[2] key = str(e[3]) if len(e) == 4 else '%d:%d' % (e[3], e[4]) @@ -170,7 +184,7 @@ def calibrate(R, adapters): d, dens, nz = B.matrix_digest_1415(f['entrance'], f['terminal']) need(d == f['left']['matrix_sha256'] and dens == f['left']['denominator_exponents'] and nz == f['left']['nonzero_entries'], 'FX kernel B reproduces #1415 pair %d' % f['pair']) - out['pr1415'] = 'kernel B reproduces the three operator digests of T_U o T_E^-1' + out['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)' pairs = R.lean_fixtures() rec = adapters['recipes'] for key, k in (('3:998', 2), ('2:999', 3)): @@ -181,21 +195,39 @@ def calibrate(R, adapters): return out +def cross_check(A, word, adapters): + """kernel B's monomial and F_w against kernel A's on every column of sample records (the frame operator is + calibrated on #702 / #1415 separately).""" + rec = adapters['recipes'] + for k in ('2', '423', '0:124', '0:1000', '3:998'): + for side in ('left', 'right'): + m = rec[k][side] + cols = A.columns(A.run(A.monomial(m), A.radix(0)), A.radix(0)) + for x in range(B.DIM): + need(B.monomial_apply(m, {x: (1, 0)}) == cols.get(x, {}), 'FX kernel B monomial = kernel A: ' + k) + for w in (1, 4, 8, 9): + cols = A.columns(A.run(A.fourier(w), A.radix(w)), A.radix(w)) + for x in (0, 1, 77, 300, 511): + col, e = B.fourier_apply(w, {x: (1, 0)}, 0) + need(e == w and col == cols.get(x, {}), 'FX kernel B F_w = kernel A') + return 'kernel B monomials (10, all columns) and F_w (w = 1, 4, 8, 9) equal kernel A' + + def evaluate(A, word, adapters): frames = word['frames'] - out = {} + nA = nB = 0 Ks = Counter() for k, r in sorted(adapters['recipes'].items()): E, U = end_of(k) w = len(frames[U]) - len(frames[E]) - need(B.wrapper_identity(frames[E], frames[U], r['left'], r['right'], w) is None, 'E kernel B ' + k) + nB += B.wrapper_identity(frames[E], frames[U], r['left'], r['right'], w) is None lhs = A.canonical_frame(frames[E]) + A.monomial(r['right']) + A.fourier(w) + A.monomial(r['left']) rhs = A.canonical_frame(frames[U]) - need(A.same_operator(lhs, rhs), 'E kernel A ' + k) + nA += A.same_operator(lhs, rhs) Ks[max(A.c_gates(lhs), A.c_gates(rhs))] += 1 - out[k] = 'EXACT' - return dict(records=len(out), columns=B.DIM, global_phase_included=True, both_kernels=True, - K_histogram={str(k): x for k, x in sorted(Ks.items())}) + need(nA == nB == len(adapters['recipes']), 'E both kernels accept every record') + return dict(records=len(adapters['recipes']), kernel_A_exact=nA, kernel_B_exact=nB, columns=B.DIM, + global_phase_included=True, K_histogram={str(k): x for k, x in sorted(Ks.items())}) def _mut(m, field, fn): @@ -223,7 +255,8 @@ def cz(Q): 'cz_term': lambda L, R_, w: (_mut(L, 'quadratic_rows', cz), R_, w), 'translation': lambda L, R_, w: (L, _mut(R_, 'offset', lambda b: b ^ 256), w), 'swapped_wrappers': lambda L, R_, w: (R_, L, w), - 'width_off_by_one': lambda L, R_, w: (L, R_, w - 1 if w > 1 else w + 1), + 'width_minus_one': lambda L, R_, w: (L, R_, w - 1), + 'width_plus_one': lambda L, R_, w: (L, R_, w + 1), 'transposed_matrix': lambda L, R_, w: (_mut(L, 'matrix_rows', lambda G: [sum(((G[j] >> i) & 1) << j for j in range(9)) for i in range(9)]), R_, w), } out = {} @@ -289,6 +322,7 @@ def main(): data, adapters, checks, binding = bind(R) inv = inventory(A, data['word'], data['programs'], adapters) cal = calibrate(R, adapters) + cal['kernel_B_vs_kernel_A'] = cross_check(A, data['word'], adapters) ev = evaluate(A, data['word'], adapters) ctrl = controls(A, data['word'], adapters, checks) result = dict(status='PASS_FRONTIER1094_RESIDUAL_WRAPPERS_EXACT', binding=binding, inventory=inv, calibration=cal,