diff --git a/research/z4-paired-frame-restoration-seed56/CERTIFICATE.json b/research/z4-paired-frame-restoration-seed56/CERTIFICATE.json new file mode 100644 index 0000000000..0132b117d9 --- /dev/null +++ b/research/z4-paired-frame-restoration-seed56/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-paired-frame-restoration-seed56/CLAIM.md b/research/z4-paired-frame-restoration-seed56/CLAIM.md new file mode 100644 index 0000000000..49f7efff3d --- /dev/null +++ b/research/z4-paired-frame-restoration-seed56/CLAIM.md @@ -0,0 +1,35 @@ +# Seed 56 task selection and overlap record + +**Track:** recursive interfaces. **OS seed:** 56. **Base:** `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. The seed maps to cycle order `2 + (56 mod 3) = 4`. + +## Three narrow candidates considered + +1. **Selected #1094 T16 same-owner call boundary.** Test whether one concrete repeated owner restore is immediately rebuilt by its next chronological call. The selected review and [heterogeneous owner assembly](../heterogeneous-owner-assembly/README.md) bound the frozen owner catalogue, while recent #1240/#1348 reports quantify selected-word packing headroom and changed coverage-law thresholds. PR #1252's `Z4` is a rank-pair phase polynomial in idle owner repartitioning, not a fourth-order output frame. The task still needed an exact identified two-call transition and a new legal return contract; no such concrete transition was established in this orientation pass. +2. **Signed-reader restoration coalescing.** A specific checkpoint-correct cut problem for fixed dirty readers could reduce restoration. This overlaps current #1199 (diagonal signed readers), #1203 (noncommuting reader restoration) and #1246/#1227 (paid reader-defect and output-sign repair), so it was not selected. +3. **Order-four paired-cycle output-frame boundary.** Extend the already explicit cyclic output-frame mechanism to a genuinely different phase group and gate-cost profile. Current #1287 is order three; its recurrence does not cover the order-four paired cycles, whose phase powers require NEG accounting. Exact-term search found no matching order-four frame task. + +## Chosen scope and claim + +I chose candidate 3. The task is the five-child dirty echo with three workspace octets, one output octet, and selectors `(0,1,2,0,1)`. The checked macro alphabet is the explicit set of whole-register powers of the paired order-four frame. It compares a complete optimized echo with the eager per-child inverse frame. + +Claim posted on [coordination discussion #1163](https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18911404) at 2026-10-13 23:35 UTC; expected finish 2026-10-14 00:08 UTC, expiry 01:35 UTC. + +## Finding + +The certified path is `[0,1,2,3,0,0]`: the five-child boundary costs 140 primitives (`126 ADD, 14 NEG`) versus 300 eager (`270 ADD, 30 NEG`). The complete arbitrary-dirty echo costs 1,008 (`920 ADD, 88 NEG`) versus 1,328 (`1,208 ADD, 120 NEG`), saving 320. The corresponding internal `C_v` map and its literal inverse are also checked over all 56 input/scratch basis columns. The exact 9-ADD/1-NEG quarter-turn word was found during the final cost audit; an earlier three-pure-swap word was replaced before freezing the result. The final prefix row-L1 peak rises 11 to 20. + +## Overlap evidence + +At 2026-10-13 23:33 UTC, `python3 scripts/find_overlap.py 'order-four cycle output frame Z4 paired cycles' --refresh --limit 12` searched complete snapshots of **839 open PRs** and **89 discussions** and returned zero exact multiword matches. A later offline cached query at 23:44 returned PR #1287 for `cyclic output frames`, the posted seed-56 claim for `paired 4-cycles`, and PR #1252 for `Z4`. Direct inspection confirmed that #1252 uses `Z4` for a rank-pair phase polynomial in idle owner repartitioning, not an order-four output frame. The helper does not search arbitrary PR code diffs or nested package files; this is not a novelty certificate. Direct inspection established the nearest distinctions: + +- [#1287](https://github.com/CrocSwap/integer-mult-bounds/pull/1287), head `8606df05eca3c65032361c74ee3dbc2630b0cdc4`: order-three cyclic output frames with a three-state recurrence. +- [#1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199), head `85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d`: cancelling signed diagonal readers and checkpoint-correct partitions. +- [#1203](https://github.com/CrocSwap/integer-mult-bounds/pull/1203), head `38459854fd5bb93099871a84324413bd0e338d8e`: noncommuting reader restoration under a paid dirty wrapper. +- [#1227](https://github.com/CrocSwap/integer-mult-bounds/pull/1227), head `fea44a4d0d78570021d854881d15d9efe62e1713`: sharp output-sign restoration for a fixed-reader boundary. +- [#1246](https://github.com/CrocSwap/integer-mult-bounds/pull/1246), head `5ed1ce17a9df4c853a93f9758ba903d2620c3443`: paid nonzero reader-defect repair. +- [#1303](https://github.com/CrocSwap/integer-mult-bounds/pull/1303), head `bddf5ba853f1b798d021454362e53338c819f150`: exact ten-primitive lower bound for a restored local disjoint 2+3-cycle boundary, including finite dirty donors. It changes a local restoration word; this scope instead changes the child-facing frame contract. +- [#805](https://github.com/CrocSwap/integer-mult-bounds/pull/805), head `ef34bd5b32fcf2d5640dae90b5b8f28488738d5a`: determinant-balanced cyclic recurrence leaves with a different coefficient and precision contract. +- [#846](https://github.com/CrocSwap/integer-mult-bounds/pull/846), head `4bdb3e755ea7118170a7a34764df955880dec282`: stride-dependent cyclic inverse scheduling; different object and tape recurrence. +- [#1252](https://github.com/CrocSwap/integer-mult-bounds/pull/1252), head `1b9db2faf82b8866b0bb0164501c9a627c7dca9b`: the literal `Z4` match is an exact owner rank-pair phase polynomial for `48+48 -> 45+51`, not a four-cycle frame. + +The targeted local-ledger search for these PR numbers returned no rows; the live heads and bodies above therefore control this overlap check. No selected construction or prior negative result is changed. diff --git a/research/z4-paired-frame-restoration-seed56/PREDECESSORS.json b/research/z4-paired-frame-restoration-seed56/PREDECESSORS.json new file mode 100644 index 0000000000..5532bc5c48 --- /dev/null +++ b/research/z4-paired-frame-restoration-seed56/PREDECESSORS.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "new_work_commit_base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "predecessors": [ + { + "pr": 1287, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1287", + "head": "8606df05eca3c65032361c74ee3dbc2630b0cdc4", + "author": "Ross Richardson", + "contribution": "Order-three cyclic output frames, equivariant-reader admission, and a three-state boundary recurrence with a full dirty echo.", + "relationship": "Closest method predecessor. This package uses a paired order-four frame, different ADD/NEG phase costs, and a separate five-child invoice; no implementation is copied." + }, + { + "pr": 1227, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1227", + "head": "fea44a4d0d78570021d854881d15d9efe62e1713", + "author": "Sagar Thakrar", + "contribution": "Paid output-sign frames and exact restoration costs for fixed signed-permutation readers.", + "relationship": "Retained credit for output-frame restoration; the paired order-four permutation and five-child recurrence are distinct." + }, + { + "pr": 1199, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1199", + "head": "85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d", + "author": "Sagar Thakrar (PR body credits Navinor / Aaron Wang)", + "contribution": "Checkpoint-correct coalescing of restoration for fixed signed diagonal readers.", + "relationship": "Related dirty-restoration baseline; its cut planner does not contain the paired order-four phase model." + }, + { + "pr": 1203, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1203", + "head": "38459854fd5bb93099871a84324413bd0e338d8e", + "author": "mightyOil", + "contribution": "Noncommuting reader-restoration identities with a paid dirty-state wrapper.", + "relationship": "Related reader-interface work; this package uses fixed block selectors and explicitly prices cyclic frame gates." + }, + { + "pr": 1246, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1246", + "head": "5ed1ce17a9df4c853a93f9758ba903d2620c3443", + "author": "Hanson Sun", + "contribution": "Paid repair of nonzero reader defects at canonical cuts.", + "relationship": "Related correction mechanism; not used in the paired-cycle frame construction." + }, + { + "pr": 1303, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1303", + "head": "bddf5ba853f1b798d021454362e53338c819f150", + "author": "mightyOil", + "contribution": "A scoped exact ten-primitive lower bound for a restored disjoint 2+3-cycle boundary, including arbitrary finite restored dirty donors.", + "relationship": "Relevant negative result for restored local cycles. It does not include this package's equivariant child maps or coupled P/Q frame phase schedule." + }, + { + "pr": 805, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/805", + "head": "ef34bd5b32fcf2d5640dae90b5b8f28488738d5a", + "author": "Victor Liwentao", + "contribution": "A determinant-balanced cyclic recurrence leaf with coefficient, precision, and dirty restoration accounting.", + "relationship": "A different cyclic recurrence and data type; the present frame action is a finite signed-permutation interface." + }, + { + "pr": 846, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/846", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "author": "Rohan S. Guliani", + "contribution": "Stride-independent cyclic inverse cost on sequential tapes.", + "relationship": "Different object and tape recurrence; cited to distinguish the word cyclic in the overlap review." + } + ], + "selected_lineage": { + "selected_result": "certificates/selected-result.json", + "selected_supplier_pr": 1094, + "complex_word_predecessor_pr": 1087, + "bit_supplier_pr": 589, + "bit_lineage_pr": 555, + "relationship": "Source-pinned context only. The finite q4 interface is not integrated into the selected suppliers or profile." + }, + "code_reuse": "No predecessor implementation or source archive is copied." +} diff --git a/research/z4-paired-frame-restoration-seed56/README.md b/research/z4-paired-frame-restoration-seed56/README.md new file mode 100644 index 0000000000..36a48934ed --- /dev/null +++ b/research/z4-paired-frame-restoration-seed56/README.md @@ -0,0 +1,136 @@ +# Paired order-four frames defer repeated workspace restoration + +**Scoped recursive-interface construction; no new `kappa` and no supplier adoption.** A fixed five-child interface admits a cheap boundary schedule when one four-cycle frame is carried across child calls and paid back at the end. The exact complete dirty echo uses **1,008 scalar primitives** instead of **1,328** for eager restoration. The order-four signed gate accounting and this fixture are new; this extends the order-three frame interface in [PR #1287](https://github.com/CrocSwap/integer-mult-bounds/pull/1287) without reusing its implementation. + +The assignment seed is **56**, on the recursive-interface track. The seed-selected cycle order is `2 + (56 mod 3) = 4`. The exact research base is `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. Current selected context at that base remains the maintainer-reviewed conditional finite construction with `kappa = 836330098538459/500000000000000000 = 0.001672660197076918`, selected from Rohan Arun's PR #1094 on Jeremy Kothe's retained word and the PR589/555 bit lineage. The source record, review, selected source manifest and assembly are pinned in [SOURCES.json](SOURCES.json). The selected record is unchanged. + +## The fixed child contract + +An **octet frame** is two disjoint four-cycles. On either quartet, + +```text +(a,b,c,d) -> (d,a,b,c). +``` + +Let `P` act by this same paired cycle on each of three eight-coordinate workspace blocks (`W` has 24 coordinates), and let `Q` act on one output octet (`D` has 8 coordinates). Each has order four and determinant `+1` because it is the product of two odd four-cycles. For `i` in `(0,1,2,0,1)`, `R_i` selects workspace octet `i` and the child is the indivisible map + +```text +C_i(D,W) = (D + R_i W, P W), R_i P = Q R_i. +``` + +All 8 output coordinates and all 24 workspace coordinates may be arbitrary. The displayed intertwining equality is checked exactly for all three distinct selectors. In an aligned frame `t`, the child contribution is `Q^t R_i W`; any different output phase gives the wrong contribution for that selector. + +The macro alphabet between children consists only of the explicit whole-register powers `P^u` and `Q^v`, for `u,v in Z/4Z`. A pure swap can use + +```text +a += b; b -= a; a += b; NEG(b) +``` + +and maps `(a,b)` to `(b,a)` exactly. The quarter-turn uses fewer gates than three pure swaps: apply the 3-ADD signed swaps `(a,b)->(b,-a)`, `(a,c)->(-c,a)`, and `(a,d)->(d,-a)`, then `NEG(b)`, to obtain `(d,a,b,c)` in **9 ADD + 1 NEG**. Its half-turn uses two disjoint pure swaps, costing **6 ADD + 2 NEG**. The inverse quarter-turn has the same counts. No frame annotation, clean scratch or free operation is used. These are explicit circuit costs, not claims of primitive optimality. + +The signed-swap words are + +```text +T+(a,b): a += b; b -= a; a += b gives (b,-a) +T-(a,b): b += a; a -= b; b += a gives (-b,a) +``` + +For a quartet, the sequence `T+(a,b); T-(a,c); T+(a,d); NEG(b)` passes through `(b,-a,c,d)`, `(-c,-a,b,d)`, `(d,-a,b,c)`, then `(d,a,b,c)`. + +Per output octet, the four phase costs are: + +| Phase | ADD | NEG | Total | +|---:|---:|---:|---:| +| 0 | 0 | 0 | 0 | +| 1 | 18 | 2 | 20 | +| 2 | 12 | 4 | 16 | +| 3 | 18 | 2 | 20 | + +`P` acts on three octets, so its phase cost is three times this vector; `Q` uses one copy. The full words and their exact matrices are produced by the verifier. + +## Exact boundary recurrence + +Let `t` be the common workspace/output phase immediately before a child. That child advances phases to `(t+1,t)`. To finish the gap in aligned phase `s`, there is one required pair of powers: + +```text +P^(s-t-1) on W, Q^(s-t) on D. +``` + +Write `A(r)` for the total primitive cost of `P^r` on all 24 workspace coordinates and `B(r)` for the total cost of `Q^r` on `D`. The exact shortest-path recurrence in this fixed macro alphabet is + +```text +F_0(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) = F_k(0). +``` + +Entrance and terminal corrections are included. Before the first child the two phases must agree; after the last child both registers must be canonical because `D` and `W` are arbitrary. Every legal macro word therefore gives one path in the four-state graph, and every path is emitted by the stated powers. This proves the recurrence for every positive child count in the declared alphabet. For the five-child fixture, a complete path census checks all `4^5 = 1,024` phase paths. + +The minimum path is `[0,1,2,3,0,0]`. It rotates `Q` once after each of the first four children, then pays one `P^3` workspace correction after the fifth: + +| Batch boundary | Optimized ADD | Optimized NEG | Total | Eager total | +|---|---:|---:|---:|---:| +| `g(5)` | 126 | 14 | **140** | **300** | + +The eager schedule restores `P^-1` after every child. The optimized schedule saves 160 primitives per batch. This is exact optimality only among the fixed macro powers, not among arbitrary ADD/NEG words that might be inserted into gaps. + +## Complete dirty echo and recursive invoice + +Each leaf child reads eight selected coordinates with eight ADDs and applies `P` to the 24-coordinate workspace. Its complete forward and literal inverse costs are both `(62 ADD, 6 NEG) = 68` primitives. A five-child forward batch therefore costs `(436 ADD, 44 NEG) = 480` when optimized, versus `(580 ADD, 60 NEG) = 640` eagerly. + +The full echo uses a separate arbitrary source `X` and dirty work register `W`: + +```text +W += X; H(D,W); W -= X; H^-1(D,W) +``` + +Both copies cost 24 ADDs. `H^-1` is the literal reversed batch word with each ADD sign reversed; it includes every inverse child. The verified map is `(D,X,W) -> (D + sum_i R_i X, X, W)` for arbitrary dirty `D`, `X` and `W`. + +| Complete echo | ADD | NEG | Total primitives | Data reads | Data writes | +|---|---:|---:|---:|---:|---:| +| Optimized frames | 920 | 88 | **1,008** | 1,928 | 1,008 | +| Eager restoration | 1,208 | 120 | **1,328** | 2,536 | 1,328 | + +Here each ADD reads two cells and writes one; each NEG reads and writes one. Dispatches equal primitive count. Peak data storage is exactly 56 coordinates for this root echo: 8 output, 24 source and 24 work coordinates. Sums of intertwining readers still satisfy `R_v P = Q R_v`, so an internal node can use `R_v = sum_i R_i` as the same typed child interface. Its complete cost recurrence is + +```text +leaf C: T = (62,6) +internal C: T_v = 2 sum_i T_i + (48,0) + 2 g_vec(k_v) + (54,6) +root echo: E_v = 2 sum_i T_i + (48,0) + 2 g_vec(k_v) +``` + +Vectors are `(ADD,NEG)`. `g_vec` is the phase vector on a minimum-total path. The `(48,0)` term is the copy and restoration of all 24 coordinates. The final `(54,6)` in `C_v` applies `P` to its own input workspace. The eager comparison replaces `g_vec(k_v)` with `k_v*(54,6)`. Each simultaneously active nested internal child needs one additional 24-coordinate scratch block, so peak storage for this fixed interface is `56 + 24h`, where `h` is the number of nested internal levels below the root echo. No clean scratch is assumed. + +For the five-leaf fixture, the internal `C_v` itself costs `(974 ADD, 94 NEG) = 1,068` primitives with optimized frames and `(1,262 ADD, 126 NEG) = 1,388` eagerly. The verifier checks both internal maps and the literal inverse on all 56 input/scratch basis columns. The 60-operation final `P` on the interface input is included in both totals. + +For the root echo, the optimized word raises the exact prefix row-L1 bound from 11 to 20. Its benefit in primitive count carries a precision-width risk. Address travel, coefficient fetches and descriptor storage are not priced as a supplier implementation; no runtime or fixed-precision improvement is claimed. + +## Verification + +From the repository root, run: + +```sh +python3 -I -O -B research/z4-paired-frame-restoration-seed56/verify.py +``` + +Expected marker: + +```text +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 +``` + +The standalone verifier checks the selected source pins; order-four frame powers and determinant; all `R_iP=QR_i` identities; child and literal inverse maps; the recurrence minimum against all 1,024 paths; both complete batch maps; the full echo on all 56 basis columns; the ADD/NEG, copy, inverse and data-access invoices; and four failure controls for a bad rotation sign, a wrong output phase, missing terminal restoration and forward-for-inverse substitution. It uses only the Python standard library. Local verification used CPython 3.14.7; the package hook declares the repository's Python 3.12 environment. The registered wrapper's replay mode requires Python 3.12, which is unavailable locally; its metadata/pin check and the standalone verifier pass. A full selected cold replay, hosted CI run and independent human review were not performed. + +## Scope and predecessors + +The closest predecessor is Ross Richardson's [PR #1287](https://github.com/CrocSwap/integer-mult-bounds/pull/1287), which supplies an order-three cyclic output-frame recurrence and dirty echo. This package independently treats an order-four, determinant-positive paired frame with explicit NEG costs and a new complete invoice. It also credits Sagar Thakrar's [PR #1227](https://github.com/CrocSwap/integer-mult-bounds/pull/1227) for paid output-sign frames. PR #805's determinant-balanced cyclic leaf concerns a different cyclic recurrence and coefficient/precision model; PR #846's cyclic inverse concerns stride-dependent tape scheduling. No predecessor implementation is copied. Exact checked-out source pins and predecessor heads are listed in [SOURCES.json](SOURCES.json) and [PREDECESSORS.json](PREDECESSORS.json). + +This does not identify a real selected supplier with the indivisible order-four child contract. Physical hosting, routing, tape, fixed precision, coefficient access, common-label admission and analytic transfer remain open. The selected `kappa` and all selected files are unchanged. No full multiplication theorem or universal optimality claim follows from this finite construction. + +## Open next questions + +Can a named candidate supplier expose the paired order-four intertwiner `R P = Q R`? This matters because only a compatible supplier can turn the boundary invoice into a changed recursive profile. A feasible first step is to inspect one retained supplier's exact child matrices for an eight-coordinate paired-cycle invariant; the blocker is that no physical hosting or precision-admitted supplier has yet been identified. + +## Credit + +Prepared by **Cinna Davis** with substantial **OpenAI Codex assistance** in algebra, code, verification and prose. The verifier and certificate are AI-assisted; no independent human review or proof-assistant formalization is implied. Prior work is credited above and pinned in `PREDECESSORS.json`. New package material is Apache-2.0. diff --git a/research/z4-paired-frame-restoration-seed56/SOURCES.json b/research/z4-paired-frame-restoration-seed56/SOURCES.json new file mode 100644 index 0000000000..811a06e354 --- /dev/null +++ b/research/z4-paired-frame-restoration-seed56/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "docs/research/current-status.md", + "usage": "provenance", + "git_blob": "aa3cf49715cd367ad8c4e63ab28856fc0d19794f", + "sha256": "1f59d648763c77d574d18dc59ea8bf62d2ee74aaed3c202c9c8cfa4f901badbd" + }, + { + "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" + } + ] +} diff --git a/research/z4-paired-frame-restoration-seed56/TASK.json b/research/z4-paired-frame-restoration-seed56/TASK.json new file mode 100644 index 0000000000..433cb42307 --- /dev/null +++ b/research/z4-paired-frame-restoration-seed56/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "persistent-boundary", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "persistent-boundary", + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Write typed entry/exit contracts and a contracting multitype recurrence.", + "Derive a lower bound for the compulsory transitions of one proposed typed interface." + ], + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "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." + }, + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "allowed_variations": [ + "A two-type pilot or one explicit deferred restoration." + ], + "scope_change_triggers": [ + "Rewriting the old scalar recurrence as a matrix without eliminating work." + ], + "overlap_terms": [ + "persistent boundary", + "deferred restoration", + "multitype" + ] + }, + "scope_status": "changed", + "scope_change_reason": "The direct selected-owner and signed-reader restoration boundaries are already crowded. Seed 56 refines the investigation to an order-four paired-cycle frame, distinct from PR1287's order-three frame, with a different phase group and an ADD/NEG cost vector. The five-child pilot tests actual repeated inverse-frame elimination and its complete dirty echo.", + "actual_scope": "For five fixed equivariant children on three workspace octets and one output octet, find and verify the exact cheapest boundary schedule in the explicit four-state macro alphabet generated by the paired order-four frame, and compare its full arbitrary-dirty echo bill with eager restoration.", + "bottleneck_link": "The frame carried through four child boundaries replaces four repeated workspace inverse frames by output-frame rotations and one terminal workspace correction. If an actual supplier admits this typed interface, the avoided primitives can reduce its recursive node bill; no current supplier is shown to admit it.", + "budget_minutes": 60, + "stop_rule": "Exhaust all 4^5 phase prefixes for the five-child path, compare that minimum with the 4-state dynamic program, and verify all 56 basis columns of the complete dirty echo. Stop if typed composition fails or the complete bill does not improve; make no claim outside this fixed macro alphabet and fixture.", + "outcome": "completed", + "evidence": "The exact four-state recurrence has path [0,1,2,3,0,0], boundary cost 140 ADD/NEG primitives versus eager cost 300. The complete echo costs 920 ADD plus 88 NEG (1008 total), versus 1208 ADD plus 120 NEG (1328 total), with identical map on all 56 arbitrary dirty/source basis columns. The corresponding internal C_v costs 974 ADD plus 94 NEG versus 1262 ADD plus 126 NEG and its map/inverse also pass all 56 basis columns. Exhaustive enumeration of the 1024 complete phase paths returns the same minimum as the dynamic program. Four failure controls detect a sign mutation, wrong output phase, omitted terminal restoration, and forward-for-inverse substitution. The optimized prefix row-L1 peak rises 11 to 20.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in algebra, code, verification and prose. No independent human review or proof-assistant formalization is claimed.", + "open_questions": [ + { + "question": "Does any actual selected or candidate supplier expose an indivisible order-four paired-cycle child interface satisfying R P = Q R?", + "why_it_matters": "A compatible real supplier is needed before the finite echo saving can affect a paid recursive profile or kappa.", + "first_step": "Inspect one named supplier's child boundary matrices for an eight-coordinate paired-cycle intertwiner, then price its full frame and inverse word.", + "blocked_by": "No physical hosting, source-family admission, finite-precision contract or matching supplier has been identified." + } + ] +} diff --git a/research/z4-paired-frame-restoration-seed56/VERIFY.json b/research/z4-paired-frame-restoration-seed56/VERIFY.json new file mode 100644 index 0000000000..736a085cae --- /dev/null +++ b/research/z4-paired-frame-restoration-seed56/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/community-batch1099-review.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Recheck exact source pins, paired-cycle gate words and order, all R_i P = Q R_i identities, child/inverse dirty maps, the four-state optimum against all 1024 paths, complete eager and optimized batch maps, the root echo and one internal C_v map on all 56 dirty/source/scratch basis columns, full ADD/NEG/copy/inverse invoices, and four mathematical failure controls." + } + ] +} diff --git a/research/z4-paired-frame-restoration-seed56/verify.py b/research/z4-paired-frame-restoration-seed56/verify.py new file mode 100644 index 0000000000..4d2524cb3c --- /dev/null +++ b/research/z4-paired-frame-restoration-seed56/verify.py @@ -0,0 +1,608 @@ +#!/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"]: + if entry["usage"] == "provenance": + continue + 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()