Remove one scalar ADD from the selected P104 word (no κ)

research/selected-p104-scalar-fusion/README.md

@@ -0,0 +1,130 @@
+# One fewer scalar ADD in the selected P104 word
+
+The selected PR6030 word admits an exact one-ADD reduction, from 22,803 to
+22,802 events. Replace its zero-based event 231 by
+`["ADD",210,403,"1/2",3]` and omit event 392. Both original events are
+`["ADD",210,403,"1/4",3]`. Every other event and every non-program field
+is retained literally.
+
+Claim type: finite exact certificate with a scoped rewrite proof. This is
+a logical scalar-event improvement. The complete recursive paid and productive
+profiles are unchanged, so no new kappa is claimed. This contribution was
+produced by Nick Petalas. Independent human and formal proof-kernel review
+are unclaimed. Apache-2.0.
+
+## Proof
+
+Write A(c) for the update `x_210 += c*x_403`. For an intervening ADD
+`x_u += d*x_v`, the sufficient commutation conditions are `u != 403` and
+`v != 210`. They follow either by expanding both compositions on arbitrary
+inputs, or by multiplying their elementary matrices. A SCALE commutes with
+A(c) when its role is neither 210 nor 403.
+
+The 160 intervening events at indices 232 through 391 consist of 158 ADDs
+and two SCALEs. Every one is at frame 3. Every ADD satisfies the displayed
+conditions. The SCALEs act on roles 204 and 193, with coefficients 1/2
+and -1. Thus every intervening event commutes with A(1/4). Move the later
+A(1/4) left through this region and use
+`A(1/4) A(1/4) = A(1/2)`. This proves equality on arbitrary inputs at the
+end of the region, including all dirty roles. There are no intervening
+MOVE, INIT, COPY or CLEAR events and no intermediate external boundary.
+
+The region uses 133 roles. The verifier also constructs both complete
+133 by 133 rational operators and checks every entry. A separate scalar
+execution checks all 133 basis columns and eight dirty vectors. These are
+finite corroboration of the displayed identity; the proof is not an
+extrapolation from sample inputs. Tensoring the scalar identity with any
+column space gives the same local rewrite at every column multiplicity.
+
+The prefix, suffix, initial and final frames, live and owned sets, native
+events, lifetimes and productive targets are identical. All later states
+therefore agree exactly whenever the original program is defined. Each
+native transition is applied to the same state. The original native and
+caller results remain cited premises rather than new audit deliverables.
+All 3,453 MOVE, 861 SCALE, 31 INIT, 31 CLEAR and 23 COPY events are retained;
+the ADD count changes from 18,404 to 18,403. No intermediate rounded-error
+bound or physical runtime comparison follows from exact endpoint equality.
+
+## Reproduction
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/selected-p104-scalar-fusion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/selected-p104-scalar-fusion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/selected-p104-scalar-fusion
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/selected-p104-scalar-fusion --check-source-history
+```
+
+Any CPython 3.12 installation can replace this local interpreter path.
+Expected marker: `PASS_SELECTED_P104_SCALAR_FUSION`, with 17,689 exact
+operator entries, 133 basis columns, eight dirty vectors and eleven
+rejecting controls. Checks remain active under optimized Python.
+The receipt is generated on stdout and binds all five package files,
+the source word and the complete transformed word by SHA256. No receipt
+is hand-written. The checker writes no files.
+
+To materialize the full verified word, add `--emit-word` and redirect stdout
+to a scratch location outside the checkout. This runs the same full checks
+before emitting JSON. The package stores the two-event edit as code, avoiding
+a second committed copy of the predecessor word.
+
+## Scope and predecessor credit
+
+The scientific base is canonical main
+`2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8. The current
+source-binding orientation passes. It is metadata orientation, not a
+scientific replay. The original `p104-side-correction` card is explicitly
+changed to this scalar side result. Its full invoice improvement gate is
+unmet. The first reduction ended the search; no maximality is claimed.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19291931)
+records the question before the experiment.
+
+Credit DreamingOfClouds for PR6030's full word and its PR5907 predecessor;
+Ali Romman for PR5827's retained supplier chain and PR6169's distinct
+common-response resynthesis on PR6144; and the P104/native/helper/controller/
+caller/compiler/BIT lineage retained by those packages. PR5828 and the older
+commuting-cancellation work are methodological predecessors. Elementary-matrix
+commutation and addition of transvection coefficients are classical. The new
+contribution is this literal selected-source reduction and its certificate.
+No predecessor file or credit line is edited.
+
+Before publication, live handoffs, active Discussions, open PRs, merged PR
+queries and main README terms were searched. PR6169's certificate contains
+no change to the two `210 <- 403` events, which its PR6144 input also retains.
+That is an overlap check, not a replay of its mathematical result. Sparse
+local overlap coverage is incomplete. Unpublished work and arbitrary nested
+code are outside the search, so no global novelty guarantee is asserted.
+
+The selected frontier is unchanged. Native all-column implementation, owned
+erasure, compiler closure, precision/tape and analytic recovery remain the
+five inherited framework assumptions. Native/caller/BIT/outer suites, rounded
+execution, Lean and Docker are outside this contribution and were not run.
+The exact proof does not establish a complete multiplication theorem,
+supplier admission, a wall-time improvement or a better recursive invoice.
+
+## Engineering bounds
+
+There is no recursion, subprocess, network call or write path. The fixed
+source has 22,803 events; both operators have 133 rows and columns and at
+most 162 gates. Every function has fewer than 60 lines. Source reads are
+capped at 256 KiB compressed and 4 MiB decompressed, package reads at 1 MiB
+each. The word copy and exact rational matrices are bounded by this fixed
+authenticated input. Python's dynamic allocation is a managed-runtime
+deviation from Power of Ten rule 3; no allocation-free claim is made.
+The compensating control is the fixed source hash and bounded finite
+domains. Larger domains require revisiting the bounds. Warning-strict normal
+and optimized execution provide the available diagnostics; no separate
+static analyzer is configured. All semantic checks use explicit exceptions.
+
+## Open next questions
+
+Can a scalar rewrite also remove a native transition or change a legal
+productive target? Start with one explicit paid-path topology and its full
+signed invoice. The unchanged invoice here gives no kappa headroom, and the
+family expansion gate must be met before another construction round.
+
+Does this exact reduction admit a favorable rounded implementation? Compare
+the complete intermediate error and precision cost of the two region
+programs under one actual caller. Exact endpoint equality alone does not
+settle that question. Neither follow-on is reserved by this contribution.

research/selected-p104-scalar-fusion/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "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/p104-helper470-twin-rung-removal/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760",
+      "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f"
+    },
+    {
+      "path": "research/p104-helper470-twin-rung-removal/README.md",
+      "usage": "provenance",
+      "git_blob": "147c732eb452884a49aa4b1c18608a95b0c47e6e",
+      "sha256": "86eba866ef0af654bc06ffada16c18cb795443da33f7f636cf5c1e7aee0f6cbc"
+    },
+    {
+      "path": "research/p104-common-response-resynthesis/README.md",
+      "usage": "provenance",
+      "git_blob": "72d8f4f38e2ae8213730522767d837666c1b81cc",
+      "sha256": "fbb76054e91d0e18edcb9fb7e0ee01c0ea07fccf3898de6c707565197ba9a886"
+    },
+    {
+      "path": "research/p104-common-response-resynthesis/CERTIFICATE.json",
+      "usage": "provenance",
+      "git_blob": "2e9911c6d36b74c044201b8b1e7af3b8098f1c55",
+      "sha256": "36bcc79135fe2ba85bcc4583ac93c700effccb6fbfd42d7fecf49e39e9e90102"
+    }
+  ]
+}

research/selected-p104-scalar-fusion/TASK.json

@@ -0,0 +1,125 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "original_card": {
+    "id": "p104-side-correction",
+    "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "research/p104-helper-subspace-splits/README.md",
+      "research/dyadic-helper-channel-capacity/README.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "P104",
+      "helper basis",
+      "helper split",
+      "5718",
+      "dyadic capacity"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4133: literal-slot defect",
+        "evidence": "research/p104-literal-slot-defect/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4136: uniform commutation gap",
+        "evidence": "research/p104-uniform-commutation-gap/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4140: uniform encoding gap",
+        "evidence": "research/p104-uniform-encoding-gap/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance",
+        "evidence": "research/p104-source-chart-shortcut/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4154: fiber-tag seam mismatch",
+        "evidence": "research/p104-fiber-tag-seam/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "One exact scalar ADD fusion on the selected PR6030 word, preserving its entire native stream and boundary.",
+  "scope_change_reason": "The original helper split/invoice question is replaced by a bounded source-level scalar improvement. The complete invoice gate remains unmet.",
+  "bottleneck_link": "A scalar side result reduces one logical addition in the current precision/tape program; it does not improve the binding recursive moment.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop construction search at the first verified one-event reduction; no wider optimization.",
+  "outcome": "completed",
+  "evidence": "verify.py checks the complete 133-role region operator, independent basis execution, envelope invariants and eleven rejecting controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a scalar rewrite remove an actual native transition or legally change a productive target?",
+      "why_it_matters": "Only a changed complete signed invoice can improve kappa at this interface.",
+      "first_step": "Exhibit one paid-path topology and compute its full signed invoice before another construction round.",
+      "blocked_by": "No paid or productive profile changes in this contribution."
+    },
+    {
+      "question": "What is the complete rounded-error and precision cost of the fused region under an actual caller?",
+      "why_it_matters": "Exact endpoints do not compare intermediate rounding errors.",
+      "first_step": "Evaluate both region programs with one source-bound rounded caller and include all precision costs.",
+      "blocked_by": "A rounded caller and its error contract are not supplied."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19291931",
+  "claim_type": "finite certificate and scoped rewrite proof"
+}

research/selected-p104-scalar-fusion/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-helper470-twin-rung-removal/WORD.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Complete exact region operator, independent basis execution, boundary preservation and eleven rejecting controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same complete checks with Python assertions disabled."
+    }
+  ]
+}