Research: exact 12/13 frame281 boundary and two fewer ADDs (no new kappa)

research/r439-frame281-seed15/CLAIM.md

@@ -0,0 +1,56 @@
+# Bit supplier sprint claim, seed 15
+
+- Assignment: first operating-system cryptographic random draw, rejection sampled
+  uniformly from 0 through 99, was **15** (bit supplier).
+- Exact base: `bbc600db2fc15007b7c914f4f2b2ed55fa909c87`.
+- Claim recorded: 2026-10-13 15:34 UTC; target handoff: 16:18 UTC.
+- Object: complete six-register phase-A frame **281** (quad 15) in the R439
+  bit word; compare the selected PR589 word and the retained PR952 candidate.
+- Method: bounded exact nonnegative row-subtraction synthesis for the fixed
+  positive transfer, with repeated destination writes, followed by independent
+  matrix replay, dirty-column and paid-frame checks. This differs from PR952's
+  bounded pivot-order Boolean elimination scan and PR925's frame-267 matrix.
+- Expected deliverable: one source-pinned finite circuit improvement or scoped
+  exact class boundary, a reproducible checker, negative controls and attribution.
+- Budget: one matrix, at most 1,000,000 discovery states initially; one
+  evidence-driven pivot allowed within this same frame. Final quarter reserved
+  for independent verification, overlap refresh and handoff.
+
+Three candidates considered: (1) frame281 fixed-transfer synthesis (chosen by
+seed15 among the 60 complete six-register phase-A frames); (2) another phase-B
+fixed-factor schedule (declined because the ten blocks have recent direct
+contributions); (3) multi-helper D compensation (declined because PR965/967
+already investigate coupled helpers and restored stars). Existing PR933 closes
+the selected word's relocation/Steinberg class; this claim changes the full
+six-wire circuit instead. PR904/936/952 prefix results and PR925 are predecessor
+work, not imported savings unless explicitly replayed and compared.
+
+The issues page at claim selection showed only issues #913 and #650 and no
+pinned sprint coordination issue. No reservation issue was opened. Public
+Curiosity Bot searches checked recent bit/frame PRs and frame281 references;
+the local claim is used as requested. No selected frontier or upstream edit.
+
+Selected result at the base: PR942, conditional kappa 0.001661960547713947,
+complex-bound, retaining PR589 on PR555. This task does not promise a new kappa.
+
+Prepared for contributor @woklerx with substantial OpenAI Codex assistance.
+
+## Result update (2026-10-13)
+
+Completed the single evidence-driven pivot to PR952's distinct frame281
+integer transfer after detecting that the initial selected-word matrix is
+conjugate to PR925's prior result. The final 12-ADD circuit saves two complete
+local ADDs, including cleanup: 23,673 -> 23,671. Two different exhaustive
+implementations establish the fixed-transfer minimum12 and reverse-envelope
+minimum13. Exact source/dirty-column/exported-record checks pass; native C++
+and full make verification remain unavailable in this environment.
+
+Final overlap refresh inspected concurrent PR980 at
+`ba1cf68bef0c97dfb120add04304e2de0db6f29c`: its frame281 still has the same
+13-ADD transfer. Its general admission method is credited separately and its
+other block savings are not composed here. All workers stayed within this
+frame's discovery, independent proof, replay or review scope.
+
+Reviewable result:
+[frame281 package on the submission branch](https://github.com/woklerx/integer-mult-bounds/tree/research/seed15-bit-supplier/research/r439-frame281-seed15).
+One focused upstream PR is the handoff; no merge or selected-frontier edit.

research/r439-frame281-seed15/NOTICE.md

@@ -0,0 +1,51 @@
+# Attribution and license
+
+Prepared for GitHub contributor **woklerx (@woklerx)** with substantial
+**OpenAI Codex assistance** in task selection, research, implementation,
+proof analysis, independent implementations, verification and documentation.
+Several scoped AI workers collaborated; no independent human review is claimed.
+New work is offered under the repository's **Apache-2.0 license**.
+
+This contribution depends on and credits:
+
+- **Gareth Davidson (@bitplane), PR952**: the complete six-wire Boolean-synthesis
+  candidate is the actual input, including its earlier PR904 contributions.
+  Its exact `candidate.json.gz` is consumed without modification; its `verify.py`
+  supplies credited whole-word scalar/prefix checks, and its `common.py` is
+  imported by that verifier. Earlier savings remain his and the named
+  predecessors' work. Source PR head: `11d24706f06e95271804c9438869546724c67aab`.
+- **Ross Richardson (@RossRichardson), PR936 and PR925**: the five-wire parent
+  of PR952, the earlier exact positive-transfer frame267 result, and framing,
+  cleanup and exported-record verification routines. `search.py` adapts PR925's
+  row-subtraction recurrence with attribution. The selected PR589 frame281
+  matrix is conjugate to PR925's target, so that initial lower bound is prior
+  work. The distinct PR952 transfer and the paired reverse-envelope boundary
+  are the new scoped objects. `verify.py` imports PR925 helper checks unchanged.
+- **Jeffrey Cox, PR754**, and **mtpsl, PR691**: small-GL prefix synthesis and
+  the earlier fixed-integer-transfer/reverse-domination lineage, respectively,
+  as credited by the consumed PR904/925 packages.
+- **Gareth Davidson, concurrent PR980**, and the **PR857/906** lineage credited
+  there: complete-prefix admission despite local entrywise growth. PR980's
+  broader construction is separately credited; this contribution establishes
+  an exact fixed-transfer/guard boundary at frame281, which PR980 leaves at
+  13 ADDs. Its changes and claimed whole-word savings are not imported here.
+- **eumemic, PR543/555**, **DreamingOfClouds, PR545/589/510**, **Dylan Crow**,
+  **Zhihao Chen**, **DaysSky**, and retained supplier contributors: R439 word,
+  frame geometry, original H1-H5 audit, exporter, stage/cohort checks, hosting
+  and pricing foundations. The selected PR589 head remains
+  `a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46`.
+- **Ali Romman, PR688**, and Ross Richardson: the optional native harness is
+  adapted from their credited replay wrapper. The underlying C++ checkers and
+  all supplier files remain untouched. No new native execution is claimed.
+- **Jonathan Capalbo, PR942**, with the U8/T21/T16 owner lineage credited in the
+  selected maintainer review: current conditional-frontier context only.
+
+`independent.py` was written separately from the discovery algorithm and
+imports no discovery code. It uses first-gate column subtraction and a paired
+column search, while discovery uses last-gate row subtraction and shortest-path
+pruning. This is algorithmic independence inside an AI-assisted contribution,
+not a claim of independent authorship from every predecessor or human review.
+
+Source file SHA-256 pins and the exact base are in `SOURCES.json`. Original
+source notices and licenses remain in their existing package locations. The
+selected certificate, upstream sources and predecessor packages are unchanged.

research/r439-frame281-seed15/OVERLAP.json

@@ -0,0 +1,127 @@
+{
+  "frame": 281,
+  "gates": 13,
+  "head": "ba1cf68bef0c97dfb120add04304e2de0db6f29c",
+  "ops": [
+    [
+      3,
+      0
+    ],
+    [
+      4,
+      0
+    ],
+    [
+      3,
+      1
+    ],
+    [
+      4,
+      1
+    ],
+    [
+      2,
+      4
+    ],
+    [
+      3,
+      5
+    ],
+    [
+      1,
+      2
+    ],
+    [
+      4,
+      2
+    ],
+    [
+      5,
+      2
+    ],
+    [
+      0,
+      2
+    ],
+    [
+      1,
+      3
+    ],
+    [
+      4,
+      3
+    ],
+    [
+      0,
+      3
+    ]
+  ],
+  "own_gates": 12,
+  "path": "research/r439-global-prefix-admission/candidate.json.gz",
+  "positive_matrix": [
+    [
+      3,
+      2,
+      1,
+      1,
+      1,
+      1
+    ],
+    [
+      2,
+      3,
+      1,
+      1,
+      1,
+      1
+    ],
+    [
+      1,
+      1,
+      1,
+      0,
+      1,
+      0
+    ],
+    [
+      1,
+      1,
+      0,
+      1,
+      0,
+      1
+    ],
+    [
+      3,
+      3,
+      1,
+      1,
+      2,
+      1
+    ],
+    [
+      1,
+      1,
+      1,
+      0,
+      1,
+      1
+    ]
+  ],
+  "pr": 980,
+  "registers": [
+    263,
+    275,
+    310,
+    374,
+    410,
+    491
+  ],
+  "same_positive_matrix_as_pr952": true,
+  "scope": "Comparison only; PR980 candidate is not composed or executed here.",
+  "sha256": "fffc0484a3572c76bf3bb5284d4a40eeb723c4b3acf3da5e2d9e113ac1747ec6",
+  "slice": [
+    789,
+    802
+  ]
+}

research/r439-frame281-seed15/PROOF.md

@@ -0,0 +1,114 @@
+# Fixed-transfer factorization and the reverse guard
+
+Use the ordered existing registers `[263,275,310,374,410,491]`. A gate `(d,s)`
+means `register[d] += register[s]`; its Boolean action uses XOR, while its
+positive integer action is used for the cancellation-free precision envelope.
+The PR952 frame281 transfer is
+
+```text
+3 2 1 1 1 1
+2 3 1 1 1 1
+1 1 1 0 1 0
+1 1 0 1 0 1
+3 3 1 1 2 1
+1 1 1 0 1 1
+```
+
+The emitted 12-ADD circuit is
+
+```text
+(5,1) (4,0) (3,5) (2,4) (5,2) (3,0)
+(2,1) (1,3) (1,2) (4,1) (0,3) (0,2)
+```
+
+Its exact forward integer matrix equals the original 13-ADD circuit's matrix.
+Independent column evaluation and all 64 Boolean inputs verify the identity.
+
+## Complete finite minimum recurrence
+
+Let `E_ds = I + e_ds` for `d != s`. Starting from identity, any positive
+ADD-only program stays entrywise at least identity. Removing its last gate
+subtracts row s from row d. Retain precisely those predecessor matrices P
+still entrywise at least I. Every valid program has one such predecessor;
+conversely each retained edge reverses to a legal positive ADD. The source
+row has diagonal at least one, so every subtraction strictly lowers entry sum.
+The graph is finite, and for this matrix the maximum path length is at most
+`42 - 6 = 36`.
+
+Set `D(I)=0`; otherwise `D(M)=1+min D(P)` over retained predecessors, with
+infinity when none reaches identity. The exhaustive row-subtraction recurrence
+in `search.py` gives **D(M)=12**, with 41,235 vertices, 209,118 edges and 88
+dead ends. Its sentinel 999 exceeds every possible finite distance; a resource
+cap is reported as incomplete, never as an impossibility result.
+
+`independent.py` instead removes the **first** ADD: right multiplication by
+`E_ds^-1` subtracts column d from column s. A breadth-first traversal checks
+every layer below 12 before accepting the first identity. It visits 41,203
+states and examines 208,824 edges from completed layers. It imports no discovery
+code. Different closure counts are expected: one method finishes the entire
+last-gate graph; the other stops at the first identity layer in the first-gate
+graph.
+
+## An exact stricter-class minimum
+
+Let B be the positive matrix obtained by executing PR952's original 13 gates
+in reverse order, without negating them. The new circuit exceeds B in four
+entries: `(2,1):0->2`, `(5,1):0->2`, `(5,2):1->3`, `(5,3):0->2`.
+Thus it fails an entrywise reverse-domination guard.
+
+Discovery traverses only shortest-distance edges `D(P)=D(M)-1`, accumulating
+the positive reverse-prefix matrix of each peeled last gate. It prunes a branch
+as soon as that matrix exceeds B; all entries can only increase. Exhausting
+116 paired states and 283 surviving edges gives no guarded 12-gate witness.
+All shorter words were already excluded by D(M)=12. The original 13-gate word
+satisfies the guard with equality, proving guarded minimum **13**.
+
+The independent proof uses first-gate paired-column BFS and accumulates the
+reverse product by column addition. It explores every retained paired state
+through depth 12 and first reaches identity at 13, visiting 735 states. Positive
+prefix monotonicity justifies its separate guard pruning. This independently
+establishes the same minimum without using the discovery distances. Both
+proofs concern a final **positive matrix** bound; no claim is made about every
+possible arithmetic circuit or other norm-based guard.
+
+## Whole-word substitution and complete cost
+
+Only `A[825:838]` of the pinned PR952 candidate changes, at the same frame281.
+All six registers occur in the replacement. Phase C is regenerated as the
+literal reverse of the z-destination gates of A then B at the full frame,
+exactly as required by the retained H4. D, scatter, B, frame geometry, retained
+totals, start/final frames and other A gates are unchanged. Frame paths are
+compared for all 661 registers, and all COPY/ERASE and MOVE costs are rechecked
+in the actual emitted instructions.
+
+One forward ADD plus one mandatory cleanup ADD is saved. The complete count
+is 23,673 -> 23,671; no new helper, copy, source access, frame conversion,
+restoration call or recursive child is hidden. All 661 arbitrary-input columns
+and original H1-H5 conditions hold. The paid rank histogram remains
+`{1:1323,2:1342,3:79,4:44,5:102,6:11,7:19}`, with rank mass 5,129 and nine
+rank-seven COPYs (decoder constant 63).
+
+The local reverse guard is sufficient but unnecessarily strong here. Direct
+positive replay of the whole word gives F=41,287 before and after, and
+B=833,084 -> 832,712. The exact local expression `64*F^3*B^2` remains below
+`2^104` (92 bits). The inherited nine-stage expression `2^18*F^5*B^4` is
+AST-bound to the pinned `global_k.py`; it changes from
+
+```text
+15148224495959132732497298498295876067945200524197888
+```
+
+to
+
+```text
+15121185848152904741114841695242575582734804360101888
+```
+
+and remains 174 bits under the 192-bit allowance. This exact expression check
+does not constitute a native 5/9/11-stage replay or a hosted global invoice.
+Those execution/adoption obligations remain open. The rank moment is unchanged
+and the selected result is complex-bound, so no kappa improvement follows.
+
+These are finite algebraic arguments supported by exhaustive exact programs,
+not a Lean proof of the multiplication theorem. Assumptions and attribution
+remain as stated in README and NOTICE.