Prove a fixed-schedule obstruction for PR6345 helper respanning

research/p104-respan-stop-obstruction/PROOF.md

@@ -0,0 +1,117 @@
+# A fixed contact obstructs a stop deletion
+
+## Model and claim
+
+An epoch is a visit by one register to one frame between consecutive MOVE
+events. INIT starts a new owned lifetime and CLEAR ends it. An intermediate
+stop is an epoch with both an incoming and an outgoing MOVE in the same
+lifetime. Initial and terminal epochs are excluded.
+
+Freeze the word in DreamingOfClouds's PR6345, at the source bytes recorded in
+SOURCES.json. Let S be its public non-main registers with exactly one MOVE.
+The main registers are `live` and `112 + live`, as in the predecessor contract.
+
+Consider the following simultaneous relaxation.
+
+1. Every register in S may replace both endpoint frames by arbitrary binary
+   subspaces, retaining its unique MOVE at its original position among scalar
+   events. These endpoint choices need not belong to the published catalogue.
+2. Choose one intermediate stop U of a different register r. Replace its two
+   neighboring transports A -> U -> C by one transport A -> C. This transport
+   may occur at any cut between the retained surrounding epochs. In particular,
+   the scalar events formerly at U may be divided between A and C.
+3. All other epochs retain their frames, and scalar coefficients, operands,
+   operations, lifetime boundaries and scalar order are fixed. Scalar chart
+   annotations may be rewritten, but each ADD or COPY still requires equal
+   source and destination frames. Additional transports are excluded.
+
+The new result is a scoped impossibility statement. No such assignment exists
+for any intermediate stop of this word. There are exactly 2,660 such stops,
+2,654 public and six owned, and S has 42 members. This is a stronger endpoint
+freedom than choosing just one helper from the existing native catalogue.
+
+This statement concerns deletion of one stop while the other non-S epochs
+remain fixed. It does not exclude coordinated changes to two non-S registers,
+changed scalar schedules, new transports or a different word.
+
+## Fixed-contact lemma
+
+Suppose an intermediate stop U of r contains an ADD or COPY involving another
+register s. Suppose s is outside S and its epoch at that event stays fixed at
+U. If U differs from both neighboring frames A and C, deleting the visit to U
+is impossible under the model above.
+
+Proof. At the contact, the common-chart rule forces r's frame to equal s's
+fixed frame U. After replacing A -> U -> C by A -> C, r's frame at every
+scalar event between the surrounding epochs is either A or C. Neither is U.
+Thus the contact cannot satisfy the common-chart rule. This argument permits
+any position of the merged transport and does not depend on the new endpoint
+frames of registers in S. QED.
+
+## Exact application to the frozen word
+
+`certificate` in verify.py indexes every constant-frame epoch and each
+ADD/COPY contact. For every intermediate stop it chooses the first contact
+whose other register is outside S. The direct contact itself is the witness;
+no transitive equality inference or optimization solver is needed.
+
+Each witness has seven integers:
+
+```text
+[register, lifetime, stop ordinal, event index,
+ partner register, partner lifetime, partner epoch ordinal]
+```
+
+Event indices and public lifetime numbers start at zero. Owned lifetimes start
+at one. Stop ordinal k means the epoch after the kth MOVE of that lifetime.
+For each candidate, explicit binary spans show strict nesting of the three
+neighboring frames, increasing for public registers and decreasing for owned
+registers. In particular U differs from A and C as subspaces, irrespective of
+frame labels or basis choices.
+
+Every one of the 2,660 candidates has a direct fixed-partner contact. A second
+streaming implementation, `check_certificate`, discovers its candidate set by
+recording the epoch left by every MOVE after the first MOVE of a lifetime.
+It checks exact candidate coverage, unique witnesses, actual event operands,
+both current epoch identities, the common chart and the partner's exclusion
+from S. It does not call the primary trace builder or domain enumerator.
+The fixed-contact lemma therefore applies separately to every candidate.
+
+The generated receipt contains every witness and hashes of the input,
+decompressed payload and package files. The receipt is generated on request
+outside the checkout. Reproduction computes all witnesses anew.
+
+## Consequence for the open question
+
+PR6345 asks whether a re-spanned helper can enable a stop drop elsewhere.
+For the stated fixed-schedule, single-stop move, even all 42 one-step helpers
+together cannot do so. A successful continuation must alter at least one
+additional non-S epoch at a blocking contact, change the scalar incidence or
+schedule, introduce another transport, or change the word. This is a necessary
+change of scope, not a sufficiency theorem for any of these alternatives.
+
+The predecessor's legality, paid invoice and reported crossing are premises,
+not results re-established here. No price calculation or native operator replay
+is needed to rule out a move that already fails a necessary chart equality.
+No new kappa, supplier admission or complete multiplication theorem is claimed.
+
+Ali Romman's PR5590 already supplies an all-frame price floor with all scalar
+contact frames fixed on PR5580. That theorem is credited rather than repeated.
+The present finite step concerns the different PR6345 word and allows helper
+contact charts to vary with the 42 re-spanned helpers. It finds a different,
+fixed-partner contact at each stop. Common-chart equality is inherited syntax;
+the new contribution is its complete source-bound obstruction in this move
+domain, not a new general theory of frame transport.
+
+## Controls and limits
+
+The verifier rejects an omitted witness, a duplicate witness, five incorrect
+contact/epoch fields, a free-helper partner, an unanchored toy and a collapsed
+toy with a fixed contact. Two positive toy controls demonstrate an anchored
+stop and an actual unanchored stop deletion enabled by helper respanning.
+These toys test chart constraints only, not complete productive suppliers.
+
+The two implementations are new code by the same contributor. They do not
+constitute independent scientific review or formal proof-kernel checking.
+
+New result, proof and implementation produced by Nick Petalas. Apache-2.0.

research/p104-respan-stop-obstruction/README.md

@@ -0,0 +1,86 @@
+# One-step helper respanning cannot unlock a single P104 stop deletion
+
+This package proves a new scoped obstruction for the exact word of
+[PR6345](https://github.com/CrocSwap/integer-mult-bounds/pull/6345).
+Even if all 42 one-step helpers may change both endpoint subspaces at once,
+none of its 2,660 intermediate stops can be deleted while all other epochs
+outside those helpers retain their frames and the scalar schedule is fixed.
+The count includes 2,654 public stops and six owned stops.
+
+Every stop has an explicit ADD/COPY contact with another register whose epoch
+stays fixed. That contact forces the original intermediate frame to be visited.
+[PROOF.md](PROOF.md) states the exact model and proves the implication.
+This is a scoped proof with a finite structural certificate. No new kappa is
+claimed, and the selected frontier is unchanged.
+
+This extends PR6345's second Open next question. The predecessor establishes
+price-null helper freedom; the new step is an obstruction to using that freedom
+alone to remove one stop elsewhere. Existing word legality, native operators,
+invoice and supplier assumptions are premises, not review deliverables here.
+
+Ali Romman's [PR5590](https://github.com/CrocSwap/integer-mult-bounds/pull/5590)
+already proves a price floor for the older PR5580 word when every scalar contact
+frame is fixed. Here contacts involving freely re-spanned helpers may change
+charts. The new certificate finds a contact with a fixed partner at every
+candidate stop of the different PR6345 word. The common-chart equality itself
+is an inherited rule, not a new general theorem.
+
+## 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/p104-respan-stop-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p104-respan-stop-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-respan-stop-obstruction
+```
+
+Expected: `PASS_P104_RESPAN_STOP_OBSTRUCTION`, 2,660 stops, 42 free helpers,
+ten semantic rejections, two positive toy controls, and
+`PASS_REGISTERED_RESEARCH_PACKAGE` from the registered runner.
+
+Pass `--receipt /absolute/path/outside/checkout/receipt.json` to the direct
+verifier to save every contact witness with source and package file hashes.
+The verifier generates this receipt; no retained receipt is required.
+In a sparse checkout, materialize
+`research/p104-frontier-symmetric-ladders` first.
+
+## Scope
+
+The helper MOVE positions, scalar operands/order and all non-selected epochs
+outside the one-step helpers stay fixed. The merged transport replacing the
+selected stop may be placed at any intervening cut. The proof allows arbitrary
+new helper endpoint subspaces, including ones absent from the native catalogue.
+It rules out this local move before pricing or native synthesis matters.
+
+Coordinated changes to multiple epochs outside the one-step helper set,
+changed scalar schedules, additional transports and other words remain open.
+The package does not
+classify optimal frame assignments or prove a global price ceiling. The five
+inherited framework assumptions remain. Full native, caller, compiler, rounded
+execution and all-size replays are outside this obstruction's claim and were
+not run. [VALIDATION.md](VALIDATION.md) records checks and implementation bounds.
+
+## Open next questions
+
+- Can changing a blocking partner epoch together with the selected stop admit
+  a legal two-register deletion? Start with one generated contact witness and
+  trace the partner's other contacts. Full frame legality, productive target
+  changes and the complete signed bill are unresolved.
+- Can moving one helper's unique MOVE across scalar contacts evade the fixed
+  schedule obstruction without adding paid work? Start with an explicit
+  reordered scalar program and preserve every arbitrary public input.
+  Chronology, restoration and full pricing are blockers.
+
+The structured versions are in [TASK.json](TASK.json).
+
+## Credit and coordination
+
+The new obstruction, proof and verifier were produced by Nick Petalas.
+The input word, price-null freedom and open question are DreamingOfClouds's
+PR6345. Its predecessor is Ali Romman's PR6167 retained-operand construction
+over DreamingOfClouds's PR6144/PR6143 and the retained P104/native/caller lineage.
+Their source files and credit remain unchanged. No predecessor implementation
+is imported or copied into the verifier. All new work is Apache-2.0.
+
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358834).

research/p104-respan-stop-obstruction/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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/p104-frontier-symmetric-ladders/README.md",
+      "usage": "input",
+      "git_blob": "5c8f2af74ba2f44485fb446027c02ef00ccbe666",
+      "sha256": "7606e0c63a4a958fc0da9aba0a6fcadb947ef4575b846774b824f12e0d16b45a"
+    },
+    {
+      "path": "research/p104-frontier-symmetric-ladders/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "613301460170b30f7185cf1df5b99c767541568a",
+      "sha256": "b525237058cdb30d358f5332987fa5f72dc966579f55becd1b6702f62829eda8"
+    },
+    {
+      "path": "research/p104-fixed-contact-ceiling/README.md",
+      "usage": "provenance",
+      "git_blob": "1570338984271f48d18084fcd1d1ac1c322565f4",
+      "sha256": "125cf485ba91fba3d3a87fae503782c95d72b20039adf7f7a7ee753ed72c0c06"
+    }
+  ]
+}