Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions docs/research/pr-ledger.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,13 @@ The earlier construction family #533–#537 and formal connections #513/#528 are

This frozen round covers #543/#545/#555 and related construction, research and tooling packages through #588. Each disposition distinguishes completed checks, publication and remaining obligations. The separate formalization PRs and later arrivals are not approved by this round.

## Proposed circuit consolidation (not yet published)

The [supplier-circuit integration batch](supplier-circuit-consolidation.md)
retains six pending research packages, composes compatible circuits and records
exact-head coverage and post-merge recommendations. It does not change this
ledger's historical dispositions or claim GitHub closures.

## Remaining priorities

1. Follow the new Linux CI for the published #442/#484/#509/#516/#520 batch; the [scoped review](community-formal-20261012-review.md) records completed local checks.
Expand Down
45 changes: 45 additions & 0 deletions docs/research/supplier-circuit-consolidation.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
# Proposed supplier-circuit integration batch

This is a reviewable integration candidate for PR681, based on
`66849e1475c930fd7732b1a0067ffee7e1e95f60`. It is not a publication receipt or a
change to the selected frontier. See the [executable package](../../research/supplier-circuit-consolidation/README.md),
[proof](../../research/supplier-circuit-consolidation/PROOF.md),
[exact-head dispositions](../../research/supplier-circuit-consolidation/DISPOSITIONS.json),
and [validation](../../research/supplier-circuit-consolidation/VALIDATION.md).

| Complete measured bill | Before | After |
|---|---:|---:|
| R420 local XOR additions | 26,916 | 18,378 (31.72% fewer) |
| R420 hosted instructions | 8,603,712 | 6,144,768 (28.58% fewer) |
| Selected CK forward scalar real primitives | 224,938 | 169,618 (24.59% fewer) |
| Selected JP8 forward scalar real primitives | 257,232 | 200,380 (22.10% fewer) |
| Raw complex factory forward primitives | 170,488 | 123,768 (27.40% fewer) |

The bit hosted prefix allocation increases from 192 to 256 bits and is fully
repriced. Its two-level allocation remains 512 bits. κ remains
`0.001635527380375392`; instruction savings are not an exponent or runtime claim.

The batch retains six complete research packages: Ali Romman's #688, mtpsl's
#691, Greer Guthrie's #694, Sagar Thakrar's #696/#708, and Scott Woolsey
Biggart's #713. yongjae321's #670 and x0hu's #674 circuits are retained through
#688's vendored certificates. Alluri's #681 factory changes are composed with
#696 on the raw complex word. Credit remains with the circuit authors.

Integration required two compatibility changes: target-row factoring is rerun
on the helper-transformed compensation matrix, and 23 of #708's 27 decoder
pairs are selected under the unchanged local precision cap. The original
packages and their complete recipes are also preserved and separately replayed.
The semantic D-prefix extension is explicit; old literal H2 checkers are not
weakened. Actual native and hosted programs are checked independently.

The central ledger's historical dispositions are unchanged. After this batch
is merged, maintainers can compare the six imported PRs' current heads with
the retained heads and resolve fully covered research contributions with a link
to this evidence. The #670/#674 subset does not establish complete-PR coverage.
No automatic merge or closure is performed. Later commits and unreviewed
higher-κ proposals remain separate work.

Prepared for Alluri with substantial OpenAI Codex assistance, Apache-2.0.
No independent human review, full theorem formalization or practical speedup
is claimed. Inherited compiler, physical, hosting, tape and analytic assumptions
remain as stated in the selected review.
24 changes: 24 additions & 0 deletions research/complex-dyadic-lowering/CLAIM.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
{
"track": "Complex supplier: scalar coefficient circuit",
"assignment_seed": 22,
"randomness": "Python secrets.randbelow(100), operating-system randomness",
"base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
"claimed_at_utc": "2026-10-13T04:10:00Z",
"expected_finish_utc": "2026-10-13T04:36:37Z",
"coordination": "No pinned issue exists; only open issue #650 requests Discussions. Scope recorded locally.",
"object": "Dyadic scalar-add primitive lowering in the selected PR626 CK and JP8 local programs, both orientations",
"method": "Replace clear plus leading-bit addition by copy; specialize unit coefficients to signed accumulation plus work clear. Exact rational symbolic replay and primitive recount, without changing scalar macros or frame events.",
"deliverable": "Executable lowering, finite verification receipt, proof of unchanged boundaries and prefix envelope, meaningful negative controls; no new kappa",
"candidates": [
{"task": "Invertible factory coordinate-total resynthesis", "disposition": "Rejected overlap with PR681 at 80d4edbc2d53f058787cb5c43bd0fc22c7e7fdff"},
{"task": "Selected butterfly pivot/frame scheduling", "disposition": "Rejected overlap with pivot-swap and entrance work in PR641/655"},
{"task": "Dyadic coefficient primitive lowering", "disposition": "Selected; changes the scalar implementation underneath fixed macro/frame words"}
],
"prior_work_checked": [651, 679, 681, 683, 687, 667],
"prior_negative_results": "research/structural-gain/factory/README.md and research/experiment-log/README.md. No closed packet, hosting, or retiming search is reopened.",
"seed_use": "Seed 22 selects CK first and the 22nd distinct nonunit coefficient for mutation controls. All coefficients and all four programs are covered, with no randomized search.",
"status": "completed",
"result": "All four 716-column primitive replays and all 686 coefficient checks pass; 10 negative controls rejected. Saved real primitives: CK forward 55320/backward 55352, JP8 forward 56852/backward 56884. Paid profiles and kappa unchanged.",
"pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/696",
"final_overlap_check": "513 open PRs through #693; no matching selected-word coefficient-lowering scope. Historical #411 credited; PR681 changes a factory scalar word. origin/main still equals the exact base."
}
145 changes: 145 additions & 0 deletions research/complex-dyadic-lowering/EXPECTED.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,145 @@
{
"controls": {
"coefficient": "-8403008",
"rejected": [
"missing_cleanup",
"missing_source_copy",
"wrong_sign",
"redundant_work",
"endpoint_neutral_prefix_growth",
"unit_dirty_work_not_cleared",
"nondyadic",
"zero_coefficient",
"source_alias",
"work_alias"
]
},
"distinct_coefficients": 686,
"programs": {
"ck/backward": {
"additions": 21451,
"all_input_columns": 716,
"baseline_real_primitives": 224986,
"charged_payload_bits": 192,
"dirty_helper_columns_restored": 492,
"new_real_primitives": 169634,
"paid_profile": {
"1": 2596,
"2": 552,
"3": 304,
"4": 160,
"5": 70,
"6": 8,
"8": 8
},
"primitive_tags": {
"add": 24236,
"clear": 42934,
"copy": 30452,
"double": 11170,
"halve": 38998,
"negate": 696,
"subtract": 21148
},
"primitive_word_sha256": "e342c630489789aa7e2aa938d8740ffc63d267d2420994be902893e7d9b50bf4",
"retained_prefix_l1_upper": "146068000389976309073/32",
"saved_real_primitives": 55352,
"scalar_macros": 21936,
"unit_additions": 6225
},
"ck/forward": {
"additions": 21443,
"all_input_columns": 716,
"baseline_real_primitives": 224938,
"charged_payload_bits": 192,
"dirty_helper_columns_restored": 492,
"new_real_primitives": 169618,
"paid_profile": {
"1": 2596,
"2": 552,
"3": 304,
"4": 160,
"5": 70,
"6": 8,
"8": 8
},
"primitive_tags": {
"add": 23838,
"clear": 42918,
"copy": 30468,
"double": 11170,
"halve": 38998,
"negate": 696,
"subtract": 21530
},
"primitive_word_sha256": "16ae874e3352c4df265026f62db95359a30399f1edc4c1b151d564d71902380c",
"retained_prefix_l1_upper": "920709848294",
"saved_real_primitives": 55320,
"scalar_macros": 21936,
"unit_additions": 6217
},
"jp8/backward": {
"additions": 22219,
"all_input_columns": 716,
"baseline_real_primitives": 257280,
"charged_payload_bits": 192,
"dirty_helper_columns_restored": 492,
"new_real_primitives": 200396,
"paid_profile": {
"1": 2512,
"2": 400,
"3": 448,
"4": 160,
"5": 70,
"6": 8,
"8": 8
},
"primitive_tags": {
"add": 29176,
"clear": 44470,
"copy": 31992,
"double": 32576,
"halve": 39438,
"negate": 692,
"subtract": 22052
},
"primitive_word_sha256": "c71f7fd2d52031e730f3ed42e56e38878e5746c053d990aad9d6e5c0d55d2bbd",
"retained_prefix_l1_upper": "16753412757380464429924108070201913461/8388608",
"saved_real_primitives": 56884,
"scalar_macros": 22693,
"unit_additions": 6223
},
"jp8/forward": {
"additions": 22211,
"all_input_columns": 716,
"baseline_real_primitives": 257232,
"charged_payload_bits": 192,
"dirty_helper_columns_restored": 492,
"new_real_primitives": 200380,
"paid_profile": {
"1": 2512,
"2": 400,
"3": 448,
"4": 160,
"5": 70,
"6": 8,
"8": 8
},
"primitive_tags": {
"add": 29050,
"clear": 44454,
"copy": 32008,
"double": 32576,
"halve": 39438,
"negate": 692,
"subtract": 22162
},
"primitive_word_sha256": "21bdebedaf5ef43d0a9149e56d15e6287c87d5031bcfaad13973fb5c24a662fe",
"retained_prefix_l1_upper": "4536094588619580433782972610869617/281474976710656",
"saved_real_primitives": 56852,
"scalar_macros": 22693,
"unit_additions": 6215
}
},
"status": "PASS_COMPLEX_DYADIC_LOWERING"
}
165 changes: 165 additions & 0 deletions research/complex-dyadic-lowering/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,165 @@
# Smaller dyadic circuits for the selected complex suppliers

This finite circuit improvement reduces the scalar primitive bill of the
selected PR626 complex programs by 22.1–24.6%. It replaces coefficient work
inside each scalar macro, preserving the exact macro, its frame and its source
and target registers. It does not claim a new κ or a measured runtime speedup.

| Provider | Orientation | Original real primitives | Replacement | Saved |
| --- | --- | ---: | ---: | ---: |
| CK | Forward | 224,938 | 169,618 | 55,320 |
| CK | Backward | 224,986 | 169,634 | 55,352 |
| JP8 | Forward | 257,232 | 200,380 | 56,852 |
| JP8 | Backward | 257,280 | 200,396 | 56,884 |

These counts include all scalar macros in each complete emitted local program,
including preconditions, compensation, centers and cleanup. They count both real
components of the complex streams. They exclude the unchanged recursive children,
frame adapters and residual wrappers, exactly as the original
`real_component_primitive_bound` field does.

## Reproduce

From a checkout containing this contribution, with Python 3.11+ and no external
dependencies:

```sh
python3 -B research/complex-dyadic-lowering/verify.py
```

Expected:

```text
PASS_COMPLEX_DYADIC_LOWERING programs=4 columns=716 savings=55320,55352,56852,56884 controls=10
```

The command is offline and writes no files. `--json` prints the deterministic
receipt after checking it against [EXPECTED.json](EXPECTED.json). It verifies
source hashes before replaying; gzip pins cover decompressed payload bytes.
It can be run from another working directory by using the script's absolute path.

## Circuit and cost

For a nonzero dyadic coefficient `q = ±a/2^k` in reduced form, a scalar macro
updates `T ← T + qS`. The existing binary Horner implementation first clears
private work `W`, then adds `S` for the leading binary digit of `a`. Both
instructions together set `W = S`, even for arbitrary initial `W`. The
replacement uses one copy instruction for that assignment and retains every
remaining binary digit, halving, signed accumulation and final work clear.

For `q = ±1`, the replacement is simply `T ← T ± S; W ← 0`. The clear is still
charged, so this circuit does not assume a clean private input. Both replacements
have the complete three-register map

```text
(T, S, W) → (T + qS, S, 0).
```

The original cost per real component is
`3 + floor(log2(a)) + popcount(a) + k`. Copy initialization saves one primitive
for every nonunit coefficient. The unit replacement costs two primitives,
instead of four. Thus a program with `A` additions, of which `U` have unit
coefficients, saves exactly `2(A + U)` real-component primitives.

The executable replacement is [lower.py](lower.py). Its primitive vocabulary is
clear, copy, doubling, halving, negation and signed addition. Scale macros retain
their original signed-power-of-two lowering. Each primitive stays at the scalar
macro's frame. No source is temporarily modified; no helper, source access,
frame change, center copy, restoration or recursive child is added or omitted.
The existing two real coefficient-work streams suffice.

## Prefix bound and substitution argument

For a nonunit coefficient, the new copy reaches precisely the old state after
the leading addition. The rest of the instruction sequence is identical. Each
new register value therefore occurs in the old prefix trace, including the
arbitrary initial private-work value.

For a unit coefficient, the target reaches its old final value directly. The
source remains unchanged. Work retains its initial value until the clear.
Each of these register values also occurs in the original trace. This proves
containment of the maximum over prefixes and registers; it does not assert
entrywise domination of simultaneous transfer matrices.

The argument holds for arbitrary real or complex inputs and correlated input
values. In particular, it preserves the inherited maximum-row norm bound.
The verifier also reconstructs the original nonnegative scalar/Horner envelope
from the full macro stream and matches the pinned independent replay's exact
`prefix_l1_upper`. Its existing 192-bit charged payload allowance is retained.
This is an exact-arithmetic circuit argument. The all-size rounding and tape
interfaces remain inherited, as they are in the selected result.

Replacing a macro by a circuit with the same source, target and cleared-work
boundary preserves every following macro's inputs. Induction over the fixed
event stream then preserves the complete scalar program. Frame events,
normalization wrappers, center lifetimes and recursive calls are unchanged.
The existing geometric and physical admission is inherited from the pinned
selected supplier; this package does not independently prove it.

## Evidence and limits

[verify.py](verify.py) expands every scalar macro into primitives and executes
those primitives with exact rational sparse rows. Each of the four programs
checks all 716 input columns, including 492 arbitrary dirty helper columns,
plus an arbitrary coefficient-work input column. It verifies the required
forward or backward shear, restored helpers, and cleared private registers.
The imaginary component uses the same real-coefficient circuit, so the exact
linear identity applies separately to it.

For all 686 distinct addition coefficients, a separate three-register check
compares every candidate register row with the complete reference Horner trace.
This includes the initial state. It checks the full boundary and exact primitive
count. The receipt records hashes of the expanded primitive words, their
operation counts, unchanged paid profiles and inherited prefix bounds.

Ten controls reject missing cleanup, missing initialization, a wrong sign,
unnecessary work, excessive intermediate growth with a restored endpoint,
uncleared private dirt for a unit coefficient, a nondyadic coefficient, zero,
and source/target or source/work aliasing. The growth control must fail the
prefix check specifically; the unnecessary-work control must fail the count.

This is deterministic complete coverage of these four frozen programs and their
686 coefficients. There is no randomized circuit search and no optimality claim.
Seed 22 selects the first provider and a coefficient for mutation controls; it
does not stand in for coverage. The general leading-bit proof above is distinct
from the finite replay and does not formalize the multiplication theorem.

The paid profiles and assembly parameters are unchanged, so the accepted
conditional κ remains `51110230636731/31250000000000000`, or
`0.001635527380375392`. This package supplies an executable local lowering and
an independently reviewable receipt. It does not replace the selected emitter,
regenerate its certificates, or change the accepted frontier.

## Provenance and sprint scope

Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
[SOURCE-PINS.json](SOURCE-PINS.json) pins every consumed source, the original
lowering and invoice code, and the selected record. The selected PR626 head is
`660de893d27bb7abd1d5b01b1640207528a5c851`; its construction descends from PR622
at `f69477f4f6d3c7eb1f740b166881bffed4ffa9f6`.

Credit goes to icekylinx for the scalar operation and coefficient-work lineage
through PR425/433/531, Jeremy Kothe for the K492 construction and schedules,
Chafik Boukhalfa for the selected PR626 packing, and the predecessors retained in
the [maintainer review](../../docs/research/community-k492-review.md), including
DreamingOfClouds' cold-helper construction and Rohan Arun's recurrence correction.
The retained bit supplier is eumemic's PR543.

Eumemic's historical [PR411](https://github.com/CrocSwap/integer-mult-bounds/pull/411)
at `f58d95f2c5da03445e704ea9c72cc55df9e68190` already used paid copy, halving,
accumulation and clear for quarter/eighth coefficients. It is related prior work,
not a code dependency. This contribution specializes the fixed selected macro
streams and covers all their coefficients, arbitrary private dirt and prefix
containment. It makes no priority claim for copy-based coefficient preparation.

Current [PR681](https://github.com/CrocSwap/integer-mult-bounds/pull/681), reviewed
for overlap at `80d4edbc2d53f058787cb5c43bd0fc22c7e7fdff`, resynthesizes an
87-operation factory window into 35 scalar operations. That changes a scalar
word. This contribution reduces the primitive cost inside unchanged macros and
does not depend on PR681. PR667 concerns exact logarithm evaluation. Raw-face
sharing, cold-end scheduling and closed packet-factory searches are not reopened.

The [local claim](CLAIM.json) records seed 22, the three candidate tasks and the
absence of a pinned sprint issue. Contribution by Sagar Thakrar / `thakrarsagar`,
with substantial OpenAI Codex assistance in research, implementation, proof
writing and review. New files are under the repository's Apache-2.0 license.
Loading