From 157a7239166b8fe640edb232f5eee9a4b2579569 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Wed, 14 Oct 2026 15:13:13 -0400 Subject: [PATCH] Add heterogeneous 3|7 two-bank order-four boundary package (persistent-boundary card) --- .../z4-hetero-two-bank-seedba18/NOTICE.md | 27 + .../z4-hetero-two-bank-seedba18/README.md | 144 +++++ .../z4-hetero-two-bank-seedba18/RESULT.json | 258 ++++++++ .../z4-hetero-two-bank-seedba18/SOURCES.json | 65 ++ .../z4-hetero-two-bank-seedba18/TASK.json | 64 ++ .../z4-hetero-two-bank-seedba18/VERIFY.json | 22 + .../inputs/PR1391/CERTIFICATE.json | 240 +++++++ .../inputs/PR1391/verify.py | 606 ++++++++++++++++++ .../inputs/PR1410-README.md | 67 ++ .../z4-hetero-two-bank-seedba18/verify.py | 603 +++++++++++++++++ 10 files changed, 2096 insertions(+) create mode 100644 research/z4-hetero-two-bank-seedba18/NOTICE.md create mode 100644 research/z4-hetero-two-bank-seedba18/README.md create mode 100644 research/z4-hetero-two-bank-seedba18/RESULT.json create mode 100644 research/z4-hetero-two-bank-seedba18/SOURCES.json create mode 100644 research/z4-hetero-two-bank-seedba18/TASK.json create mode 100644 research/z4-hetero-two-bank-seedba18/VERIFY.json create mode 100644 research/z4-hetero-two-bank-seedba18/inputs/PR1391/CERTIFICATE.json create mode 100644 research/z4-hetero-two-bank-seedba18/inputs/PR1391/verify.py create mode 100644 research/z4-hetero-two-bank-seedba18/inputs/PR1410-README.md create mode 100644 research/z4-hetero-two-bank-seedba18/verify.py diff --git a/research/z4-hetero-two-bank-seedba18/NOTICE.md b/research/z4-hetero-two-bank-seedba18/NOTICE.md new file mode 100644 index 0000000000..25326971ab --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/NOTICE.md @@ -0,0 +1,27 @@ +# NOTICE + +Prepared by **Aaron Wang**, with help from opencode (substantial AI assistance; no +independent human review or proof-assistant formalization is claimed). New material +is Apache-2.0 under the repository license. + +Pinned predecessor material (byte copies under `inputs/`, hashes in `SOURCES.json`): + +- PR #1391 (Cinna Davis / 1337isnot1337), head + `6ce8017e4c27c8b220b6c3a27a53bb18f138212a`: the order-four child family and its + basis replay, via `inputs/PR1391/CERTIFICATE.json` and `inputs/PR1391/verify.py` + (snapshots as retained by `research/z4-distinct-source-seed55/inputs/PR1391/`). +- PR #1410 (Cinna Davis), head `5b1c00b9f2770aabaa0085539405757f7818a14a`: the + same-source persistent boundary, via `inputs/PR1410-README.md`. +- `research/z4-distinct-source-seed55` (Cinna Davis): the phase-indexed typed child + contract `C_(i,t)`, the exact boundary recurrence, the two-bank wrapper/handoff + accounting and the 5|5 construction this package reproduces as its positive + control. The model loader and word machinery in `verify.py` follow that package's + `verify.py` with attribution. +- `research/z4-heterogeneous-pair-seed3x7` (PR #1768, 1337isnot1337): the + heterogeneous 3+7 reader schedules `[0,1,2]` and `[2,1,0,2,1,0,2]`. +- `research/z4-persistent-pair-seed57` (PR #1410 package, Cinna Davis): the paired + order-four boundary lineage, credited through the pinned README snapshot. + +Selected-result context: Rohan Arun's PR #1094 on Jeremy Kothe's #1087 construction, +resolved through `certificates/selected-result.json`; nothing in this package +changes it. No κ, supplier, moment or frontier claim is made. diff --git a/research/z4-hetero-two-bank-seedba18/README.md b/research/z4-hetero-two-bank-seedba18/README.md new file mode 100644 index 0000000000..a3c591cf70 --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/README.md @@ -0,0 +1,144 @@ +# Heterogeneous 3+7 echoes on two distinct source banks share one order-four boundary + +**Scoped recursive-interface construction and exact finite law. No new κ, supplier +admission, or change to the selected result.** Agent: **Aaron Wang**, with help from +opencode (substantial AI assistance; no independent human review is claimed). + +## Object + +This package fills the one uncovered cell of the pinned PR1391 order-four typed +boundary interface. On that interface, two consecutive root echoes can share one +carried workspace phase instead of paying two independent boundary schedules: + +- `research/z4-persistent-pair-seed57` and `research/z4-heterogeneous-pair-seed3x7`: + two calls on **one shared source** (identical 5|5, then heterogeneous 3|7 with the + canonical phase path); +- `research/z4-distinct-source-seed55`: two **identical** five-child calls on **two + distinct source banks**, with the handoff at the 5|5 midpoint. + +Missing until now: **heterogeneous reader schedules across two distinct source +banks**, where the source handoff sits at an asymmetric boundary. Here type A has +three children reading source octets `[0,1,2]` of bank `X`; type B has seven children +reading `[2,1,0,2,1,0,2]` of bank `Y`; one arbitrary dirty output octet `D` and one +24-coordinate arbitrary dirty workspace `W` must both be restored exactly. + +## Construction + +The child family is the pinned phase-indexed typed child +`C_(i,t): D += Q^(-t) R_i W; W += (P-I)W` of `research/z4-distinct-source-seed55` +(the identity `Q^(-t) R_i P^t = R_i` is re-checked here for all 12 +phase/reader pairs over blocks `{0,1,2}`). The joint word is one ten-child typed +echo over the concatenated schedule `[0,1,2,2,1,0,2,1,0,2]`, with the charged +source handoff `W += P^t (Y-X)` placed after child 2 — the 3|7 boundary, at +workspace phase `t = 1` on the optimal path — instead of the midpoint. As in the +predecessor, the complete call copies `X` in, runs the typed body, applies the +handoff and the `Y` restore, and closes with the literal inverse body. + +## Exact results + +Child cost is the pinned leaf `(62,6)`, each single-source call pays a `2d = 48` +ADD copy/restore wrapper, and the two-source handoff costs 48 ADDs. The workspace +boundary charge `g(k)` comes from the exact recurrence +`F_0(t) = A(t)`, `F_(j+1)(s) = min_t F_j(t) + A((s-t-1) mod 4)`, terminal phase `0`, +with `A = [(0,0),(54,6),(36,12),(54,6)]`. + +| Execution | ADD | NEG | Primitives | Reads | Prefix row-L1 peak | Map | +|---|---:|---:|---:|---:|---:|---| +| A then B, separate (3 and 7 children) | 1,552 | 144 | 1,696 | 3,248 | 18 | pass, 80 columns | +| Joint ten-child, asymmetric 3-to-7 handoff | 1,408 | 144 | **1,552** | **2,960** | 21 | pass, 80 columns | +| 5-to-5 predecessor control (reproduced) | 1,552 → 1,408 | 144 | 1,696 → 1,552 | 3,248 → 2,960 | 16 → 21 | pass, 80 columns | +| 2-to-8 even split (both words) | 1,408 | 144 | 1,552 | 2,960 | — | pass, 80 columns | + +The joint 3|7 call **saves 144 primitives and 288 reads** against the two separate +calls, with both sources read-only, all four banks arbitrary dirty, and the exact +map `(D,X,Y,W) -> (D + sum_{b in [0,1,2]} R_b X + sum_{b in [2,1,0,2,1,0,2]} R_b Y, X, Y, W)` +checked on all 80 basis columns. The 5|5 row reproduces +`research/z4-distinct-source-seed55`'s published figures exactly (positive control). + +## Boundary law (exact for this interface) + +Because `A` has period 4 under the min-plus recurrence, `g(k) = g(k mod 4)`: +`g(0) = (0,0)`, `g(1) = g(3) = (54,6)`, `g(2) = (36,12)` (checked against exhaustive +coverage at `k = 3, 5, 7, 10`: 64 + 1,024 + 16,384 + 1,048,576 phase paths, and for +`k = 1..16` by the recurrence). The complete charged invoice of the two-bank pair +therefore obeys + +`separate(k1,k2) - joint(k1,k2) = 2 * (g(k1) + g(k2) - g(k1+k2))`. + +For `k1 + k2 = 10` this saving is **144 primitives exactly when both child counts +are odd, and 0 when both are even**. The emitted-word checks confirm both sides: +the 3|7 pair realizes the full 144, while the 2|8 pair (same banks, same child +family, handoff after child 1) is a legal composition whose two invoices are +identical — it merges no boundary work. The heterogeneous invoice is also identical +to the 5|5 invoice: on this interface the saving depends on the parities of the +child counts, not on how the children are distributed between the calls. + +## Controls and evidence + +`verify.py` re-checks the pinned PR1391/PR1410 input blobs and the selected-record +hash at base `e112d71c8d7bb32435debcc54df932593dd8223a`, the 12 typed-child +identities and gate counts, recurrence-versus-exhaustive agreement at all four +sizes, and six negative controls on the 3|7 cell: switching at the midpoint +instead of the 3|7 boundary, a wrong handoff phase, a mutated A-side reader, an +omitted B call, a missing terminal `Y` restoration, and a missing literal inverse — +each rejected by the exact map. `RESULT.json` is the recomputed evidence and must +match byte-for-byte on a second run. + +## Reproduce + +```sh +python3 -I -B research/z4-hetero-two-bank-seedba18/verify.py +python3 -B scripts/research_package.py --package research/z4-hetero-two-bank-seedba18 --check-only +``` + +Expected marker: + +```text +PASS_Z4_HETERO_TWO_BANK_3_7 g3=60 g7=60 g10=48 separate=1696 joint=1552 saved=144 reads_saved=288 law=odd_splits_only even28_saved=0 paths=64+1024+16384+1048576 basis=80 controls=6 +``` + +The registered package replay is declared for Python 3.12 in `VERIFY.json`; the +local runs above used CPython 3.12 as well. + +## Scope and limits + +The result is exact for the declared order-four phase-indexed child alphabet and +these fixed reader schedules. It is not a lower bound for arbitrary ADD/NEG words. +Output-row reindexing is free in this word model (it is the typed ADD target); +address calculation, physical row routing, source hosting, tape travel, +fixed-precision admission, recursive assembly into a selected supplier and analytic +transfer are unproved. The joint word raises the prefix row-L1 peak from 18 to 21, +so precision remains a live obligation. No κ, selected moment, supplier or frontier +change is claimed. + +## Open next questions + +- **Can a named selected supplier realize the heterogeneous typed readers at the + 3|7 handoff?** This matters because the 144-primitive saving transfers to a + recursive profile only through an admitted supplier. A feasible first step is to + extract one retained #1094 child matrix and test `Q^(-t) R_b P^t = R_b` for the + block schedules `[0,1,2]` and `[2,1,0,2,1,0,2]`, then price the handoff routing. + Blocked by: no physical host, tape schedule or precision-admitted supplier for the + paired order-four interface exists yet; both predecessor packages record the same + blocker. +- **Is the parity law sharp beyond the fixed ten-child total?** The identity + `separate - joint = 2(g(k1)+g(k2)-g(k1+k2))` is proved for this alphabet at the + invoice level; whether any non-typed schedule beats `g` at odd/odd splits is open. + A first step is an exhaustive search over non-typed boundary words at `k = 3`. + Blocked by: the typed recurrence is optimal only within the typed alphabet; a + different reader family needs its own model. + +## Credit + +The order-four child emitter, the typed reader identity and the two-bank handoff +mechanism are Cinna Davis's (1337isnot1337), from PR #1391, PR #1410 and the +packages `research/z4-paired-frame-restoration-seed56`, +`research/z4-persistent-pair-seed57`, `research/z4-distinct-source-seed55`; the +heterogeneous 3|7 reader schedule is from +`research/z4-heterogeneous-pair-seed3x7` (PR #1768). All are pinned byte-for-byte +in `inputs/` and `SOURCES.json`. The new material here is the heterogeneous +two-bank composition with the asymmetric handoff, the exact map and invoice checks +for it, the period-4 boundary law with its odd/even saving classification, and the +2|8 zero-saving control. Prepared by **Aaron Wang** with help from opencode. +New material is Apache-2.0; the repository license and all source attribution are +retained. diff --git a/research/z4-hetero-two-bank-seedba18/RESULT.json b/research/z4-hetero-two-bank-seedba18/RESULT.json new file mode 100644 index 0000000000..d5af2260e8 --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/RESULT.json @@ -0,0 +1,258 @@ +{ + "assignment": { + "card_selection_note": "second-choice card after the centre-path-sharing pair collision", + "chooser_nonce": "ba18ac446df7d55ddc50d91395fd9a57", + "priority_revision": 3, + "scope_key": "026be4b6e61971d51838", + "task_id": "persistent-boundary", + "track": "recursive-interfaces" + }, + "assumptions_and_limits": [ + "Output-row reindexing is part of the typed ADD target choice and has no additional scalar ADD/NEG instruction in this word model.", + "Address, tape, source-hosting, precision admission, recursive assembly into a selected supplier and analytic transfer are not charged or proved.", + "The joint word raises the prefix row-L1 envelope; no precision improvement is claimed.", + "The finite recurrence is exact only for the declared order-four phase-indexed child alphabet; it is not a lower bound for arbitrary words.", + "No new kappa or selected-result change is claimed." + ], + "base_commit": "e112d71c8d7bb32435debcc54df932593dd8223a", + "controls": { + "exhaustive_phase_coverage": "PASS at 64 + 1024 + 16384 + 1048576 paths", + "midpoint_switch_instead_of_3_7_boundary": "REJECTED", + "missing_final_Y_restoration": "REJECTED", + "missing_literal_inverse": "REJECTED", + "mutated_A_reader": "REJECTED", + "omitted_B_call": "REJECTED", + "predecessor_5_5_invoices_and_maps": "PASS", + "typed_child_phase_identity_checks": "PASS for 12 (phase,reader) pairs", + "wrong_handoff_phase": "REJECTED" + }, + "dimensions": { + "D": 8, + "W": 24, + "X": 24, + "Y": 24, + "total_basis_columns": 80 + }, + "even_split_2_8_control": { + "A_blocks": [ + 0, + 1 + ], + "B_blocks": [ + 2, + 1, + 0, + 2, + 1, + 0, + 2, + 2 + ], + "joint_ADD_NEG": { + "ADD": 1408, + "NEG": 144 + }, + "map": "PASS on all 80 basis columns for both words", + "meaning": "even splits merge no boundary work; the 144 saving needs both child counts odd", + "saving": { + "primitives": 0, + "reads": 0 + }, + "separate_ADD_NEG": { + "ADD": 1408, + "NEG": 144 + } + }, + "joint_3_7_two_banks": { + "ADD_NEG": { + "ADD": 1408, + "NEG": 144 + }, + "map": "PASS on all 80 basis columns", + "prefix_row_l1_peak": 21, + "primitives": 1552, + "reads": 2960 + }, + "phase_reader": "C_(i,t): D += Q^(-t) R_i W; W += (P-I)W; type t has same ADD/NEG count as C_i.", + "predecessor_5_5_control": { + "joint_ADD_NEG": { + "ADD": 1408, + "NEG": 144 + }, + "joint_primitives": 1552, + "map": "PASS on all 80 basis columns", + "matches_research/z4-distinct-source-seed55": true, + "separate_ADD_NEG": { + "ADD": 1552, + "NEG": 144 + }, + "separate_primitives": 1696 + }, + "predecessors": { + "PR1391_certificate_sha256": "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3", + "PR1391_head": "6ce8017e4c27c8b220b6c3a27a53bb18f138212a", + "PR1391_verifier_sha256": "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05", + "PR1410_head": "5b1c00b9f2770aabaa0085539405757f7818a14a", + "PR1410_readme_sha256": "6dda7d5b83b41c71d73711401edbc146271a546a518ef6b038b0bdbb6578d405", + "nearest_packages": [ + "research/z4-distinct-source-seed55 (typed two-bank 5|5, midpoint handoff)", + "research/z4-heterogeneous-pair-seed3x7 (heterogeneous 3|7, one shared source, canonical phase path)" + ] + }, + "recurrence": { + "F0(t)": "A(t)", + "Fnext(s)": "min_t F(t)+A((s-t-1) mod 4)", + "g10_ADD_NEG": { + "ADD": 36, + "NEG": 12 + }, + "g10_exhaustive_paths": 1048576, + "g10_path": [ + 0, + 1, + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 0 + ], + "g3_ADD_NEG": { + "ADD": 54, + "NEG": 6 + }, + "g3_exhaustive_paths": 64, + "g3_path": [ + 0, + 1, + 2, + 0 + ], + "g5_ADD_NEG": { + "ADD": 54, + "NEG": 6 + }, + "g5_exhaustive_paths": 1024, + "g5_path": [ + 0, + 0, + 1, + 2, + 3, + 0 + ], + "g7_ADD_NEG": { + "ADD": 54, + "NEG": 6 + }, + "g7_exhaustive_paths": 16384, + "g7_path": [ + 0, + 1, + 2, + 0, + 1, + 2, + 3, + 0 + ], + "period_4_law": "g(k) = g(k mod 4) with g(0) = (0,0); checked for k = 1..16", + "split_invoice_law": "separate(k1,k2) - joint(k1,k2) = 2*(g(k1)+g(k2)-g(10)); at total 10 this is 144 ADDs iff both child counts are odd and 0 when both are even", + "split_law_vectors": { + "1": { + "ADD": 144, + "NEG": 0 + }, + "2": { + "ADD": 0, + "NEG": 0 + }, + "3": { + "ADD": 144, + "NEG": 0 + }, + "4": { + "ADD": 0, + "NEG": 0 + }, + "5": { + "ADD": 144, + "NEG": 0 + }, + "6": { + "ADD": 0, + "NEG": 0 + }, + "7": { + "ADD": 144, + "NEG": 0 + }, + "8": { + "ADD": 0, + "NEG": 0 + }, + "9": { + "ADD": 144, + "NEG": 0 + } + }, + "terminal_phase": 0, + "workspace_phase_costs_ADD_NEG": [ + { + "ADD": 0, + "NEG": 0 + }, + { + "ADD": 54, + "NEG": 6 + }, + { + "ADD": 36, + "NEG": 12 + }, + { + "ADD": 54, + "NEG": 6 + } + ] + }, + "saving": { + "primitives": 144, + "reads": 288 + }, + "scope": "Exact phase-indexed typed child family with heterogeneous reader schedules on two distinct source banks; not an admitted selected supplier.", + "separate_calls": { + "ADD_NEG": { + "ADD": 1552, + "NEG": 144 + }, + "map": "PASS on all 80 basis columns", + "prefix_row_l1_peak": 18, + "primitives": 1696, + "reads": 3248 + }, + "status": "PASS_Z4_HETERO_TWO_BANK_3_7", + "types": { + "A_blocks": [ + 0, + 1, + 2 + ], + "A_source": "X", + "B_blocks": [ + 2, + 1, + 0, + 2, + 1, + 0, + 2 + ], + "B_source": "Y", + "handoff": "W += P^t (Y-X) after child 2, t = phase[3]; 48 ADDs", + "handoff_phase": 1 + } +} diff --git a/research/z4-hetero-two-bank-seedba18/SOURCES.json b/research/z4-hetero-two-bank-seedba18/SOURCES.json new file mode 100644 index 0000000000..6dcb4c0839 --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/SOURCES.json @@ -0,0 +1,65 @@ +{ + "base_commit": "e112d71c8d7bb32435debcc54df932593dd8223a", + "external_sources": [ + { + "commit": "6ce8017e4c27c8b220b6c3a27a53bb18f138212a", + "git_blob": "0132b117d90f1a7a97c40af3e38503c117604e00", + "local_path": "research/z4-hetero-two-bank-seedba18/inputs/PR1391/CERTIFICATE.json", + "path": "research/z4-paired-frame-restoration-seed56/CERTIFICATE.json", + "repository": "CrocSwap/integer-mult-bounds", + "role": "exact predecessor child and recurrence certificate (byte copy of research/z4-distinct-source-seed55/inputs/PR1391/CERTIFICATE.json)", + "sha256": "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3" + }, + { + "commit": "6ce8017e4c27c8b220b6c3a27a53bb18f138212a", + "git_blob": "9d866bbf57a6d1f012a21687bde2e231c90efd14", + "local_path": "research/z4-hetero-two-bank-seedba18/inputs/PR1391/verify.py", + "path": "research/z4-paired-frame-restoration-seed56/verify.py", + "repository": "CrocSwap/integer-mult-bounds", + "role": "pinned signed-ADD child word and basis replay (byte copy of research/z4-distinct-source-seed55/inputs/PR1391/verify.py)", + "sha256": "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05" + }, + { + "commit": "5b1c00b9f2770aabaa0085539405757f7818a14a", + "git_blob": "001929a89cd64f4bbb0d4194c6bde96f45b7ded2", + "local_path": "research/z4-hetero-two-bank-seedba18/inputs/PR1410-README.md", + "path": "research/z4-persistent-pair-seed57/README.md", + "repository": "CrocSwap/integer-mult-bounds", + "role": "same-source persistent-boundary predecessor snapshot (byte copy of research/z4-distinct-source-seed55/inputs/PR1410-README.md)", + "sha256": "6dda7d5b83b41c71d73711401edbc146271a546a518ef6b038b0bdbb6578d405" + } + ], + "files": [ + { + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "path": "docs/research/agent-task-catalog.json", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "usage": "provenance" + }, + { + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "path": "certificates/selected-result.json", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "usage": "provenance" + }, + { + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "path": "docs/research/community-batch1099-review.md", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb", + "usage": "provenance" + }, + { + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b", + "usage": "provenance" + }, + { + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/z4-hetero-two-bank-seedba18/TASK.json b/research/z4-hetero-two-bank-seedba18/TASK.json new file mode 100644 index 0000000000..a9f2805ec6 --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/TASK.json @@ -0,0 +1,64 @@ +{ + "actual_scope": "For the pinned PR1391 order-four child family, compose two consecutive root echoes with heterogeneous reader schedules on two distinct source banks: type A has three children reading source octets [0,1,2] of bank X, type B has seven children reading [2,1,0,2,1,0,2] of bank Y. Compare the two separate typed root calls with one joint ten-child phase-indexed echo whose charged 48-ADD source handoff sits at the 3|7 boundary rather than the midpoint, and verify the exact arbitrary-dirty map on all 80 basis columns.", + "ai_assistance": "Substantial AI assistance: with help from opencode, in derivation, construction, exact verifier implementation, source pinning and prose. No independent human review or proof-assistant formalization is claimed.", + "author": "Aaron Wang", + "base_commit": "e112d71c8d7bb32435debcc54df932593dd8223a", + "bottleneck_link": "The typed boundary carries one workspace phase across both calls and removes the per-call workspace restoration and boundary re-schedule. The complete recurrence prices the eliminated boundary work against the 48-ADD source handoff; supplier routing, precision and tape admission decide whether any of it can transfer to a multiplication profile.", + "budget_minutes": 60, + "card_selection_note": "First-choice card centre-path-sharing matched already-claimed recent objects (centre-sharing claims in discussion 1166 at 12:58 and 13:03 UTC on 2026-10-14), so per the pair-collision rule the second-choice card persistent-boundary was taken. Recorded as a card-level scope change.", + "chooser_nonce": "ba18ac446df7d55ddc50d91395fd9a57", + "evidence": "The exact 80x80 maps pass for the 3|7 separate calls and the joint ten-child call with the handoff at the 3|7 boundary. Complete vectors are (1552,144) = 1,696 primitives / 3,248 reads separate and (1408,144) = 1,552 / 2,960 joint, saving 144 primitives and 288 reads; prefix row-L1 peaks 18 -> 21. The period-4 boundary law g(k) = g(k mod 4) is checked against exhaustive coverage at 64 + 1024 + 16384 + 1048576 phase paths and for k = 1..16. The predecessor 5|5 figures reproduce exactly. The 2|8 even-split word pair passes both maps with zero saving, confirming that the 144 saving needs both child counts odd. Six negative controls reject.", + "open_questions": [ + { + "blocked_by": "No physical host, tape schedule or precision-admitted supplier for the paired order-four interface has been identified; both predecessor packages record the same blocker.", + "first_step": "Extract one exact child matrix from the retained #1094 supplier inventory, test Q^(-t)R_b P^t = R_b for the blocks [0,1,2] and [2,1,0,2,1,0,2], then price the 3|7 handoff routing and the prefix coefficient envelope.", + "question": "Does any named selected supplier realize the heterogeneous typed readers Q^(-t)R_b with the asymmetric 3|7 handoff at unchanged address, tape and precision costs?", + "why_it_matters": "The 144-primitive boundary saving transfers to a recursive profile only if a physical supplier admits this paired interface; the joint word also raises the prefix row-L1 envelope." + } + ], + "original_card": { + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "allowed_variations": [ + "A two-type pilot or one explicit deferred restoration." + ], + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Find a concrete consecutive-call boundary in the selected review and list its entry/exit obligations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "id": "persistent-boundary", + "methods": [ + "Write typed entry/exit contracts and a contracting multitype recurrence.", + "Derive a lower bound for the compulsory transitions of one proposed typed interface." + ], + "overlap_terms": [ + "persistent boundary", + "deferred restoration", + "multitype" + ], + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "scope_change_triggers": [ + "Rewriting the old scalar recurrence as a matrix without eliminating work." + ], + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ] + }, + "outcome": "completed", + "priority_revision": 3, + "schema_version": 1, + "scope_change_reason": "The catalogue card asks for a consecutive-call restoration saving. Like research/z4-distinct-source-seed55 this task changes the interface hypothesis to the phase-typed order-four child contract with a two-bank source handoff; unlike that package the two calls have different child counts and reader schedules, so the handoff sits at an asymmetric boundary. This is the one cell of {identical, heterogeneous} x {same source, distinct sources} not covered by the two predecessor packages.", + "scope_key": "026be4b6e61971d51838", + "scope_status": "changed", + "stop_rule": "Search only the 3|7 split with the two declared reader schedules and the fixed ten-child terminal phase. Exhaust all 4^3, 4^7 and 4^10 phase assignments; stop after the exact two-bank map, the invoice comparison and the listed mutation controls. Do not generalize beyond the declared order-four typed alphabet or begin supplier optimization in this package.", + "task_id": "persistent-boundary", + "track": "recursive-interfaces" +} diff --git a/research/z4-hetero-two-bank-seedba18/VERIFY.json b/research/z4-hetero-two-bank-seedba18/VERIFY.json new file mode 100644 index 0000000000..43d3eb9433 --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/VERIFY.json @@ -0,0 +1,22 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "checks": "Checks exact predecessor pins, all phase-indexed child identities, the phase recurrence against exhaustive 4^3/4^7/4^10 path coverage and its period-4 law, the 5|5 predecessor positive control, the 3|7 two-bank separate and joint 80-column dirty maps, full ADD/NEG/read invoices and row-L1 peaks, and six negative controls.", + "timeout_seconds": 420 + } + ], + "inputs": [ + "research/z4-hetero-two-bank-seedba18/inputs/PR1391/CERTIFICATE.json", + "research/z4-hetero-two-bank-seedba18/inputs/PR1391/verify.py", + "research/z4-hetero-two-bank-seedba18/inputs/PR1410-README.md" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/z4-hetero-two-bank-seedba18/inputs/PR1391/CERTIFICATE.json b/research/z4-hetero-two-bank-seedba18/inputs/PR1391/CERTIFICATE.json new file mode 100644 index 0000000000..0132b117d9 --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/inputs/PR1391/CERTIFICATE.json @@ -0,0 +1,240 @@ +{ + "assignment": { + "cycle_order": 4, + "os_seed": 56, + "track": "recursive interfaces" + }, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "boundary": { + "children": 5, + "dynamic_program_total": 140, + "eager_ADD": 270, + "eager_NEG": 30, + "eager_total": 300, + "eager_word_sha256": "90bf97554a5a1529e96f128ad93e54aeadbfeffbdd73f3c546ceb4f1e0d91273", + "exhaustive_path_count": 1024, + "exhaustive_path_minimum": 140, + "macro_alphabet": "canonical powers P^u and Q^v using the listed explicit words", + "optimized_ADD": 126, + "optimized_NEG": 14, + "optimized_word_sha256": "3459ba0aca8bd5e598696333a1a5b520d4a0e5353553d685732cf7d49acbd097", + "saved_per_batch": 160, + "states": [ + 0, + 1, + 2, + 3, + 0, + 0 + ], + "transitions": [ + { + "P_power": 0, + "Q_power": 1, + "after": 1, + "before": 0 + }, + { + "P_power": 0, + "Q_power": 1, + "after": 2, + "before": 1 + }, + { + "P_power": 0, + "Q_power": 1, + "after": 3, + "before": 2 + }, + { + "P_power": 0, + "Q_power": 1, + "after": 0, + "before": 3 + }, + { + "P_power": 3, + "Q_power": 0, + "after": 0, + "before": 0 + } + ] + }, + "child": { + "checked_basis_columns": 96, + "distinct_block_checks": [ + { + "ADD": 62, + "NEG": 6, + "basis_columns": 32, + "block": 0, + "inverse_word_sha256": "12a83c7b67cc26872a45569df66568dce8d6f47697ae23d08a7731d1c3e957d4", + "word_sha256": "24a9f259f8d8bcd826a8feec7f0dbbf22f10c5fa10e2ed0b5e101ea22bebfe95" + }, + { + "ADD": 62, + "NEG": 6, + "basis_columns": 32, + "block": 1, + "inverse_word_sha256": "ed74b775d98f56e0b6a9b6153f5dce0e352d7597dd275e84bdfe7ef91db8282c", + "word_sha256": "33c9708615463d38ac54c283ff87d3755c2a02edfa6535a3fdce7555ed8091ea" + }, + { + "ADD": 62, + "NEG": 6, + "basis_columns": 32, + "block": 2, + "inverse_word_sha256": "8f1ba7d29abb2b862f689a3ca7aec86cc9c7c8387aa5d66c905472dbcd6f46b5", + "word_sha256": "2d9232ba4a81a06041bf4057a798aa538985524cbf97b40caca085fcefd309e4" + } + ], + "per_call": { + "ADD": 62, + "NEG": 6, + "total": 68 + }, + "selection_blocks": [ + 0, + 1, + 2, + 0, + 1 + ] + }, + "complete_echo": { + "all_arbitrary_dirty_basis_columns": 56, + "dispatches": { + "eager": 1328, + "optimized": 1008 + }, + "eager": { + "ADD": 1208, + "NEG": 120, + "total": 1328 + }, + "eager_word_sha256": "ee0e4afaf3cf2b1dbfc65e2eff076c92dba34fe8aa768fc8b506f9d22382c883", + "internal_C_v_example": { + "all_arbitrary_input_and_scratch_basis_columns": 56, + "eager": { + "ADD": 1262, + "NEG": 126, + "total": 1388 + }, + "eager_word_sha256": "b63466d5724bf7e60b6fcdb8bca73feaec48788326b43f70804dff1764cc07dc", + "optimized": { + "ADD": 974, + "NEG": 94, + "total": 1068 + }, + "optimized_word_sha256": "436ab81a02fc6013b6b167937c2294d4547b6f8ffd3888db5569f5c2cedc3131" + }, + "layout": { + "output_D": 8, + "source_X": 24, + "total_data_coordinates": 56, + "working_W": 24 + }, + "map": "(D,X,W)->(D+sum_i R_i X,X,W)", + "optimized": { + "ADD": 920, + "NEG": 88, + "total": 1008 + }, + "optimized_word_sha256": "ecaf6008f7c81a6c495ce146b971b53d4c3a9b1fea6289645285045796235451", + "prefix_row_l1_peak": { + "eager": 11, + "optimized": 20 + }, + "reads": { + "eager": 2536, + "optimized": 1928 + }, + "saved_total_primitives": 320, + "writes": { + "eager": 1328, + "optimized": 1008 + } + }, + "controls": { + "count": 4, + "names": [ + "rotation sign mutation", + "wrong output phase", + "missing terminal restoration", + "forward word substituted for inverse" + ] + }, + "frame": { + "determinant": 1, + "intertwining_verified": true, + "order": 4, + "output_octets": 1, + "per_register": "two disjoint 4-cycles on one octet", + "phase_costs_per_octet": [ + { + "ADD": 0, + "NEG": 0, + "phase": 0, + "total": 0, + "word_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945" + }, + { + "ADD": 18, + "NEG": 2, + "phase": 1, + "total": 20, + "word_sha256": "652fe5774a3dc187f9df6fd2e578f0270a4a898e76edd1c5e57446ad5281d6fa" + }, + { + "ADD": 12, + "NEG": 4, + "phase": 2, + "total": 16, + "word_sha256": "3db669a9548039bbfc034e92b0c3edf8a540d8b147cb95618eddd3e225e13bb4" + }, + { + "ADD": 18, + "NEG": 2, + "phase": 3, + "total": 20, + "word_sha256": "278ea7a94adedef7155f32189da6002570d43d68701817674a62494c22d0ea22" + } + ], + "readers": [ + 0, + 1, + 2, + 0, + 1 + ], + "workspace_octets": 3 + }, + "recursive_interface_cost": { + "complete_root_echo": "2*sum(child vectors) + (48,0) + 2*g(k_v)", + "depth_storage": "56 data coordinates for the root echo plus 24 per active nested internal C_v level", + "eager_comparator": "replace g(k_v) by k_v*(54,6)", + "g(k)": "minimum 4-state recurrence below; vector ADD/NEG invoice retained along chosen path", + "internal_C_v": "2*sum(child vectors) + (48,0) + 2*g(k_v) + (54,6)", + "leaf_forward": { + "ADD": 62, + "NEG": 6 + } + }, + "schema_version": 1, + "scope": "Exact finite dirty-state interface construction and macro-alphabet optimum for five children; no actual supplier admission, selected profile change, new kappa, or multiplication theorem.", + "selected_context": { + "decimal": "0.001672660197076918", + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "selected_source_pr": 1094 + }, + "source_pins": { + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "docs/research/agent-task-catalog.json": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce", + "docs/research/community-batch1099-review.md": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb", + "docs/research/current-status.md": "1f59d648763c77d574d18dc59ea8bf62d2ee74aaed3c202c9c8cfa4f901badbd", + "research/community-frontier1094-audit/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + "task": "z4-paired-frame-restoration-seed56" +} diff --git a/research/z4-hetero-two-bank-seedba18/inputs/PR1391/verify.py b/research/z4-hetero-two-bank-seedba18/inputs/PR1391/verify.py new file mode 100644 index 0000000000..9d866bbf57 --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/inputs/PR1391/verify.py @@ -0,0 +1,606 @@ +#!/usr/bin/env python3 +"""Exact finite check for a paired order-four dirty-output frame.""" + +import argparse +import hashlib +import itertools +import json +import math +from pathlib import Path + + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parent.parent +CERT = PKG / "CERTIFICATE.json" +SEED = 56 +BASE = "bce54fb3f895cbe5cd4c0eb477c3afeed100190f" +BLOCKS = (0, 1, 2, 0, 1) +WORK_OCTETS = 3 +OUTPUT_WIDTH = 8 +WORK_WIDTH = 8 * WORK_OCTETS +LOCAL_WIDTH = OUTPUT_WIDTH + WORK_WIDTH +ECHO_WIDTH = OUTPUT_WIDTH + WORK_WIDTH + WORK_WIDTH + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(target, source, sign=1): + require(sign in (-1, 1), "ADD sign must be +/-1") + return ("ADD", target, source, sign) + + +def neg(target): + return ("NEG", target, None, 0) + + +def inverse_word(word): + inverse = [] + for kind, target, source, sign in reversed(word): + inverse.append(add(target, source, -sign) if kind == "ADD" else neg(target)) + return inverse + + +def lift_word(word, indices): + lifted = [] + for kind, target, source, sign in word: + lifted.append((kind, indices[target], None if source is None else indices[source], sign)) + return lifted + + +def swap_word(a, b): + """Pure swap (a,b)->(b,a), using three ADDs and one NEG.""" + return [add(a, b), add(b, a, -1), add(a, b), neg(b)] + + +def signed_swap_positive(a, b): + """Three ADDs map (a,b)->(b,-a).""" + return [add(a, b), add(b, a, -1), add(a, b)] + + +def signed_swap_negative(a, b): + """Three ADDs map (a,b)->(-b,a).""" + return [add(b, a), add(a, b, -1), add(b, a)] + + +def one_cycle_word(phase, base=0): + """Powers of (a,b,c,d)->(d,a,b,c) on one four-register cycle.""" + require(phase in range(4), "invalid phase") + a, b, c, d = (base + i for i in range(4)) + if phase == 0: + return [] + if phase == 1: + # Three signed swaps compose to (d,-a,b,c); one NEG on b gives + # the requested pure cycle (d,a,b,c). + return (signed_swap_positive(a, b) + signed_swap_negative(a, c) + + signed_swap_positive(a, d) + [neg(b)]) + if phase == 2: + return swap_word(a, c) + swap_word(b, d) + return inverse_word(one_cycle_word(1, base)) + + +def octet_word(phase, base=0): + """Apply the same phase to two disjoint four-cycles.""" + return one_cycle_word(phase, base) + one_cycle_word(phase, base + 4) + + +def workspace_word(phase, base=0): + """Apply P^phase to three disjoint eight-register blocks.""" + return sum((octet_word(phase, base + 8 * j) for j in range(WORK_OCTETS)), []) + + +def word_counts(word): + adds = sum(kind == "ADD" for kind, *_ in word) + negs = sum(kind == "NEG" for kind, *_ in word) + return (adds, negs) + + +def word_sha256(word): + payload = json.dumps(word, separators=(",", ":"), ensure_ascii=True).encode("ascii") + return hashlib.sha256(payload).hexdigest() + + +def vector_add(a, b): + return tuple(x + y for x, y in zip(a, b)) + + +def vector_scale(a, n): + return tuple(n * x for x in a) + + +def vector_total(a): + return sum(a) + + +def phase_counts(phase): + return word_counts(octet_word(phase)) + + +def work_phase_counts(phase): + return word_counts(workspace_word(phase)) + + +def apply_word_matrix(word, width): + """Return output rows as exact integer linear forms in the input rows.""" + rows = [[int(i == j) for j in range(width)] for i in range(width)] + for kind, target, source, sign in word: + require(0 <= target < width, "gate target outside matrix") + if kind == "ADD": + require(source is not None and 0 <= source < width, "gate source outside matrix") + rows[target] = [a + sign * b for a, b in zip(rows[target], rows[source])] + else: + rows[target] = [-x for x in rows[target]] + return rows + + +def matmul(a, b): + require(bool(a) and bool(b) and len(a[0]) == len(b), "bad matrix dimensions") + bt = list(zip(*b)) + return [[sum(x * y for x, y in zip(row, col)) for col in bt] for row in a] + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def matrix_power(a, exponent): + out = identity(len(a)) + for _ in range(exponent): + out = matmul(out, a) + return out + + +def expected_octet_frame(): + rows = [[0] * 8 for _ in range(8)] + for base in (0, 4): + # New tuple is (old d, old a, old b, old c). + for target, source in ((base, base + 3), (base + 1, base), + (base + 2, base + 1), (base + 3, base + 2)): + rows[target][source] = 1 + return rows + + +def block_diag(blocks): + widths = [len(block) for block in blocks] + total = sum(widths) + out = [[0] * total for _ in range(total)] + offset = 0 + for block, width in zip(blocks, widths): + for i in range(width): + for j in range(width): + out[offset + i][offset + j] = block[i][j] + offset += width + return out + + +def reader_matrix(block): + rows = [[0] * WORK_WIDTH for _ in range(OUTPUT_WIDTH)] + for j in range(OUTPUT_WIDTH): + rows[j][8 * block + j] = 1 + return rows + + +def child_word(block): + word = [add(j, OUTPUT_WIDTH + 8 * block + j) for j in range(OUTPUT_WIDTH)] + work_indices = [OUTPUT_WIDTH + j for j in range(WORK_WIDTH)] + return word + lift_word(workspace_word(1), work_indices) + + +def expected_child(block): + r = reader_matrix(block) + p = matrix_power(expected_octet_frame(), 1) + rows = [] + for i in range(OUTPUT_WIDTH): + rows.append([int(i == j) for j in range(OUTPUT_WIDTH)] + r[i]) + for i in range(WORK_WIDTH): + rows.append([0] * OUTPUT_WIDTH + block_diag([p] * WORK_OCTETS)[i]) + return rows + + +def expected_child_inverse(block): + r = reader_matrix(block) + p_inverse = matrix_power(expected_octet_frame(), 3) + correction = matmul(r, block_diag([p_inverse] * WORK_OCTETS)) + rows = [] + for i in range(OUTPUT_WIDTH): + rows.append([int(i == j) for j in range(OUTPUT_WIDTH)] + [-x for x in correction[i]]) + for i in range(WORK_WIDTH): + rows.append([0] * OUTPUT_WIDTH + block_diag([p_inverse] * WORK_OCTETS)[i]) + return rows + + +def batch_word(states, blocks=BLOCKS, wrong_first_output_phase=False, omit_last_gap=False): + """Emit a batch; states list aligned phases at entrance/after each child.""" + require(len(states) == len(blocks) + 1, "wrong state path length") + require(all(p in range(4) for p in states), "phase outside Z/4Z") + work_indices = [OUTPUT_WIDTH + j for j in range(WORK_WIDTH)] + word = lift_word(octet_word(states[0]), list(range(OUTPUT_WIDTH))) + word += lift_word(workspace_word(states[0]), work_indices) + for i, block in enumerate(blocks): + word += child_word(block) + if omit_last_gap and i == len(blocks) - 1: + continue + old, new = states[i], states[i + 1] + u = (new - old - 1) % 4 + v = (new - old) % 4 + if wrong_first_output_phase and i == 0: + v = (v + 1) % 4 + word += lift_word(workspace_word(u), work_indices) + word += lift_word(octet_word(v), list(range(OUTPUT_WIDTH))) + return word + + +def boundary_components(states): + total = vector_add(work_phase_counts(states[0]), phase_counts(states[0])) + for i, (old, new) in enumerate(zip(states, states[1:])): + u = (new - old - 1) % 4 + v = (new - old) % 4 + total = vector_add(total, work_phase_counts(u)) + total = vector_add(total, phase_counts(v)) + return total + + +def dynamic_plan(k): + require(k > 0, "positive child count required") + wcost = [vector_scale(phase_counts(p), WORK_OCTETS) for p in range(4)] + ocost = [phase_counts(p) for p in range(4)] + f = [vector_total(vector_add(wcost[t], ocost[t])) for t in range(4)] + predecessors = [] + for _ in range(k): + g = [0] * 4 + pred = [0] * 4 + for s in range(4): + choices = [] + for t in range(4): + u, v = (s - t - 1) % 4, (s - t) % 4 + step = vector_add(wcost[u], ocost[v]) + choices.append((f[t] + vector_total(step), t)) + g[s], pred[s] = min(choices) + f = g + predecessors.append(pred) + state = 0 # final arbitrary-output/restoration endpoint is canonical + reverse_states = [state] + for pred in reversed(predecessors): + state = pred[state] + reverse_states.append(state) + states = list(reversed(reverse_states)) + return states, f[0], boundary_components(states) + + +def brute_boundary_min(k): + best = None + for prefix in itertools.product(range(4), repeat=k): + states = list(prefix) + [0] + cost = vector_total(boundary_components(states)) + best = cost if best is None else min(best, cost) + return best + + +def expected_batch(blocks=BLOCKS): + rsum = [[0] * WORK_WIDTH for _ in range(OUTPUT_WIDTH)] + for block in blocks: + r = reader_matrix(block) + for i in range(OUTPUT_WIDTH): + rsum[i] = [a + b for a, b in zip(rsum[i], r[i])] + rows = [] + for i in range(OUTPUT_WIDTH): + rows.append([int(i == j) for j in range(OUTPUT_WIDTH)] + rsum[i]) + rows.extend([[0] * OUTPUT_WIDTH + row for row in identity(WORK_WIDTH)]) + return rows + + +def lifted_batch_word(states): + local = batch_word(states) + mapping = list(range(OUTPUT_WIDTH)) + [OUTPUT_WIDTH + WORK_WIDTH + i for i in range(WORK_WIDTH)] + return lift_word(local, mapping) + + +def echo_word(states): + word = [add(OUTPUT_WIDTH + WORK_WIDTH + i, OUTPUT_WIDTH + i) for i in range(WORK_WIDTH)] + body = lifted_batch_word(states) + word += body + word += [add(OUTPUT_WIDTH + WORK_WIDTH + i, OUTPUT_WIDTH + i, -1) for i in range(WORK_WIDTH)] + word += inverse_word(body) + return word + + +def expected_echo(blocks=BLOCKS): + rsum = [[0] * WORK_WIDTH for _ in range(OUTPUT_WIDTH)] + for block in blocks: + r = reader_matrix(block) + for i in range(OUTPUT_WIDTH): + rsum[i] = [a + b for a, b in zip(rsum[i], r[i])] + rows = [] + for i in range(OUTPUT_WIDTH): + rows.append([int(i == j) for j in range(OUTPUT_WIDTH)] + rsum[i] + [0] * WORK_WIDTH) + rows.extend([[0] * OUTPUT_WIDTH + row + [0] * WORK_WIDTH for row in identity(WORK_WIDTH)]) + rows.extend([[0] * (OUTPUT_WIDTH + WORK_WIDTH) + row for row in identity(WORK_WIDTH)]) + return rows + + +def internal_c_word(states): + """Implement one internal C_v using source X and a separate dirty scratch.""" + word = echo_word(states) + source_indices = [OUTPUT_WIDTH + j for j in range(WORK_WIDTH)] + return word + lift_word(workspace_word(1), source_indices) + + +def expected_internal_c(): + echo = expected_echo() + p = block_diag([expected_octet_frame()] * WORK_OCTETS) + rows = [row[:] for row in echo[:OUTPUT_WIDTH]] + rows.extend([[0] * OUTPUT_WIDTH + p[i] + [0] * WORK_WIDTH + for i in range(WORK_WIDTH)]) + rows.extend([[0] * (OUTPUT_WIDTH + WORK_WIDTH) + row + for row in identity(WORK_WIDTH)]) + return rows + + +def reject_controls(states, batch_expected): + controls = 0 + # A sign mutation in the rotation circuit must not pass its frame identity. + broken = octet_word(1) + kind, target, source, sign = broken[0] + broken[0] = (kind, target, source, -sign) + require(apply_word_matrix(broken, 8) != expected_octet_frame(), "bad rotation control escaped") + controls += 1 + + # An extra output phase at the first gap violates the reader/frame contract. + misaligned = batch_word(states, wrong_first_output_phase=True) + require(apply_word_matrix(misaligned, LOCAL_WIDTH) != batch_expected, + "misaligned phase control escaped") + controls += 1 + + # Omitting the terminal correction must leave a noncanonical dirty workspace. + unclosed = batch_word(states, omit_last_gap=True) + require(apply_word_matrix(unclosed, LOCAL_WIDTH) != batch_expected, + "missing terminal restoration control escaped") + controls += 1 + + # A forward batch followed by itself is not the literal inverse operation. + forward = batch_word(states) + doubled = forward + forward + require(apply_word_matrix(doubled, LOCAL_WIDTH) != identity(LOCAL_WIDTH), + "forward-for-inverse control escaped") + controls += 1 + return controls + + +def permutation_determinant(matrix): + columns = [] + signs = [] + for row in matrix: + nonzero = [(j, x) for j, x in enumerate(row) if x] + require(len(nonzero) == 1 and nonzero[0][1] in (-1, 1), + "frame is not a signed permutation") + columns.append(nonzero[0][0]) + signs.append(nonzero[0][1]) + inversions = sum(columns[i] > columns[j] + for i in range(len(columns)) for j in range(i + 1, len(columns))) + return (-1 if inversions % 2 else 1) * math.prod(signs) + + +def prefix_row_l1_peak(word, width): + rows = identity(width) + peak = max(sum(abs(x) for x in row) for row in rows) + for kind, target, source, sign in word: + if kind == "ADD": + rows[target] = [a + sign * b for a, b in zip(rows[target], rows[source])] + else: + rows[target] = [-x for x in rows[target]] + peak = max(peak, *(sum(abs(x) for x in row) for row in rows)) + return peak + + +def verify_source_pins(): + pins = json.loads((PKG / "SOURCES.json").read_text()) + require(pins["base_commit"] == BASE, "SOURCES base mismatch") + for entry in pins["files"]: + path = ROOT / entry["path"] + require(path.is_file(), "missing pinned input: " + entry["path"]) + got = hashlib.sha256(path.read_bytes()).hexdigest() + require(got == entry["sha256"], "pinned input bytes changed: " + entry["path"]) + return {entry["path"]: entry["sha256"] for entry in pins["files"]} + + +def build_certificate(): + source_pins = verify_source_pins() + p1 = expected_octet_frame() + phase_vectors = [word_counts(octet_word(p)) for p in range(4)] + require(phase_vectors == [(0, 0), (18, 2), (12, 4), (18, 2)], "octet gate-cost vector changed") + for phase in range(4): + require(apply_word_matrix(octet_word(phase), 8) == matrix_power(p1, phase), + "octet phase word does not implement P^phase") + require(apply_word_matrix(workspace_word(phase), WORK_WIDTH) + == block_diag([matrix_power(p1, phase)] * WORK_OCTETS), + "workspace phase word does not implement P^phase") + require(matrix_power(p1, 4) == identity(8) and p1 != identity(8), "frame is not order four") + require(matrix_power(p1, 2) != identity(8), "frame has order two") + require(permutation_determinant(p1) == 1, "paired four-cycle frame is not orientation-preserving") + + q = p1 + readers = [reader_matrix(block) for block in BLOCKS] + for r in readers: + require(matmul(r, block_diag([p1] * WORK_OCTETS)) == matmul(q, r), + "reader does not intertwine P and Q") + + child_counts = [] + child_columns = 0 + for block in sorted(set(BLOCKS)): + word = child_word(block) + expected = expected_child(block) + require(apply_word_matrix(word, LOCAL_WIDTH) == expected, + "child word differs from its declared dirty-state map") + inv = inverse_word(word) + require(apply_word_matrix(inv, LOCAL_WIDTH) == expected_child_inverse(block), + "literal child inverse differs from the block inverse formula") + require(matmul(apply_word_matrix(inv, LOCAL_WIDTH), expected) == identity(LOCAL_WIDTH), + "child inverse does not restore arbitrary input") + require(word_counts(word) == (62, 6), "child invoice changed") + require(word_counts(inv) == word_counts(word), "literal child inverse count changed") + child_counts.append({"block": block, "ADD": 62, "NEG": 6, + "word_sha256": word_sha256(word), + "inverse_word_sha256": word_sha256(inv), + "basis_columns": LOCAL_WIDTH}) + child_columns += LOCAL_WIDTH + + states, optimum, chosen_vector = dynamic_plan(5) + require(states == [0, 1, 2, 3, 0, 0], "unexpected deterministic shortest path") + require(optimum == 140 and chosen_vector == (126, 14) and vector_total(chosen_vector) == optimum, + "four-state recurrence returned an unexpected boundary cost") + require(brute_boundary_min(5) == optimum, "exhaustive 4^5 schedule census disagrees") + eager_vec = vector_scale(work_phase_counts(3), 5) + require(eager_vec == (270, 30) and vector_total(eager_vec) == 300, + "eager per-child restoration invoice changed") + + batch = batch_word(states) + batch_map = apply_word_matrix(batch, LOCAL_WIDTH) + expected_h = expected_batch() + require(batch_map == expected_h, "optimized batch does not implement the full typed map") + batch_inv = inverse_word(batch) + require(matmul(apply_word_matrix(batch_inv, LOCAL_WIDTH), batch_map) + == identity(LOCAL_WIDTH), "literal inverse batch fails on dirty columns") + eager_states = [0] * (len(BLOCKS) + 1) + eager_batch = batch_word(eager_states) + require(apply_word_matrix(eager_batch, LOCAL_WIDTH) == expected_h, + "eager baseline does not implement the same batch map") + require(word_counts(batch) == (436, 44), "optimized batch primitive invoice changed") + require(word_counts(eager_batch) == (580, 60), "eager batch primitive invoice changed") + + echo_opt = echo_word(states) + echo_eager = echo_word(eager_states) + echo_expected = expected_echo() + require(apply_word_matrix(echo_opt, ECHO_WIDTH) == echo_expected, + "optimized echo fails arbitrary dirty/source inputs") + require(apply_word_matrix(echo_eager, ECHO_WIDTH) == echo_expected, + "eager echo is not the same complete map") + require(word_counts(echo_opt) == (920, 88), "optimized echo primitive invoice changed") + require(word_counts(echo_eager) == (1208, 120), "eager echo primitive invoice changed") + require(len(echo_opt) == 1008 and len(echo_eager) == 1328, + "complete echo totals changed") + + internal_opt = internal_c_word(states) + internal_eager = internal_c_word(eager_states) + internal_expected = expected_internal_c() + require(apply_word_matrix(internal_opt, ECHO_WIDTH) == internal_expected, + "internal recursive C_v map fails arbitrary input/scratch columns") + require(apply_word_matrix(internal_eager, ECHO_WIDTH) == internal_expected, + "eager internal C_v map differs from the optimized interface") + require(matmul(apply_word_matrix(inverse_word(internal_opt), ECHO_WIDTH), internal_expected) + == identity(ECHO_WIDTH), "internal C_v literal inverse fails") + require(word_counts(internal_opt) == (974, 94), "optimized internal C_v invoice changed") + require(word_counts(internal_eager) == (1262, 126), "eager internal C_v invoice changed") + + control_count = reject_controls(states, expected_h) + phase_changes = [] + for old, new in zip(states, states[1:]): + phase_changes.append({"before": old, "after": new, + "P_power": (new - old - 1) % 4, + "Q_power": (new - old) % 4}) + return { + "schema_version": 1, + "task": "z4-paired-frame-restoration-seed56", + "base_commit": BASE, + "assignment": {"os_seed": SEED, "track": "recursive interfaces", + "cycle_order": 2 + SEED % 3}, + "selected_context": { + "kappa": "836330098538459/500000000000000000", + "decimal": "0.001672660197076918", + "selected_source_pr": 1094, + "review": "docs/research/community-batch1099-review.md", + }, + "frame": { + "per_register": "two disjoint 4-cycles on one octet", + "determinant": 1, + "order": 4, + "phase_costs_per_octet": [ + {"phase": p, "ADD": c[0], "NEG": c[1], "total": sum(c), + "word_sha256": word_sha256(octet_word(p))} + for p, c in enumerate(phase_vectors) + ], + "workspace_octets": WORK_OCTETS, + "output_octets": 1, + "readers": list(BLOCKS), + "intertwining_verified": True, + }, + "boundary": { + "children": len(BLOCKS), + "states": states, + "transitions": phase_changes, + "dynamic_program_total": optimum, + "exhaustive_path_count": 4 ** len(BLOCKS), + "exhaustive_path_minimum": brute_boundary_min(5), + "optimized_ADD": chosen_vector[0], + "optimized_NEG": chosen_vector[1], + "eager_ADD": eager_vec[0], + "eager_NEG": eager_vec[1], + "eager_total": vector_total(eager_vec), + "saved_per_batch": vector_total(eager_vec) - optimum, + "optimized_word_sha256": word_sha256(batch), + "eager_word_sha256": word_sha256(eager_batch), + "macro_alphabet": "canonical powers P^u and Q^v using the listed explicit words", + }, + "child": {"per_call": {"ADD": 62, "NEG": 6, "total": 68}, + "selection_blocks": list(BLOCKS), "distinct_block_checks": child_counts, + "checked_basis_columns": child_columns}, + "complete_echo": { + "layout": {"output_D": OUTPUT_WIDTH, "source_X": WORK_WIDTH, + "working_W": WORK_WIDTH, "total_data_coordinates": ECHO_WIDTH}, + "map": "(D,X,W)->(D+sum_i R_i X,X,W)", + "optimized": {"ADD": 920, "NEG": 88, "total": 1008}, + "eager": {"ADD": 1208, "NEG": 120, "total": 1328}, + "saved_total_primitives": 320, + "dispatches": {"optimized": 1008, "eager": 1328}, + "reads": {"optimized": 1928, "eager": 2536}, + "writes": {"optimized": 1008, "eager": 1328}, + "optimized_word_sha256": word_sha256(echo_opt), + "eager_word_sha256": word_sha256(echo_eager), + "all_arbitrary_dirty_basis_columns": ECHO_WIDTH, + "prefix_row_l1_peak": {"optimized": prefix_row_l1_peak(echo_opt, ECHO_WIDTH), + "eager": prefix_row_l1_peak(echo_eager, ECHO_WIDTH)}, + "internal_C_v_example": { + "optimized": {"ADD": 974, "NEG": 94, "total": 1068}, + "eager": {"ADD": 1262, "NEG": 126, "total": 1388}, + "optimized_word_sha256": word_sha256(internal_opt), + "eager_word_sha256": word_sha256(internal_eager), + "all_arbitrary_input_and_scratch_basis_columns": ECHO_WIDTH, + }, + }, + "recursive_interface_cost": { + "leaf_forward": {"ADD": 62, "NEG": 6}, + "internal_C_v": "2*sum(child vectors) + (48,0) + 2*g(k_v) + (54,6)", + "complete_root_echo": "2*sum(child vectors) + (48,0) + 2*g(k_v)", + "g(k)": "minimum 4-state recurrence below; vector ADD/NEG invoice retained along chosen path", + "eager_comparator": "replace g(k_v) by k_v*(54,6)", + "depth_storage": "56 data coordinates for the root echo plus 24 per active nested internal C_v level", + }, + "controls": {"count": control_count, + "names": ["rotation sign mutation", "wrong output phase", "missing terminal restoration", + "forward word substituted for inverse"]}, + "source_pins": source_pins, + "scope": "Exact finite dirty-state interface construction and macro-alphabet optimum for five children; no actual supplier admission, selected profile change, new kappa, or multiplication theorem.", + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--emit", action="store_true", help="write the exact computed certificate") + args = parser.parse_args() + certificate = build_certificate() + encoded = json.dumps(certificate, sort_keys=True, indent=2) + "\n" + if args.emit: + CERT.write_text(encoded) + else: + require(CERT.is_file(), "missing CERTIFICATE.json; run --emit once while authoring") + saved = json.loads(CERT.read_text()) + require(saved == certificate, "committed certificate differs from recomputed evidence") + echo = certificate["complete_echo"] + print("PASS_Z4_PAIRED_FRAME boundary=140_vs_300 " + "echo=1008_vs_1328 saved=320 root_cost=ADD920+NEG88 " + "basis_columns=56 controls=4 no_new_kappa") + + +if __name__ == "__main__": + main() diff --git a/research/z4-hetero-two-bank-seedba18/inputs/PR1410-README.md b/research/z4-hetero-two-bank-seedba18/inputs/PR1410-README.md new file mode 100644 index 0000000000..001929a89c --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/inputs/PR1410-README.md @@ -0,0 +1,67 @@ +# A persistent order-four boundary across two root echoes + +**Scoped recursive-interface construction; no new `kappa`, supplier admission, or change to the selected result.** For the pinned PR #1391 child family, two identical five-child root echoes on the same source can be replaced by one ten-child dirty echo that carries its order-four phase across the midpoint. The complete word has 1,904 scalar primitives versus 2,016 for two separate calls, saving 112 primitives and 232 data reads. Its peak prefix row-L1 is 42 instead of 30, so this result does not establish a precision improvement. + +## Assignment and scope + +The OS assignment seed was **57**, on the recursive-interfaces track. The pinned base is `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. Candidate tasks recorded before selection were (1) share the midpoint restoration between two identical PR #1391 root echoes, (2) extend the paired frame alphabet to order five, and (3) test a six-child extension. Seed rule `57 mod 3 = 0` selected the first. The short claim is recorded in [discussion #1163](https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18911847). + +This is exact for the stated order-four macro alphabet and the fixed two-call same-source family. It composes the predecessor's five-child interface; it does not change the physical child supplier, address routing, precision model, selected certificate, or theorem exponent. The motivating interface card asks whether two consecutive calls can eliminate a restoration reconstructed by the next call. Here the joint word removes one separate call's copy/restoration wrapper and avoids paying two independent boundary schedules. It does not prove an improvement for heterogeneous calls or arbitrary ADD/NEG interleavings. + +## Recurrence and complete cost + +For phase `t` in `Z/4Z`, let `A(t)` be the cost of the three-octet workspace frame and `B(t)` the cost of the output frame. The source-pinned phase vectors are + +```text +B = [(0,0), (18,2), (12,4), (18,2)] +A = 3 B +``` + +where each pair is `(ADD, NEG)`. The predecessor recurrence is independently re-evaluated for five and ten children: + +```text +F0(t) = A(t) + B(t) +F(j+1)(s) = min_t { F(j)(t) + A(s-t-1 mod 4) + B(s-t mod 4) } +g(k) = Fk(0) +``` + +The five-child control has path `[0,1,2,3,0,0]`, boundary vector `(126,14)`, total 140; all `4^5 = 1,024` paths are checked. For ten children the optimum is `[0,1,2,3,0,1,2,3,0,1,0]`, with midpoint phase 1, boundary vector `(216,32)`, total 248; all `4^10 = 1,048,576` paths are checked. + +The complete dirty root echo has map + +```text +(D, X, W) -> (D + 2 sum_i R_i X, X, W) +``` + +for arbitrary input vectors `D`, `X`, and `W`. Its full invoice is + +| Schedule | ADD | NEG | Primitives | Reads | Writes | Prefix row-L1 peak | +|---|---:|---:|---:|---:|---:|---:| +| Two separate five-child calls | 1,840 | 176 | 2,016 | 3,856 | 2,016 | 30 | +| Joint ten-child call | 1,720 | 184 | 1,904 | 3,624 | 1,904 | 42 | +| Eager ten-child control | 2,368 | 240 | 2,608 | — | — | — | + +The joint schedule uses 120 fewer ADDs and 8 more NEGs than the two-call schedule. The total decreases by 112. Prefix row-L1 grows by 12; coefficient width, fixed-precision safety, and tape costs are outside this experiment. In particular the result is a gate-count construction, not a resource-admitted supplier or a revised recursive bound. + +## Evidence and reproduction + +`inputs/PR1391-CERTIFICATE.json`, `inputs/PR1391-verify.py`, and `inputs/PR1391-README.md` preserve the predecessor material from PR #1391 at head `6ce8017e4c27c8b220b6c3a27a53bb18f138212a`; hashes and Git blob IDs are checked before importing its word emitter. The inherited source pins are checked against the exact base. The new verifier independently implements the recurrence, complete vector invoice, map expectation, and full path census. The emitted predecessor circuit is reused only as the pinned child-word emitter. + +Run from the repository root: + +```sh +python3 -I -O -B research/z4-persistent-pair-seed57/verify.py +``` + +Expected output begins `PASS_Z4_PERSISTENT_PAIR` and reports `g5 140 g10 248 paths 1048576`, followed by `two_calls 2016 joint 1904 saving 112`. The same verifier also checks 56 basis columns for both separate and joint maps and rejects three controls: omitting the second call, using a wrong output phase, and failing terminal restoration. `test_package.py` repeats focused recurrence and result-receipt assertions. All arithmetic is exact integer arithmetic; the state/path search domain and stopping rule are the finite four-phase paths for exactly 5 and 10 children, exhaustively enumerated. Local replay and package-pin validation passed on CPython 3.14.7, and `make selected-record-check` passed with the exact base kappa unchanged. The registered wrapper declares Python 3.12, which is unavailable locally; that replay, hosted CI, and independent human review remain pending. Exact command receipts are in [VALIDATION.json](VALIDATION.json). + +## Predecessors and attribution + +This result extends the fixed order-four paired-frame construction in [PR #1391](https://github.com/CrocSwap/integer-mult-bounds/pull/1391), which in turn credits Ross Richardson's order-three cyclic-output frame in [PR #1287](https://github.com/CrocSwap/integer-mult-bounds/pull/1287) and Sagar Thakrar's paid output-sign frames in [PR #1227](https://github.com/CrocSwap/integer-mult-bounds/pull/1227). The imported emitter and predecessor certificate are byte-pinned. The ten-child recurrence, exhaustive census, composed dirty map and complete two-call comparison are new in this package. + +Prepared by **Cinna Davis** with substantial **OpenAI Codex assistance** in research, algebra, code, verification and prose. No independent human review or formal proof assistant is claimed. New package material is Apache-2.0; the copied predecessor README/code/certificate retain their upstream attribution and license context. + +## Open next questions + +- Does a named selected supplier expose this exact paired order-four intertwiner? This is necessary before transferring the gate saving into a selected recursive profile. First step: inspect one retained supplier's actual child matrix for the paired-cycle invariant. Blocked by the absence of a precision-admitted physical supplier with this interface. +- Can the 12-unit increase in prefix row-L1 be absorbed under the selected fixed-precision profile? First step: propagate the joint word's exact prefix coefficient envelope through the named host schedule. Blocked by the missing supplier and address/tape admission. diff --git a/research/z4-hetero-two-bank-seedba18/verify.py b/research/z4-hetero-two-bank-seedba18/verify.py new file mode 100644 index 0000000000..9efbfbbcb2 --- /dev/null +++ b/research/z4-hetero-two-bank-seedba18/verify.py @@ -0,0 +1,603 @@ +#!/usr/bin/env python3 +"""Heterogeneous 3+7 root echoes on two distinct source banks (order-four typed boundary). + +Model, child emitter and pin loader are copied from the pinned predecessor +research/z4-distinct-source-seed55/verify.py (itself built on the pinned +PR1391 child family and PR1410 same-source boundary), with attribution in +NOTICE.md. New here: asymmetric heterogeneous reader schedules across two +source banks, the handoff at the 3|7 boundary, the period-4 boundary law, +and the associated map and control checks. +""" +from __future__ import annotations + +import hashlib +import itertools +import json +import subprocess +import sys +import types +from pathlib import Path + +sys.dont_write_bytecode = True + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +INPUTS = PACKAGE / "inputs" +BASE = "e112d71c8d7bb32435debcc54df932593dd8223a" +PR1391_HEAD = "6ce8017e4c27c8b220b6c3a27a53bb18f138212a" +PR1410_HEAD = "5b1c00b9f2770aabaa0085539405757f7818a14a" +PINS = { + "inputs/PR1391/CERTIFICATE.json": ( + "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3", + "0132b117d90f1a7a97c40af3e38503c117604e00", + ), + "inputs/PR1391/verify.py": ( + "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05", + "9d866bbf57a6d1f012a21687bde2e231c90efd14", + ), + "inputs/PR1410-README.md": ( + "6dda7d5b83b41c71d73711401edbc146271a546a518ef6b038b0bdbb6578d405", + "001929a89cd64f4bbb0d4194c6bde96f45b7ded2", + ), +} +D = 8 +BANK = 24 +X = D +Y = D + BANK +W = D + 2 * BANK +TOTAL = D + 3 * BANK +# Type A reads source octets [0,1,2] of bank X (three children). +BLOCKS_A = (0, 1, 2) +# Type B reads source octets [2,1,0,2,1,0,2] of bank Y (seven children). +BLOCKS_B = (2, 1, 0, 2, 1, 0, 2) +BLOCKS_AB = BLOCKS_A + BLOCKS_B +SWITCH_INDEX = len(BLOCKS_A) - 1 # handoff after child 2, at the 3|7 boundary +BLOCKS5 = (0, 1, 2, 0, 1) +BLOCKS10 = BLOCKS5 + BLOCKS5 + + +def require(ok: bool, message: str) -> None: + if not ok: + raise ValueError(message) + + +def git_blob(data: bytes) -> str: + return subprocess.run( + ["git", "hash-object", "--stdin"], input=data, cwd=ROOT, + check=True, capture_output=True, + ).stdout.decode().strip() + + +def load_predecessor(): + for rel, (sha, blob) in PINS.items(): + raw = (PACKAGE / rel).read_bytes() + require(hashlib.sha256(raw).hexdigest() == sha, "pinned input SHA drift: " + rel) + require(git_blob(raw) == blob, "pinned input Git blob drift: " + rel) + source_readme = (PACKAGE / "inputs/PR1410-README.md").read_text() + require("two identical five-child root echoes on the same source" in source_readme + and "(D, X, W)" in source_readme, "PR1410 predecessor snapshot mismatch") + + cert_path = INPUTS / "PR1391/CERTIFICATE.json" + code_path = INPUTS / "PR1391/verify.py" + legacy = types.ModuleType("pinned_pr1391") + legacy.__file__ = str(code_path) + exec(compile(code_path.read_bytes(), str(code_path), "exec"), legacy.__dict__) + legacy.PKG = code_path.parent + legacy.ROOT = ROOT + legacy.CERT = cert_path + cert = json.loads(cert_path.read_text()) + require(cert["base_commit"] == "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "PR1391 research base") + require(cert["assignment"]["os_seed"] == 56 and cert["frame"]["order"] == 4, + "PR1391 assignment/frame pin") + require(cert["recursive_interface_cost"]["leaf_forward"] == {"ADD": 62, "NEG": 6}, + "PR1391 leaf cost pin") + for path, digest in cert["source_pins"].items(): + raw = subprocess.run(["git", "show", cert["base_commit"] + ":" + path], + cwd=ROOT, check=True, capture_output=True).stdout + require(hashlib.sha256(raw).hexdigest() == digest, + "PR1391 inherited source pin: " + path) + selected = subprocess.run(["git", "show", BASE + ":certificates/selected-result.json"], + cwd=ROOT, check=True, capture_output=True).stdout + require(hashlib.sha256(selected).hexdigest() == + "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected record base pin") + return legacy, cert + + +def plus_rows(target, source, sign=1): + return [a + sign * b for a, b in zip(target, source)] + + +def matmul(a, b): + require(bool(a) and bool(b) and len(a[0]) == len(b), "matrix dimensions") + return [[sum(a[i][k] * b[k][j] for k in range(len(b))) + for j in range(len(b[0]))] for i in range(len(a))] + + +def zero(n, m): + return [[0] * m for _ in range(n)] + + +def identity(n): + out = zero(n, n) + for i in range(n): + out[i][i] = 1 + return out + + +def block_diag(blocks): + rows = sum(len(b) for b in blocks) + cols = sum(len(b[0]) for b in blocks) + out = zero(rows, cols) + r0 = c0 = 0 + for b in blocks: + for i, row in enumerate(b): + out[r0 + i][c0:c0 + len(row)] = row[:] + r0 += len(b) + c0 += len(b[0]) + return out + + +def matrix_power(a, exponent): + require(exponent >= 0, "negative matrix exponent") + out = identity(len(a)) + for _ in range(exponent): + out = matmul(out, a) + return out + + +def apply_word(word, width): + rows = identity(width) + for kind, target, source, sign in word: + if kind == "ADD": + rows[target] = plus_rows(rows[target], rows[source], sign) + elif kind == "NEG": + rows[target] = [-v for v in rows[target]] + else: + raise ValueError("unknown operation kind") + return rows + + +def word_counts(word): + counts = {"ADD": 0, "NEG": 0} + for op in word: + counts[op[0]] += 1 + return counts + + +def row_l1_peak(word, width): + rows = identity(width) + peak = max(sum(abs(v) for v in row) for row in rows) + for kind, target, source, sign in word: + if kind == "ADD": + rows[target] = plus_rows(rows[target], rows[source], sign) + elif kind == "NEG": + rows[target] = [-v for v in rows[target]] + peak = max(peak, max(sum(abs(v) for v in row) for row in rows)) + return peak + + +def map_local(word, mapping, legacy): + return legacy.lift_word(word, mapping) + + +def phase_reader(legacy, q, block): + qmat = legacy.expected_octet_frame() + r = legacy.reader_matrix(block) + return matmul(matrix_power(qmat, (-q) % 4), r) + + +def typed_child(legacy, q, block): + """C_(block,q): D += Q^-q R_block W; W += (P-I)W.""" + r = phase_reader(legacy, q, block) + word = [] + for j, row in enumerate(r): + nz = [(i, c) for i, c in enumerate(row) if c] + require(len(nz) == 1 and nz[0][1] in (-1, 1), "typed reader is not signed selector") + i, sign = nz[0] + word.append(legacy.add(j, D + i, sign)) + word += legacy.lift_word(legacy.workspace_word(1), [D + i for i in range(BANK)]) + return word + + +def check_typed_children(legacy): + q = legacy.expected_octet_frame() + p = block_diag([q] * 3) + for block in sorted(set(BLOCKS_AB)): + r = legacy.reader_matrix(block) + for phase in range(4): + typed = phase_reader(legacy, phase, block) + require(matmul(typed, matrix_power(p, phase)) == r, + "Q^-t R_i P^t identity") + word = typed_child(legacy, phase, block) + actual = apply_word(word, D + BANK) + expected = identity(D + BANK) + for i in range(D): + expected[i][D:D + BANK] = typed[i][:] + expected[D:] = [[0] * D + row for row in p] + require(actual == expected, "typed child dirty-state map") + require(word_counts(word) == word_counts(legacy.child_word(block)), + "phase type changed the child ADD/NEG invoice") + + +def phase_costs(legacy): + return [word_counts(legacy.workspace_word(r)) for r in range(4)] + + +def cost_vector_add(a, b): + return {"ADD": a["ADD"] + b["ADD"], "NEG": a["NEG"] + b["NEG"]} + + +def best_phase_path(legacy, children): + """F_0(t)=A(t), F_(j+1)(s)=min_t F_j(t)+A(s-t-1), final s=0.""" + a = phase_costs(legacy) + state = {t: (a[t].copy(), (t,)) for t in range(4)} + for _ in range(children): + nxt = {} + for s in range(4): + options = [] + for t, (v, path) in state.items(): + gap = a[(s - t - 1) % 4] + nv = cost_vector_add(v, gap) + options.append((nv["ADD"] + nv["NEG"], path + (s,), nv)) + _, path, v = min(options) + nxt[s] = (v, path) + state = nxt + vector, path = state[0] + return tuple(path), vector + + +def exhaustive_phase_minimum(legacy, children): + a = phase_costs(legacy) + best = None + checked = 0 + for prefix in itertools.product(range(4), repeat=children): + states = prefix + (0,) + v = a[states[0]].copy() + for old, new in zip(states, states[1:]): + v = cost_vector_add(v, a[(new - old - 1) % 4]) + record = (v["ADD"] + v["NEG"], states, v) + if best is None or record < best: + best = record + checked += 1 + return best, checked + + +def lift_batch(legacy, states, blocks, source_switch=False, switch_index=SWITCH_INDEX, + switch_phase_delta=0, bad_reader_index=None): + """Emit D/W body with phase-typed readers and optional X-to-Y handoff.""" + require(len(states) == len(blocks) + 1, "path/block count") + require(states[-1] == 0, "terminal workspace phase") + local_map = list(range(D)) + [W + i for i in range(BANK)] + word = legacy.lift_word(legacy.workspace_word(states[0]), [W + i for i in range(BANK)]) + for i, block in enumerate(blocks): + phase = states[i] + if bad_reader_index == i: + phase = (phase + 1) % 4 + word += map_local(typed_child(legacy, phase, block), local_map, legacy) + gap = (states[i + 1] - states[i] - 1) % 4 + word += legacy.lift_word(legacy.workspace_word(gap), [W + j for j in range(BANK)]) + if source_switch and i == switch_index: + t = (states[i + 1] + switch_phase_delta) % 4 + p = block_diag([matrix_power(legacy.expected_octet_frame(), t)] * 3) + for j, row in enumerate(p): + nz = [(k, sign) for k, sign in enumerate(row) if sign] + require(len(nz) == 1 and nz[0][1] in (-1, 1), "handoff frame selector") + k, sign = nz[0] + word.append(legacy.add(W + j, Y + k, sign)) + word.append(legacy.add(W + j, X + k, -sign)) + return word + + +def source_wrapper(legacy, source, sign): + return [legacy.add(W + i, source + i, sign) for i in range(BANK)] + + +def make_root(legacy, states, blocks, source, phase_reader_mutation=None): + body = lift_batch(legacy, states, blocks, bad_reader_index=phase_reader_mutation) + return (source_wrapper(legacy, source, 1) + body + source_wrapper(legacy, source, -1) + + legacy.inverse_word(body)) + + +def expected_map(legacy, pairs): + """pairs is a list of (bank_offset, blocks); one +1 per block occurrence.""" + out = identity(TOTAL) + for bank, blocks in pairs: + for j in range(D): + for block in blocks: + out[j][bank + 8 * block + j] += 1 + return out + + +def vector_total(v): + return v["ADD"] + v["NEG"] + + +def vector_reads(v): + return 2 * v["ADD"] + v["NEG"] + + +def run(): + legacy, cert = load_predecessor() + check_typed_children(legacy) + leaf = cert["recursive_interface_cost"]["leaf_forward"] + a_costs = phase_costs(legacy) + + # Phase recurrence: exact paths and exhaustive coverage at the three sizes used. + path3, g3 = best_phase_path(legacy, 3) + path5, g5 = best_phase_path(legacy, 5) + path7, g7 = best_phase_path(legacy, 7) + path10, g10 = best_phase_path(legacy, 10) + brute3, paths3 = exhaustive_phase_minimum(legacy, 3) + brute5, paths5 = exhaustive_phase_minimum(legacy, 5) + brute7, paths7 = exhaustive_phase_minimum(legacy, 7) + brute10, paths10 = exhaustive_phase_minimum(legacy, 10) + require(brute3[2] == g3 and paths3 == 64, "three-child recurrence vs exhaustive") + require(brute5[2] == g5 and paths5 == 1024, "five-child recurrence vs exhaustive") + require(brute7[2] == g7 and paths7 == 16384, "seven-child recurrence vs exhaustive") + require(brute10[2] == g10 and paths10 == 1048576, "ten-child recurrence vs exhaustive") + + # Period-4 boundary law of the fixed interface: g(k) depends only on k mod 4. + law = {} + for k in range(1, 17): + _, gv = best_phase_path(legacy, k) + require(gv == best_phase_path(legacy, k % 4)[1] if k % 4 else gv == a_costs[0], + "period-4 boundary law at k=" + str(k)) + law[k] = gv + require(g3 == {"ADD": 54, "NEG": 6} and g7 == {"ADD": 54, "NEG": 6} + and g10 == {"ADD": 36, "NEG": 12}, "g3/g7/g10 exact vectors") + + # Positive control: reproduce the predecessor's published 5|5 two-bank figures. + expected55 = expected_map(legacy, [(X, BLOCKS5), (Y, BLOCKS5)]) + root_x = make_root(legacy, path5, BLOCKS5, X) + root_y = make_root(legacy, path5, BLOCKS5, Y) + separate55 = root_x + root_y + plain55 = lift_batch(legacy, path10, BLOCKS10) + switched55 = lift_batch(legacy, path10, BLOCKS10, source_switch=True, switch_index=4) + joint55 = (source_wrapper(legacy, X, 1) + switched55 + source_wrapper(legacy, Y, -1) + + legacy.inverse_word(plain55)) + require(apply_word(separate55, TOTAL) == expected55, "5|5 separate map control") + require(apply_word(joint55, TOTAL) == expected55, "5|5 joint map control") + sep55_vec = word_counts(separate55) + jnt55_vec = word_counts(joint55) + require(sep55_vec == {"ADD": 1552, "NEG": 144}, "5|5 separate invoice control") + require(jnt55_vec == {"ADD": 1408, "NEG": 144}, "5|5 joint invoice control") + require((vector_total(sep55_vec), vector_total(jnt55_vec), + vector_reads(sep55_vec), vector_reads(jnt55_vec)) == + (1696, 1552, 3248, 2960), "5|5 totals/reads control") + require(g5 == {"ADD": 54, "NEG": 6} and path5 == (0, 0, 1, 2, 3, 0) + and path10 == (0, 1, 0, 1, 2, 3, 0, 1, 2, 3, 0), + "predecessor g5/g10 paths control") + + # New cell: heterogeneous 3|7 readers on two distinct source banks. + expected37 = expected_map(legacy, [(X, BLOCKS_A), (Y, BLOCKS_B)]) + root_a = make_root(legacy, path3, BLOCKS_A, X) + root_b = make_root(legacy, path7, BLOCKS_B, Y) + separate37 = root_a + root_b + plain37 = lift_batch(legacy, path10, BLOCKS_AB) + switched37 = lift_batch(legacy, path10, BLOCKS_AB, source_switch=True, + switch_index=SWITCH_INDEX) + joint37 = (source_wrapper(legacy, X, 1) + switched37 + source_wrapper(legacy, Y, -1) + + legacy.inverse_word(plain37)) + require(apply_word(separate37, TOTAL) == expected37, + "3|7 heterogeneous two-bank separate map") + require(apply_word(joint37, TOTAL) == expected37, + "3|7 heterogeneous two-bank joint map") + + sep37_vec = word_counts(separate37) + jnt37_vec = word_counts(joint37) + # Recurrence invoices: E_1(k) = 2k*leaf + (2d,0) + 2g(k); joint = 2k*leaf + (4d,0) + 2g(k). + pred_a = cost_vector_add( + cost_vector_add({"ADD": 2 * len(BLOCKS_A) * leaf["ADD"], + "NEG": 2 * len(BLOCKS_A) * leaf["NEG"]}, + {"ADD": 2 * BANK, "NEG": 0}), + {"ADD": 2 * g3["ADD"], "NEG": 2 * g3["NEG"]}) + pred_b = cost_vector_add( + cost_vector_add({"ADD": 2 * len(BLOCKS_B) * leaf["ADD"], + "NEG": 2 * len(BLOCKS_B) * leaf["NEG"]}, + {"ADD": 2 * BANK, "NEG": 0}), + {"ADD": 2 * g7["ADD"], "NEG": 2 * g7["NEG"]}) + pred_sep = cost_vector_add(pred_a, pred_b) + pred_jnt = cost_vector_add( + cost_vector_add({"ADD": 2 * len(BLOCKS_AB) * leaf["ADD"], + "NEG": 2 * len(BLOCKS_AB) * leaf["NEG"]}, + {"ADD": 4 * BANK, "NEG": 0}), + {"ADD": 2 * g10["ADD"], "NEG": 2 * g10["NEG"]}) + require(sep37_vec == pred_sep == {"ADD": 1552, "NEG": 144}, + "3|7 separate invoice and recurrence agreement") + require(jnt37_vec == pred_jnt == {"ADD": 1408, "NEG": 144}, + "3|7 joint invoice and recurrence agreement") + require((vector_total(sep37_vec), vector_total(jnt37_vec), + vector_reads(sep37_vec), vector_reads(jnt37_vec)) == + (1696, 1552, 3248, 2960), "3|7 totals/reads") + saving = {"primitives": vector_total(sep37_vec) - vector_total(jnt37_vec), + "reads": vector_reads(sep37_vec) - vector_reads(jnt37_vec)} + require(saving == {"primitives": 144, "reads": 288}, "3|7 saving") + + # Invoice law across splits: separate - joint = 2*(g(k1)+g(k2)-g(k1+k2)). + # With k1+k2 = 10 this is (144,0) exactly when both child counts are odd, + # and (0,0) when both are even: g(1)=g(3)=(54,6), g(2)=(36,12), g(0)=(0,0). + split_law = {} + for k1 in range(1, 10): + k2 = 10 - k1 + _, gk1 = best_phase_path(legacy, k1) + _, gk2 = best_phase_path(legacy, k2) + diff = cost_vector_add(cost_vector_add( + {"ADD": 2 * gk1["ADD"], "NEG": 2 * gk1["NEG"]}, + {"ADD": 2 * gk2["ADD"], "NEG": 2 * gk2["NEG"]}), + {"ADD": -2 * g10["ADD"], "NEG": -2 * g10["NEG"]}) + split_law[k1] = diff + expected_diff = {"ADD": 144, "NEG": 0} if k1 % 2 else {"ADD": 0, "NEG": 0} + require(diff == expected_diff, "split invoice law at " + str(k1)) + + # Even-split instance (2|8): the joint word is legal but merges no boundary work. + blocks_even = (0, 1) + (2, 1, 0, 2, 1, 0, 2, 2) + path2, g2 = best_phase_path(legacy, 2) + path8, g8 = best_phase_path(legacy, 8) + require(g2 == {"ADD": 36, "NEG": 12} and g8 == {"ADD": 0, "NEG": 0}, "g2/g8 vectors") + expected28 = expected_map(legacy, [(X, blocks_even[:2]), (Y, blocks_even[2:])]) + root_a2 = make_root(legacy, path2, blocks_even[:2], X) + root_b2 = make_root(legacy, path8, blocks_even[2:], Y) + separate28 = root_a2 + root_b2 + plain28 = lift_batch(legacy, path10, blocks_even) + switched28 = lift_batch(legacy, path10, blocks_even, source_switch=True, switch_index=1) + joint28 = (source_wrapper(legacy, X, 1) + switched28 + source_wrapper(legacy, Y, -1) + + legacy.inverse_word(plain28)) + require(apply_word(separate28, TOTAL) == expected28, "2|8 separate map") + require(apply_word(joint28, TOTAL) == expected28, "2|8 joint map") + sep28_vec = word_counts(separate28) + jnt28_vec = word_counts(joint28) + require(vector_total(sep28_vec) == vector_total(jnt28_vec), + "2|8 even split must merge no boundary work") + require(sep28_vec == jnt28_vec, "2|8 even-split invoice equality") + + # Negative controls for the 3|7 cell. + wrong_switch = lift_batch(legacy, path10, BLOCKS_AB, source_switch=True, switch_index=4) + wrong_switch_word = (source_wrapper(legacy, X, 1) + wrong_switch + + source_wrapper(legacy, Y, -1) + legacy.inverse_word(plain37)) + require(apply_word(wrong_switch_word, TOTAL) != expected37, + "midpoint-switch control escaped") + wrong_phase = lift_batch(legacy, path10, BLOCKS_AB, source_switch=True, + switch_index=SWITCH_INDEX, switch_phase_delta=1) + wrong_phase_word = (source_wrapper(legacy, X, 1) + wrong_phase + + source_wrapper(legacy, Y, -1) + legacy.inverse_word(plain37)) + require(apply_word(wrong_phase_word, TOTAL) != expected37, + "wrong handoff phase control escaped") + wrong_reader_root = make_root(legacy, path3, BLOCKS_A, X, phase_reader_mutation=2) + require(apply_word(wrong_reader_root + root_b, TOTAL) != expected37, + "mutated A reader control escaped") + require(apply_word(root_a, TOTAL) != expected37, "omitted B call control escaped") + missing_restore = (source_wrapper(legacy, X, 1) + switched37 + legacy.inverse_word(plain37)) + require(apply_word(missing_restore, TOTAL) != expected37, + "missing final Y restoration control escaped") + missing_inverse = (source_wrapper(legacy, X, 1) + switched37 + + source_wrapper(legacy, Y, -1)) + require(apply_word(missing_inverse, TOTAL) != expected37, + "missing literal inverse control escaped") + + return { + "status": "PASS_Z4_HETERO_TWO_BANK_3_7", + "base_commit": BASE, + "assignment": { + "track": "recursive-interfaces", + "task_id": "persistent-boundary", + "chooser_nonce": "ba18ac446df7d55ddc50d91395fd9a57", + "scope_key": "026be4b6e61971d51838", + "priority_revision": 3, + "card_selection_note": "second-choice card after the centre-path-sharing pair collision", + }, + "predecessors": { + "PR1391_head": PR1391_HEAD, + "PR1410_head": PR1410_HEAD, + "PR1391_certificate_sha256": PINS["inputs/PR1391/CERTIFICATE.json"][0], + "PR1391_verifier_sha256": PINS["inputs/PR1391/verify.py"][0], + "PR1410_readme_sha256": PINS["inputs/PR1410-README.md"][0], + "nearest_packages": [ + "research/z4-distinct-source-seed55 (typed two-bank 5|5, midpoint handoff)", + "research/z4-heterogeneous-pair-seed3x7 (heterogeneous 3|7, one shared source, canonical phase path)", + ], + }, + "scope": "Exact phase-indexed typed child family with heterogeneous reader schedules on two distinct source banks; not an admitted selected supplier.", + "dimensions": {"D": D, "X": BANK, "Y": BANK, "W": BANK, "total_basis_columns": TOTAL}, + "types": { + "A_blocks": list(BLOCKS_A), + "A_source": "X", + "B_blocks": list(BLOCKS_B), + "B_source": "Y", + "handoff": "W += P^t (Y-X) after child 2, t = phase[3]; 48 ADDs", + "handoff_phase": path10[SWITCH_INDEX + 1], + }, + "phase_reader": "C_(i,t): D += Q^(-t) R_i W; W += (P-I)W; type t has same ADD/NEG count as C_i.", + "recurrence": { + "workspace_phase_costs_ADD_NEG": a_costs, + "F0(t)": "A(t)", + "Fnext(s)": "min_t F(t)+A((s-t-1) mod 4)", + "terminal_phase": 0, + "period_4_law": "g(k) = g(k mod 4) with g(0) = (0,0); checked for k = 1..16", + "g3_path": list(path3), "g3_ADD_NEG": g3, "g3_exhaustive_paths": paths3, + "g5_path": list(path5), "g5_ADD_NEG": g5, "g5_exhaustive_paths": paths5, + "g7_path": list(path7), "g7_ADD_NEG": g7, "g7_exhaustive_paths": paths7, + "g10_path": list(path10), "g10_ADD_NEG": g10, "g10_exhaustive_paths": paths10, + "split_invoice_law": "separate(k1,k2) - joint(k1,k2) = 2*(g(k1)+g(k2)-g(10)); at total 10 this is 144 ADDs iff both child counts are odd and 0 when both are even", + "split_law_vectors": {str(k): v for k, v in split_law.items()}, + }, + "predecessor_5_5_control": { + "separate_ADD_NEG": sep55_vec, + "joint_ADD_NEG": jnt55_vec, + "separate_primitives": vector_total(sep55_vec), + "joint_primitives": vector_total(jnt55_vec), + "map": "PASS on all 80 basis columns", + "matches_research/z4-distinct-source-seed55": True, + }, + "separate_calls": { + "ADD_NEG": sep37_vec, + "primitives": vector_total(sep37_vec), + "reads": vector_reads(sep37_vec), + "prefix_row_l1_peak": row_l1_peak(separate37, TOTAL), + "map": "PASS on all 80 basis columns", + }, + "joint_3_7_two_banks": { + "ADD_NEG": jnt37_vec, + "primitives": vector_total(jnt37_vec), + "reads": vector_reads(jnt37_vec), + "prefix_row_l1_peak": row_l1_peak(joint37, TOTAL), + "map": "PASS on all 80 basis columns", + }, + "saving": saving, + "even_split_2_8_control": { + "A_blocks": list(blocks_even[:2]), + "B_blocks": list(blocks_even[2:]), + "separate_ADD_NEG": sep28_vec, + "joint_ADD_NEG": jnt28_vec, + "saving": {"primitives": vector_total(sep28_vec) - vector_total(jnt28_vec), + "reads": vector_reads(sep28_vec) - vector_reads(jnt28_vec)}, + "map": "PASS on all 80 basis columns for both words", + "meaning": "even splits merge no boundary work; the 144 saving needs both child counts odd", + }, + "controls": { + "predecessor_5_5_invoices_and_maps": "PASS", + "typed_child_phase_identity_checks": "PASS for 12 (phase,reader) pairs", + "exhaustive_phase_coverage": "PASS at 64 + 1024 + 16384 + 1048576 paths", + "midpoint_switch_instead_of_3_7_boundary": "REJECTED", + "wrong_handoff_phase": "REJECTED", + "mutated_A_reader": "REJECTED", + "omitted_B_call": "REJECTED", + "missing_final_Y_restoration": "REJECTED", + "missing_literal_inverse": "REJECTED", + }, + "assumptions_and_limits": [ + "Output-row reindexing is part of the typed ADD target choice and has no additional scalar ADD/NEG instruction in this word model.", + "Address, tape, source-hosting, precision admission, recursive assembly into a selected supplier and analytic transfer are not charged or proved.", + "The joint word raises the prefix row-L1 envelope; no precision improvement is claimed.", + "The finite recurrence is exact only for the declared order-four phase-indexed child alphabet; it is not a lower bound for arbitrary words.", + "No new kappa or selected-result change is claimed.", + ], + } + + +def main(): + result = run() + certificate_path = PACKAGE / "RESULT.json" + canonical = json.dumps(result, indent=2, sort_keys=True) + "\n" + if sys.argv[1:] == ["--write-result"]: + certificate_path.write_text(canonical, encoding="utf-8", newline="\n") + print("WROTE_RESULT " + str(certificate_path.relative_to(ROOT))) + else: + require(certificate_path.is_file(), "missing RESULT.json; run --write-result once") + require(certificate_path.read_text(encoding="utf-8") == canonical, + "RESULT.json differs from the recomputed exact evidence") + print(result["status"] + + f" g3={vector_total(result['recurrence']['g3_ADD_NEG'])}" + f" g7={vector_total(result['recurrence']['g7_ADD_NEG'])}" + f" g10={vector_total(result['recurrence']['g10_ADD_NEG'])}" + f" separate={result['separate_calls']['primitives']}" + f" joint={result['joint_3_7_two_banks']['primitives']}" + f" saved={result['saving']['primitives']}" + f" reads_saved={result['saving']['reads']}" + f" law=odd_splits_only even28_saved={result['even_split_2_8_control']['saving']['primitives']}" + f" paths=64+1024+16384+1048576 basis=80 controls=6") + + +if __name__ == "__main__": + main()