Reduce complete P104 span-fact replay time by 67.09% (no new κ)

research/p104-span-bitset/BENCHMARK.json

@@ -0,0 +1,119 @@
+{
+  "complete": {
+    "completed_commands": 10,
+    "errors": 0,
+    "median_seconds": {
+      "bitset": 13.66525241592899,
+      "scalar": 14.982166209025308
+    },
+    "range_seconds": {
+      "bitset": [
+        13.1230415829923,
+        14.27175220916979
+      ],
+      "scalar": [
+        14.12012662482448,
+        16.949109292123467
+      ]
+    },
+    "reduction": 0.08789875741086128,
+    "seconds": {
+      "bitset": [
+        14.27175220916979,
+        13.563843125011772,
+        14.195595792029053,
+        13.66525241592899,
+        13.1230415829923
+      ],
+      "scalar": [
+        14.982166209025308,
+        16.07360037509352,
+        16.949109292123467,
+        14.541455458151177,
+        14.12012662482448
+      ]
+    },
+    "transcript_sha256": [
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782",
+      "0a65172e526d75a026bb8232eb90f9b44190cbc843c2149f6920fc2f13a43782"
+    ]
+  },
+  "implementation_sha256": {
+    "benchmark.py": "f3a8f6e6ef9b9de9a675001c89cab7a03882c513571b56f633d22c320f1f0d84",
+    "incidence.py": "0599f6e7089188325a96a0ac1e0370fdd6140179b09a9bed460e47313b153f4d",
+    "replay.py": "049cee0cfd3a7d09ca5f6a13d1d9ec796f463ab07e3580a20d3f47ad06921aee",
+    "verify.py": "814774f1dd60a138f9b21891a1ce9115271aa47682a178a47310fcdd9f7e23aa"
+  },
+  "load_average_after": [
+    5.599609375,
+    4.28857421875,
+    3.248046875
+  ],
+  "load_average_before": [
+    3.95166015625,
+    3.69189453125,
+    2.8828125
+  ],
+  "logical_cpus": 18,
+  "method": "five alternating fresh-process pairs per complete command; all work timed",
+  "numpy": "2.5.4",
+  "platform": "macOS-27.0.1-arm64-arm-64bit",
+  "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+  "schema_version": 1,
+  "source_manifest_sha256": "b6c2761575d51090e9095837a9b53cac704972bb1265ff178c95344701e262f0",
+  "span": {
+    "completed_commands": 10,
+    "errors": 0,
+    "median_seconds": {
+      "bitset": 0.8545080840121955,
+      "scalar": 2.596336791990325
+    },
+    "range_seconds": {
+      "bitset": [
+        0.8319042918737978,
+        0.8727450419683009
+      ],
+      "scalar": [
+        2.4367482499219477,
+        2.9179103339556605
+      ]
+    },
+    "reduction": 0.6708793379008666,
+    "seconds": {
+      "bitset": [
+        0.8434213330037892,
+        0.861412291880697,
+        0.8319042918737978,
+        0.8727450419683009,
+        0.8545080840121955
+      ],
+      "scalar": [
+        2.4666792501229793,
+        2.4367482499219477,
+        2.596336791990325,
+        2.9179103339556605,
+        2.6245213749352843
+      ]
+    },
+    "transcript_sha256": [
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0",
+      "32919ac4d4a527e2fa3aadf8b9bdd27d994289adbe2d96d3c32405defadb91c0"
+    ]
+  }
+}

research/p104-span-bitset/PROOF.md

@@ -0,0 +1,94 @@
+# Equivalence of the incidence substitution
+
+This scoped implementation argument is produced by Nick Petalas. The P104
+facts, root model, original assertions and bounded verification domain are
+Matarener's PR6188. This argument concerns the new implementation, not an
+independent proof of those mathematical facts.
+
+Let the ordered port labels be P=(p_0,...,p_(n-1)). For each nonzero binary
+section label z, define an integer
+
+    Z_z = sum_i 2^i [popcount(p_i & z) is even].
+
+The summands have distinct bit positions. Consequently bit i of Z_z is one
+if and only if the old ldot(p_i,z) equals zero. The old single-section count
+is therefore popcount(Z_z), and its two-section count is
+popcount(Z_z & Z_y). Integer AND has no cross-coordinate carries. Python's
+unbounded nonnegative integers compute these identities exactly.
+
+The implementation constructs Z_z for every z=1,...,511 and retains the
+original maximum over all z and every z<y. There are still 130,305 pairs.
+It does not identify planes modulo basis changes or discard equivalent pairs.
+The only reuse is the incidence of a fixed port with a fixed section.
+All maxima, including empty port sets in the test interface, are over the
+same nonempty sets of section labels.
+
+The source-bound adapter replaces only the S0 count computation. It retains
+the original definitions used later, the original S0 log and assertions, and
+every S1/S2' line. Adding a raw prefix to the initial docstring preserves its
+literal unrecognised backslash-H escape and removes its compilation warning.
+No executable statement changes for that spelling adjustment. Both engines
+make that same docstring adjustment. For the enclosing verifier, the only
+substitution selects the new span command at its original subprocess site.
+All other subprocesses, log authentication, assertions, result comparisons,
+controls and Lean-source checks execute unchanged. The inherited FULL mode is
+removed from the comparison environment so the command has the bounded
+contract. Neither engine runs the historical full census or a Lean build.
+
+Every live input is checked against its pinned SHA256 before compilation.
+The adapter accepts only this pinned source version; no claim of compatibility
+with future edits is made. A changed source needs a new pin and a new adapter
+review. Child commands always run without optimization. This preserves every
+predecessor assertion even when the new conformance driver runs under -O.
+The replay adapter rejects direct optimized invocation rather than silently
+dropping assertions.
+
+The conformance checker independently computes each parity as a sum of bit
+products, checks every represented coordinate and every actual two-section
+intersection, and compares the complete scalar and bitset outputs for both
+commands. Only the leading elapsed-time field is normalized. Counts, witness
+summaries, PASS markers and all remaining text must match exactly. Checks use
+explicit exceptions and remain active under optimization.
+
+# Resource and diagnostic scope
+
+The new incidence API admits widths 2..9 and at most 512 distinct labels.
+It stores at most 511 nonnegative 512-bit masks. Each capacity computation
+visits at most 130,305 pairs. The fixed conformance domains are 281 port sets,
+including all subsets at widths two and three, eight width-four fixtures,
+and the actual 104-port input. Each child has a 180-second timeout. The
+source inventory is bounded to 256 rows, each file to 16 MiB; files are read
+one at a time. Functions are below 60 lines. No new recursion or retry loop
+is introduced.
+
+Python allocates managed objects during execution. This is a Power of Ten
+rule 3 deviation, bounded by the fixed domains above; runtime/library
+allocation is not independently instrumented. Executing the source-bound
+adapter is a rule 8 deviation: both substitution sites are fixed, all input
+bytes are authenticated, and the comparator exercises the retained complete
+commands. The predecessor's own control flow and libraries remain inherited
+and unmodified. The purpose is a bounded replay improvement, not a rewrite
+of the older implementation under new coding rules.
+
+Warning-strict normal and optimized conformance are registered. The retained
+span docstring is the sole source spelling adjustment; no diagnostic is
+suppressed. The benchmark uses five alternating fresh-process pairs per
+scope, counts failed commands as errors, consumes and compares the complete
+output within each run, and includes source authentication and startup in
+its timed region. Its output contains the interpreter, numpy version,
+platform, processor count, load, raw samples and implementation hashes.
+Performance percentages are local measurements, not portable guarantees.
+
+# Descriptive timing comparison
+
+STATISTICS.json is generated from the saved BENCHMARK.json and binds its SHA256.
+For each scope put U=sum(a>b for a in scalar for b in bitset). Enumerate every
+five-element subset of the ten measurements as a possible scalar allocation.
+For each allocation recompute U, and count abs(2U-25) at least as large as the
+observed value. The complete domain has binomial(10,5)=252 allocations. The
+span command has U=25 with two tail allocations; the complete verifier has
+U=23 with eight. All five paired differences in each scope are positive.
+These exact calculations describe the supplied small sample. Independence
+from host load or a speed guarantee on another host is not proved. Registered
+conformance validates the main timing record; the descriptive calculation is
+separately recorded for inspection and is not a new runtime benchmark.

research/p104-span-bitset/README.md

@@ -0,0 +1,117 @@
+# Bitset incidence shortens the complete P104 B-form replay
+
+The complete P104 span-fact command has a 67.09% lower local median wall time,
+from 2.596 to 0.855 seconds. The scalar range is 2.437..2.918 seconds and the
+bitset range is 0.832..0.873 seconds. Five alternating fresh-process pairs
+produce identical normalized standard output and zero errors.
+
+The enclosing bounded B-form verifier has an observed 8.79% lower median,
+14.982 to 13.665 seconds. Its whole-caller wall-time comparison is inconclusive
+because the ranges overlap and host variation exceeds the median difference.
+All ten complete caller outputs still agree, with zero errors.
+[BENCHMARK.json](BENCHMARK.json) contains every sample, environment details,
+transcript hashes and implementation/input bindings.
+
+Claim type: measured complete-span verifier improvement with a scoped implementation-equivalence
+proof and exact finite conformance. No new mathematical bound or kappa is claimed.
+This contribution is produced by Nick Petalas.
+
+The profile locates the span command's dominant cost in repeated scalar label
+parities. Integer incidence masks reuse those parities while retaining every
+one of the 130,305 section pairs. The enclosing command retains the original
+S1/S2' checks, biclique replay, singular-rank self-test, authenticated census logs,
+result comparison, Lean-source scan and controls. The saved timing ranges are
+14.120..16.949 seconds for the scalar caller and
+13.123..14.272 seconds for the bitset caller.
+All five paired complete-verifier samples favor the bitset implementation.
+The complete ranges overlap; the exact descriptive rank-sum tail is 8/252
+(two-sided p=0.031746). [STATISTICS.json](STATISTICS.json) binds that calculation
+to the generated timing record. The whole-caller timing remains
+inconclusive. The clear span-command improvement has no portable speed guarantee. The standalone span median equals 17.3% of the complete scalar median. The
+end-to-end result is consistent with its available headroom. The remaining
+singular-rank stage limits the gain. The machine had other work running;
+alternating order and the recorded load averages make that limitation explicit.
+
+[PROOF.md](PROOF.md) explains the incidence identity, the exact source adapter,
+assertion preservation, resource bounds and deviations. Only the S0 count
+computation changes. A raw prefix preserves an inherited literal docstring
+escape while permitting warning-strict compilation. The original files remain
+unchanged. All 105 live inputs are pinned. A stable checkout is required while
+a command authenticates and reads its source files.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and numpy 2.5.4:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-span-bitset/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/p104-span-bitset/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-span-bitset
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-span-bitset --check-source-history --check-modes
+```
+
+Another CPython 3.12 path may replace the local path. The direct marker is
+`PASS_P104_SPAN_BITSET`. Both registered commands are bounded by 180 seconds.
+To execute only the faster complete consumer:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-span-bitset/replay.py --scope complete --engine bitset
+```
+
+To repeat the five alternating timing pairs for each command:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-span-bitset/benchmark.py
+```
+
+The benchmark prints a generated JSON record; save new output outside the
+checkout. It does not overwrite the published record. The conformance checker
+validates that record's hashes, raw-sample medians/ranges, error counts and
+transcripts. Its three record-corruption controls reject changed input bindings,
+medians and transcript hashes.
+
+## Evidence and limits
+
+The literal scalar oracle checks 281 fixtures and 136,569 section pairs,
+including every actual P104 section pair. Thirteen domain, section,
+source-corruption and normalization controls plus three record controls remain
+active under optimization. Complete scalar/bitset output comparisons execute
+both the span command and its enclosing bounded verifier. Child commands run
+without optimization, so the predecessor assertions remain enabled.
+
+The performance percentage is a single-host measurement on CPython 3.12.15,
+macOS arm64 with 18 logical CPUs and numpy 2.5.4. CI checks conformance and
+record integrity; it does not certify this host's percentage. The predecessor
+manifest pins a different numpy release. Both measured engines here use 2.5.4;
+no cross-version speed comparison is made.
+
+The enclosing bounded verifier authenticates recorded census logs. It does
+not recompute the full historical census or build Lean. This package preserves
+that coverage and does not claim independent acceptance of the predecessor
+mathematics. Full census, Lean, selected-supplier cold replay, native/caller
+admission and the complete multiplication theorem remain unrun. Independent
+human and formal proof-kernel review are unclaimed. The selected frontier is
+unchanged. Hosted CI is pending at publication.
+
+## Related open work
+
+- PR6218 supplies hand/Lean root and span facts and a different B-form reduction. This package accelerates the retained PR6188 bounded command; it does not re-check or replace PR6218's proof or compatible-plane work.
+- PR6198 proves E8 span inputs over odd-characteristic fields. Its span predicates and theorem are distinct; no common numerical result is compared.
+- PR6217 and PR6219 study P104 wire routing and disjoint A2 packing. They share the root geometry but do not implement this span-count substitution or measure this replay.
+
+## Open next questions
+
+Can the same incidence representation help another explicit finite-fact
+consumer? First profile a different complete command and specify its full
+output and checks. No other consumer is measured or adapted here. Further
+optimization of the other B-form replay stages is left unclaimed.
+
+## Credit
+
+Matarener retains PR6188's mathematical facts, root model, finite domains,
+original verifier, recorded evidence and attribution. DreamingOfClouds retains
+the underlying nine-term decoder/geometry code and its credited predecessor
+lineage. The incidence implementation, source adapter, implementation-equivalence
+argument and measurements are produced by Nick Petalas. Bitset intersection
+and population count are standard methods; no literature-priority claim is made.
+Apache-2.0. Frozen evidence and predecessor credit lines are unchanged.