Reduce P104 chart-127 suffix by 119 events and 2,510 scalar units (no new κ)

research/p104-chart127-suffix/PROOF.md

@@ -0,0 +1,104 @@
+# Exact circuit and substitution proof
+
+Produced by Nick Petalas. Apache-2.0.
+
+## 1. Declared local map
+
+Let W be the decompressed source word pinned in SOURCES.json and let
+`B = W.program[17461:20431]`. All 2,970 events of B are ADD or SCALE at
+chart 127. Let R be the sorted union of all its source and destination
+roles. There are 545 roles. At entry, assign an independent formal value
+to every role in R, regardless of any additional relations that the full
+word might happen to impose. All other roles are left alone.
+
+An ADD `r <- r + q s` is an elementary matrix with inverse obtained by
+negating q. A SCALE `r <- q r` is invertible over Z[1/2] exactly when
+q is a signed power of two; its inverse uses 1/q. The replacement obeys
+these conditions. This proves invertibility of each operation without
+assuming any initial helper is zero.
+
+## 2. Construction and finite equality
+
+The constructor starts with the exact matrix M of B. It greedily subtracts
+one current row from another at a dyadic coefficient when this removes at
+least two nonzero entries. There are 245 such steps in this instance.
+It then chooses sparse dyadic-unit pivots, normalizes each pivot, and
+eliminates its column from every other row. Pivots outside Z[1/2]'s units
+are rejected. The resulting permutation matrix is returned to the literal
+identity by 218 exchanges. Each exchange is the charged four-operation word
+
+```text
+r += s; s -= r; r += s; s = -s.
+```
+
+No external zero cell or free role permutation is used. All operations are
+on the original role set. If the chronological elimination matrices are
+E_1,...,E_k, the checked invariant at completion is
+
+`E_k ... E_1 M = I`.
+
+Hence `M = E_1^-1 ... E_k^-1`. The emitted chronological replacement is
+`E_k^-1,...,E_1^-1`. Its 2,851 operations are authenticated by the fixed
+canonical JSON digest in verify.py.
+
+The mathematical claim is finite and has a separate direct check. The
+verifier initializes a dense integer identity matrix, retaining one binary
+denominator exponent per row. For an ADD it aligns the two denominator
+exponents, performs the integer row addition, and cancels common powers of
+two; SCALE is analogous. This engine does not call the sparse row routines.
+It computes every coefficient of the original and emitted matrices and
+requires equality of their canonical normalized integer representations.
+All 297,025 coefficients agree. Role 758 is explicitly retained even though
+it appears in no emitted operation. Thus the equality includes its identity
+row and column, rather than silently shrinking the interface.
+
+Equality over the rational dyadic coefficients proves equality on every
+module over Z[1/2], in particular arbitrary real or complex payload arrays.
+The finite integer certificate proves this named matrix identity; it does
+not prove a universal synthesis algorithm or an optimality bound.
+
+## 3. Legal substitution in the full word
+
+Replace B in W by the emitted circuit B'. All preceding and subsequent
+events remain identical. The source-authenticated complete-word interpreter
+checks that every new source/destination is available at chart 127 and
+that all chronological transports, owned lifetimes, COPY preconditions
+and final frames hold. The new interval contains no MOVE, INIT, CLEAR or
+COPY. All original non-scalar events retain their order and literal values.
+
+Because B and B' agree on arbitrary entry values of all touched roles,
+they agree on the actual state reached by any prefix of W. They also agree
+on the unchanged roles. Applying the identical continuation therefore
+preserves every whole-word endpoint. The explicit ADD at ordinal 20431
+is not crossed: it remains the first event after the replacement and
+uses chart 245. The full replay confirms every one of 799 squared endpoint
+coefficients and the original storage inventory.
+
+Recursive paid calls are determined by the unchanged MOVE events. Productive
+helper ranks use the unchanged public entry/exit frames and main-role set.
+Their histograms therefore remain identical. This is why the local scalar
+gain supplies no new exponent saving.
+
+## 4. Complete scalar charge
+
+Use the tariff in the pinned complete-word checker. For q=n/d in reduced
+form, with n positive after taking the absolute value, an ADD costs
+
+`2 (3 + bitlength(n)-1 + popcount(n) + bitlength(d)-1)`.
+
+A signed power-of-two SCALE costs
+
+`2 (abs(bitlength(n)-bitlength(d)) + [q<0])`.
+
+There are no uncharged exchanges, scales or access changes inside this
+abstract scalar tariff. Summing over the entire original interval gives
+25,988; summing over the emitted interval gives 23,478. The improvement is
+2,510, and event count improves by 119. All other events are unchanged,
+so the full-word allowance is 189,428 - 2,510 = 186,918 and the event count
+is 22,803 - 119 = 22,684. The new complete-word interpreter independently
+recounts that allowance from the emitted word.
+
+The dense engine also tracks the l1 norm of every intermediate local row.
+Both maxima equal 67. This supports a local absolute-magnitude comparison
+from identical entry values. It establishes no rounded error accumulation,
+physical memory traffic, native runtime or supplier integration theorem.

research/p104-chart127-suffix/README.md

@@ -0,0 +1,150 @@
+# A smaller exact chart-127 scalar suffix
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: a finite exact circuit certificate with a scoped substitution
+proof. On the selected PR6030 word, replace the chart-127 scalar interval
+`[17461,20431)` as follows:
+
+```text
+events                    2970 -> 2851       saving 119
+real scalar allowance    25988 -> 23478      saving 2510
+complete-word events     22803 -> 22684
+complete-word allowance 189428 -> 186918
+```
+
+All permutations, signs and power-of-two scales are charged. There are
+2,402 ADDs and 449 SCALEs in the replacement, versus 2,691 and 279 before.
+No additional roles are used. The ordered MOVE, INIT, CLEAR and COPY events,
+productive targets and recursive paid profile are unchanged. No new kappa
+or selected-frontier change is claimed.
+
+This answers the second-disjoint-block question in CubeJerry's
+[PR #6116](https://github.com/CrocSwap/integer-mult-bounds/pull/6116),
+head `815dd9844f1b43a4488ad06d09141a827621078c`.
+That contribution treats the separate first 9,895-event prefix. Its
+construction and checks are cited, not imported or replayed here.
+The new suffix circuit applies its whole-block synthesis approach to
+a different exact matrix. No combined word containing both improvements
+is claimed or tested.
+
+## Exact boundary and evidence
+
+Ordinals are zero-based and the upper endpoint is excluded. The retained
+event at 20431 is `ADD 533,453,2` at chart 245. It is an observation boundary,
+and the replacement stops before it. Every replacement operand is an
+already available role at chart 127. It uses only invertible dyadic
+ADD/SCALE operations and preserves the entire arbitrary-entry linear map.
+[PROOF.md](PROOF.md) explains the substitution and exact pricing.
+
+The constructor uses sparse Fraction rows. A separate integer-row engine
+compares all **297,025 coefficients** of the 545-by-545 matrices. One role,
+758, is touched by the original circuit and is identity in the final map;
+the replacement leaves it untouched. Both matrices include that role.
+The maximum intermediate row l1 norm relative to the local entry values
+is exactly 67 for both circuits. This is a local exact bound, not a
+rounded whole-word precision theorem.
+
+Ali Romman's source-authenticated complete-word interpreter then checks
+the new 22,684-event word, all 638,401 endpoint coefficients, chronological
+charts and storage. It reports 770 public inputs, 29 owned fields,
+31 owned lifetimes and peak 13 owned fields. The unchanged paid profile is
+`{1:2219,2:457,3:496,4:100,5:163,6:11,7:6,8:1}`, with rank mass 5,952.
+The target histogram is included in the generated receipt.
+
+Eleven negative controls reject a sign fault, missing scale, wrong chart,
+unavailable or aliased source, zero/non-dyadic/nonunit coefficients and
+corrupted scientific inputs. A two-role hand-computed dyadic matrix and
+the exact inverse block are positive controls. The synthesis stopped at
+its first candidate that improved both event count and charged allowance.
+No alternative pivot orders or further blocks were searched.
+
+## Reproduction
+
+From the repository root, with the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-chart127-suffix/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/p104-chart127-suffix/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-chart127-suffix
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-chart127-suffix --check-source-history
+```
+
+An equivalent CPython 3.12 path can replace the local path. Direct success
+prints `PASS_P104_CHART127_SUFFIX events=2970->2851 allowance=25988->23478`.
+Both registered commands have 180-second timeouts and use explicit checks
+that remain enabled under optimization.
+
+The direct command accepts `--receipt /absolute/external/path/result.json`
+for a generated receipt bound to all package and input file hashes, and
+`--emit-word /absolute/external/path/WORD.json` for the complete candidate.
+Both outputs must be absent and outside the checkout. Default replay writes
+nothing. No generated log, candidate word or receipt is kept in the package.
+The direct verifier also runs in a Git-free export with both declared inputs.
+
+Canonical compact sorted-key JSON hashes, excluding a trailing newline:
+
+```text
+replacement: ed9afcb5d55fe74f4306d8bc8928f59f0ee8201882597672013c90f4cb11c896
+whole word:  3dac0f56a818f426d609b0bcbdf412777fb46a4bbd49a9dde0b23fe7fe978d96
+```
+
+## Scope and implementation limits
+
+This is a local exact substitute and complete scalar-word check. The native
+operators and caller are unchanged premises. Full native, physical-caller,
+compiler, rounded precision, stock, tape and outer cold replays were not run.
+No optimality, measured runtime gain, complete supplier admission or complete
+multiplication theorem follows. All five selected framework assumptions remain.
+Independent human and formal proof-kernel review are unclaimed.
+
+The constructor uses at most 799 rows, 26,000 scalar events and 2,000 sharing
+steps; the actual domain has 545 rows and 245 sharing steps. Each step removes
+at least two sparse entries. Elimination has one pivot per role, and the
+permutation phase has at most one charged exchange per role. Every emitted
+coefficient is checked against a 16-bit numerator/denominator capacity.
+There is no recursive call, solver or network access. Python allocation is
+a managed-runtime deviation from fixed allocation; live matrix sizes are
+bounded by these capacities. Each function is below 60 physical lines.
+The only dynamic source execution is the pinned, explicitly selected
+complete-word interpreter. Normal and optimized warning-strict execution
+supply language diagnostics; no separate static analyzer is installed on PATH.
+
+## Open next questions
+
+- Can the two disjoint replacements here and in PR #6116 pass one complete
+  supplier, native, caller and precision replay? Start with the emitted
+  words and source-bound interval substitution. Pending independent review
+  and the complete integration replay remain blockers.
+- Can a changed helper or paid trajectory use the smaller scalar allowance
+  without spending it in restoration or target debits? First specify a
+  complete arbitrary-dirty boundary and price its full signed invoice.
+  This circuit by itself changes no recursive saving.
+
+## Credit and provenance
+
+The new circuit, standalone constructor and certificate were produced by
+Nick Petalas. CubeJerry supplies PR #6116's whole-block row-synthesis approach
+and second-block question. Sparse sharing, dyadic Gaussian elimination and
+elementary exchanges are classical, and no priority is claimed for them.
+DreamingOfClouds supplies PR #6030 and #5907, Ali Romman supplies the retained
+word/checker lineage, Matarener supplies PR #5975's global scalar-resynthesis
+question, and Mason Hale supplies PR #5811. Cinna Davis, Gareth Davidson,
+David Arias, Douglas Colkitt and all retained P104/native/compiler contributors
+keep their predecessor credit. No predecessor file or credit line is changed.
+
+The scientific base is canonical main
+`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8, with selected
+conditional kappa `781451/250000000`. Source-binding orientation passed.
+[SOURCES.json](SOURCES.json) pins the word and reused checker. The pending
+PR #6116 is scholarly context, not a live-code or Git-history dependency.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19242050)
+initially named the larger suffix `[17461,22795)` as one chart-127 block.
+The [scope update](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19242077)
+records its intervening chart-245 event and the narrower delivered interval.
+The larger interval was not synthesized. TASK.json explicitly changes the
+scalar-to-moment card to a local circuit side result; its signed moment is
+unchanged. Live claims, open PR bodies, main-tree notes and merged PR searches
+were checked. Sparse local and arbitrary historical-diff coverage is incomplete;
+a search miss is not a novelty certificate.

research/p104-chart127-suffix/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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/p104-helper470-twin-rung-removal/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760",
+      "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f"
+    },
+    {
+      "path": "research/p104-unread-path-resynthesis/local.py",
+      "usage": "input",
+      "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223",
+      "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597"
+    }
+  ]
+}