Research: complete the scalar layer with one clean carry

research/rank7-one-carry-scalars/CHECKS.json

@@ -0,0 +1,61 @@
+{
+  "status": "PASS_AUTHOR_CHECKED_LOCAL_COMPOSITION",
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS 27.0.1 arm64",
+    "ruff": "0.17.1"
+  },
+  "source_python_sha256": {
+    "bindings.py": "cca060f9b8bb33c92c19c8ea391dc5862293b008afaa445f49cfc83284532705",
+    "checks.py": "6190ac5c32e8eae3ff07dc1ad2a63e0997307fcaf12b59c9bd7ea997d28717fe",
+    "scalars.py": "9b49ce697507551c1eece96b8c327c5479fe61cbc9464827ad2b54149e4e840c",
+    "test_scalars.py": "10f6b44200f13f70bbe36b731bd53bd65bc87fdc58c6adcdfbd6daf7693b41b4",
+    "verify.py": "701dd0d3da88300074b02d37552f67b36359edcd255c675184c56cd8cad923dc"
+  },
+  "commands": [
+    {
+      "command": "TMPDIR=\"$RUN/tmp\" uv run --python 3.12 --no-project python -B scripts/research_package.py --package research/rank7-one-carry-scalars",
+      "result": "PASS_REGISTERED_RESEARCH_PACKAGE; both final stable-code commands passed"
+    },
+    {
+      "command": "uv tool run ruff check --no-cache --select E9,F,B research/rank7-one-carry-scalars",
+      "result": "All checks passed"
+    },
+    {
+      "command": "uv tool run ruff format --no-cache --check research/rank7-one-carry-scalars",
+      "result": "All files formatted"
+    },
+    {
+      "command": "Python 3.12 compile() on every new .py with -W error; AST function length check",
+      "result": "5 sources compile; every function <=60 lines"
+    },
+    {
+      "command": "python -O -W error -B research/rank7-one-carry-scalars/test_scalars.py",
+      "result": "12 behavioral groups pass"
+    },
+    {
+      "command": "Direct verify.py --work \"$RUN/export-replay\" from a plain export of this package plus exactly its 30 declared inputs, with no .git; cmp export-result.json RESULT.json",
+      "result": "PASS; byte-identical deterministic receipt"
+    },
+    {
+      "command": "Recompute all 32 SOURCE SHA256/Git blobs, declared-input set, recorded Python digests and four literal invoices",
+      "result": "PASS_32_SOURCE_PINS_INVOICE_AND_TESTED_CODE_DIGESTS"
+    }
+  ],
+  "review": {
+    "kind": "internal read-only review, not independent human review",
+    "resolved": [
+      "Forward-only templates included via all-stream alphabet union",
+      "Signed powers cannot require stronger hidden divisibility",
+      "SCALE recipe must match the canonical guarded coefficient word",
+      "Width checked before input bit allocation"
+    ],
+    "remaining_findings": []
+  },
+  "limits": [
+    "No full supplier, routing or native dirty-bank ownership proof",
+    "No independent implementation of retained native/capacity engine",
+    "No compiler/kernel formal proof",
+    "Hosted CI not claimed; inspect the PR checks"
+  ]
+}

research/rank7-one-carry-scalars/ENGINEERING.md

@@ -0,0 +1,62 @@
+# Engineering scope and checks
+
+Build the Lever shaped the deliverable: the literal generator, cold replay and
+complete invoice are rerunnable artifacts. Prove It Works required execution of
+the emitted Boolean gates, restored source/carry checks and fresh native bindings.
+Power of Ten shaped the finite width, coefficient, gate and truth-column limits.
+The autonomous-run exit predicate is one complete source-bound scalar composition
+with a strict local logical-gate reduction and one clean carry, with the changed
+exclusive-borrow premise explicit. No full supplier or kappa predicate is claimed.
+
+## Code inspection
+
+- Structured loops, exceptions and context-managed temporary directories; no
+  recursive call cycle. Native source is frozen and its engine remains inherited.
+- Width 4..256 in the primitive, 23..256 for the full-layer tariff; shifts −12..8,
+  at most nine coefficient terms, at most 32 recipe units, at most 20,000 gates.
+  Right-shift k<W is enforced; supported full-layer shifts are only −3..1.
+- Dependency inventory is bounded to 64 records, with 30 live inputs and two provenance rows, each at most 8 MB.
+  Native replay enforces its retained source bounds. Temporary replay outputs
+  are owned by the calling session and default cleanup uses TemporaryDirectory.
+- Every new function is under 60 physical lines in normal formatting. Runtime
+  `require` contracts remain active under optimized Python. Gate ports are
+  distinct and constrained to two operand banks plus one carry.
+- Exhaustive batches are capped at 65,536 truth columns; actual widths 4..7 use
+  at most 16,384 input pairs per template. Larger fixtures are 5 widths × 31
+  templates × 10 cases. Gate loops have the explicit gate bound above.
+- Hash comparisons occur before predecessor import. CLI `--work` rejects an
+  occupied path and output inside the repository. The final JSON is compared
+  with the committed receipt on every normal replay.
+- No generated code, dynamic evaluation, preprocessing, network access or extra
+  checkout is part of replay. All runtime input paths are declared in VERIFY.
+- Diagnostics: Ruff E9/F/B correctness checks, Ruff formatting, Python compilation
+  with warnings as errors, registered Python 3.12 replay and optimized controls.
+  Shared CI configuration is unchanged; this package opts into its runner.
+
+## Managed runtime and dispatch deviations
+
+Rule: 3, fixed memory capacity.
+Location: all Python generators/interpreters and the retained native replay.
+Reason: Python allocates objects during arithmetic and collection construction;
+fixed-allocation execution would require replacing the runtime and frozen engine.
+Scope: finite local verification, not a production memory-bound claim.
+Compensating control: widths, coefficients, gates, truth columns, input sizes and
+registered runtime are bounded; temporary output is context-managed.
+Verification: boundary rejection controls, small exhaustive runs and the registered
+cold replay; object-count bounds above. Python/library allocation is not instrumented.
+Follow-up: supply an allocation-accounted backend before claiming physical memory
+or all-size supplier storage from this executable model.
+
+Rule: 9, indirect calls.
+Location: verify.factory and checks.run.
+Reason: the source-bound circuit/guard pair is supplied across the checker boundary;
+Python dispatch and the frozen native engine are retained.
+Scope: one build closure (this package's circuit with the authenticated expansion)
+and one guard target (PR3094 caller.guards); no plugin or runtime target search.
+Compensating control: named fixed targets, authenticated imports and bounded alphabets.
+Verification: both interpreters, semantic mutants and all four native bindings.
+Follow-up: remove this substitution boundary if the checker and implementation
+are later combined into a production backend; no such backend is claimed here.
+
+No unavailable static typing/compiler guarantee or complete inherited-engine
+Power-of-Ten compliance is claimed. New code does not edit or widen that engine.

research/rank7-one-carry-scalars/OVERLAP.json

@@ -0,0 +1,51 @@
+{
+  "checked_at_utc": "2026-10-17T10:31:08.592475+00:00",
+  "upstream_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+  "priority_revision": 6,
+  "coverage": {
+    "open_prs": {
+      "fetched_at": "2026-10-17T10:30:31.030520+00:00",
+      "complete_pagination": true,
+      "records": 273
+    },
+    "discussions": {
+      "fetched_at": "2026-10-17T10:30:57.983474+00:00",
+      "complete_pagination": true,
+      "records": 1910
+    }
+  },
+  "search_terms": [
+    "one carry",
+    "one-carry",
+    "Cuccaro",
+    "complete scalar"
+  ],
+  "limitations": [
+    "No arbitrary code-diff search; closed work searched only through retained notes/ledger, with sparse paths omitted.",
+    "Exact related PR heads were inspected separately; no-match is not novelty proof."
+  ],
+  "related": [
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3081",
+      "head": "d764f9c11c86c40d35fd67811e60284feb1b8f10",
+      "distinction": "Already proves wired one-carry local dyadic ADD; this composition credits and generalizes its interface to the complete actual scalar stream."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3088",
+      "head": "19fefab093b802a58d0c432debfa72fa4b381b2d",
+      "distinction": "Already shares sign fill over four physical half-ADDs. No repetition of that result; this package addresses complete scalar clean-carry stock, including SCALE."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3094",
+      "head": "b7a761ce2d6198509adb4b09ebf22b5b17ea2f55",
+      "distinction": "Complete source-bound scalar guard/baseline replay reused exactly; replaces gate-level read-only source with exclusive mutable borrowing."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3150",
+      "head": "e5c265f1be9cd0593f49628ec6552e52bd90af61",
+      "distinction": "Separate A13 frame/climb Boolean implementation with W-1 carry bank, not this full scalar composition. No dependency or incorporation."
+    }
+  ],
+  "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-18996179",
+  "result_status": "author-checked with internal read-only review; not independent human validation"
+}

research/rank7-one-carry-scalars/PROOF.md

@@ -0,0 +1,128 @@
+# One-clean-carry scalar composition
+
+## Boundary and claim
+
+Fix a width `23 <= W <= 256`. Two disjoint W-bit two's-complement banks
+hold target T and auxiliary/source S; one additional bit initially holds zero.
+Both banks are exclusively writable for the duration of a scalar macro.
+The circuit returns S exactly and returns the carry bit to zero. It uses
+no coefficient scratch word. For ADD, S is the actual source. For SCALE,
+S can be arbitrary dirty data, but a disjoint writable bank must be supplied.
+No native owner assignment for that SCALE bank is established here.
+
+For a reduced dyadic ADD coefficient q, require that S be divisible by its
+denominator. For exact signed interpretation, require T, S and the completed
+endpoint to fit W signed bits. For SCALE, retain every inherited target-walk
+prefix alignment and range guard. `replay.bind` re-establishes those guards
+for the two literal PR3076 providers and both orientations at the PR3094
+seven-fractional-bit, `P+20` capacity. Intermediate ADD and negation states
+below are modular; they need no additional signed guard bits.
+
+The result is a conditional physical scalar implementation. Exclusive mutable
+access strengthens the borrowing premise relative to PR3094's gate-level
+read-only source implementation. Unknown access, routing, clean-stock and
+consumer costs are not zero.
+
+## MAJ/UMA primitive and shifts
+
+The adder is the credited Cuccaro–Draper–Kutin–Moulton MAJ/UMA construction,
+already used for local dyadic ADDs in PR3081. See the original
+[2004 paper](https://arxiv.org/abs/quant-ph/0410184). No new adder is claimed.
+At position i, write a=S_i, b=T_i, c=the incoming carry wire. The MAJ gates
+are `c ^= a; b ^= a; a ^= b & c`. They place
+`majority(a_old,b_old,c_old)` in a. The outgoing carry is therefore available
+as the next position's c. At the top bit, `b ^= a; b ^= c` supplies the
+modular sum without retaining overflow. Descending positions apply
+`a ^= b & c; c ^= a; b ^= c`, restoring a and c while leaving the sum in b.
+This proves source and clean-carry return by descending induction.
+
+For n active bits, n>=2, the literal count is `2n−2` Toffolis and `4n−2`
+CNOTs; n=1 uses one CNOT. There are n−1 MAJ and n−1 UMA blocks plus two top
+CNOTs. Each block has one Toffoli and two CNOTs. The implementation retains
+the standard literal gates rather than claiming a gate minimum.
+
+For exponent e>=0, add source bits `[0,W−e)` to target bits `[e,W)`.
+Those wires represent `2^e S mod 2^W`; omitted low target bits stay fixed.
+If e>=W the increment is zero. If W−e=1 use the one-CNOT case.
+For a right shift k=−e, require k<W and the low k source bits zero.
+Copy the sign into those k bits with k CNOTs; connect the distinct source
+wires in order `S[k:W] + S[0:k]`; run the adder; undo the k copies.
+These wires encode the arithmetic quotient S/2^k. The adder restores every
+source wire before unfill, including the original sign. This costs
+`2W−2` Toffolis and `4W−2+2k` CNOTs and uses one clean carry.
+
+For q=sum sign_j*2^e_j, concatenate the shifted adders, reversing a term's
+entire gate list when its sign is negative. Every term restores S and carry,
+so terms compose. The inherited signed-power expansion has at most nine terms,
+and every exponent is at least the negative reduced-denominator exponent.
+Thus denominator divisibility supplies all required low zeros. The sum has
+exact coefficient q; intermediate target wrap is harmless modulo 2^W.
+
+## SCALE and arbitrary dirty auxiliary data
+
+HALF and DOUBLE retain the inherited reversible rotation and sign-fill
+circuits, each costing `3W−2` CNOTs. Their inherited alignment and redundant
+sign-bit guards remain necessary.
+
+For negation, use the same one-carry modular adder three times and then
+swap the two banks with W three-CNOT swaps:
+
+```text
+(T,S) -> (T+S,S) -> (T+S,-T) -> (S,-T) -> (-T,S)  modulo 2^W
+```
+
+Every adder returns its own carry. S needs no clean bits or numerical bound
+beyond being a W-bit word, and is restored after the swap. The exact cost is
+`6W−6` Toffolis and `15W−6` CNOTs. This costs more gates than PR3094's
+carry-bank negation but permits the whole scalar layer to reuse a single
+clean bit. Signed SCALE interpretation follows from the unchanged endpoint
+and prefix guards, not from interpreting the temporary shears as signed values.
+
+## Complete source-bound invoice
+
+Cold replay authenticates the complete 30-file predecessor dependency set,
+rebuilds both native programs, replays the complete native/capacity checks,
+and rebinds all 9,992 scalar macros per orientation. The actual histogram
+has 9,438 ADD and 554 SCALE macros. For both real components, the signed-power
+ADD counts by exponent are:
+
+| Exponent | −3 | −2 | −1 | 0 | 1 |
+|---|---:|---:|---:|---:|---:|
+| Calls | 210 | 5,432 | 7,040 | 5,862 | 478 |
+
+SCALE additionally uses 924 negations, 222 HALF and 300 DOUBLE operations.
+These counts are identical for the two providers and both orientations.
+The dispatch hashes bind the chronology; no macro, frame, child or cleanup
+operation is removed from the source stream.
+
+Summing the literal formulas gives, per provider/orientation and both real
+components, for every supported W:
+
+| Implementation | CNOTs | Toffolis |
+|---|---:|---:|
+| PR3094 direct caller | `82274W−104534` | `77936W−119740` |
+| One-carry caller | `91514W−9476` | `43588W−44544` |
+| Old minus new | `−9240W−95058` | `34348W−75196` |
+
+The combined unweighted logical-gate saving is `25108W−170254`, strictly
+positive throughout 23<=W<=256 (at W=23 it is 407,230).
+At W=84, CNOTs increase by 871,218, Toffolis fall by 2,810,036, and the
+combined saving is 1,938,818. Clean carry stock falls from 83 bits to one;
+the two operand banks total 168 bits in both template layouts. The changed
+SCALE borrowing obligation must still be implemented on actual native owners.
+A weighted tariff or physical time need not track this unweighted sum.
+
+## Evidence and limits
+
+`RESULT.json` records fresh native dispatch bindings, circuit hashes and all
+four invoices. The verifier exhausts all aligned signed sources and every
+modular target for ADDs at W=4..7. For SCALE it exhausts every arbitrary
+auxiliary bank and each target satisfying the inherited guards. Complete
+output states and reversed gate lists are checked on 314,560 truth columns
+across 124 circuits. A separate Boolean-list evaluator checks 1,550 larger-width
+fixtures through W=256. The written argument supplies the width-uniform proof.
+Meaningful malformed/sign/cleanup controls run separately under optimized Python.
+The reused native engine is executed, not independently reimplemented.
+
+No recursive paid profile, moment, kappa, selected frontier, full native caller,
+multitape routing bound or unconditional multiplication theorem is changed.