Reduce complete E8 root-swap replay time by 13.95% (no new κ)

research/e8-root-swap-fast-inner/PROOF.md

@@ -0,0 +1,49 @@
+# Exact substitution and retained checks
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For the default scientific command pinned in SOURCES.json, replacing
+`verify.dot` and `extension_check.dot` by `replay.dot8` preserves the full
+result and every rejection predicate. This is implementation equivalence,
+not independent acceptance of the predecessor's mathematical conclusions.
+
+The two source dot functions receive eight-coordinate integer or rational
+vectors. In the primary these are roots, normals, simple vectors and rows of
+an eight-dimensional rational inverse. In the extension they are the same
+doubled coordinate vectors, inverse rows and explicit eight-coordinate
+fixtures. Frozen constructors and dimension checks fix this domain. Floating
+point and overloaded scalar protocols are excluded.
+
+Put s_0=0 and s_(j+1)=s_j+a_j*b_j for j=0,...,7. The original generator/sum
+computes s_8. The new expression has the same eight terms and left-associated
+additions, starting with zero. Exact integer/Fraction arithmetic proves equality
+by induction on j. The new length check succeeds on the admitted calls.
+Substituting an equal pure function preserves callers' values, branches and
+checks by induction over execution. No memoization, pruning, approximation or
+fixture-dependent answer is introduced. The Cartan and Gaussian algebra
+implementations are unchanged.
+
+The adapter authenticates all ten scientific inputs before compiling the four
+original source modules at their original file locations. Compilation bypasses
+adjacent bytecode caches. Import order is geometry, algebra, extension, primary.
+The original default main executes, including the original full RESULT.json
+comparison, and must return zero. Existing module objects, path and argument
+lists are restored on exit. Stable files during execution are assumed, as in
+the original source-hash check. Lean source bytes are authenticated because
+they occur in that receipt, but Lean is not executed.
+
+Checked mode compares old and new results at all 5,096,623 substituted calls
+in one complete execution. A separate 576-case set includes all 64 ordered
+basis pairs and both orientations of 256 signed rational fixtures. Six wrong
+lengths and one invalid mode reject. Ten physical source-byte mutations and
+one missing file reject before compilation. A wrong-dot integration control
+reaches the original root-norm failure and rejects the complete command.
+These are nineteen controls. Module sentinels check namespace restoration.
+Explicit exceptions retain checks under optimized Python.
+
+Performance is a local observation. Five alternating fresh-process pairs time
+the original default CLI and new default CLI, including startup and output
+capture. Every run must return zero, print the original success line and have
+empty stderr. Input authentication before and after timing checks stability.
+The generated report records every command, time and failure. It is not a
+portable runtime bound, mathematical theorem or CI performance threshold.

research/e8-root-swap-fast-inner/README.md

@@ -0,0 +1,120 @@
+# Faster complete E8 root-swap replay
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+The new exact eight-coordinate dot product reduces the complete retained
+[PR3166](https://github.com/CrocSwap/integer-mult-bounds/pull/3166) replay's
+local median wall time by **13.95%**, from **6.131 s to 5.275 s**. Five
+alternating fresh-process pairs execute the full scientific command on both
+sides. All ten runs succeed with identical stdout and no stderr. Every
+candidate run is faster than every baseline run in this sample.
+
+Claim type: scoped implementation-equivalence proof, exact finite conformance,
+and local performance evidence. The decoder mathematics and its certificates
+remain conorholds's contribution. No new kappa or scientific audit is claimed.
+
+`replay.py` authenticates ten scientific files, compiles the four original
+modules from their authenticated bytes, replaces only the primary and
+extension dot products, and calls the original main. The separate Cartan
+implementation, Gaussian algebra, geometry, rejection controls, source hashes
+and complete RESULT.json comparison remain active. Frozen files are unchanged.
+[PROOF.md](PROOF.md) gives the substitution argument and scope.
+
+## Measured complete consumer
+
+CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. Initial shared-host load
+averages were 2.27, 2.58, 1.99. No other replay from this contribution ran during
+timing; other contributors could use the machine. Both commands use
+`-I -W error -B`, including startup, imports, every check and output capture.
+
+| Pair | Original, seconds | Specialized, seconds |
+|---|---:|---:|
+| 1 | 6.333281 | 5.110564 |
+| 2 | 6.083976 | 5.607583 |
+| 3 | 6.376638 | 5.199241 |
+| 4 | 6.130820 | 5.275435 |
+| 5 | 6.124533 | 5.409365 |
+| Median | 6.130820 | 5.275435 |
+| Range | 6.083976 to 6.376638 | 5.110564 to 5.607583 |
+
+The percentage uses nanosecond medians 6,130,819,750 and 5,275,434,583.
+A separate baseline profile attributes 3.718 s of its 17.878 s instrumented
+run to the two replaced dot functions. The measured saving is below that
+20.8% share. Generator/sum overhead is the changed cost; the other checks
+limit the saving. Profile seconds are not estimates of uninstrumented time.
+This local result implies no runtime bound on another host or input.
+
+`benchmark.py` generates stdout evidence containing every command, elapsed
+nanosecond count, return code, stdout digest and failure count. The table
+transcribes that report. No timing receipt is hand-written. CI runs
+conformance, not a performance threshold.
+
+## Reproduce
+
+From the repository root with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e8-root-swap-fast-inner/replay.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e8-root-swap-fast-inner/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/e8-root-swap-fast-inner/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e8-root-swap-fast-inner/benchmark.py --pairs 5
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e8-root-swap-fast-inner
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e8-root-swap-fast-inner --check-source-history
+```
+
+Another CPython 3.12 executable may replace the absolute path. Set `TMPDIR`
+to a private external directory for temporary custody controls. The fast
+command prints the unchanged source success line. The new verifier emits a
+generated JSON receipt with `PASS_E8_ROOT_SWAP_FAST_INNER`, 5,096,623 exact
+old/new dot comparisons, 576 scalar fixtures, nineteen controls and hashes of
+all eight package files. Source mathematical check counts are inherited
+coverage. Each registered normal/optimized command has a 120-second limit.
+Benchmarking is optional and excluded from CI.
+
+## Sources and limits
+
+Canonical base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priorities revision 8.
+The selected record resolves to PR6030, kappa .003125804. The card's first
+binding control passed with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; this is
+orientation only. TASK.json refines replay-runtime to this complete command.
+SOURCES.json pins ten live scientific inputs and historical provenance.
+
+Credit conorholds / PR3166 for the original replay, proofs, checks and
+certificates, and DreamingOfClouds / PR2816, PR2826, PR2862 and PR3154 with
+their retained E8 lineage. Their files and notices are unchanged. Fixed-product
+unrolling is standard. This contribution supplies its source-bound adaptation,
+preservation argument and measured complete consumer. Nick Petalas / PR6164
+optimized publication-byte preflight using this package as a fixture; it did
+not accelerate this scientific command.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370259)
+states this scope. Main, merged and live PRs, recent account work, handoffs and
+local reservations were checked. The overlap cache covered 506 open PRs and
+6,501 Discussion records; sparse local-note coverage was incomplete. Arbitrary
+historical diffs, unpublished work and literature priority remain outside coverage.
+
+Equivalence covers the pinned default command and exact integer/rational
+eight-coordinate arguments. Arbitrary overloaded scalar types, receipt-emission
+CLI options, arbitrary module-cache states and future source changes are
+excluded. Lean source bytes are authenticated; Lean is not run. No native or
+physical caller, precision, tape, stock, compiler, outer or selected cold replay,
+new supplier or complete multiplication theorem is supplied. All five selected
+framework assumptions and the selected frontier remain unchanged.
+
+New functions stay below sixty lines and have bounded fixture/module/input
+loops and no recursion. Managed allocation is a Power of Ten rule 3 deviation
+for this fixed workload and ten inputs capped at 1 MiB each. Authenticated
+compilation of four unchanged modules is a rule 8 deviation; it generates no
+new source. The two substitutions, comparison closure and source main are
+fixed rule 9 dispatch targets. Frozen predecessor loop/function constraints
+are retained. Warning-strict normal/optimized replay supplies the available
+diagnostics; no separate static analyzer or real-time guarantee is claimed.
+
+## Open next questions
+
+1. Integrate into one maintained replay entry while retaining the checkers'
+   intended arithmetic independence. First identify the active consumer and
+   measure its full command. This adapter targets a historical fixture.
+2. Profile that consumer's remaining bottleneck before another optimization.
+   The first verified improvement ends this contribution; no follow-up is reserved.

research/e8-root-swap-fast-inner/SOURCES.json

@@ -0,0 +1,78 @@
+{
+  "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/e8-d0-root-swaps/EXTENSION.md",
+      "usage": "input",
+      "git_blob": "99dc1c21b72e90e7669386d77506334900992286",
+      "sha256": "47f86fca33843bb2bc2b5ddbc07b91d846fe04952b8c133ff02dcbb9637b6357"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/PROOF.md",
+      "usage": "input",
+      "git_blob": "79051f9f431863259dd7d714e096ce9e865b151b",
+      "sha256": "531b1dcb0de5f652fa2ca8dca97174c4973face53c877bd919cf584afa632953"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/RESULT.json",
+      "usage": "input",
+      "git_blob": "e1a89572dc2e18b745655a562bbb8e9bece54a93",
+      "sha256": "d894b32076290b688d9838e9889989d837bacd378ba6b9654d25658a44661403"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/algebra_check.py",
+      "usage": "input",
+      "git_blob": "b108bbd226f895f4291002ec06613ed4b3e7faa4",
+      "sha256": "45dad6b59a4fad6d2ccf6c6d7f726e5f9813f03e9ff1f33e84107797ca7bc040"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/extension_check.py",
+      "usage": "input",
+      "git_blob": "659edb7f09a73ab417997e43344306d2882f71fc",
+      "sha256": "a246c10ab650b46c13ec86ddc814306338ac84c65a93e2c6cda45c2fcf8c5b70"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/formal/RootSwapConnectedCover.lean",
+      "usage": "input",
+      "git_blob": "4351c589eca198ff65af72a671dc6268dde89fd2",
+      "sha256": "9205ffe7c3ee68e7ade608631378ebb9e8d8f3e28d6c873de9cbdd7b1becf9b2"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/formal/RootSwapOneExceptional.lean",
+      "usage": "input",
+      "git_blob": "2041473a4640aa1adf17284bf73eb99b6bfcddbc",
+      "sha256": "7c506e82ccef28ec502eb7bcf214450c23b9decbd38c94d9b5b1fe66b81834a9"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/formal/RootSwapQuartet.lean",
+      "usage": "input",
+      "git_blob": "d7aecfd2f356956dadd136ac0f53a7b80643e529",
+      "sha256": "43edf0c90eba5ba805b691cd0b36b8b1e8abc5f80519a5ee1e5cc163bfd8a3e6"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/geometry_audit.py",
+      "usage": "input",
+      "git_blob": "3084be53d349da489e947d1e5a1c689eeb5148bc",
+      "sha256": "dc6c51d1a9376498d35dd35f8f24eb33c2c461656b249a76bf6c41ec3cac91ad"
+    },
+    {
+      "path": "research/e8-d0-root-swaps/verify.py",
+      "usage": "input",
+      "git_blob": "7be154af0f4fba335addd9acd6404c82b44142d9",
+      "sha256": "ff2e84dd385490434435b871216044700bc949d00c7ea351fe91af5b07bb0217"
+    }
+  ]
+}

research/e8-root-swap-fast-inner/TASK.json

@@ -0,0 +1,67 @@
+{
+  "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": "Source-bound exact dot-product specialization reducing complete default PR3166 scientific replay runtime with all original checks retained.",
+  "scope_change_reason": "Narrow the runtime card to one pinned complete command; predecessor theorems are not audited or claimed anew.",
+  "bottleneck_link": "Reduce exact arithmetic overhead in a complete research replay without dropping checks; this historical component does not alter the selected supplier invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified complete replay speedup; one candidate is retained.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives exact substitution. verify.py compares 5096623 actual dots, 576 scalar fixtures and nineteen controls. README.md records five alternating pairs, zero failures and 13.9522152319 percent less median wall time.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the specialization be integrated into one maintained replay entry while preserving intended arithmetic independence?",
+      "why_it_matters": "The adapter accelerates a historical fixture rather than current supplier cold replay.",
+      "first_step": "Identify one active consumer, preserve all comparisons and controls, and measure its full command.",
+      "blocked_by": "No maintained consumer integration is supplied."
+    },
+    {
+      "question": "Which remaining bottleneck matters in that consumer?",
+      "why_it_matters": "Unmodified work limits further speedup.",
+      "first_step": "Profile that complete consumer after integration.",
+      "blocked_by": "The first improvement ends this contribution; no further optimization is reserved."
+    }
+  ]
+}

research/e8-root-swap-fast-inner/VERIFY.json

@@ -0,0 +1,45 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e8-d0-root-swaps/EXTENSION.md",
+    "research/e8-d0-root-swaps/PROOF.md",
+    "research/e8-d0-root-swaps/RESULT.json",
+    "research/e8-d0-root-swaps/algebra_check.py",
+    "research/e8-d0-root-swaps/extension_check.py",
+    "research/e8-d0-root-swaps/formal/RootSwapConnectedCover.lean",
+    "research/e8-d0-root-swaps/formal/RootSwapOneExceptional.lean",
+    "research/e8-d0-root-swaps/formal/RootSwapQuartet.lean",
+    "research/e8-d0-root-swaps/geometry_audit.py",
+    "research/e8-d0-root-swaps/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All 5096623 actual specialized/original dots, complete original scientific command and receipt, 576 scalar fixtures, nineteen custody/domain/integration controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same complete conformance and rejection coverage with optimized Python."
+    }
+  ]
+}