Pack Newton membership into nine guarded subtractions (no κ)

research/packed-newton-membership/PERFORMANCE.md

@@ -0,0 +1,73 @@
+# Local timing evidence
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+The complete public membership call takes 45.35% less median time on one
+accepted rank-nine fixture. This includes type and size validation, packing,
+the full transform, unpacking and every divisibility check. It includes the
+new 8192-bit component-limit check. It does not time only packed subtraction.
+
+The fixture is the positive encoding used by PR5374's existing benchmark at
+coefficient width 1025 bits. Encoded input components reach 1034 bits. The
+exact input SHA256 is
+`151857dd471120344f0f7c0e8c5ab6542b8f7d815e5cbb56348eacd77f3c770b`.
+The same arrays and positive endpoint are used on both sides. No result is
+cached. Input encoding is outside the API timer on both sides.
+
+Five fresh processes per side ran 1000 calls each, alternating order between
+trials. All 10,000 complete calls accepted, with zero errors. Separate
+processes ran the complete inherited scientific replay five times per side;
+all ten returned the same complete result hash and zero errors.
+
+| Timed work | Reference median, range in seconds | Packed median, range in seconds |
+| --- | --- | --- |
+| 1000 complete rank-nine API calls | 0.290105, 0.271077 to 0.366769 | 0.158548, 0.147782 to 0.162996 |
+| Complete source scientific replay call | 0.907932, 0.901498 to 1.010443 | 0.859743, 0.850917 to 0.915044 |
+| Whole fresh process for that replay | 0.948728, 0.938971 to 1.104224 | 0.899336, 0.890138 to 0.956943 |
+
+The API ranges do not overlap. Complete-replay timing is inconclusive:
+its observed median falls by 5.31%, but the ranges overlap and the gap is
+smaller than the observed variation. No end-to-end replay speedup is claimed.
+Whole-process timing includes process startup, plan initialization, source
+authentication, imports, output comparison and printing. None of these
+measurements predicts a collector, tape implementation or supplier speedup.
+The change is opt-in; the shared default command is unchanged.
+
+Environment: CPython 3.12.15, macOS 27.0.1, arm64, standard library only.
+The shared host has 18 logical CPUs; the pre-measurement load averages were
+2.99, 2.77 and 2.08. Other work was not stopped. Alternation and the reported
+ranges expose the observed scheduling variation. Both implementations use
+their ordinary interpreter configuration with no tuning knobs changed.
+
+## Limiter and end-to-end share
+
+An untimed cProfile run of the new API spent 0.2905 of
+0.3898 profiled seconds cumulatively in validation and
+packing, while the packed transform itself spent 0.0109 seconds.
+Packing and validation now dominate. The old API's nested validation
+generators and scalar transform account for most of its profile. The
+improvement includes fusing validated input reduction into packing as well
+as batching the arithmetic.
+
+A separate untimed full-replay profile spent 0.5868 of 3.1432
+profiled seconds cumulatively in the bounded membership predicate, about
+18.7%. The unchanged Gaussian source validation alone spent
+1.8896 seconds cumulatively. Profile durations are diagnostic and are
+excluded from the timing table. The unchanged work limits the end-to-end gain.
+The complete replay preserves its independent decoder,
+subset checks, rejection tests and all 96 literal collector prefixes.
+
+## Repeat
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/packed-newton-membership/benchmark.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/packed-newton-membership/benchmark.py --sample reference --profile
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/packed-newton-membership/benchmark.py --sample packed --profile
+```
+
+The benchmark prints every unrounded sample, per-sample error and work counts,
+fixture/result hashes, environment, and hashes of its four controlling files.
+It writes no files. Timing is not a registered correctness acceptance gate.
+The ordinary registered replay reruns the exact preservation checks.

research/packed-newton-membership/PROOF.md

@@ -0,0 +1,109 @@
+# Guarded packed differences preserve Newton membership
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algorithm-preservation proof. Ali Romman's PR5374 supplies
+bounded residues and Clear1nsight's PR3382 supplies the Gaussian Newton lattice.
+Those mathematical predicates are premises, not new results here.
+
+## Contract
+
+Let `N=2^r`, `0<=r<=9`, and let `values` be a list of N Gaussian-integer
+pairs with absolute component bit lengths at most 8192. Set `b=ceil(r/2)`
+and `M=2^b`. The reference computes the Boolean difference coefficients,
+modulo M in each component, and returns the first mask failing its existing
+power-of-1+i divisibility test. The new implementation returns exactly the
+same tuple `(mask, real_residue, imaginary_residue, b)`, or None. It preserves
+the input. This includes negative components, r=0 and every value in the
+stated domain. It rejects malformed inputs and inputs outside that domain.
+It does not claim the reference's unbounded-rank API outside this domain.
+
+## Lane arithmetic
+
+Store real and imaginary residues as separate base-256 digits, in that
+order at each mask. Each digit is in `[0,M-1]`, and `M<=32`. At a stage
+for address bit k, select the upper masks, whose k-th bit is one. Let U
+be the packed word restricted to their low b bits. Let L be the low b
+bits of the corresponding lower masks, shifted by `16*2^k` bits into
+the upper positions. Let G have digit 128 in each selected component lane
+and digit zero elsewhere. Then one integer subtraction
+
+    D = (U | G) - L
+
+has the intended independent digit values `128+u-l` at selected lanes and
+zero elsewhere. Every selected digit is between 97 and 159, so no digit
+borrows from another or carries into another. Unselected digits subtract
+zero from zero. This is an equality in base 256, proved by independent
+nonnegative digit differences. Masking D to the low b bits in selected lanes
+therefore yields `(u-l) mod M`. The discarded guard has zero residue modulo
+M. The lower lanes are copied unchanged from the previous word.
+
+`lower = upper >> shift` in the public plan selects precisely the lower
+partner lanes. The implementation masks the word before shifting, which
+keeps even intermediate positive integers within 16N bits. The shift never
+moves a real digit into an imaginary digit or a different Boolean pair.
+
+This guard is necessary for the simple packed-subtraction scheme.
+Without it, two destination bytes 0 minus two source bytes 1 give low-five-bit
+residues `0x1e1f`, rather than the desired `0x1f1f`. With guards the masked
+result is `((0x8080-0x0101)&0x1f1f)=0x1f1f`.
+
+## Stage induction and certificate
+
+The invariant after each processed address bit is equality, in every real
+and imaginary component, with the reference partial Boolean difference
+transform modulo M. Packing establishes it before the first stage. The lane
+lemma proves one simultaneous stage, so induction proves every final
+coefficient. It holds for all inputs in the domain, rather than only for the
+finite fixtures.
+
+The unpacking uses the same increasing mask order and the same existing
+divisibility predicate as PR5374. Equal complete coefficient arrays therefore
+produce the same first failing mask, both identical residues and the same b.
+For r=0 there are no stages, residues are zero modulo 1 and every valid
+Gaussian input is accepted. All work uses newly allocated local objects;
+none writes into the input list or its tuples.
+
+## Exact work and bounds
+
+The reference uses rN modular component subtractions. The packed transform
+uses r packed integer subtractions, plus its masks, shifts, packing,
+unpacking, validation and existing divisibility tests. At rank nine these
+counts are 4608 and 9. These are different operation alphabets; their ratio
+is not a bit-complexity or runtime speedup. The packed word has at most
+16N bits, hence 8192 bits at rank nine, including unused and guard bits.
+The private residue byte array has 2N bytes, hence 1024 bytes at rank nine.
+The plan is immutable and depends only on rank and mask positions. No
+coefficient, verdict, receipt or scientific result is cached.
+
+Packing and unpacking each scan N pairs; each transform stage operates on
+O(N) machine bits. Input type checks and the 8192-bit limit run on every
+call. Precomputed public plans for ranks zero through nine are built once
+at module import. This cost is outside steady API timing and inside the
+fresh-process end-to-end timing. Python object overhead, integer allocation
+and physical tape costs are additional. No fixed-allocation or paid physical
+scan bound follows from the bit counts.
+
+## Verification and limits
+
+The executable checker exhausts guarded subtraction on all residue digit
+pairs for b=1 through 5, checks every small binary Gaussian array through
+rank two and all rank-three real arrays over residues 0 through 3, compares
+complete first-failure tuples and preserves inputs. A separate subset-sum
+definition checks complete transformed arrays, including signed rank-nine
+fixtures. Boundary and source-drift controls reject.
+
+An opt-in adapter runs the complete original PR5374 scientific replay with
+only its member/obstruction globals replaced by this implementation. Its
+independent source decoder, subset oracle, literal collector, source hashes,
+rejection controls and recorded output comparison remain executed. The old
+receipt's `rank9_modular_subtractions=4608` describes the original reference
+algorithm, not instrumentation of the substituted transform. New operation
+counts are reported separately. This is a preservation check for the new
+implementation, not a scientific re-review of the predecessor result.
+
+No lattice theorem, sharp residue modulus, decoder, producer admission,
+physical caller, native frame operation, owned erasure, precision/tape,
+compiler or multiplication theorem is proved here. Selected kappa and all
+five framework assumptions retain their status. No proof assistant or
+independent human review is claimed.

research/packed-newton-membership/README.md

@@ -0,0 +1,124 @@
+# Packed Gaussian Newton membership
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algorithm-preservation proof with finite corroboration
+and local performance evidence. At rank nine, a guarded packed transform
+uses nine integer subtractions in place of 4608 component subtractions.
+These are different arithmetic operations; the count ratio is not a speedup.
+
+For lists of Gaussian integer pairs on ranks zero through nine, with absolute
+component bit lengths at most 8192, [packed.py](packed.py) returns exactly
+PR5374's membership decision and first failing coefficient tuple. It preserves
+the input, including arbitrary signed components. [PROOF.md](PROOF.md) proves
+borrow isolation and stage induction for every input in this domain.
+
+This builds on Ali Romman's [PR5374](https://github.com/CrocSwap/integer-mult-bounds/pull/5374)
+bounded-residue algorithm and Clear1nsight's
+[PR3382](https://github.com/CrocSwap/integer-mult-bounds/pull/3382) Gaussian
+Newton lattice. Their lattice, sharp modulus and collector results remain
+credited premises. No predecessor file or credit line changes.
+
+## Evidence
+
+The new checker passes 1364 guarded digit-pair cases, 65,812 small arrays,
+160 signed and component-boundary fixtures, complete transformed-array
+comparisons with independent subset sums, malformed-input/source controls,
+and a fault injected into the production transform with its guards removed.
+All checks use explicit exceptions and remain active under optimized Python.
+
+The opt-in adapter also executes the complete inherited scientific replay
+with only the membership functions replaced. Its output is identical,
+including all 96 literal collector prefixes. Source decoding, independent
+oracles and failure controls remain executed. This is preservation evidence
+for the new algorithm, not an audit deliverable for PR5374.
+
+[PERFORMANCE.md](PERFORMANCE.md) records five alternating fresh-process
+trials per side. It reports the complete public API separately from the
+complete scientific replay and whole-process costs. All timed work runs,
+input/results match, and no errors occur. The benchmark prints raw samples
+and controlling-file hashes; no timing threshold controls acceptance.
+
+## Reproduce
+
+From the repository root, using standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/packed-newton-membership
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/packed-newton-membership/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/packed-newton-membership/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/packed-newton-membership --check-source-history
+```
+
+The verifier prints `PASS_PACKED_NEWTON_MEMBERSHIP`, all exact counts and
+hashes of its package files. It writes nothing. The generic launcher runs
+both normal and optimized checks. For a different checkout, substitute its
+CPython 3.12 interpreter path. Timing commands are in PERFORMANCE.md.
+
+[SOURCES.json](SOURCES.json) pins canonical base
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a` and every imported predecessor
+input. [TASK.json](TASK.json) records the change from the broad replay-runtime
+card to this exact public validation algorithm. The
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19380573)
+states the original bounded target. No source or result cache is added.
+
+## Limits and credit
+
+The API has a declared finite rank and bit-width domain. It does not replace
+the unbounded reference API outside that domain and emits no decoded wide
+coefficients. No default caller is patched. Runtime numbers describe one
+host and one fixture. A faster logical predicate does not price input
+movement, physical validation, allocation, erasure or restoration.
+
+There is no new kappa, selected-frontier change, supplier admission, native
+implementation, uniform compiler or complete multiplication theorem. All
+five selected framework assumptions remain. No selected cold replay, Lean
+or Docker run is claimed. Independent human and formal proof-kernel review
+are unclaimed.
+
+Credit Ali Romman for PR5374's algorithm and replay; Chris R / Clear1nsight
+for the PR3382 lattice and collector; ywz65, Arham Tahir, Tekalign / PR3025,
+Ross Richardson and the retained word, wrapper and period-domain lineage.
+Guarded packed arithmetic and Boolean difference transforms are standard
+techniques. The new work is their concrete implementation, proof and
+source-bound integration for this validator. No literature-priority claim
+for the general techniques is made.
+
+## Open next questions
+
+1. Can a physical membership-only consumer benefit after input acquisition,
+   movement and restoration are fully charged? First name and price one
+   actual consumer. No physical scan or supplier contract is supplied here.
+2. Can the unchanged input-validation and independent-decoder work in a
+   complete replay be reduced without losing diagnostics? First profile one
+   source-bound replacement. This contribution stops at the membership step.
+
+## Implementation bounds
+
+The new call graph has no recursion. Public input is capped at 512 pairs and
+8192 bits per component. Plan construction has ten ranks, at most nine stages
+and 1024 bytes per mask. A call has at most nine transform stages, 512 packing
+iterations and 512 certificate tests. The independent subset oracle has at
+most 512 squared iterations per fixture. The finite checker does not retain
+its census; source replay has its existing finite bounds. New functions are
+at most 60 lines. Exceptions enforce meaningful contracts under `-O`.
+
+Power of Ten rule 3 deviation: CPython allocates integers, byte arrays and
+library objects while running. Fixed-capacity allocation is unavailable in
+this runtime. The finite input limits bound live data; packed integers use at
+most 8192 positive bits, and each source read is capped at 32 MiB and closed
+with a context manager. The full source replay retains its predecessor's
+managed-memory contract. A fixed-allocation port would be a separate task
+if this predicate becomes a physical backend component.
+
+Rules 8 and 9 deviation: the preservation adapter imports a fixed finite set
+of authenticated Python modules, and the benchmark selects between two fixed
+functions. All targets are explicit and source-pinned. Module/path bindings
+are restored after import; no shared predecessor module is modified.
+This boundary is retained to execute the actual source replay. Source-drift
+controls and the full replay check it. A static native integration would
+need its own loader and memory contract.
+
+Warning-strict normal and optimized Python checks, development mode and
+source compilation provide diagnostics. No external static analyzer is
+available in the selected environment; no repository-wide settings change.