From 3ff7f7922d879a810aecb24d6dca66546014198d Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Tue, 13 Oct 2026 20:46:58 -0500 Subject: [PATCH] Add phase-typed distinct-source echo research --- research/z4-distinct-source-seed55/NOTICE.md | 10 + research/z4-distinct-source-seed55/README.md | 117 ++++ .../z4-distinct-source-seed55/RESULT.json | 163 +++++ .../z4-distinct-source-seed55/SOURCES.json | 65 ++ research/z4-distinct-source-seed55/TASK.json | 82 +++ .../z4-distinct-source-seed55/VERIFY.json | 22 + .../inputs/PR1391/CERTIFICATE.json | 240 +++++++ .../inputs/PR1391/verify.py | 606 ++++++++++++++++++ .../inputs/PR1410-README.md | 67 ++ research/z4-distinct-source-seed55/verify.py | 542 ++++++++++++++++ 10 files changed, 1914 insertions(+) create mode 100644 research/z4-distinct-source-seed55/NOTICE.md create mode 100644 research/z4-distinct-source-seed55/README.md create mode 100644 research/z4-distinct-source-seed55/RESULT.json create mode 100644 research/z4-distinct-source-seed55/SOURCES.json create mode 100644 research/z4-distinct-source-seed55/TASK.json create mode 100644 research/z4-distinct-source-seed55/VERIFY.json create mode 100644 research/z4-distinct-source-seed55/inputs/PR1391/CERTIFICATE.json create mode 100644 research/z4-distinct-source-seed55/inputs/PR1391/verify.py create mode 100644 research/z4-distinct-source-seed55/inputs/PR1410-README.md create mode 100644 research/z4-distinct-source-seed55/verify.py diff --git a/research/z4-distinct-source-seed55/NOTICE.md b/research/z4-distinct-source-seed55/NOTICE.md new file mode 100644 index 0000000000..deaa47268c --- /dev/null +++ b/research/z4-distinct-source-seed55/NOTICE.md @@ -0,0 +1,10 @@ +# Source notices + +This package is distributed under the repository's Apache-2.0 license. + +The following unmodified predecessor snapshots are included for exact replay and attribution: + +- `inputs/PR1391/CERTIFICATE.json` and `inputs/PR1391/verify.py`, from `CrocSwap/integer-mult-bounds` commit `6ce8017e4c27c8b220b6c3a27a53bb18f138212a`, PR #1391. SHA256 values are recorded in `SOURCES.json` and checked by `verify.py`. +- `inputs/PR1410-README.md`, from commit `5b1c00b9f2770aabaa0085539405757f7818a14a`, PR #1410. Its SHA256 and Git blob are checked by `verify.py`. + +PR #1391 and PR #1410 credit the order-three frame and paid output-sign-frame predecessors, PR #1287 by Ross Richardson and PR #1227 by Sagar Thakrar. This package retains those attributions and does not modify their snapshots. diff --git a/research/z4-distinct-source-seed55/README.md b/research/z4-distinct-source-seed55/README.md new file mode 100644 index 0000000000..485ca1205a --- /dev/null +++ b/research/z4-distinct-source-seed55/README.md @@ -0,0 +1,117 @@ +# Phase-indexed order-four echo across distinct sources + +**Scoped recursive-interface construction; no new κ or supplier admission.** This package extends the order-four five-child interface of PR #1391 and the same-source, two-root composition of PR #1410. It composes two five-child calls on independent source banks while preserving an arbitrary dirty output and restoring both sources and workspace. + +Research base: `4040a0f46d67b41c36a472a7cd4af791fd4c36cc`. Exact PR #1391 and PR #1410 dependency heads and content pins are recorded in [SOURCES.json](SOURCES.json). + +The main construction indexes each child's output reader by the carried workspace phase. If the original child reads through `R_i` and advances workspace by `P`, define + +```text +C_(i,t)(D,W) = (D + Q^(-t) R_i W, P W), t in Z/4Z. +``` + +When `W = P^t w`, the child contributes the original `R_i w`, since `Q^(-t) R_i P^t = R_i`. The typed reader is an eight-row signed selector: it changes which output register each ADD targets while retaining the child's eight ADDs and its 24-coordinate `P` update. This is an explicit change to the child contract. + +## Exact boundary recurrence + +The pinned predecessor has 24 workspace coordinates. The complete `P^r` gate vectors are + +| `r` | ADD | NEG | Total | +|---:|---:|---:|---:| +| 0 | 0 | 0 | 0 | +| 1 | 54 | 6 | 60 | +| 2 | 36 | 12 | 48 | +| 3 | 54 | 6 | 60 | + +Let `A(r)` be that vector. With starting workspace phase `t`, the entry charge is `A(t)`. After a child at phase `t`, the workspace has advanced once under `P`; reaching the next phase `s` costs `A((s-t-1) mod 4)`. The exact recurrence is + +```text +F_0(t) = A(t) +F_(j+1)(s) = min_t [F_j(t) + A((s-t-1) mod 4)] +g(k) = F_k(0) +``` + +The verifier compares this recurrence with every path for the two fixed sizes: all 1,024 five-child paths and all 1,048,576 ten-child paths. The exact minima are: + +- `g(5) = (54,6)`, total 60, on phases `[0,0,1,2,3,0]`. +- `g(10) = (36,12)`, total 48, on phases `[0,1,0,1,2,3,0,1,2,3,0]`. + +Let `T_i=(62,6)` be the complete forward cost of child `i`, including its eight data ADDs and 24-coordinate workspace update. The paired child body and literal inverse contribute `2 sum_i T_i`. For one source, the source copy and reset cost `2d` ADDs; for two sources, the entry copy, two-sided handoff, and exit reset cost `4d` ADDs, where `d=24`. The complete cost recurrences are + +```text +E_1(k) = 2 sum_(i=1..k) T_i + (2d,0) + 2 g(k) +E_2(k1,k2) = 2 sum_(i=1..k1+k2) T_i + (4d,0) + 2 g(k1+k2) +``` + +The inverse uses the same exact phase word in reverse and has the same ADD/NEG vector. These equations include every child, source update, phase change, and restoration charged by this finite interface. + +For the two-source call, the ten-child path is at phase 3 after the first five children. At that point the workspace contains `P^3(W+X)`. The handoff applies `P^3(Y-X)`, using two ADDs per each of 24 coordinates, for 48 ADDs. The second five children then read `Y`. The complete word is + +```text +W += X +phase-typed 10-child forward body, with W += P^3(Y-X) after child 5 +W -= Y +literal inverse of the no-handoff 10-child body +``` + +The resulting map is + +```text +(D,X,Y,W) -> (D + sum_(i=0..4) R_i X + sum_(i=5..9) R_i Y, X, Y, W). +``` + +All 80 basis columns (8 output, 24 coordinates in each of `X`, `Y`, and `W`) are checked exactly. The two source banks are read-only, and arbitrary initial values in all four banks are allowed. + +## Complete invoice + +The joint typed invoice is + +```text +20*(62,6) + (96,0) + 2*(36,12) = (1408,144) +``` + +for 1,552 primitives and 2,960 data reads. Two separate calls using the same typed child family cost + +```text +2 * [10*(62,6) + (48,0) + 2*(54,6)] = (1552,144) +``` + +for 1,696 primitives and 3,248 reads. The joint typed call saves **144 primitives and 288 reads**. Its exact prefix row-L1 peak is 21, compared with 16 for the two separate typed calls; this is a coefficient-width cost that could affect fixed-precision admission. + +For comparison, the unchanged-reader interface from PR #1410 also composes across two distinct sources when charged with the same 48-ADD handoff. Its exact joint invoice is 1,952 primitives versus 2,016 for two separate original calls, saving 64 primitives and 136 reads. Its prefix row-L1 peaks are 42 joint and 30 separate. This is a matched same-contract construction; it is not included in the typed-call saving above. + +## Reproduction and evidence + +From the repository root, with CPython 3.12: + +```sh +python3.12 scripts/research_package.py --package research/z4-distinct-source-seed55 +``` + +Expected verifier marker: + +```text +PASS_Z4_DISTINCT_SOURCE_PHASE_TYPED_ECHO g5=60 g10=48 separate=1696 joint=1552 saved=144 reads_saved=288 paths=1024+1048576 basis=80 controls=5 +``` + +The registered replay checks the base and predecessor pins, all twelve `(phase, reader)` identities, unchanged child ADD/NEG counts, both complete 80-column maps, every phase path at both sizes, exact ADD/NEG/read invoices, prefix row-L1 peaks, and five negative controls. The exact evidence is frozen in [RESULT.json](RESULT.json). + +## Scope and limits + +The phase recurrence is exact for the stated phase-indexed order-four child alphabet. It is not a lower bound for arbitrary ADD/NEG programs. Output-row reindexing is encoded by the static target of each ADD and costs no additional scalar ADD/NEG instruction in this word model. Address calculation, physical row routing, source hosting, tape travel, fixed-precision admission, recursive assembly into a selected supplier, and analytic transfer remain unproved. The row-L1 increase makes precision a live obligation. The selected result at the pinned base remains κ = `836330098538459/500000000000000000`; this package does not change it or claim a new κ. + +## Overlap check + +The live refresh found several adjacent connector results. PR #1158 gives an exact readout-price census for a four-source/four-output Hadamard connector. PR #1438 and Cinna Davis's Discussion #1412 study a second arbitrary-dirty root and paid full-row transfers for universal five-source masks. PR #1439 studies a persistent `z = z_initial + Bx` boundary across a paid source mutation `x += Cu`, correcting it by `z += BCu`; PR #1442 proves a weighted query optimum under chronological output-delivery cuts. Here the interface keeps one 24-coordinate dirty workspace and changes between two read-only source banks by the explicit 48-ADD delta `P^t(Y-X)` inside a fixed five-child echo. Its separate evidence is the order-four phase-indexed reader identity, exhaustive five- and ten-child recurrence, and complete arbitrary-dirty two-call map/invoice, not a four-source Hadamard census, two-root transfer bound, general mutable-source connector theorem, or delivery-cut optimum. We make no priority claim for those connector mechanisms and retain their distinct scopes. + +## Open next questions + +Does a named selected supplier realize all four phase-indexed signed target rows with the charged handoff and no binding routing or precision cost? This matters before the operation saving can alter a multiplication profile. First inspect one retained #1094 child matrix and test `Q^(-t) R_i P^t = R_i` for every phase, then price target routing and the prefix envelope. The blocker is that no physical host, tape schedule, or precision-admitted supplier for this paired interface has been identified. + +## Credit and license + +This work builds on Cinna Davis's PR #1391 order-four child family and PR #1410 same-source persistent boundary, and retains their attribution. Those results extend Ross Richardson's PR #1287 and Sagar Thakrar's PR #1227. The selected-result context is Rohan Arun's PR #1094 on Jeremy Kothe's #1087 construction. The exact PR #1391 certificate and verifier snapshots are preserved under `inputs/PR1391/`; the direct PR #1410 README snapshot is pinned under `inputs/`. See [NOTICE.md](NOTICE.md) for source heads and snapshot hashes. + +The overlap review also credits Cinna Davis's PR #1158 for an adjacent four-source Hadamard connector census, woklerx's PRs #1438, #1439, and #1442, and Cinna Davis's concurrent Discussion #1412 for distinct two-root, mutable-source, and chronological-delivery models. + +Prepared by **Cinna Davis** with substantial **OpenAI Codex assistance** in derivation, implementation, exact verification, source pinning, and prose. No independent human review or proof-assistant formalization is claimed. New material is Apache-2.0; the project license is retained. diff --git a/research/z4-distinct-source-seed55/RESULT.json b/research/z4-distinct-source-seed55/RESULT.json new file mode 100644 index 0000000000..c217415b61 --- /dev/null +++ b/research/z4-distinct-source-seed55/RESULT.json @@ -0,0 +1,163 @@ +{ + "assignment_seed": 55, + "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 finite state 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": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc", + "complete_paid_cost_recurrence": { + "child_forward_ADD_NEG": { + "ADD": 62, + "NEG": 6 + }, + "d": 24, + "literal_inverse": "counted by the factor 2 on every child and phase boundary; inverse leaves preserve ADD/NEG counts", + "single_source": "2*sum_i(T_i) + (2d,0) + 2*g(k)", + "two_source_split": "2*sum_i(T_i) + (4d,0) + 2*g(k1+k2)", + "wrapper_accounting": "single: W+=X and W-=X; two-source: W+=X, two ADDs per coordinate for P^t(Y-X), and W-=Y" + }, + "controls": { + "fixed_reader_midpoint_carry": "PASS", + "missing_final_source_restore": "REJECTED", + "missing_literal_inverse": "REJECTED", + "omitted_source_handoff": "REJECTED", + "typed_child_phase_identity_checks": "PASS for 12 (phase,reader) pairs", + "wrong_handoff_phase": "REJECTED", + "wrong_reader_type": "REJECTED" + }, + "dimensions": { + "D": 8, + "W": 24, + "X": 24, + "Y": 24, + "total_basis_columns": 80 + }, + "handoff": { + "ADDs": 48, + "formula": "W += P^t (Y-X) at the 5|5 boundary, t=phase[5]", + "selected_phase": 3 + }, + "joint_distinct_sources": { + "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.", + "predecessors": { + "PR1391_certificate_sha256": "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3", + "PR1391_head": "6ce8017e4c27c8b220b6c3a27a53bb18f138212a", + "PR1391_verifier_sha256": "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05", + "PR1410_head": "5b1c00b9f2770aabaa0085539405757f7818a14a", + "PR1410_readme_sha256": "6dda7d5b83b41c71d73711401edbc146271a546a518ef6b038b0bdbb6578d405" + }, + "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 + ], + "g10_total": 48, + "g5_ADD_NEG": { + "ADD": 54, + "NEG": 6 + }, + "g5_exhaustive_paths": 1024, + "g5_path": [ + 0, + 0, + 1, + 2, + 3, + 0 + ], + "g5_total": 60, + "terminal_phase": 0, + "workspace_phase_costs_ADD_NEG": [ + { + "ADD": 0, + "NEG": 0 + }, + { + "ADD": 54, + "NEG": 6 + }, + { + "ADD": 36, + "NEG": 12 + }, + { + "ADD": 54, + "NEG": 6 + } + ] + }, + "same_reader_control": { + "joint_ADD_NEG": { + "ADD": 1768, + "NEG": 184 + }, + "joint_prefix_row_l1_peak": 42, + "joint_primitives": 1952, + "joint_reads": 3720, + "map": "PASS on all 80 basis columns", + "phase_path": [ + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 0, + 1, + 0 + ], + "saving_primitives": 64, + "separate_ADD_NEG": { + "ADD": 1840, + "NEG": 176 + }, + "separate_prefix_row_l1_peak": 30, + "separate_primitives": 2016, + "separate_reads": 3856 + }, + "saving": { + "primitives": 144, + "reads": 288 + }, + "scope": "Exact phase-indexed typed child family for two distinct source banks and the pinned PR1391 five-child reader sequence; not an admitted selected supplier.", + "separate_calls": { + "ADD_NEG": { + "ADD": 1552, + "NEG": 144 + }, + "map": "PASS on all 80 basis columns", + "prefix_row_l1_peak": 16, + "primitives": 1696, + "reads": 3248 + }, + "status": "PASS_Z4_DISTINCT_SOURCE_PHASE_TYPED_ECHO" +} diff --git a/research/z4-distinct-source-seed55/SOURCES.json b/research/z4-distinct-source-seed55/SOURCES.json new file mode 100644 index 0000000000..47c3b74183 --- /dev/null +++ b/research/z4-distinct-source-seed55/SOURCES.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "base_commit": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "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": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + } + ], + "external_sources": [ + { + "repository": "CrocSwap/integer-mult-bounds", + "commit": "6ce8017e4c27c8b220b6c3a27a53bb18f138212a", + "path": "research/z4-paired-frame-restoration-seed56/CERTIFICATE.json", + "local_path": "research/z4-distinct-source-seed55/inputs/PR1391/CERTIFICATE.json", + "git_blob": "0132b117d90f1a7a97c40af3e38503c117604e00", + "sha256": "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3", + "role": "exact predecessor child and recurrence certificate" + }, + { + "repository": "CrocSwap/integer-mult-bounds", + "commit": "6ce8017e4c27c8b220b6c3a27a53bb18f138212a", + "path": "research/z4-paired-frame-restoration-seed56/verify.py", + "local_path": "research/z4-distinct-source-seed55/inputs/PR1391/verify.py", + "git_blob": "9d866bbf57a6d1f012a21687bde2e231c90efd14", + "sha256": "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05", + "role": "pinned signed-ADD child word and basis replay" + }, + { + "repository": "CrocSwap/integer-mult-bounds", + "commit": "5b1c00b9f2770aabaa0085539405757f7818a14a", + "path": "research/z4-persistent-pair-seed57/README.md", + "local_path": "research/z4-distinct-source-seed55/inputs/PR1410-README.md", + "git_blob": "001929a89cd64f4bbb0d4194c6bde96f45b7ded2", + "sha256": "6dda7d5b83b41c71d73711401edbc146271a546a518ef6b038b0bdbb6578d405", + "role": "direct same-source predecessor and matched baseline context" + } + ] +} diff --git a/research/z4-distinct-source-seed55/TASK.json b/research/z4-distinct-source-seed55/TASK.json new file mode 100644 index 0000000000..5f9f4473fc --- /dev/null +++ b/research/z4-distinct-source-seed55/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "persistent-boundary", + "priority_revision": 2, + "base_commit": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc", + "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", + "actual_scope": "For the pinned PR1391 order-four child family, compare a same-reader 5|5 source handoff with a phase-indexed child type C_(i,t) whose reader is Q^(-t)R_i. Optimize the fixed 5-child and 10-child workspace phase recurrences, fully charge copy/restore and the X-to-Y handoff, and verify arbitrary dirty D, X, Y, W.", + "scope_change_reason": "The catalogue card asks for a specified consecutive-call restoration saving. The current task changes its interface hypothesis: the source changes across the midpoint, and the main construction indexes each child reader by the carried phase so output remains canonical. This tests a concrete typed boundary absent from the same-source PR1410 result; the unchanged-reader schedule is also replayed as a matched comparison.", + "bottleneck_link": "The phase-indexed type replaces repeated output-frame restoration gates with statically selected signed ADD targets. The complete recurrence shows the scalar operation saving and its source-handoff price; supplier routing, precision and tape admission decide whether it can transfer to a multiplication bound.", + "budget_minutes": 60, + "stop_rule": "Only the pinned five-child and 5|5 ten-child cases are searched. Exhaust all 4^5 and 4^10 phase assignments with the terminal phase fixed; stop after the exact two-source map, invoice and listed mutations. Do not generalize the finite recurrence beyond the declared order-four typed alphabet or begin supplier optimization in this package.", + "outcome": "completed", + "evidence": "The exact 80x80 map passes for both the typed joint call and two typed separate calls. The typed recurrence has g(5)=(54,6), g(10)=(36,12); complete vectors are (1552,144) for separate calls and (1408,144) for the joint call, saving 144 primitives and 288 reads. The unchanged-reader source handoff also passes, at 1952 versus 2016 primitives, saving 64. Exhaustive phase-path checks and five negative controls pass.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, prototype construction, exact verifier implementation, source pinning and prose. No independent human review or proof-assistant formalization is claimed.", + "open_questions": [ + { + "question": "Does any named selected supplier realize the phase-indexed signed target rows Q^(-t)R_i with the same address, tape and precision costs?", + "why_it_matters": "The finite scalar saving transfers only if the actual supplier can implement every phase type and the 5|5 handoff while satisfying its physical and fixed-precision contracts.", + "first_step": "Extract one exact child matrix from the retained #1094 supplier inventory and test all four identities Q^(-t)R_i P^t=R_i, then price its target routing and prefix coefficient envelope.", + "blocked_by": "No physical host, tape schedule or precision-admitted supplier for this paired order-four interface has been identified." + } + ], + "track": "recursive interfaces", + "assignment_seed": 55, + "candidate_tasks": [ + { + "id": "distinct_source_order4_midpoint", + "decision": "selected", + "question": "Can PR1410\u2019s order-four boundary cross a 5|5 split when the source changes from X to independent Y, after charging the handoff and both wrappers?", + "method": "exact 4-state recurrence, first with the unchanged reader and then with phase-indexed Q^(-t)R_i child types" + }, + { + "id": "gauge44_slots_t16_order4_intertwiner", + "decision": "deferred", + "question": "Does the retained #1094 gauge44-slots-t16 child matrix admit the paired order-four identity Q^(-t)R_iP^t=R_i for all four phases?", + "reason": "PR1410 names supplier compatibility as its direct next question; defer this most obvious follow-up to keep the selected task independently distinct." + }, + { + "id": "two_dirty_root_paid_transfer", + "decision": "deferred", + "question": "For universal five-source masks, can a second dirty connector plus paid complete transfer z1 += z0 establish a sharp transfer bound?", + "reason": "Fresh PR #1438 at a61170c97c9ea2c396f6d76a953b0cf74a455cdd and Discussion #1412 already investigate the two-row connector alphabet; this task has a different object and paid source-port contract." + } + ] +} diff --git a/research/z4-distinct-source-seed55/VERIFY.json b/research/z4-distinct-source-seed55/VERIFY.json new file mode 100644 index 0000000000..3f38ec8594 --- /dev/null +++ b/research/z4-distinct-source-seed55/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/z4-distinct-source-seed55/inputs/PR1391/CERTIFICATE.json", + "research/z4-distinct-source-seed55/inputs/PR1391/verify.py", + "research/z4-distinct-source-seed55/inputs/PR1410-README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Checks exact predecessor pins, all phase-indexed child identities, 4-state recurrence against exhaustive path coverage, 80-column dirty-state maps, full ADD/NEG/read invoices, row-L1 peaks and five negative controls." + } + ] +} diff --git a/research/z4-distinct-source-seed55/inputs/PR1391/CERTIFICATE.json b/research/z4-distinct-source-seed55/inputs/PR1391/CERTIFICATE.json new file mode 100644 index 0000000000..0132b117d9 --- /dev/null +++ b/research/z4-distinct-source-seed55/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-distinct-source-seed55/inputs/PR1391/verify.py b/research/z4-distinct-source-seed55/inputs/PR1391/verify.py new file mode 100644 index 0000000000..9d866bbf57 --- /dev/null +++ b/research/z4-distinct-source-seed55/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-distinct-source-seed55/inputs/PR1410-README.md b/research/z4-distinct-source-seed55/inputs/PR1410-README.md new file mode 100644 index 0000000000..001929a89c --- /dev/null +++ b/research/z4-distinct-source-seed55/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-distinct-source-seed55/verify.py b/research/z4-distinct-source-seed55/verify.py new file mode 100644 index 0000000000..34f3045401 --- /dev/null +++ b/research/z4-distinct-source-seed55/verify.py @@ -0,0 +1,542 @@ +#!/usr/bin/env python3 +"""Exact phase-indexed two-source echo construction and bounded recurrence.""" +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 = "4040a0f46d67b41c36a472a7cd4af791fd4c36cc" +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 +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(BLOCKS5)): + 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_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 == 4: + 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_two_source(legacy): + out = identity(TOTAL) + for j in range(D): + for block in BLOCKS5: + out[j][X + 8 * block + j] += 1 + out[j][Y + 8 * block + j] += 1 + return out + + +def make_naive_fixed_reader(legacy, states): + """Control: try the midpoint handoff with the original common output frame.""" + blocks = BLOCKS10 + work_global = [W + j for j in range(BANK)] + local_map = list(range(D)) + work_global + body = legacy.lift_word(legacy.octet_word(states[0]), list(range(D))) + body += legacy.lift_word(legacy.workspace_word(states[0]), work_global) + for i, block in enumerate(blocks): + body += legacy.lift_word(legacy.child_word(block), local_map) + gap = (states[i + 1] - states[i] - 1) % 4 + out_phase = (states[i + 1] - states[i]) % 4 + body += legacy.lift_word(legacy.workspace_word(gap), work_global) + body += legacy.lift_word(legacy.octet_word(out_phase), list(range(D))) + if i == 4: + t = states[i + 1] + p = block_diag([matrix_power(legacy.expected_octet_frame(), t)] * 3) + for j, row in enumerate(p): + k, sign = next((k, v) for k, v in enumerate(row) if v) + body.append(legacy.add(W + j, Y + k, sign)) + body.append(legacy.add(W + j, X + k, -sign)) + base = legacy.lift_word( + legacy.batch_word(states, blocks=blocks), + [*range(D), *[W + j for j in range(BANK)]], + ) + return (source_wrapper(legacy, X, 1) + body + source_wrapper(legacy, Y, -1) + + legacy.inverse_word(base)) + + +def run(): + legacy, cert = load_predecessor() + check_typed_children(legacy) + path5, g5 = best_phase_path(legacy, 5) + path10, g10 = best_phase_path(legacy, 10) + brute5, paths5 = exhaustive_phase_minimum(legacy, 5) + brute10, paths10 = exhaustive_phase_minimum(legacy, 10) + require((path5, g5, paths5, brute5[0]) == + ((0, 0, 1, 2, 3, 0), {"ADD": 54, "NEG": 6}, 1024, 60), + "five-child phase recurrence and exhaustive minimum") + require((brute5[1], brute5[2]) == (path5, g5), + "five-child recurrence path matches exhaustive witness") + require((path10, g10, paths10, brute10[0]) == + ((0, 1, 0, 1, 2, 3, 0, 1, 2, 3, 0), + {"ADD": 36, "NEG": 12}, 1048576, 48), + "ten-child phase recurrence and exhaustive minimum") + require((brute10[1], brute10[2]) == (path10, g10), + "ten-child recurrence path matches exhaustive witness") + + expected = expected_two_source(legacy) + root_x = make_root(legacy, path5, BLOCKS5, X) + root_y = make_root(legacy, path5, BLOCKS5, Y) + separate = root_x + root_y + plain_body = lift_batch(legacy, path10, BLOCKS10) + switched_body = lift_batch(legacy, path10, BLOCKS10, source_switch=True) + joint = (source_wrapper(legacy, X, 1) + switched_body + source_wrapper(legacy, Y, -1) + + legacy.inverse_word(plain_body)) + separate_map = apply_word(separate, TOTAL) + joint_map = apply_word(joint, TOTAL) + require(separate_map == expected, "two separate arbitrary-dirty source calls") + require(joint_map == expected, "joint distinct-source arbitrary-dirty map") + + leaf = cert["recursive_interface_cost"]["leaf_forward"] + joint_vector = word_counts(joint) + separate_vector = word_counts(separate) + require(joint_vector == {"ADD": 1408, "NEG": 144}, "joint complete ADD/NEG invoice") + require(separate_vector == {"ADD": 1552, "NEG": 144}, "separate complete ADD/NEG invoice") + k = len(BLOCKS10) + expected_joint_vector = { + "ADD": 2 * k * leaf["ADD"] + 4 * BANK + 2 * g10["ADD"], + "NEG": 2 * k * leaf["NEG"] + 2 * g10["NEG"], + } + expected_separate_vector = { + "ADD": 2 * (2 * len(BLOCKS5) * leaf["ADD"] + 2 * BANK + 2 * g5["ADD"]), + "NEG": 2 * (2 * len(BLOCKS5) * leaf["NEG"] + 2 * g5["NEG"]), + } + require(joint_vector == expected_joint_vector, "joint recurrence matches emitted word") + require(separate_vector == expected_separate_vector, "separate recurrence matches emitted words") + joint_total = sum(joint_vector.values()) + separate_total = sum(separate_vector.values()) + joint_reads = 2 * joint_vector["ADD"] + joint_vector["NEG"] + separate_reads = 2 * separate_vector["ADD"] + separate_vector["NEG"] + require((joint_total, separate_total, joint_reads, separate_reads) == + (1552, 1696, 2960, 3248), "complete operation/read comparison") + + # Same-reader two-source composition is the matched original-interface control. + # Reuse the published PR1410 same-source optimum as the naive common-output + # phase control; it has a different recurrence from the phase-typed variant. + naive_path = (0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 0) + fixed_reader_joint = make_naive_fixed_reader(legacy, naive_path) + fixed_reader_joint_map = apply_word(fixed_reader_joint, TOTAL) + require(fixed_reader_joint_map == expected, "fixed-reader two-source carry map") + fixed_path5 = (0, 1, 2, 3, 0, 0) + fixed_root_x = legacy.lift_word( + legacy.echo_word(fixed_path5), + [*range(D), *[X + j for j in range(BANK)], *[W + j for j in range(BANK)]], + ) + fixed_root_y = legacy.lift_word( + legacy.echo_word(fixed_path5), + [*range(D), *[Y + j for j in range(BANK)], *[W + j for j in range(BANK)]], + ) + fixed_reader_separate = fixed_root_x + fixed_root_y + require(apply_word(fixed_reader_separate, TOTAL) == expected, + "fixed-reader two-call baseline map") + fixed_joint_vector = word_counts(fixed_reader_joint) + fixed_separate_vector = word_counts(fixed_reader_separate) + require(fixed_joint_vector == {"ADD": 1768, "NEG": 184}, + "fixed-reader joint invoice") + require(fixed_separate_vector == {"ADD": 1840, "NEG": 176}, + "fixed-reader separate invoice") + require(sum(fixed_separate_vector.values()) - sum(fixed_joint_vector.values()) == 64, + "fixed-reader source-pair saving") + + no_handoff = (source_wrapper(legacy, X, 1) + plain_body + source_wrapper(legacy, Y, -1) + + legacy.inverse_word(plain_body)) + require(apply_word(no_handoff, TOTAL) != expected, "omitted source handoff control escaped") + wrong_handoff = lift_batch(legacy, path10, BLOCKS10, source_switch=True, + switch_phase_delta=1) + wrong_handoff_word = (source_wrapper(legacy, X, 1) + wrong_handoff + + source_wrapper(legacy, Y, -1) + legacy.inverse_word(plain_body)) + require(apply_word(wrong_handoff_word, TOTAL) != expected, + "wrong handoff phase control escaped") + wrong_reader = make_root(legacy, path5, BLOCKS5, X, phase_reader_mutation=2) + require(apply_word(wrong_reader + root_y, TOTAL) != expected, + "wrong reader-type control escaped") + missing_restore = (source_wrapper(legacy, X, 1) + switched_body + + legacy.inverse_word(plain_body)) + require(apply_word(missing_restore, TOTAL) != expected, + "missing final Y restoration control escaped") + missing_inverse = (source_wrapper(legacy, X, 1) + switched_body + + source_wrapper(legacy, Y, -1)) + require(apply_word(missing_inverse, TOTAL) != expected, + "missing literal inverse control escaped") + # The selected phase type costs the same number of primitives as the old child; + # this check records the gate-count premise used by the typed recurrence. + require(all(word_counts(typed_child(legacy, q, b)) == word_counts(legacy.child_word(b)) + for q in range(4) for b in set(BLOCKS5)), "phase-type child gate census") + + return { + "status": "PASS_Z4_DISTINCT_SOURCE_PHASE_TYPED_ECHO", + "base_commit": BASE, + "assignment_seed": 55, + "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], + }, + "scope": "Exact phase-indexed typed child family for two distinct source banks and the pinned PR1391 five-child reader sequence; not an admitted selected supplier.", + "dimensions": {"D": D, "X": BANK, "Y": BANK, "W": BANK, "total_basis_columns": TOTAL}, + "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.", + "handoff": { + "formula": "W += P^t (Y-X) at the 5|5 boundary, t=phase[5]", + "ADDs": 2 * BANK, + "selected_phase": path10[5], + }, + "recurrence": { + "workspace_phase_costs_ADD_NEG": phase_costs(legacy), + "F0(t)": "A(t)", + "Fnext(s)": "min_t F(t)+A((s-t-1) mod 4)", + "terminal_phase": 0, + "g5_path": list(path5), + "g5_ADD_NEG": g5, + "g5_total": sum(g5.values()), + "g5_exhaustive_paths": paths5, + "g10_path": list(path10), + "g10_ADD_NEG": g10, + "g10_total": sum(g10.values()), + "g10_exhaustive_paths": paths10, + }, + "complete_paid_cost_recurrence": { + "child_forward_ADD_NEG": leaf, + "single_source": "2*sum_i(T_i) + (2d,0) + 2*g(k)", + "two_source_split": "2*sum_i(T_i) + (4d,0) + 2*g(k1+k2)", + "d": BANK, + "wrapper_accounting": "single: W+=X and W-=X; two-source: W+=X, two ADDs per coordinate for P^t(Y-X), and W-=Y", + "literal_inverse": "counted by the factor 2 on every child and phase boundary; inverse leaves preserve ADD/NEG counts", + }, + "separate_calls": { + "ADD_NEG": separate_vector, + "primitives": separate_total, + "reads": separate_reads, + "prefix_row_l1_peak": row_l1_peak(separate, TOTAL), + "map": "PASS on all 80 basis columns", + }, + "joint_distinct_sources": { + "ADD_NEG": joint_vector, + "primitives": joint_total, + "reads": joint_reads, + "prefix_row_l1_peak": row_l1_peak(joint, TOTAL), + "map": "PASS on all 80 basis columns", + }, + "same_reader_control": { + "phase_path": list(naive_path), + "separate_ADD_NEG": fixed_separate_vector, + "separate_primitives": sum(fixed_separate_vector.values()), + "joint_ADD_NEG": fixed_joint_vector, + "joint_primitives": sum(fixed_joint_vector.values()), + "joint_reads": 2 * fixed_joint_vector["ADD"] + fixed_joint_vector["NEG"], + "separate_reads": 2 * fixed_separate_vector["ADD"] + fixed_separate_vector["NEG"], + "joint_prefix_row_l1_peak": row_l1_peak(fixed_reader_joint, TOTAL), + "separate_prefix_row_l1_peak": row_l1_peak(fixed_reader_separate, TOTAL), + "map": "PASS on all 80 basis columns", + "saving_primitives": sum(fixed_separate_vector.values()) - sum(fixed_joint_vector.values()), + }, + "saving": {"primitives": separate_total - joint_total, + "reads": separate_reads - joint_reads}, + "controls": { + "fixed_reader_midpoint_carry": "PASS", + "omitted_source_handoff": "REJECTED", + "wrong_handoff_phase": "REJECTED", + "wrong_reader_type": "REJECTED", + "missing_final_source_restore": "REJECTED", + "typed_child_phase_identity_checks": "PASS for 12 (phase,reader) pairs", + "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 finite state 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) + 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() == canonical, + "RESULT.json differs from the recomputed exact evidence") + print(result["status"] + + f" g5={result['recurrence']['g5_total']} g10={result['recurrence']['g10_total']}" + f" separate={result['separate_calls']['primitives']}" + f" joint={result['joint_distinct_sources']['primitives']}" + f" saved={result['saving']['primitives']} reads_saved={result['saving']['reads']}" + f" paths=1024+1048576 basis=80 controls=5") + + +if __name__ == "__main__": + main()