Reduce complete partial-Pauli replay time by 5.20% (no κ)

research/partial-pauli-action-tables/PROOF.md

@@ -0,0 +1,94 @@
+# Exact finite binary actions with invocation-local tables
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Equivalence on the declared domain
+
+Let `v=(v_0,...,v_(k-1))`, with `0<=k<=4` and each v_j an integer in
+0..15. Let `0<=x<2^k`. The original action is the XOR of those v_j
+whose bit j in x is one. It is defined even for zero or dependent columns.
+
+Initialize `T[0]=0`. For c=1,...,2^k-1, let b be its least set bit,
+with b=2^j, and set
+
+```text
+T[c] = T[c xor b] xor v_j.
+```
+
+Because `c xor b<c`, strong induction proves that every T[c] is precisely
+the original action. The removed bit j occurs once and every other set bit
+is retained. This proves the replacement on the entire declared domain.
+The bound four is the fixed caller's two-qubit domain, not a restriction on
+the predecessor's written dimension-uniform mathematical theorem.
+
+The dictionary key is a tuple copy of the columns. A later mutation of an
+input list therefore selects a different value key. Tables belong to a
+single `make_action` closure and cannot be reused across independent replay
+invocations. The fast path trusts the authenticated caller's integer-column
+contract; it is not a general parser for arbitrary Python numeric objects.
+Fresh-key validation and the mask check reject the named malformed controls.
+
+There are at most `sum_(k=0)^4 16^k=69905` possible valid keys and
+`sum_(k=0)^4 32^k=1082401` entries across all possible tables. The implementation
+enforces key and table capacities. For the actual complete command it builds
+only 3,466 tables and 32,551 entries. Each table takes one action-value XOR
+per entry after zero, giving 29,085 such XORs. Direct counting of every
+original mask gives 468,473 accumulator XORs. Index XORs and dictionary work
+are excluded from these operation counts and included in wall measurements.
+
+## Binding to the complete caller
+
+The adapter reads and SHA256-authenticates the exact declared source before
+compiling those bytes, so preexisting Python bytecode cannot replace the
+retained verifier. It changes only the private module's `act` binding, then
+calls the original `main` unchanged. Every original action call uses at most
+four four-bit columns and a valid coordinate mask. The complete transcript
+checks this finite binding against every original action, and exhaustive
+domain equality establishes the replacement independently of digest equality.
+
+Identical action values leave group/subspace enumeration, completion-fiber
+minima, selected representatives, signed corrections, literal rational
+matrix columns and controls unchanged. No mathematical success, source
+table, completion list or signed lift is reused from an earlier process.
+Source authentication, table construction and every original check occur
+inside each timed command. Both timing sides use the same authentication
+wrapper; only the action implementation differs.
+
+The result is an implementation-equivalence proof and a bounded finite
+certificate of less repeated work. It does not independently re-establish
+Ali Romman's rank theorem. The local timing observation is empirical and
+does not follow from the XOR count alone.
+
+## Implementation bounds and deviations
+
+New functions are below sixty physical lines. New loops have explicit fixed
+domain limits: four columns, sixteen entries per table, 69,905 tables,
+1,082,401 exhaustive actions, twelve named controls, and at most twelve
+benchmark pairs. Child commands have thirty-second timeouts; registered
+checks have 120-second timeouts. Explicit exceptions remain active under
+optimized Python. New code uses no recursion or network service.
+
+Power of Ten rule 1: the unchanged authenticated source retains its recursive
+symplectic enumerator. Its fixed n<=2 caller permits at most five active
+`extend` frames, with column lists of length at most four. Changing that
+enumerator would expand this frozen-source adapter task. The complete replay
+exercises its finite bound; a future source change requires a new pin and
+separate inspection. A byte-exact interpreter-stack budget is unclaimed.
+
+Rule 3: Python allocates managed integers, tuples, dictionaries and lists.
+The capacities above bound the new table storage; the exhaustive check does
+not claim constant-space execution. Existing rational arithmetic and source
+collections remain bounded by their fixed complete fixture. A native port
+would need its own static-capacity arithmetic and allocation ledger.
+
+Rules 8 and 9: executing a hash-pinned source module and replacing its one
+action binding are the explicit adapter boundary. Source size is capped at
+65,536 bytes. The only production call targets are the retained action or
+the new action closure. Test tracing and the one fixed source-corruption
+mock are bounded instrumentation. No unauthenticated code is executed.
+Any broader plugin or dynamic-input interface needs a separate contract.
+
+Rule 10: warning-strict normal and optimized executions and in-memory syntax
+checks are available. No separate Python static analyzer is installed on the
+local PATH; stronger static-analysis coverage is unclaimed. No shared build
+configuration or diagnostics are weakened for this isolated package.

research/partial-pauli-action-tables/README.md

@@ -0,0 +1,121 @@
+# Exact action tables reduce complete partial-Pauli replay time
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped implementation-equivalence proof with exact finite
+conformance and local performance evidence. No new mathematical rank bound,
+kappa or supplier admission is claimed.
+
+An optional adapter reduces the median wall time of Ali Romman's complete
+[PR5342 replay](https://github.com/CrocSwap/integer-mult-bounds/pull/5342)
+by **5.20%**, from 0.254097 to 0.240896 seconds on the measured local host.
+Six alternating fresh-process pairs have identical complete stdout and zero
+failures. Both sides include Python startup, source authentication, compilation
+and the entire original `main`. No persistent table or cached successful check
+is used. The original verifier and its proof remain unchanged.
+
+The complete command retains 10,113 completion fibers, 386 signed lifts,
+848 literal Gaussian-rational matrix-column checks and all five original
+controls. The adapter replaces only binary `act` evaluation. Its 307,191
+calls use 3,466 tables with 32,551 entries, built within that invocation.
+Action-value accumulation uses 29,085 XORs instead of 468,473, saving 439,388.
+These counts exclude index arithmetic and dictionary work; the complete wall
+measurement includes that overhead. Discovery stopped at this first improvement.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/partial-pauli-action-tables/replay.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/partial-pauli-action-tables/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/partial-pauli-action-tables/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/partial-pauli-action-tables
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/partial-pauli-action-tables --check-source-history
+```
+
+Replace the interpreter path on other hosts. `replay.py --original` runs the
+unchanged algorithm through the same source-authentication wrapper. Both
+replay modes print `PASS_PARTIAL_PAULI_GAUSSIAN_MINIMUM` and the complete
+original counts. The registered normal and optimized conformance commands
+print `PASS_PARTIAL_PAULI_ACTION_TABLES`, with a generated file-hash-bound
+receipt on stdout. No receipt is hand-written or committed.
+
+The verifier compares the complete ordered action transcripts and stdout,
+then directly checks all 1,082,401 actions on every tuple of zero through four
+four-bit columns. That domain includes zero and dependent columns. Twelve
+named controls cover fresh-cache invalid requests, invocation isolation,
+mutable-list keys and source corruption before execution. Assertions are
+not used for admission. [PROOF.md](PROOF.md) gives the induction and scope.
+
+To repeat timing, supply a new absolute output path outside the checkout:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/partial-pauli-action-tables/benchmark.py --output /absolute/scratch/measurement.json
+```
+
+Timing is not a CI passing threshold. The complete output SHA256 is
+`32ba2068f05bf13e509776284f64834442447bd12dd8d2bed93e10e585c388bb`.
+
+## Measurement record
+
+CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. Load averages before
+were 2.421/2.742/2.257 and after 2.467/2.746/2.261. Other research processes
+shared the machine; the measurements were serial and interleaved.
+One warmup of each side preceded the twelve timed complete commands.
+
+| Pair | Original seconds | Table seconds |
+| --- | ---: | ---: |
+| 1 | 0.255615333 | 0.240823125 |
+| 2 | 0.275469167 | 0.243438208 |
+| 3 | 0.253116833 | 0.244139875 |
+| 4 | 0.255076584 | 0.240015208 |
+| 5 | 0.249899458 | 0.240258291 |
+| 6 | 0.250187750 | 0.240967959 |
+
+The original range is 0.249899458..0.275469167 seconds; the table range is
+0.240015208..0.244139875. Medians are 0.2540967085 and 0.2408955420 seconds.
+This is a local matched-wrapper observation, not a host-independent guarantee.
+An untimed original profile places 0.049 of 0.673 instrumented seconds in
+`act`; literal rational word checks dominate at 0.464 seconds. Thus the
+measured small end-to-end gain is consistent with the targeted work's share.
+Profiler times are not the benchmark samples.
+
+The measured implementation SHA256 is
+`43aa41ca77f3339249844f700b133319c974e10ddf8a7db3d9e71375b2a7f2c0`.
+The benchmark SHA256 is
+`41913d342a171c3a22ec7e970363da722d9c11374b00d99d0c3ad1d37629d1ff`.
+The source manifest SHA256 is
+`a818b2f68ded7caa6fe2b188dcfa973f767cabc771a823188858b4c863bdf0e9`.
+
+## Scope and credit
+
+Ali Romman / PR5342 supplies the complete original replay, rank theorem,
+fixture choices and five controls. JoyboyBrian / PR5051 supplies the signed
+partial-map conventions and lift lineage; David Ganz / Dugongue / PR4841
+supplies the native compiler context. Nick Petalas's partial-transvection
+work remains a different tariff result. Classical XOR subset evaluation
+retains its credit. The new contribution is this bounded adapter and its
+complete-process implementation improvement, not an audit of those results.
+
+The refined `replay-runtime` card, source bytes and selected-record provenance
+are pinned at main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority 8.
+The selected source-binding orientation passed. Cached overlap covered 572
+open PRs and 6,639 Discussion records, but only 135 of 8,917 local notes.
+Direct main and merged-PR searches supplemented that incomplete local view.
+Arbitrary historical diffs and unpublished work remain unknown.
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375443).
+
+No new completion construction, physical contact, literal phase theorem,
+rounded implementation, stock/tape bound, compiler closure or full multiplier
+is supplied. All five selected framework assumptions remain. Independent
+human and formal proof-kernel review are unclaimed. The selected cold replay,
+Lean and Docker were outside scope and unrun.
+
+## Open next questions
+
+Does a named larger consumer benefit from the same table policy? First pin
+that consumer and profile its complete action-call distribution. This matters
+because the measured gain is limited to this complete fixture. Larger source
+contracts, memory bounds and a complete physical bill are absent here.
+The structured question is in [TASK.json](TASK.json).

research/partial-pauli-action-tables/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/partial-pauli-gaussian-minimum/README.md",
+      "usage": "input",
+      "git_blob": "e25c78371f422b1ee6fbec130abeb2329abde760",
+      "sha256": "b18eae1ab495f00aeadc053f8925f27a3a2c43bebc8110f9195b6a770bce9f6f"
+    },
+    {
+      "path": "research/partial-pauli-gaussian-minimum/verify.py",
+      "usage": "input",
+      "git_blob": "7c1b4af0f65db4cb0ebe58c63e6dd8651831f8ff",
+      "sha256": "ec496729abac96537cefc5d93f1fd216c56fa9131f29471df5927d4d3fc49c16"
+    }
+  ]
+}

research/partial-pauli-action-tables/TASK.json

@@ -0,0 +1,61 @@
+{
+  "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": "Invocation-local exact action tables for the complete PR5342 partial-Pauli Gaussian-minimum replay.",
+  "scope_change_reason": "One measured bottleneck in one unchanged complete source-authenticated replay; no theorem audit or new rank claim.",
+  "bottleneck_link": "Reduces repeated exact work in a complete enabling-interface replay while retaining every predecessor check.",
+  "budget_minutes": 60,
+  "stop_rule": "Freeze the first verified complete-process improvement; package it without optimizing another stage.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; warning-strict normal and optimized full conformance; exhaustive bounded action-domain equivalence; complete-process alternating measurements in README.md.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does a named larger consumer benefit from the same table policy?",
+      "why_it_matters": "The measured speed improvement is limited to the complete PR5342 fixture.",
+      "first_step": "Pin that consumer and profile its complete action-call distribution before changing its implementation.",
+      "blocked_by": "No larger consumer or complete physical cost contract is supplied."
+    }
+  ]
+}

research/partial-pauli-action-tables/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/partial-pauli-gaussian-minimum/README.md",
+    "research/partial-pauli-gaussian-minimum/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete unchanged replay and ordered action trace, exhaustive 1082401-action domain, named invalid-input, lifetime, mutable-key and source-corruption controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete conformance checks with Python assertions disabled."
+    }
+  ]
+}