Reduce complete extension-field tensor replay time by 16.56% (no κ)

research/extension-field-row-kernel/PROOF.md

@@ -0,0 +1,107 @@
+# Exact row-output preservation
+
+This scoped implementation proof was produced by Nick Petalas. Apache-2.0.
+It treats Ali Romman's PR5637 recognizer and complete caller as credited
+inputs. It does not reprove the tensor classification.
+
+## Contract
+
+Let `f` be an unmodified field constructed by the pinned `Field` class,
+with order at most 25. Let `a` be a rectangular matrix of canonical field
+elements, with at most 729 rows and at most 162 columns. The pivot width
+is between zero and its row length. Empty matrices are allowed. The new
+public `RowKernel.rref` validates this contract and returns exactly the
+same full rows and ordered pivot columns as the pinned `rref`, including
+every augmented column. It does not mutate or alias an input row.
+
+These capacities contain the complete caller. Its seven fields have
+orders 2, 3, 4, 8, 9, 16 and 25. Its positive fixtures have dimension at
+most nine. The largest nucleus system therefore has at most `9^3 = 729`
+rows and `2*9^2 = 162` columns. Its inverse and coordinate systems fit
+these capacities. The complete F2/F4 domain has dimension two. The source
+validation rejects malformed tensors before elimination, and its internal
+field operations preserve canonical coefficients and rectangular shapes.
+The private adapter calls `reduce` on these trusted internal matrices,
+retaining explicit row/column capacity checks rather than repeating their
+coefficient validation on every internal call.
+
+## Stepwise identity
+
+Preparation constructs the immutable table
+
+```
+updates[c][x][y] = f.add[x][f.mul[c][y]].
+```
+
+This is the original elimination expression for `x + c*y`. The table is
+computed separately for each new field object. It is never keyed only by
+field order, so different irreducible-polynomial presentations cannot share
+an arithmetic cache accidentally. The copied multiplication, inverse and
+negation tables likewise belong to that object.
+
+Induct on the pivot-column loop. Initially both algorithms copy every
+input row and have the same pivot list and next pivot-row index. If the
+current rows agree, scanning from the same index chooses the same first
+nonzero pivot or skips the same column. Both swap the same rows. The new
+normalization binds `mul[inv[pivot]]` once and indexes it for each entry;
+the source indexes that same row repeatedly. Thus their normalized full
+rows agree, including columns outside the pivot width.
+
+For each other nonzero row, both choose `c = -row[j]`. The new full-row
+comprehension looks up `updates[c][x][y]`; the source evaluates its defining
+expression. Hence every resulting entry agrees. The pivot list, next-row
+index and termination condition agree. This proves exact returned rows
+and pivot order, not only equality of row spaces. The copied rows also
+prove input preservation and absence of input/output row aliases.
+
+All other recognizer functions are unchanged. They resolve `rref` in their
+own private loaded module. The adapter changes only that binding and the
+field constructor that prepares its arithmetic. Consequently every later
+branch, certificate, rejection reason and independent checker expression
+has the same value on the declared domain. The unchanged verifier itself
+still constructs and visits every tensor and orbit element.
+
+## Costs and limits
+
+The table holds `q^3 <= 15625` field-element references. Preparation costs
+O(q^3) lookups, paid inside each complete timed process. The row algorithm
+keeps the source's O(rows*columns*min(rows,width)) field-update bound.
+The improvement is a constant-factor Python implementation change, with
+no asymptotic improvement claimed. Replacing repeated attribute accesses
+and nested arithmetic lookups by prepared table accesses is classical.
+
+The adapter is scoped to this bounded caller. It is not a replacement for
+the source API at arbitrary field order or dimension. Mutating a field's
+arithmetic tables after preparation is outside the contract. There is no
+new field-recognition theorem, supplier, kappa or selected-frontier change.
+
+## Code constraints
+
+The new functions are shorter than 60 lines. There is no recursion. All
+kernel loops have capacities derived above. The benchmark has five to ten
+pairs and a 150-second timeout per child, checks every child status and
+stderr, and consumes its complete report before accepting a timing.
+
+Rule 3, managed allocation. Python requires object and list allocation
+during each elimination and process run. This deviation is confined to
+the new bounded engine and replay harness. The engine permits at most
+729 by 162 coefficients per matrix and 25 cubed fused entries per field.
+It holds copied input/output rows and no history of previous matrices.
+The source caller constructs a fixed finite field/fixture set. The
+benchmark retains at most twenty small result reports and at most one
+child process at a time. Capacity, invalid-input and complete-caller
+checks exercise these bounds. A fixed-storage native implementation
+would be a separate follow-up, not an asserted Python guarantee.
+
+Rule 9, runtime dispatch. The private module adapter selects between the
+pinned and prepared elimination implementations. Both targets are explicit
+and have a fresh-process lifetime. Source authentication precedes import;
+no global installed module or predecessor file is changed. Both complete
+paths and the arithmetic-mutation rejection are exercised.
+
+Rule 10, interpreted diagnostics. Registered checks use isolated,
+warning-strict development mode with normal and optimized Python. Every
+verification condition uses an explicit exception. No additional static
+analyzer was found on PATH in the supplied environment. Syntax compilation and
+AST inspection cover every new Python file; no assertion is needed for
+the contracts to remain active under `-O`.

research/extension-field-row-kernel/README.md

@@ -0,0 +1,143 @@
+# Faster complete extension-field tensor replay
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+A prepared finite-field row-update table reduces
+the runtime of Ali Romman's complete PR5637 caller. The new contribution is
+the bounded arithmetic implementation, exact-output preservation proof and
+complete-caller performance experiment. The predecessor's classification,
+transporter construction and scientific decisions are credited premises.
+
+```
+original rref:  x -> add[x][mul[c][y]] at every row entry
+prepared rref:  x -> updates[c][x][y], prepared once per field
+```
+
+The private adapter prepares each field and replaces only its module's row
+elimination. Every tensor, orbit traversal, witness equation and control
+remains in the unchanged source caller. [PROOF.md](PROOF.md) proves equality
+of every full output row and ordered pivot column, including augmented
+columns. This is stronger than preserving rank alone. No new kappa,
+classification, supplier admission or selected-frontier change is claimed.
+
+## Evidence
+
+Five alternating fresh-process pairs reduce median complete wall time from
+13.202941292 to 11.016213791 seconds, a 16.56% reduction.
+The original range is 12.879240000 to 14.055809667 seconds;
+the prepared range is 10.861282875 to 11.409663292 seconds.
+All ten processes succeed with zero errors and the same deterministic output
+SHA256 `bd7250bb19b92c00baa028d417fed1890aeb0f4865acd8c9f4a782583325f70a`.
+CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. These are local
+measurements, including contention from other work.
+
+| Pair | Original seconds | Prepared seconds |
+|---|---:|---:|
+| 1 | 13.202941292 | 10.861282875 |
+| 2 | 12.879240000 | 10.997038458 |
+| 3 | 12.914124041 | 11.016213791 |
+| 4 | 14.055809667 | 11.148343375 |
+| 5 | 13.253169500 | 11.409663292 |
+
+The standalone verifier passes 19,753 complete row-result comparisons,
+21,061 fused arithmetic entries and 65 capacity, malformed-input and
+arithmetic-mutation controls. It also runs both complete source callers and
+compares their deterministic reports. Both retain all 256 F2 and 65,536 F4
+tensors, 90 larger changed-basis presentations, 90 special-linear
+transporters, 2,322 transported basis products and 125 source controls.
+
+The timing experiment uses five alternating fresh-process pairs, with all
+field preparation, authentication, imports, orbit construction and complete
+recognition/checking inside the timed interval. No performance threshold is
+asserted in CI. The process report includes every sample, errors, platform,
+load averages and file hashes. Generated reports and logs are written outside
+the checkout. The nondeterministic elapsed-time line alone is excluded from
+the complete output comparison.
+
+The separate instrumented profile identifies `rref` as the main cost,
+9.655 seconds of an 18.299-second instrumented complete caller. Profiler
+timings are not used as the before/after measurement. This is a CPU-bound
+Python constant-factor improvement; it changes neither the number of tensor
+cases nor the asymptotic elimination cost. Other work may share the machine.
+
+## Reproduce
+
+From the repository root, CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/extension-field-row-kernel/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -X dev -B research/extension-field-row-kernel/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/extension-field-row-kernel
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/extension-field-row-kernel --check-source-history
+```
+
+Expected markers are `PASS_EXTENSION_FIELD_ROW_KERNEL`,
+`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`.
+The package commands emit hash-bound receipts to stdout and write no result
+files into the checkout. Another CPython 3.12 path may replace the displayed
+interpreter. The benchmark is opt-in and prints its generated JSON report:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/extension-field-row-kernel/benchmark.py --pairs 5
+```
+
+`replay.py original` and `replay.py prepared` run a single complete source
+caller. Every live source is authenticated before import. The declared
+inputs retain their original repository-relative paths in an official
+package export; no Git or network is needed for a direct exported replay.
+
+## Scope and limits
+
+Canonical base is `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority
+revision 8. The `replay-runtime` card is refined to this exact caller and
+kernel. [TASK.json](TASK.json) records the bounded question and stopping
+rule; [SOURCES.json](SOURCES.json) pins the exact scientific source bytes.
+The selected record and catalogue are provenance-only inputs.
+
+The engine supports canonical field tables of order at most 25, at most
+729 rows and at most 162 columns. These include every call in the retained
+complete caller. Larger fields/dimensions and mutation of field arithmetic
+after preparation are outside its contract. The source's broader API is
+unchanged. A new field owns its own tables, with at most 15,625 fused
+entries; no cross-presentation or cross-process cache is reused.
+
+The written proof covers implementation equivalence on this bounded
+contract; finite comparisons corroborate it. Local timing is host-specific.
+Independent human and formal proof-kernel review are unclaimed. No native
+producer/consumer, complete paid invoice, selected cold replay, Lean or
+Docker execution is supplied. All five selected framework assumptions remain.
+
+## Open next questions
+
+Can this engine enter a source-owned recognition API with explicit field
+and augmented-row capacities? First specify that public contract and retain
+full row and pivot-order equality. The current package deliberately uses a
+private adapter and keeps the predecessor bytes frozen. This question and
+its blocker are also recorded in [TASK.json](TASK.json). No further
+optimization is reserved by this result.
+
+## Related open work
+
+The live open-PR check found no other PR targeting this extension-field
+recognition caller or its row-elimination runtime. Other numerical and
+rank-verifier improvements concern different source callers. Later
+split-product and nonsplit recognition packages #5661/#5664 and the
+character/transport packages #5656/#5663/#5668 are merged mathematical
+extensions; this package makes no automatic transfer of its bounded adapter
+or measurement to them. No extra computations compare their results.
+
+## Credit
+
+Ali Romman, PR5637 at `86389e525d3efafe236e929f6ae401c68be1d115`, supplies
+the finite-field arithmetic, complete caller, recognition and special-linear
+transport, building on PR5540/5525 and Nick Petalas's PR5252 nucleus lineage.
+apoursh's PR5502 supplies the height criterion; Ali Romman's PR5459 supplies
+the character formula. David Ganz and all retained tensor/atlas predecessors
+keep their credit. Finite-field elimination and table-driven arithmetic are
+classical. Only the new implementation, equivalence argument and experiment
+are claimed here, without a general literature-priority claim.
+
+The advance [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19299672)
+records the scope. Live Discussion and open-PR searches, merged object/formula
+searches and all tracked main package notes were checked. Unpublished work
+and arbitrary historical diffs remain coverage limits; absent matches do not
+prove novelty.

research/extension-field-row-kernel/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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/extension-field-tensor-recognition/SOURCES.json",
+      "usage": "input",
+      "git_blob": "c7f94ddda8952e3a00e2ab41e95bd0a9b99d40c1",
+      "sha256": "604ec385e20651bd8c6e8df60ba7edf818c1bfc32ff7e487e5c8a8c60c9c1454"
+    },
+    {
+      "path": "research/extension-field-tensor-recognition/recognize.py",
+      "usage": "input",
+      "git_blob": "1066bb74c19d180bfef7d9dd1c0650ec6bbd7780",
+      "sha256": "6daa160346d04691c6ca3c9c820b3df8982de4320ec01e5db10e3cb932f42c00"
+    },
+    {
+      "path": "research/extension-field-tensor-recognition/verify.py",
+      "usage": "input",
+      "git_blob": "a8f8d85d71636ed8809e4a67f5c49bc30d106335",
+      "sha256": "52d5b7b954d64e3342043f3200a67286a9c156d908d5fa4d78c992a6c18cd71d"
+    },
+    {
+      "path": "research/frobenius-algebra-recognition/PROOF.md",
+      "usage": "input",
+      "git_blob": "0a0b7d1fe48576be453df5aa5de0cc66463352fa",
+      "sha256": "726d9c294f0b4b9085e3994ffb8c93737822b78d6f5d0c63f81e36b718419e28"
+    },
+    {
+      "path": "research/frobenius-tensor-characters/README.md",
+      "usage": "input",
+      "git_blob": "b62f9a906e6ed49605684cca52a221f064924461",
+      "sha256": "31573ba91ac69caff5b8e5a42ce7fd0d80a6d54673c08d7f225c9ee08e0e0893"
+    },
+    {
+      "path": "research/nonreduced-tensor-recognition/README.md",
+      "usage": "input",
+      "git_blob": "826c6b010725d98b6ca6599a748c4179264140e9",
+      "sha256": "2eaed94a9f12ad7b6bb7253b14bff95b86549b3e320f0e91fa4e35c0025536de"
+    }
+  ]
+}

research/extension-field-row-kernel/TASK.json

@@ -0,0 +1,61 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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": "Exact bounded table-driven row elimination in the complete PR5637 extension-field tensor-recognition caller, preserving all decisions, literal certificates and controls.",
+  "scope_change_reason": "The replay-runtime card is refined to one original arithmetic-kernel implementation on a named foreign complete caller. This is not a scientific audit or a new classification.",
+  "bottleneck_link": "Verification tooling side result: reduce complete exact replay cost without changing its tensor domain or any supplier/selected-frontier claim.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified complete-caller runtime improvement after exact row-output checks and five alternating fresh-process pairs; otherwise release a concrete failed-method handoff.",
+  "outcome": "completed",
+  "evidence": "Written stepwise implementation-equivalence proof; complete F2/F4 caller report equality, exhaustive small row comparisons and boundary/rejection controls; local benchmark generated outside the checkout.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the bounded row engine be admitted directly into a source-owned recognition API without a private module adapter?",
+      "why_it_matters": "A source-owned entry point would avoid wrapper setup and make field/shape capacities explicit for consumers.",
+      "first_step": "Define the public field and augmented-row contract and preserve exact full rows and pivot order.",
+      "blocked_by": "This contribution intentionally keeps the predecessor bytes frozen and supplies no upstream API change."
+    }
+  ]
+}