Reduce complete P112 compatibility replay time by 76.09% (no κ)

research/p112-compatibility-kernels/PROOF.md

@@ -0,0 +1,100 @@
+# Exact restriction-kernel evaluation
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+The census, decoder theorem and scientific receipt are Philipp / mightyOil's
+[PR1325](https://github.com/CrocSwap/integer-mult-bounds/pull/1325).
+Binary elimination and rank-nullity are classical. PR1325's `independent.py`
+already computes nullities by stacking equations in nine coefficient
+coordinates. No priority for that method is claimed. The new contribution is
+direct restriction of bit-string basis rows as an exact, faster evaluator
+preserving the primary command's complete scientific object and ordered digest.
+
+## The replacement identity
+
+Let V be a binary vector space of bit strings of length n. Let g_1,...,g_d
+be an independent basis. For a bit mask M, restriction to M is the linear map
+
+```text
+R_M : V -> F_2^n,     v -> v & M.
+```
+
+Its matrix has rows g_i & M. Therefore
+
+```text
+dim {v in V : v & M = 0} = d - rank_F2(g_i & M : 1<=i<=d).
+```
+
+The predecessor constructs that kernel by filtering every vector in V and
+takes log_2 of the resulting cardinality. A binary vector space of dimension k
+has exactly 2^k elements, so both methods return exactly the same integer.
+The restriction images may be dependent even when the original basis is
+independent. Elimination must occur after restriction; subtracting the number
+of nonzero restricted basis vectors would be wrong.
+
+For each plane with canonical generators x,y, the predecessor tests
+`not z & (x|y) & conflict[a][k]`. Choose
+`M=(x|y)&conflict[a][k]`. For its single-vector census choose
+`M=z&conflict[a][3]`. These are exactly the two uses replaced in `fast.py`.
+No predicate, selected mask or plane representative changes.
+
+## Complete output preservation
+
+The implementation retains each source geometry, pairing, support and span
+constructor. It visits the same sorted spaces, the same canonical plane test
+`y < x^y`, the same three anchors and the same partner order. Each dimension
+tuple is equal by the identity above. Consequently every census increment and
+every canonical byte fed to the ordered plane digest agrees.
+
+The source's real-span, code-dimension and zero-cost checks remain. Every
+decoder witness, nonconstant example and all six rejection controls are
+retained, in their original order. The new orchestration calls the pinned
+source's `decode` and `check_identity` functions. The complete returned object,
+including source hashes, is compared with the unchanged source certificate.
+The CLI prints the identical scientific success line. Exclusive `--write`
+creation produces the same sorted, indented scientific JSON and rejects
+overwriting an existing file. These statements concern preservation of the
+source contract; they are not independent validation of the decoder theorem.
+
+## Exact restriction work
+
+The three coordinate spaces have 256 elements and dimension eight; the extra
+space has 512 elements and dimension nine. For each of the 32,385 planes,
+the source masks 256+256+512 partner vectors. Its 765 single-vector queries
+each mask 512 vectors. Thus it performs
+
+```text
+32385*(256+256+512) + 765*512 = 33,553,920 vector restrictions.
+```
+
+The replacement masks 8+8+9 basis rows per plane and nine per single query:
+
+```text
+32385*(8+8+9) + 765*9 = 816,510 basis-row restrictions.
+```
+
+This removes 32,737,410 restrictions in those queries. It introduces bounded
+binary elimination and builds four bases once. The calculation is not a total
+instruction count or an asymptotic multiplication bound. The verifier counts
+all 97,920 replacement queries and their masked basis rows during the complete
+replay. Timing measures the complete CLI, including unchanged work.
+
+## Bounded conformance
+
+The conformance checker enumerates all 67 subspaces of F_2^4 and all 16 masks,
+for 1,072 cases. Its independent oracle counts literal vectors in each kernel.
+Another 320 fixtures cover basis dimensions zero through nine and 112-bit
+strings, again enumerating every vector. Five direct boundary controls cover
+the zero space, zero restriction, injective restriction, dependent restricted
+images and bit 111. The unchanged complete scientific object and digest are
+also compared. Quantified correctness follows from rank-nullity, rather than
+extrapolation from these fixtures.
+
+## Limits
+
+The evaluator is opt-in and tied to the exact retained source bytes. Its
+orchestration duplicates the source's contract and fails the source hash if
+that contract changes. The kernel routine assumes an independent basis of
+at most nine rows. Source construction and explicit dimension checks enforce
+that premise. This is a finite evaluation improvement. It supplies no new
+decoder floor, physical COPY word, paid histogram, supplier admission, kappa
+or complete multiplication theorem.

research/p112-compatibility-kernels/README.md

@@ -0,0 +1,136 @@
+# Faster exact P112 plane compatibility
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+The complete PR1325 scientific replay takes a local median **0.326 seconds**
+with the restriction-kernel evaluator, versus **1.365 seconds** with the
+retained source command, a **76.09% reduction** across five alternating runs
+per side. All runs succeed with identical scientific stdout. This is a scoped
+implementation-preservation proof, finite conformance evidence and a local
+performance observation. No new kappa is claimed.
+
+Philipp / mightyOil's [PR1325](https://github.com/CrocSwap/integer-mult-bounds/pull/1325)
+supplies the census, equality theorem, witnesses and source implementation.
+Its mathematics is a cited premise. The new step restricts bit-string basis
+rows, preserving the complete 32,385-plane and
+765-vector domains, canonical digest, witnesses and six rejection controls.
+The predecessor package stays unchanged.
+
+For a binary space with independent basis g_i, the exact replacement is
+
+```text
+log2(number of vectors v with v & mask = 0)
+    = dimension(V) - binary_rank(g_i & mask).
+```
+
+[PROOF.md](PROOF.md) proves preservation of the complete scientific object.
+The query stage masks 816,510 basis rows instead of 33,553,920 space vectors.
+It also performs binary elimination and prepares four bases. This is not a
+claim that the whole command has only 816,510 operations.
+
+## Reproduce
+
+Run from the repository root with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p112-compatibility-kernels/fast.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p112-compatibility-kernels/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p112-compatibility-kernels
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p112-compatibility-kernels --check-source-history
+```
+
+A reviewer can substitute their CPython 3.12 executable. The fast CLI prints
+the same `PASS_SPARSE_REDUNDANT_DECODER` line as the source. The conformance
+checker prints `PASS_P112_COMPATIBILITY_KERNELS` in a generated JSON stdout
+receipt bound to all eight package files. It checks 1,072 exhaustive small
+subspace/mask cases, 320 wide cases, five boundaries, the complete scientific
+object and counted query work. Both registered commands include that complete
+replay, with and without `-O`; each has a 120-second limit.
+
+To reproduce the comparison, choose a fresh output path outside the checkout:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/p112-compatibility-kernels/benchmark.py --write /tmp/p112-kernel-benchmark.json
+```
+
+The harness runs each entire command five times in alternating order, with
+identical `-I -O -W error -B` flags. It checks exit status, exact stdout and
+empty stderr for every sample. Source hashes, interpreter startup, census,
+decoder checks, controls and certificate comparison all occur inside the
+timed subprocess. It refuses to overwrite its output.
+
+## Local timing evidence
+
+CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. The machine was shared;
+the observed load averages were 9.46, 7.27 and 4.49. Other research and Git
+processes were active. Alternation limits drift but does not establish a
+portable performance guarantee. All ten commands returned success, with zero
+stderr bytes and equal stdout hashes.
+
+| Command | Five wall times, seconds | Median | Range |
+|---|---|---|---|
+| Source | 1.433095, 1.656254, 1.364952, 1.351939, 1.306152 | 1.364952 | 1.306152 to 1.656254 |
+| Kernel | 0.317710, 0.338164, 0.326321, 0.331216, 0.293263 | 0.326321 | 0.293263 to 0.338164 |
+
+CPU times are close to wall times on both sides. A separate, untimed cProfile
+run attributes most source time to `run`, which contains the compatibility
+comprehensions; all-pairs identity checks are the next substantial component.
+The reduced scans explain the gain. The complete command still executes those
+identity checks, source preparation, canonical JSON and hashing. The timing
+comparison excludes the additional conformance verifier and does not claim
+to accelerate the predecessor's independent implementation or package tests.
+
+## Scope and credit
+
+Sources are pinned to canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. The card
+`census-pruning-audit` changes scope to exact census acceleration, as recorded
+in [TASK.json](TASK.json). The selected binding positive control passed.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361674)
+names this exact evaluation target.
+
+PR1325's independent implementation already uses coefficient-space equations
+and rank-nullity. This contribution claims the faster primary-receipt evaluator,
+not priority for kernel dimensions or another mathematical verification.
+The source retains Philipp / mightyOil's attribution and the PR845,
+coordinate-reader, nine-term representation and deficiency-plane lineage.
+Classical binary elimination and rank-nullity are used here. No predecessor
+proof is audited or independently certified. Actual native delivery, dirty
+restoration in a physical caller, complete recursive charges, stock, precision
+and supplier admission remain outside this result. No selected cold replay,
+Lean, Docker or independent human/formal-kernel review is claimed.
+
+## Open next questions
+
+Can the same kernel evaluator accelerate a different complete decoder census?
+First profile its full command and identify its exact subspace-restriction
+contract. Each source's ordering, receipt and rejection controls must survive;
+this package proves no automatic compatibility. This is the sole Open next
+questions item; research stops at the first verified improvement.
+
+## Verifier bounds and deviations
+
+The new code has no recursion. Kernel elimination uses at most nine passes
+per row. Plane loops have three anchors and at most 255 by 254 candidate
+pairs per anchor. Spaces have at most 512 vectors, masks have at most 112
+bits and scientific fixtures have 112 rows. Source reads in the adapter are
+bounded at one MiB per file before hash validation. The small-space generator has
+four rounds, at most 67 spaces and sixteen vectors; wide enumeration has ten
+dimensions, 32 masks and at most 512 vectors. Benchmarking has ten subprocesses,
+each with a 60-second timeout. All new functions are below 60 physical lines.
+Explicit exceptions remain active under optimized Python.
+
+Power of Ten rules 3, 8 and 9 require managed-runtime deviations. Python
+integers, JSON and containers allocate; fixed domains bound live collections.
+One module with the exact source path is compiled from authenticated bytes,
+and the verifier similarly loads the local evaluator. No generated expression
+or user-supplied module name is executed, and bytecode caches are not read.
+The retained source and six named control callbacks are the bounded indirect
+targets. Their results are checked or intentionally discarded only where the
+source also discards unused witness arrays. A future generic external-input
+interface would require explicit capacity validation and a separate review.
+
+Warning-strict normal and optimized execution and AST/function-size inspection
+are the available diagnostics. Inherited source style is preserved through
+the immutable adapter rather than changed in a frozen package. This is an
+opt-in evaluator, not a shared verifier or CI-selection change.

research/p112-compatibility-kernels/SOURCES.json

@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "research/sparse-redundant-decoder/verify.py",
+      "sha256": "7b0e3f5eb26f43c1ce4c3c5f72769f941dbc4c9698e97a58663d29501b117b56",
+      "git_blob": "c718ae77daab508ecc8a7091bac1f2af853c5142",
+      "usage": "input"
+    },
+    {
+      "path": "research/sparse-redundant-decoder/CERTIFICATE.json",
+      "sha256": "3d347dc6be878b1e05fb545319628744c62b43d0c3d237641fe68901bc9355e5",
+      "git_blob": "c5fc4d5b06f4c1fae8e94fc1acac65180d2c5995",
+      "usage": "input"
+    },
+    {
+      "path": "research/sparse-redundant-decoder/SOURCES.json",
+      "sha256": "3a82dc2a7a89e99b3ad16cf2f5005d809126d0d83b97f937b1896e1655e02b14",
+      "git_blob": "279f42f66921b2e151ab9bd5382c3826b10b234a",
+      "usage": "input"
+    },
+    {
+      "path": "research/sparse-redundant-decoder/README.md",
+      "sha256": "e0a201011aa1eb0d3df0c0bef1bc598ffa29287af832336321fec173fab36fa5",
+      "git_blob": "f029f0d617311d1d1c0c11bb4fe99ce511db3c9f",
+      "usage": "input"
+    },
+    {
+      "path": "research/sparse-redundant-decoder/PROOF.md",
+      "sha256": "7133bd2d095ddf06b0db6059e6234e8cd8fe7130c53922e5f22249b05600121c",
+      "git_blob": "99929e38b7d5f25a0b5459600c26dcdbd01d230a",
+      "usage": "input"
+    },
+    {
+      "path": "research/complex-decoder-field-extension-seed44/PROOF.md",
+      "sha256": "a89530576d8a5e1ae8778d601b37140d954212cd46e06b87a3f565294ee251a2",
+      "git_blob": "4a3063de8fe606a88bd5bdb9b7d2e5dccb70f73f",
+      "usage": "input"
+    },
+    {
+      "path": "research/complex-frame-pair-decoders/PROOF.md",
+      "sha256": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74",
+      "git_blob": "889f3a653ed1bdbb7df61ebe3af4f2103602a1f4",
+      "usage": "input"
+    },
+    {
+      "path": "research/p112-single-lift/PROOF.md",
+      "sha256": "02147aa2a93a449dcbd15886b42d993bd0dbb554d7c15d347a9567fbe2a442e1",
+      "git_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a",
+      "usage": "input"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "research/sparse-redundant-decoder/independent.py",
+      "usage": "provenance",
+      "git_blob": "79bdb105c9693751c93f20afd9272665d2f91389",
+      "sha256": "bfeb28b49e58add76fd1e562f2342cd273b3a4bd1a7f112b81a780219765eeb2"
+    }
+  ]
+}

research/p112-compatibility-kernels/TASK.json

@@ -0,0 +1,67 @@
+{
+  "schema_version": 1,
+  "task_id": "census-pruning-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "census-pruning-audit",
+    "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?",
+    "starting_points": [
+      "research/f7-weight-parity-census-correction/README.md",
+      "docs/research/research-family-status.md"
+    ],
+    "methods": [
+      "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.",
+      "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication."
+    ],
+    "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.",
+    "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": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.",
+    "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.",
+    "allowed_variations": [
+      "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit."
+    ],
+    "scope_change_triggers": [
+      "Launching a larger census before validating the prune and explaining which active decision it changes.",
+      "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound."
+    ],
+    "overlap_terms": [
+      "2973",
+      "2542",
+      "2634",
+      "2691",
+      "weight parity",
+      "bit-0",
+      "01021323",
+      "census pruning"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact restriction-kernel evaluation of the complete PR1325 P112 plane-compatibility census, preserving its scientific receipt.",
+  "scope_change_reason": "The donation requires original work rather than predecessor validation. This changes the audit card to an implementation-preservation proof and a new exact evaluation algorithm for the unchanged finite census.",
+  "bottleneck_link": "Makes exact decoder screening cheaper without weakening finite coverage; supplies no physical COPY word or better exponent.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified complete-command improvement; do not extend the algorithm.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; full certificate and ordered stream comparison; exhaustive small-subspace conformance; alternating complete CLI benchmark.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361674",
+  "open_questions": [
+    {
+      "question": "Can the same restriction-kernel evaluator accelerate an explicitly different decoder census?",
+      "why_it_matters": "Larger source spaces make literal partner-vector scans expensive.",
+      "first_step": "Profile one complete command and expose its precise binary subspace restriction.",
+      "blocked_by": "Each source has a separate output, ordering and control contract; no automatic applicability is proved."
+    }
+  ]
+}