Research: fuse aligned FANIN4 coefficient stream

research/fanin4-aligned-source-stream-seed9983a614/PROOF.md

@@ -0,0 +1,80 @@
+# FANIN4 stream identity and cost
+
+## Model
+
+Let L be a positive integer. There are four read-only source tapes containing
+x0,...,x3 in F2^L and one writable target tape z in F2^L. The five tapes are
+aligned in one fixed coefficient order and begin at head position zero.
+One lane transition reads a source bit and advances that tape by one cell.
+The target lane transition reads z[i], writes its updated bit, and advances
+the target by one cell. A complete call returns every participating head to
+zero. Reads, writes, head steps, bit XORs, call records, and reference fields
+are charged separately. There is no scratch or frame conversion.
+
+For this package, L=4 and the coefficient space is F2[C2^2]. All source maps
+are the identity, so the connector request is exactly z <- z + sum_j xj.
+The + symbol is coefficientwise addition in characteristic two.
+
+## Correctness
+
+The singleton schedule applies z[i] <- z[i] + xj[i] for j=0,1,2,3 in four
+complete passes. Since the xj are read-only, their values do not change.
+The final target lane is z[i] + x0[i] + x1[i] + x2[i] + x3[i].
+
+The fused schedule scans lane i once across all five tapes. It reads z[i] and
+each xj[i], then applies four binary XOR gates to z[i] before advancing. Thus
+the same final lane value is obtained. Every source is unchanged. Repeating
+the fused map adds the same unchanged sum to z a second time and restores the
+original target. All five heads return by L reverse head steps.
+
+This proves the map for arbitrary dirty sources and target and every L. The
+exhaustive L=4 verifier checks 2^(5L)=1,048,576 joint states. The verifier
+also checks the inverse, all head positions, the source values, the exact
+resource ledgers, and failure controls.
+
+## Resource accounting
+
+For s sources, L coefficients, and one ordinary source-update record per
+singleton call:
+
+| Resource | Singleton sequence | Fused scan |
+|---|---:|---:|
+| Reads | 2sL | (s+1)L |
+| Writes | sL | L |
+| XORs | sL | sL |
+| Forward head steps | 2sL | (s+1)L |
+| Return head steps | 2sL | (s+1)L |
+| Call records | s | 1 |
+| Source-reference fields | s | s |
+| Target-reference fields | s | 1 |
+| Scratch | 0 | 0 |
+| Frame transitions | 0 | 0 |
+
+For s=4, L=4 these evaluate to reads 32/20, writes 16/4, XORs 16/16,
+head moves 64/40, records 4/1, source-reference fields 4/4, target-reference
+fields 4/1.
+
+Let r,w,h,p,d1,ds,t be nonnegative prices for one data read, one data write,
+one head step, one XOR, one singleton record, one fused FANIN-s record, and
+one target-reference field. The singleton-minus-fused cost is
+
+    (s-1)L*r + (s-1)L*w + 2(s-1)L*h + s*d1 - ds + (s-1)t.
+
+The XOR and source-reference terms cancel. If records have uniform price
+d1=ds=d, this simplifies to
+
+    (s-1)(L*r + L*w + 2L*h + d + t).
+
+Any one-time opcode-table or source-frame conversion expense F is subtracted
+from the saving. In the fixed aligned-frame stream instance F=0; an external
+supplier must price its own instruction encoding and frame conversion before
+claiming a net gain.
+
+## Scope boundary
+
+The construction realizes one identity-map FANIN4 update in a fixed aligned
+coefficient frame. It does not establish that a current recursive supplier
+emits these four source roles in the same frame, that the operation can be
+used in a full mask-cover word at lower total cost, or that any global
+multiplication exponent improves. The abstract query/addition limits from PR
+#2249 remain intact because all four source XORs are charged.

research/fanin4-aligned-source-stream-seed9983a614/README.md

@@ -0,0 +1,125 @@
+# FANIN4 in an aligned coefficient stream
+
+**A local reversible-stream construction. No new kappa or supplier admission is claimed.**
+
+## Result
+
+For four read-only source vectors and one arbitrary dirty target in the common
+coefficient frame of F2[C2^2], the update
+
+    z <- z XOR x0 XOR x1 XOR x2 XOR x3
+
+can be performed in one synchronized scan. Each coefficient still pays all
+four XORs. Compared with four complete singleton updates, the fused scan
+reduces reads, writes, target-head returns, and call-record overhead. It uses
+no scratch and leaves each source and the target head at its entry position.
+
+The claim is deliberately local. The sources use identity maps and are already
+aligned in the same coefficient order. This does not construct the full
+63-mask connector, map FANIN4 into the selected supplier, or change kappa. It
+does show a concrete physical stream realization for a higher-arity connector
+step while retaining the full per-source addition charge from Cycle 43.
+
+## Exact bill
+
+For s sources and L aligned coefficients, each singleton pass reads its source
+and the current target, writes the target, and returns both heads. The fused
+pass reads all s sources and the target once, writes the target once, and
+returns all s+1 heads.
+
+| Resource | s singleton updates | One FANIN-s | At s=4, L=4 |
+|---|---:|---:|---:|
+| Data reads | 2sL | (s+1)L | 32 vs 20 |
+| Data writes | sL | L | 16 vs 4 |
+| Bit XORs | sL | sL | 16 vs 16 |
+| Forward plus return head moves | 4sL | 2(s+1)L | 64 vs 40 |
+| Call records | s | 1 | 4 vs 1 |
+| Source-reference fields | s | s | 4 vs 4 |
+| Target-reference fields | s | 1 | 4 vs 1 |
+| Scratch cells / cleanup | 0 | 0 | 0 vs 0 |
+| Frame transitions | 0 | 0 | 0 vs 0 |
+
+If read, write, head-step, uniform per-record, and target-reference prices are
+r, w, h, d, and t, respectively, the fused bill saves exactly
+
+    (s-1) * (L*r + L*w + 2*L*h + d + t).
+
+The source-reference fields and sL arithmetic XORs are fully charged and
+unchanged. A variable-width encoding can use separate record prices d1 for a
+singleton and ds for FANIN-s; its exact saving is
+
+    (s-1)*L*(r+w+2*h) + s*d1 - ds + (s-1)*t.
+
+Thus a differently sized fused record is charged explicitly. Any frame
+conversion cost F is subtracted from this saving; it is zero only in the
+fixed aligned-frame instance studied here.
+
+## Exact interface and proof
+
+The object is the coefficient vector space of F2[C2^2], with L=4. Every
+source xj and target z is an arbitrary 4-bit vector. Source maps are identity.
+All five tapes begin at lane 0 in the same basis order.
+
+At each lane i, the fused schedule reads the four source bits and z[i], applies
+four binary XOR gates to z[i], writes the updated target bit, and advances all
+five heads by one lane. At the end it returns all heads by four lanes.
+Therefore each lane of the target becomes
+
+    z[i] XOR x0[i] XOR x1[i] XOR x2[i] XOR x3[i].
+
+Sources are never written. The target is arbitrary and dirty. The map is its
+own inverse because each source bit is unchanged and adding the same sum twice
+over F2 restores z. The symbolic argument holds for every L; the exact verifier
+exhausts every dirty state at L=4.
+
+Four singleton calls apply the same four XORs in four scans. Their source and
+target heads return after each call. The resource counts in the table follow
+directly from these two schedules; the verifier checks both ledgers and the
+complete state map.
+
+## Reproduce
+
+From the repository root:
+
+    python3 -B research/fanin4-aligned-source-stream-seed9983a614/verify.py
+    python3 scripts/research_package.py --package research/fanin4-aligned-source-stream-seed9983a614 --check-only
+
+Expected verifier line:
+
+    PASS_FANIN4_STREAM states=1048576 L=4 xor=16/16 reads=32/20 writes=16/4 head_moves=64/40 records=4/1 unit_saving=54 controls=6
+
+The registered command is the package verifier. Only the standard library is
+used.
+
+## Predecessors and limits
+
+- PR #2128 adds the two-source DUO connector word and notes that a real
+  supplier-level physical realization was still missing.
+- Cycle 43 PR #2249 proves an exact query/addition floor for the six-source
+  arity-4..6 abstract connector. This construction keeps the full tap price;
+  it concerns the lower-level stream bill.
+- PRs #2171 and #2207 implement ordered single-source controlled streams and
+  fallback descriptors. This package studies one aligned common-target fan-in,
+  not their selected rank-42 normalizer.
+
+No full batch path is supplied. The 63-mask recursive interface, invocation
+placement, source-frame alignment in a live provider, head-motion pricing in
+that provider, and any effect on the selected exponent remain open.
+
+## Open next questions
+
+Can two or more source operators from an emitted multiplication-supplier frame
+be put in this aligned common-target layout without spending the saved traffic
+on source-frame conversion? It matters because this package assumes identity
+source maps in one fixed frame. A feasible first step is to name one live
+supplier's source/target roles and derive its exact entry and return permutation
+bill for one FANIN4 call. The blocker is that no such supplier mapping is
+established here.
+
+## Credit
+
+The source-call connector model and DUO comparison are due to the authors of
+PR #2128; the abstract six-source high-arity floor is recorded in PR #2249.
+This package supplies the local fused scan and its complete stream bill.
+Prepared by Cinna Davis with substantial OpenAI Codex assistance. New work is
+Apache-2.0.

research/fanin4-aligned-source-stream-seed9983a614/RESULT.json

@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "status": "PASS_FANIN4_STREAM",
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "seed": "9983a6144fbaa6291d717b9b2076e816",
+  "frame": "F2[C2^2]",
+  "source_count": 4,
+  "width": 4,
+  "dirty_states_checked": 1048576,
+  "costs": {
+    "singleton_sequence": {
+      "reads": 32,
+      "writes": 16,
+      "xors": 16,
+      "head_moves": 64,
+      "call_records": 4,
+      "source_refs": 4,
+      "target_refs": 4,
+      "scratch_cells": 0,
+      "frame_transitions": 0
+    },
+    "fanin4": {
+      "reads": 20,
+      "writes": 4,
+      "xors": 16,
+      "head_moves": 40,
+      "call_records": 1,
+      "source_refs": 4,
+      "target_refs": 1,
+      "scratch_cells": 0,
+      "frame_transitions": 0
+    }
+  },
+  "weighted_saving": "(s-1)*(L*r+L*w+2*L*h+d+t)",
+  "selected_kappa_claimed": false,
+  "supplier_admission_claimed": false,
+  "uniform_unit_price_saving": 54,
+  "variable_record_saving": "(s-1)*L*(r+w+2*h)+s*d1-ds+(s-1)*t-F",
+  "F_scope": "0 within the fixed aligned-frame instance; external source conversion and opcode-table costs must be added"
+}

research/fanin4-aligned-source-stream-seed9983a614/SOURCES.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "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"
+    },
+    {
+      "path": "docs/research/community-batch1099-integration.json",
+      "usage": "provenance",
+      "git_blob": "9d60e86c0e494d17bec5e28eda41b275c9ede64e",
+      "sha256": "684c50d1ac69863e1fcc0a34bf76c54bac576f6bbde79b3c67d8432a495c8c1c"
+    }
+  ],
+  "external_references": [
+    {
+      "label": "PR #2128",
+      "head": "697369a971eed02c0fbcd75ebefec9f59945f08e",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2128",
+      "usage": "related abstract DUO construction; no code imported"
+    },
+    {
+      "label": "Cycle 43 PR #2249",
+      "head": "0c6ed7958433b2cbc0beaa331ff882aa08221a0d",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2249",
+      "usage": "prior exact high-arity connector floor; no code imported"
+    },
+    {
+      "label": "PR #2171",
+      "head": "416aac58960660edced905dc7d914c126d357290",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2171",
+      "usage": "adjacent selected controlled stream work"
+    },
+    {
+      "label": "PR #2207",
+      "head": "149d55d90d3c0877ed3d78e1deca8eb2f72e0d00",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2207",
+      "usage": "adjacent selected fallback stream work"
+    }
+  ]
+}