Reduce complete core-section replay time by 79.02% (no κ)

research/core-section-gray-replay/PROOF.md

@@ -0,0 +1,92 @@
+# Exact Gray-code replacement of the section enumerator
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped implementation-equivalence proof. Gray-code enumeration
+and packed binary columns are classical. James Reed's PR3773 supplies the
+scientific consumer and its E8 core result. Neither the geometry nor the
+published histogram is a new theorem of this package.
+
+## The computed object
+
+Let c_0,...,c_(s-1) be d-bit binary coordinate vectors. For a d-bit mask m,
+the predecessor's expression computes
+
+    h(m) = #{j : popcount(m AND c_j) is even}.
+
+It builds an integer whose set bits are the distinct original root indices
+of those j, then takes its population count. Those root indices are distinct
+because they come from the bits of a set intersection. Thus the expression
+equals h(m). The consumer requires the multiset of h(m) for all nonzero masks.
+It still evaluates every core separately, including repeated isomorphism types.
+
+## Packed columns and the invariant
+
+For 0<=i<d define the s-bit column
+
+    C_i = sum_j bit_i(c_j) 2^j.
+
+For a mask m put O(m)=XOR_(i:bit_i(m)=1) C_i. Its jth bit is the parity of
+popcount(m AND c_j), by distributivity in F_2. Hence
+
+    h(m) = s - popcount(O(m)).
+
+The binary reflected Gray map is g(t)=t XOR floor(t/2), for
+0<=t<2^d. It is a bijection. Its inverse recovers the input bits from the
+highest bit downward, since g_i=t_i XOR t_(i+1). Also
+
+    g(t) XOR g(t-1) = 2^v2(t)     for 1<=t<2^d.
+
+To see this, if t has k trailing zeroes, t XOR (t-1)=2^(k+1)-1.
+XORing that number with its right shift leaves 2^k.
+
+Start with odd=0=O(g(0)). At step t, XOR C_v2(t) into odd. The displayed
+identity proves inductively that odd=O(g(t)). Store
+s-popcount(odd) at the ordinary mask index g(t). After the last step,
+every output equals h(m), including m=0. Taking Counter(counts[1:])
+therefore preserves exactly the predecessor's nonzero-mask multiset.
+
+The proof permits repeated coordinates, zero coordinates, an empty list and
+d=0. It does not require the coordinates to span the whole space. The
+implementation bounds d to 0..10 and s to 0..256; the identity itself holds
+for every finite d and s.
+
+## Whole-consumer substitution
+
+The adapter authenticates the three declared source inputs. It compiles the
+same authenticated source bytes after replacing exactly one unique expression:
+the assignment of the section Counter. Every other source byte is retained.
+The original file location is preserved so its geometry hash and RESULT.json
+checks use their original paths. The module is private and its main function
+is called explicitly. No source file or persistent module is patched.
+
+The replacement returns the same Counter for every reached input by the
+preceding identity. Consequently the per-core equality checks, aggregate,
+pair count, source hash check and final result comparison receive the same
+values. The complete stdout is unchanged. There is no saved geometry, cached
+answer, skipped pair or reuse across processes. The checkout must remain
+stable during execution, as the original consumer rereads its result file.
+
+## Exact work counts
+
+For one s-coordinate, d-dimensional core, the replaced expression performs
+s(2^d-1) parity evaluations, plus a population count of each constructed
+global root mask. The new routine builds d columns with ds one-bit tests,
+then performs 2^d-1 packed XOR updates and population counts. It also
+validates its input and writes each mask-indexed count once. These are
+operation counts, not equal-cost CPU instructions or a runtime lower bound.
+
+The complete reached domain has 3,780 cores with s=24,d=7, established by
+the unchanged consumer. The new conformance run records every invocation.
+It accounts for 11,521,440 replaced parity evaluations, 635,040 column bit
+tests and 480,060 packed updates. It compares all 480,060 nonzero-mask
+section counts with direct parity evaluation before any histogram grouping.
+
+## Verification boundary
+
+The written invariant proves the replacement. The exhaustive smaller-list
+checks and complete reached-domain comparison corroborate its implementation.
+They do not independently validate the predecessor's mathematical conclusion.
+Local timings measure the complete scientific consumer in fresh processes.
+They do not prove portable performance, native supplier costs, a new kappa,
+or any of the selected construction's five framework assumptions.

research/core-section-gray-replay/README.md

@@ -0,0 +1,144 @@
+# Complete core-section replay with 79.02% less wall time
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped implementation-equivalence proof, exact finite conformance
+and local performance evidence. The complete authenticated PR3773 scientific
+consumer takes 79.02% less median wall time locally, from 0.654020 s to
+0.137189 s across five alternating fresh-process pairs. All ten outputs agree
+and every pair improves, with zero failures. Optimization stopped at this first
+verified improvement.
+
+The new enumerator packs the coordinate bits into columns, then walks every
+nonzero functional by binary reflected Gray code. Each step needs one packed
+XOR and one population count. [PROOF.md](PROOF.md) proves the exact mask-table
+identity and its whole-consumer substitution. The adapter changes one expression
+in private, authenticated source. All original root construction, exact rational
+coordinates, binary rank checks, 3,780 core visits, per-core histogram checks,
+aggregate and RESULT.json comparison still execute. The predecessor files remain
+unchanged. This is an opt-in consumer, with no shared implementation changes.
+
+## Credit and scope
+
+James Reed / jwr404's [PR3773](https://github.com/CrocSwap/integer-mult-bounds/pull/3773),
+head `83cb934664879552405c60987ceca100f9656a49`, supplies the complete consumer,
+root geometry and section histogram. Credit conorholds for the recorded
+section-histogram premise, Nick Petalas for the retained E8 root geometry, and
+the P112 lineage retained in those sources. Their mathematical results are
+cited inputs, not audited or claimed as new. Gray-code subset enumeration and
+packed binary columns are classical. The new result is this exact replacement,
+its complete source-bound consumer and measured replay saving.
+
+Canonical base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8,
+selected PR6030. The replay-runtime card is refined to this consumer without
+changing its coverage requirement. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371293)
+records the scope. Live open/account PRs, recent handoffs, active Discussions,
+local reservations and main/merged object and implementation searches were
+checked. Sparse local notes, arbitrary historical diffs and unpublished work
+remain limits of the overlap picture.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/core-section-gray-replay
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/core-section-gray-replay/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/core-section-gray-replay/replay.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/core-section-gray-replay/benchmark.py --pairs 5
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/core-section-gray-replay --check-source-history
+```
+
+Another CPython 3.12 path may replace the shown interpreter. The verifier prints
+`PASS_CORE_SECTION_GRAY_REPLAY` in its generated JSON. The direct scientific
+consumer prints `PASS_CORE_SECTION_CAPACITY pairs=3780 sections=127 no_new_kappa`.
+Use `replay.py --engine original` for the same authenticated original consumer.
+To save a fresh package-hash-bound verification receipt, pass `--receipt` with
+an absolute path outside the checkout. Default execution writes no artifacts.
+
+## Exact conformance
+
+The verifier checks all 5,058 coordinate lists of lengths 0..3 in dimensions
+0..4, including repetitions, zero coordinates and deficient spans. All 74,958
+mask entries agree with independent direct parity evaluation. A separate
+256-coordinate, dimension-ten case checks all 1,024 masks at the API limits.
+
+At the complete scientific consumer, every reached mask table agrees before
+histogram grouping. This covers 3,780 cores and 480,060 nonzero-mask sections.
+The source expression's 11,521,440 parity evaluations become 635,040 column
+bit tests and 480,060 packed XOR updates. These are exact loop-work counts,
+not equal-cost instruction counts. The source retains its own mathematical
+success checks and full output comparison.
+
+Seventeen boundary controls reject malformed domains, an unknown engine,
+and modified or missing bytes at each of the three live source inputs.
+Six scientific controls reject inclusion of mask zero, a missing mask,
+complemented parity, a missing coordinate, a wrong expected histogram and
+a wrong core rank. Each control requires its expected failure reason.
+Registered replay includes warning-strict normal and optimized conformance,
+plus an uninstrumented fast consumer. Timing is an optional local check.
+
+## Local timing evidence
+
+The separate profile attributes 1.788 s of the source consumer's 1.988 s
+profiled cumulative time to section construction and Counter accumulation.
+Those profiled times are excluded from the wall-time comparison. The candidate
+replaces the measured bottleneck and has no persistent cache or tuned option.
+
+The benchmark times interpreter startup, source authentication and the complete
+scientific main function. Every subprocess must exit successfully, produce the
+exact full scientific stdout and have empty stderr. Metadata validation and
+added conformance checks run separately. The original arithmetic-only
+`test_verify.py` is outside this measured scientific command; its four identities
+are already checked in the complete consumer's count and aggregate comparisons.
+
+| Pair | Original seconds | Gray seconds |
+| ---: | ---: | ---: |
+| 1 | 0.654254 | 0.139853 |
+| 2 | 0.652888 | 0.137321 |
+| 3 | 0.654020 | 0.135996 |
+| 4 | 0.660023 | 0.137189 |
+| 5 | 0.653303 | 0.136774 |
+| Median | 0.654020 | 0.137189 |
+| Range | 0.652888..0.660023 | 0.135996..0.139853 |
+
+The host is macOS 27.0.1 arm64, CPython 3.12.15, with 18 logical CPUs.
+Load averages before the pairs were 1.66, 1.96 and 2.03. Other work shared
+the host; alternating runs give both engines comparable exposure. All five
+pairs improve, and the two timing ranges do not overlap. This is local evidence,
+with no portable runtime guarantee. The measured reduction is below the
+profiled bottleneck's share of the complete consumer.
+
+## Limits and engineering inspection
+
+The executable accepts dimension 0..10 and at most 256 coordinates. Its Gray
+loop has at most 1,023 iterations, with ten columns of at most 256 bits and
+1,024 output counts. Small-list enumeration has 5,058 cases; scientific
+conformance has 3,780 calls. The benchmark permits 5..15 pairs and bounds each
+child to 60 seconds. All new functions are shorter than 60 physical lines.
+There is no recursion or network access in the package.
+
+Python allocation and exact integer objects are managed-runtime deviations
+from fixed preallocation. Every new data structure has the preceding finite
+capacity. Source loading compiles one hash-authenticated predecessor program;
+the sole replacement string is required to occur exactly once. This private
+source adapter is a bounded dynamic-code exception. Verification callbacks
+have a closed set of six scientific controls and one conformance observer.
+They do not change the timed consumer. The inherited exact geometry code
+retains its resource behavior and source notice.
+
+No predecessor scientific result is independently audited, and the written
+replacement proof is not proof-kernel checked. Linux timing, physical native
+execution, source ownership/restoration, precision, stock, tape movement,
+complete supplier/outer invoices and the five selected framework assumptions
+remain outside this result. No Lean, Docker or selected supplier replay was
+run. No new kappa or selected-frontier change is claimed. Independent human
+and formal proof-kernel review are unclaimed. Hosted CI status belongs in the
+PR body.
+
+## Open next questions
+
+Should a maintained consumer adopt this enumerator? First review the single
+expression substitution and reproduce its complete benchmark on one Linux
+host. Maintainer adoption and Linux performance evidence remain separate;
+this package reserves no continuation or wider geometry census.

research/core-section-gray-replay/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/core-section-capacity/RESULT.json",
+      "usage": "input",
+      "git_blob": "761d7c8b8285e1f21a0ebc28578fef0d1723184c",
+      "sha256": "0a153df8f62346210483b4b1b01829bcd41d13441633824c0b6937accbd506cc"
+    },
+    {
+      "path": "research/core-section-capacity/verify.py",
+      "usage": "input",
+      "git_blob": "211edb899fe96f54927bee6a1cc25708fd1d0319",
+      "sha256": "c5b7c30e41c72599f75606e73e912ba3d194bff2015c02ec2390ad4d89243d06"
+    },
+    {
+      "path": "research/p112-root-simplex-exclusion/geometry.py",
+      "usage": "input",
+      "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f",
+      "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021"
+    }
+  ]
+}

research/core-section-gray-replay/TASK.json

@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "replay-runtime",
+    "question": "Can one measured replay bottleneck be sped up without dropping coverage?",
+    "starting_points": [
+      "scripts/run_isolated_tests.py",
+      "scripts/verify_replay_coverage.py",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Profile one isolated replay and optimize the measured bottleneck.",
+      "Design source-bound reuse with explicit dependency invalidation and negative controls."
+    ],
+    "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.",
+    "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.",
+    "allowed_variations": [
+      "Profile one stage or design one source-bound cache boundary."
+    ],
+    "scope_change_triggers": [
+      "Skipping coverage or comparing different fixtures to claim speedup."
+    ],
+    "overlap_terms": [
+      "replay runtime",
+      "cache invalidation",
+      "isolated tests"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Optimize the complete PR3773 scientific consumer by Gray-code enumeration of every nonzero core functional, preserving source checks and exact output.",
+  "scope_change_reason": "The card is narrowed to one authenticated core-section consumer and one packed parity implementation. Its coverage-preserving optimization premise is unchanged.",
+  "bottleneck_link": "A faster complete geometry replay reduces the cost of checking this fixed decoder ingredient. It does not improve a supplier bill or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified complete-consumer wall-time improvement; no second optimization or larger geometry census.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py establish exact mask-table equivalence; benchmark.py records five alternating fresh-process pairs with identical complete stdout and zero failures.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Should a maintained core-section consumer adopt this enumerator?",
+      "why_it_matters": "The isolated adapter improves replay throughput without modifying frozen source.",
+      "first_step": "Review the one-expression substitution and reproduce the complete benchmark on one Linux host.",
+      "blocked_by": "Maintainer adoption and a separate Linux performance measurement are absent."
+    }
+  ],
+  "coordination": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371293",
+    "checked_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "checked_at_utc": "2026-11-03T10:09:20Z",
+    "priority_revision": 8,
+    "selected_pr": 6030,
+    "source_pr": 3773,
+    "source_author": "jwr404",
+    "limitations": "Sparse local notes, arbitrary historical diffs and unpublished work are not exhaustively searched.",
+    "overlap_coverage": {
+      "open_prs": 524,
+      "open_prs_complete": true,
+      "open_prs_at": "2026-11-03T10:08:44Z",
+      "discussion_records": 6539,
+      "discussions_complete": true,
+      "discussions_at": "2026-11-03T10:10:00Z",
+      "local_records": 120,
+      "head_note_paths": 8917
+    }
+  }
+}