Prove a receiver-only obstruction to a root-2 stage deletion (no κ)

research/p104-root2-receiver-obstruction/PROOF.md

@@ -0,0 +1,124 @@
+# A receiver-only obstruction to the direct frame-520 deletion
+
+This contribution was produced by Nick Petalas. The input word and root-relay
+construction are DreamingOfClouds's PR #6144, at
+`4f3b67e7c37ae270da9584033132866d0cf63e42`, with Ali Romman and the retained
+P104 lineage. The new result is the separating input for the attempted edit
+below, together with its receiver-only impossibility consequence.
+
+## Exact model and attempted edit
+
+Use the retained symbolic scalar convention. Every public input has an
+independent coordinate `x_r`. An ADD replaces a row by a linear combination
+of rows at the same chart. A MOVE transports its represented row and changes
+the chart. INIT and CLEAR concern owned fields. These are the algebraic
+conventions of the predecessor's finite word; no new physical primitive is
+introduced here.
+
+All event ordinals in this paragraph are zero-based in the pinned PR6144 word.
+The function `proposed` in `verify.py` defines the entire attempted edit:
+
+1. Remove events 12888, 12932, 12933 and 12934, which move helper 497 through
+   519/520 and give it the register-48 and register-228 reads.
+2. Before event 12918, move 497 directly from 3 to 737 and add register 228
+   there with coefficient 1. Register 228 is still at 737.
+3. Remove events 13484, 13485 and 13486. Before event 13487, move owned 772
+   directly from 529 to 737 and add it to 497 with coefficient -4.
+4. Replace event 15459 by the move of 497 from 737 to 914.
+
+All other events, boundary charts and fields are unchanged. The edited word
+has 22,815 events. Its moves and scalar meetings through the cut considered
+below are legal. Its operator is incorrect; it is not offered as a supplier.
+
+The old register-48 read is the linear form
+
+`V = x_48 + x_32 + x_98 + x_85`.
+
+Before original event 15647, `ADD 145,161,-1/2,914`, the edited and original
+rows differ only in fields 497 and 161. Their differences are respectively
+`-V` and `V/2`. This comparison is over all 799 symbolic input coordinates,
+including the formal owned entries before initialization. It checks the
+effect of the new edit, not the correctness of the predecessor's theorem.
+
+## Allowed repairs and theorem
+
+Freeze the edited prefix through original event 12934 and the chart trajectory
+of every field. Freeze every nonreceiver scalar event. Between the cut after
+that prefix and the cut immediately before original event 15647, allow any
+finite homogeneous linear operations on receiver 161, using any fields
+currently at its exact chart. Coefficients may be arbitrary constants;
+repeated reads, replacements of its existing scalar operations and SCALEs
+are allowed. No workspace, source mutation or changed receiver MOVE is allowed.
+
+**Theorem.** No such repair gives receiver 161 its original PR6144 row at the
+specified consumer cut, for all inputs.
+
+Take the separating input
+
+`x_32 = 1, x_5 = -1, x_r = 0 for r not in {32,5}`.
+
+The exact finite certificate in `RESULT.json` establishes the following facts:
+
+- The edited receiver is zero at the start of the repair window.
+- At every cut in the window, every other field at receiver 161's chart is
+  zero on this input.
+- There is no ADD or COPY reading 161 into another field in the window.
+- The original required receiver value at the consumer cut is `-1/2`.
+
+There are 2,712 cuts, including the entry and consumer cuts. The verifier
+checks 241,377 coframed donor occurrences. It inspects every cut, including
+ones without an existing receiver operation. Between consecutive cuts no
+frozen event changes a donor's value or chart, so extra receiver operations
+at arbitrary times have the same donor menu as a checked cut.
+
+Because the frozen program never reads the receiver into another field in
+the window, changing receiver operations cannot change the donor values.
+Induct on the frozen events and any interleaved repair operations. The
+receiver starts at zero. A homogeneous linear operation on zero arguments
+leaves it zero, and moving a zero row leaves zero. Thus it is still zero at
+the consumer cut. It cannot equal the required `-1/2`. This proves the theorem.
+
+Equivalently, the coefficient functional `row[32] - row[5]` annihilates the
+receiver's initial row and every available donor row, but evaluates to `-1/2`
+on the desired row. This is an exact linear separation certificate, not a
+failed coefficient search.
+
+## Consequence and boundaries
+
+The direct rerouting cannot be completed by adding or resynthesizing scalar
+compensation only on receiver 161 in this window. A successful construction
+must change an additional source, trajectory, earlier prefix or consumer
+contract. In particular, crediting the saved moves without delivering `V/2`
+to the consumer is invalid.
+
+This does not exclude removing frame 520 by another construction, repairing
+outside this window, or accepting and compensating a different value at the
+145/161 consumer. It does not address removing frame 737. No complete paid
+invoice, new kappa, native implementation, full predecessor replay, supplier
+admission, proof-kernel acceptance or complete multiplication theorem is
+claimed. The five selected framework assumptions remain.
+
+## Verification design and bounded code
+
+The checker authenticates the exact upstream compressed word before decoding
+it. One pass evaluates the separating input and checks every common-chart
+donor. A separate sparse symbolic interpreter compares all input coefficients
+at the consumer cut. Five false-claim controls reject a changed source anchor,
+the wrong witness sign, two unavailable reads and a wrong root-read coefficient.
+The checks use explicit exceptions and also run with optimization enabled.
+
+The code has no recursion or asynchronous work. Source dimensions fix 799
+fields, 1,093 charts of dimension at most 9 and 22,818 events; all loops and
+collections are bounded by these inventories. The two symbolic states contain
+at most 799 squared coefficients each, and no per-cut state is retained.
+Each function is shorter than 60 physical lines.
+
+Power-of-ten rule 3 has a managed-runtime deviation: Python allocates integers,
+Fractions, dictionaries and parser objects during replay. The source byte pin
+and fixed inventories bound live state; this is a terminating exact checker,
+not a steady-state service. Rules 8 and 9 retain the standard JSON decoder
+and five finite zero-argument control callbacks. They never evaluate source
+code, load plugins or dispatch to external jobs. Follow-up for a constrained
+runtime would replace these with fixed arrays and direct control invocations;
+the present package does not claim fixed-allocation execution. Warnings-as-errors
+and normal/optimized execution supply the available Python diagnostics.

research/p104-root2-receiver-obstruction/README.md

@@ -0,0 +1,97 @@
+# A direct root-2 stage deletion needs more than receiver-only compensation
+
+This contribution was produced by Nick Petalas. It builds on
+[DreamingOfClouds's PR #6144](https://github.com/CrocSwap/integer-mult-bounds/pull/6144),
+Ali Romman and the retained P104 construction lineage.
+
+**Scoped proof with an exact finite certificate; no new kappa.** One explicit
+attempt to remove owned register 772's frame-520 stage moves helper 497's root
+read to frame 737 and removes its earlier register-48 read. The missing form is
+`V = x_48 + x_32 + x_98 + x_85`. At the next 145/161 consumer, the resulting
+differences are exactly `-V` in 497 and `V/2` in 161; all other rows agree.
+
+Receiver-only compensation cannot preserve that consumer contract. The input
+`x_32=1, x_5=-1`, with all other independent inputs zero, gives zero in receiver
+161 and every field it can read throughout the stated repair window. Its
+required consumer value is `-1/2`. Arbitrary homogeneous linear compensation
+in that window therefore fails, even with unrestricted constant coefficients
+and repeated reads. [PROOF.md](PROOF.md) gives the exact edit, window and proof.
+
+This is a new obstruction to an attempted changed read/trajectory contract.
+It does not audit the predecessor or exclude its general open lead. A useful
+next construction must change another source, trajectory, earlier prefix or
+consumer contract. Frame 737 is unattempted. No new paid invoice, supplier,
+native tariff, selected-frontier change or complete multiplication theorem is
+claimed. The five inherited framework assumptions remain.
+
+## Reproduction and evidence
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-root2-receiver-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/p104-root2-receiver-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-root2-receiver-obstruction
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-root2-receiver-obstruction --check-source-history
+```
+
+Other systems may substitute their CPython 3.12 interpreter. Expected direct
+status is `PASS_ROOT2_RECEIVER_OBSTRUCTION`; the registered runner reports
+`PASS_REGISTERED_RESEARCH_PACKAGE`. Every registered check is bounded at 120
+seconds. The receipt is generated, binds its verifier and input hashes, and is
+compared byte for byte. Regenerate it only to an external path with
+`verify.py --output /absolute/scratch/RESULT.json`.
+
+The verifier checks all 2,712 cuts in the compensation window and 241,377
+coframed donor occurrences. A separate full symbolic interpreter checks the
+attempted edit's effect on every one of the 799 input coordinates at the
+consumer cut. Five false-claim controls run in normal and optimized mode.
+These are finite exact checks supporting the induction proof; they are not
+formal proof-kernel or independent human review. No full predecessor, selected
+supplier, native, compiler, outer or rounded-multiplier replay is performed.
+
+The predecessor word is retained byte for byte in `inputs/`. `UPSTREAM.json`
+records its author, original head, path, Git blob, size and SHA256. Replay needs
+no network or unmerged Git object. Its original compressed bytes were obtained
+through GitHub's contents API and checked against the API's Git blob and size.
+The task and selected-record provenance are pinned at canonical main
+`721c03822c421b7f7fcbb2598993b947c4d88419` in `SOURCES.json`.
+
+## Related open work
+
+- PR #6144 poses the root-2 stage-removal lead and supplies the input word;
+  it supersedes the closed predecessor PR #6143.
+- PR #6145 independently descends the 772/731 relay on top of #6143. This
+  certificate is bound to #6144's different word and claims no transfer to it.
+- PR #6136 studies chart-only changes on PR6030. This attempted edit changes
+  which register 497 reads and where it reads it.
+- PR #6084 excludes an endpoint-recoding approach to helper 469. The helper,
+  read graph and quantified repair class here differ.
+- PR #6154 coalesces the 791/770 owned lifetime on PR6144. This certificate
+  uses the uncoalesced predecessor and concerns the separate 772/497 path.
+
+The broader P104 scalar and helper-split packages have different contracts.
+Their results and credits remain with their authors. The overlap search checks
+metadata and scoped main-branch notes; it is not a global novelty certificate.
+
+## Open next questions
+
+Can another source or consumer contract remove root 772's frame-520 stage?
+A paid complex improvement would matter at the binding supplier. First change
+one source trajectory or the 145/161 consumer cut, track both the separating
+input and the full missing form, then charge all additional moves and target
+changes. No legal all-input construction or favorable complete invoice is
+supplied here. The structured question is in `TASK.json`.
+
+## Credit and license
+
+The input word, root-relay descent and open lead are by DreamingOfClouds.
+PR6030/PR5907 supply the previous rung-removal words; Ali Romman's PR5827
+supplies their checking conventions, following Mason Hale's PR5811 and the
+retained lineage through Pierre-Loic Doulcet's PR5565. This package contributes
+only the explicit attempted edit, its separating certificate and the scoped
+receiver-only theorem. The available-span obstruction method is classical;
+Jonathan Capalbo's PR6069 and JoyboyBrian's PR6084 provide related P104 uses.
+New material is Apache-2.0.
+
+Independent human and formal proof-kernel review are unclaimed.

research/p104-root2-receiver-obstruction/RESULT.json

@@ -0,0 +1,39 @@
+{
+  "base_window": [
+    12935,
+    15647
+  ],
+  "claim_type": "Scoped linear obstruction with an exact finite certificate",
+  "controls": [
+    "changed_source_anchor",
+    "wrong_witness_sign",
+    "unavailable_48_read",
+    "unavailable_497_read",
+    "wrong_root_read"
+  ],
+  "edited_events": 22815,
+  "edited_window": [
+    12933,
+    15644
+  ],
+  "missing_form": {
+    "32": "1",
+    "48": "1",
+    "85": "1",
+    "98": "1"
+  },
+  "observation": {
+    "coframed_source_checks": 241377,
+    "cuts": 2712,
+    "receiver_value": "0"
+  },
+  "required_receiver_value": "-1/2",
+  "source_head": "4f3b67e7c37ae270da9584033132866d0cf63e42",
+  "source_sha256": "c71985d96bf3d4a35aae111aaba87e376f7367efb4a5686278ef293732757533",
+  "status": "PASS_ROOT2_RECEIVER_OBSTRUCTION",
+  "verifier_sha256": "9042c7602638a447e5f8a76162c54d7b6a8273859ad33c554ce32c3ff217b371",
+  "witness": {
+    "32": "1",
+    "5": "-1"
+  }
+}

research/p104-root2-receiver-obstruction/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}