Reduce complete positive-frame replay time by 71.4% (no new κ)

research/positive-frame-subset-join/BENCHMARK.json

@@ -0,0 +1,117 @@
+{
+  "environment": {
+    "cores": 18,
+    "executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
+    "load_average_at_finish": [
+      5.43017578125,
+      3.62109375,
+      3.080078125
+    ],
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]"
+  },
+  "errors": 0,
+  "implementation_sha256": {
+    "SOURCES.json": "4b6b36c69d72135b80a7e4359af28bd80cc2098bf8475ba8d5214cde0c0a6194",
+    "benchmark.py": "2485364ad607abb9ea2d0895235ff1d4422b1864c7a6e601133e9accc76d2eaf",
+    "fast_support.py": "9fd50dcbd54aaffb2e2f84c1357b7937d9e4c3cec3c0f243428efd3ee0bd383c",
+    "run.py": "7c48db5e75352713e9d4900d9b3fe1feabaccdafee425d9262f53c78e467b99b"
+  },
+  "pairs": 5,
+  "runs": [
+    {
+      "elapsed_ns": 30160228625,
+      "mode": "baseline",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 8189630625,
+      "mode": "accelerated",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 28718976666,
+      "mode": "baseline",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 8254057875,
+      "mode": "accelerated",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 30836784042,
+      "mode": "baseline",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 8290262334,
+      "mode": "accelerated",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 29031493791,
+      "mode": "baseline",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 8377977166,
+      "mode": "accelerated",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 28521156625,
+      "mode": "baseline",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    },
+    {
+      "elapsed_ns": 8393955666,
+      "mode": "accelerated",
+      "returncode": 0,
+      "stderr_bytes": 0,
+      "stdout_bytes": 787,
+      "stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c"
+    }
+  ],
+  "saved_fraction": 0.7144390022200632,
+  "schema_version": 1,
+  "summary": {
+    "accelerated": {
+      "maximum_ns": 8393955666,
+      "median_ns": 8290262334,
+      "minimum_ns": 8189630625
+    },
+    "baseline": {
+      "maximum_ns": 30836784042,
+      "median_ns": 29031493791,
+      "minimum_ns": 28521156625
+    }
+  }
+}

research/positive-frame-subset-join/PROOF.md

@@ -0,0 +1,121 @@
+# Equivalence of the integer subset join
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Predicate
+
+Let L_0,...,L_5 and H_0,...,H_3 be rational triples. Let c_0,...,c_5 be
+nonnegative integer multiplicities. The predicate required for each target H is
+
+    H in {sum_i u_i L_i : 0 <= u_i <= c_i, u_i integer}.
+
+This is membership in a set of possible exponents. It is not a count of
+representations or a sum of coefficients modulo two. Repeated labels and
+cancellation of different representations must preserve existential membership.
+The predecessor uses precisely this predicate in its concrete regression.
+
+The implementation accepts six labels, four targets, three coordinates,
+sum c_i <= 8, and rational numerators and denominators of at most 256 bits.
+The algebraic equivalence below holds without these finite resource bounds.
+
+## Integer join
+
+Take D to be the least common multiple of every denominator in the six labels
+and four targets. In particular, target denominators participate. Multiplication
+by the positive integer D is injective on rational triples and maps all ten
+vectors to integer triples. Define
+
+    O = {sum_(i=0..3) u_i D L_i : 0 <= u_i <= c_i},
+    N = {sum_(i=4..5) u_i D L_i : 0 <= u_i <= c_i}.
+
+The full scaled subset set is exactly O+N. Every six-tuple of multiplicities
+splits into one four-tuple and one two-tuple, and every such pair recombines
+into a legal six-tuple. Consequently
+
+    H is in the original set  iff  some n in N has D H - n in O.
+
+`integer_vectors`, `subset_sums` and `support_mask` implement these three
+operations using exact Python integers. Sets remove duplicate values on both
+sides of the equivalence. Negative coordinates, zero counts, repeated labels
+and targets with denominators absent from the labels require no exceptions.
+No parity reduction, rounding, probabilistic hash or numerical tolerance is used.
+
+## Complete replay adapter
+
+`run.py` authenticates the exact predecessor source and every declared external
+input before compiling that source. A fresh module has the predecessor's actual
+file path, so its own input authentication uses the original repository layout.
+The baseline calls its unchanged `main`. The accelerated mode replaces only its
+`direct_support_regression` function.
+
+The replacement preserves the original outer profile order, the direction grid,
+primitive-direction filter, sorted rational scale set, rank-one checks, target
+conjunction, exact-lattice test for each support survivor, and returned counters.
+`concrete_splits` copies the original inventory construction, credited to Josie
+Elliston. Its only extracted responsibility is emitting the same concrete labels.
+The proved join replaces the full rational subset-set expression. All other
+functions, symbolic support classification, source checks, eight-call control,
+target mutation and denominator control execute their original source bytes.
+`source.TARGETS` is read at each predicate call; no result cache can retain an old
+target or split. Unknown source revisions fail authentication.
+
+Under successful execution and the authenticated source's stated domain, every
+concrete support decision and every subsequent lattice call therefore agrees.
+The complete output agrees as well. This is a scoped program-equivalence
+argument. It neither reproves nor independently accepts the predecessor theorem.
+
+## Finite corroboration and performance boundary
+
+`verify.py` compares every four-bit support mask in the complete concrete
+inventory with a separately written literal Fraction enumeration, then executes
+the complete accelerated predecessor command. It also checks small rational
+fixtures and input/source rejections. `RESULT.json` is generated by that command;
+it binds the implementation and input manifest by SHA256. Default replay checks
+the receipt and writes no files.
+
+`benchmark.py` starts a fresh complete process for each side in five or more
+alternating pairs. Timing includes source authentication, imports, every check,
+captured output and process completion. Every return code, stderr and complete
+stdout is checked. It records individual nanosecond timings, environment and
+code hashes. It does not reuse subset results across processes. Profiling is a
+separate diagnostic run, excluded from the reported timings. Hosted conformance
+does not certify a local machine's performance percentage.
+
+## Resource bounds and implementation constraints
+
+The four old-label subset loops have at most 81 iterations, and the two added
+loops at most 25, by the total-multiplicity bound of eight. Each target checks at
+most 25 integer differences. Denominator clearing visits exactly 30 coordinates.
+There are at most 442 profiles; each profile's scale generator has at most
+sum_(m=2..40)(m-1)=780 iterations, or at most 17*9 direction candidates. The
+generic conformance grid has 4^6 candidate multiplicities. Benchmarking permits
+five through nine pairs, with a 300-second timeout per complete process.
+
+New code has no recursion, persistent cache, network call or background process.
+All new functions fit within 60 lines. Explicit exceptions retain checks under
+optimized Python. Warning-strict normal and optimized execution and AST parsing
+are the diagnostics; no separate static type analyzer is claimed.
+
+Power-of-ten rule 3 deviation: CPython allocates integers, Fractions, sets and
+modules dynamically. The new join has at most 106 stored subset triples, with
+integer bit lengths below 8192 under its enforced generic input bound. The
+concrete generator stores at most 780 splits at a time. Source files are capped
+at one MiB each. Runtime allocation internals are not instrumented. A fixed
+allocation implementation is required before using this reference in an
+allocation-prohibited runtime.
+
+Rules 8 and 9 deviation: the adapter executes one hash-authenticated predecessor
+module and calls its fixed helper functions. This is required to run the actual
+unchanged complete checker without editing frozen evidence. No CLI-supplied
+code or module name is accepted. All external source paths are declared in
+VERIFY.json and authenticated. A future different source requires a new pin and
+equivalence assessment. The predecessor's preexisting lattice loops and long
+`main` remain frozen; this package makes no new resource-compliance claim about
+that retained implementation.
+
+The verifier's complete reference enumeration intentionally uses Fractions to
+avoid depending on the proposed denominator-clearing mechanism. It has at most
+144 multiplicity tuples per concrete split under the source's total bound of
+seven, and uses the same finite split inventory. This extra conformance work is
+verification overhead; it is not included as part of the accelerated scientific
+command being compared with the original scientific command.

research/positive-frame-subset-join/README.md

@@ -0,0 +1,122 @@
+# Complete positive-frame replay in less time
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: **measured verifier improvement with a scoped equivalence proof
+and finite conformance checks**. No new kappa is claimed.
+
+An exact integer subset join reduces the complete PR #6111 command's local
+median elapsed time from 29.031 s to 8.290 s, **71.4% less**.
+All ten fresh commands emit the same 787 bytes, with zero errors. The frozen
+predecessor checker and its mathematical result remain Josie Elliston's work.
+This package contributes the accelerator, its equivalence proof and measurement.
+
+| Complete command | Median | Range | Runs |
+| --- | ---: | ---: | ---: |
+| Original predicates | 29.031 s | 28.521–30.837 s | 5 |
+| Integer subset join | 8.290 s | 8.190–8.394 s | 5 |
+
+[BENCHMARK.json](BENCHMARK.json) is generated by five alternating baseline/fast
+pairs on CPython 3.12.15, macOS arm64. Timing includes fresh process startup,
+source authentication, all original checks and controls, output and exit.
+Other processes were active on this 18-core host. This is a single-host result,
+not a cross-platform performance guarantee or a new mathematical bound.
+
+## What changes
+
+The concrete scan originally constructs every rational six-label subset sum.
+The new calculation clears all label **and target** denominators once, builds
+integer subset sets for four old labels and two added labels, then tests
+membership by subtraction. The inventory, rank-one checks, exact lattice
+filters, source checks and remaining complete command execute unchanged.
+A separate profile placed 84.219 of 102.461 instrumented seconds in the concrete
+scan. The instrumented run is excluded from the benchmark. Repeated Fraction
+multiplication and addition were the measured bottleneck.
+
+[PROOF.md](PROOF.md) proves the membership equivalence, including repeated
+labels, negative coordinates, zero multiplicities and different target
+denominators. `run.py` authenticates the fixed external source bytes before
+compiling them. It changes one function in a fresh module. No source file or
+persistent cache is changed, and a changed input fails its source pin.
+
+## Evidence
+
+The generated [RESULT.json](RESULT.json) binds the new implementation and input
+manifest. The verifier compares all four target decisions on **46,916 concrete
+splits** against a separately written literal Fraction enumeration. Those are
+conformance cases for the new implementation, not a new predecessor census.
+It also checks 420 small rational cases and seven input/source rejections,
+then runs the complete accelerated source checker and checks its full output.
+Normal and optimized verification are registered in VERIFY.json.
+
+The complete output SHA256 is
+`429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c`.
+Every timed output has that hash. No non-success command is included as a fast
+sample. The generator records every return code, stderr length and elapsed time.
+The standard join technique itself is not claimed as a new algorithm.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/positive-frame-subset-join/run.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/positive-frame-subset-join/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/positive-frame-subset-join/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/positive-frame-subset-join
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/positive-frame-subset-join --check-source-history
+```
+
+Another machine can substitute its CPython 3.12 path. Add `--baseline` to run.py
+for the original predicates. To rerun the timing experiment, use `benchmark.py
+--pairs 5 --output PATH` with a chosen output path outside the checkout. The
+benchmark is opt-in; CI runs conformance rather than asserting a machine speed.
+The standalone adapter and verifier also work in the official Git-free export
+with the declared inputs. Receipt regeneration is explicit `verify.py --write
+PATH`; default replay writes nothing.
+
+## Scope, sources and limits
+
+The replay-runtime card is refined to an original exact-support performance
+question. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267812).
+Base main is `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision 8.
+The current selected source-binding orientation passed; no selected scientific
+cold replay was run. SOURCES.json pins the original source and its complete
+runtime input closure. Frozen predecessor files are unchanged.
+
+Live open PRs, recent claims and local reservations, all 373 account PRs in the
+prior seven days, distinctive main README terms and merged searches were
+inspected. The overlap helper covered all 318 open PRs and 5,870 Discussion
+records, but only 81 of 8,567 local note records. This is bounded overlap
+coverage, not proof of novelty or coverage of unpublished work. No same-checker
+performance target was found. This work does not extend this account's earlier
+endpoint theorems or use another package's open question as its target.
+
+The equivalence statement concerns successful execution of this exact checker
+on its fixed domain. It supplies no new positive-frame theorem, native word,
+physical supplier, compiler/precision/ownership proof or multiplication theorem.
+The predecessor's scientific review status is inherited. Independent human and
+formal proof-kernel review are unclaimed. No Lean, Docker, historical full suite
+or selected supplier replay was run. Managed-allocation and fixed authenticated
+module-execution deviations are recorded in PROOF.md.
+
+## Open next questions
+
+The unchanged symbolic support stage may warrant a separate integer formulation.
+First profile the complete accelerated command and define that stage's exact
+return-value contract. A separate implementation and measurement are required;
+no such improvement or follow-on reservation is claimed here.
+
+## Credit
+
+Josie Elliston's [PR #6111](https://github.com/CrocSwap/integer-mult-bounds/pull/6111)
+supplies the theorem, source checker, concrete split inventory and existing
+controls. Its retained head is `961b749fa40a1117d0746064528d2dfa290c57e0`.
+JoyboyBrian's handoff #6104 supplies the underlying two-frame question and
+parameterization; apoursh's #6089 supplies the one-frame classification and
+symmetries. Cinna Davis supplies the PR2085/2112 model; Philippe Van Velzen
+supplies the earlier eight-call floor; Nick Petalas supplies the determinant
+method. Retain the BIT and formal-model lineage credited in those sources.
+Their original notices are unchanged. Denominator clearing and subset joining
+are standard techniques; the new contribution is their source-bound integration,
+coverage argument and complete-command performance evidence.

research/positive-frame-subset-join/RESULT.json

@@ -0,0 +1,16 @@
+{
+  "benchmark_pairs": 5,
+  "complete_stdout_sha256": "429df60e41b623420af1af7119a0734a6686e3a0b4bd75e360317ea3b8efe15c",
+  "implementation_sha256": {
+    "BENCHMARK.json": "d52d116955011550bc1f7908e179018f671e16192d42e263e3f901e023d0a59f",
+    "SOURCES.json": "4b6b36c69d72135b80a7e4359af28bd80cc2098bf8475ba8d5214cde0c0a6194",
+    "fast_support.py": "9fd50dcbd54aaffb2e2f84c1357b7937d9e4c3cec3c0f243428efd3ee0bd383c",
+    "run.py": "7c48db5e75352713e9d4900d9b3fe1feabaccdafee425d9262f53c78e467b99b",
+    "verify.py": "2bbdde2ef2d7d3f40be79424da6dc94ac9babfedd97318ee1c99c987cc35f482"
+  },
+  "mask_sha256": "c55f7be3beb1c63e74d8b78473c2ec6fea526a15adaf4ac6c9030bff38a4136c",
+  "rejections": 7,
+  "small_cases": 420,
+  "source_sha256": "7d68cce0cdd09c1e6afb7dc2b78e298b6f5c92ad39958e3a79f5d53e8377f5e1",
+  "split_masks_compared": 46916
+}