Remove the paired DDG stopping counter with one owned tape cell (no new κ)

research/marked-tape-ddg-reversal/PROOF.md

@@ -0,0 +1,148 @@
+# Counterless reversal with an owned delimiter
+
+This is a scoped proof for one fixed two-tape machine. The source sampling
+law and edge-inverse lemma are credited premises, not new sampling theorems.
+The new step replaces a numerical stopping counter by a local tape boundary.
+
+## Statement and exact boundary
+
+Let the random tape contain an infinite binary string beginning at position s,
+with one caller-owned blank symbol `_` at s-1. Positions below s-1 are arbitrary
+and protected. The random head begins at s. A second tape has one stationary
+head on a dirty four-symbol cell A, interpreted as a two-bit accumulator.
+The caller supplies the fixed `(1,1)` denominator-13 DDG of zxv's PR #6072.
+Write i for its first output and T for its stopping depth on the binary string.
+
+For every string with finite T, the machine in `machine.py` terminates with
+A replaced by A XOR i, every random-tape symbol and both heads restored, the
+owned delimiter cell blank, and finite control at its fixed return label.
+It uses exactly 3T+4 two-tape transitions and 2T+4 random-head moves, has
+maximum random-head excursion T to the right and one cell to the left, and
+writes the delimiter cell exactly twice. It has no numerical stopping counter,
+position register or per-step history. A finite certificate establishes 1,563
+control states and 10,000 rules for this fixed graph.
+
+A two-tape transition reads both current symbols, writes their replacements,
+and moves the random head by -1, 0 or 1. The output head stays fixed. The random
+tape alphabet is `{0,1,_,#}`; the output alphabet has four symbols. These are
+finite-alphabet machine steps, not individual binary gates or the repository's
+native paid calls. Fixed rule selection is part of finite control, with no
+unit-cost RAM lookup assumption. Binary-alphabet lowering has an additional
+constant cost not computed here.
+
+## Predecessor facts used
+
+The retained `vendor/paired_sampler.py` is zxv's exact PR #6072 source at
+`9011bf83e85ecd0443c789cf03259442f750877d`. Only `make(1,1)` is called to obtain
+its graph, phase layout and cited expectation. Its original `main`, sampling
+census and optimality checks are not run.
+
+JoyboyBrian's PR #6102 at `0422af13625c2e7e8ece28bdd74364a61764c64a`, retained in
+`vendor/PROOF.reversal.md`, proves that the predecessor phase p, consumed bit u
+and current DDG target identify a unique previous node. For an internal target,
+recover q by adding the sum of the four binary digits to its node index. For a
+leaf, recover q from that leaf's digit slot. Then the previous node is
+(q-u)/2. The digit ordering and phase are essential. We use that lemma, rather
+than claiming a new inverse or auditing the predecessor proof.
+
+The source law gives the independent output probabilities `(144,12,12,1)/169`
+and E[T] = 9960277917013927549978 / 4649714690825496825793 < 9/4.
+These probabilistic statements remain predecessor premises. Our pathwise
+construction does not need fair bits or independent bits for reversibility.
+
+## Local machine
+
+`F(p,j)` means forward DDG state j in phase p. `B(p,j)` means that j is the
+current reverse target and the random head is immediately after its prefix.
+`R(p,j)` means that the head has moved left onto the next bit to undo.
+Here j may be a leaf in B and R. The phase is always modulo 156.
+
+1. In `entry`, move left. In `prepare`, replace the owned blank by `#`, move
+   right, and enter `F(0,0)`. These are two transitions.
+2. For `F(p,j)` reading u, apply the source edge and move right. At an internal
+   target enter its F state. At leaf i, XOR i into the second tape's symbol and
+   enter `B(p+1,leaf_i)`. Output retention is part of this last transition.
+3. In any B state, move left and enter the corresponding R state.
+4. In R on a binary symbol u, apply the predecessor's inverse edge, decrement
+   phase modulo 156, and enter its B state without moving the head.
+5. The only rule on `#` in R is `R(0,0)`: replace `#` by `_`, move right, and
+   return. Other R states have no marker transition.
+
+No transition reads an absolute coordinate, stopping depth or elapsed time.
+The Python observer's bounded loop, head coordinate and measured counters are
+outside the finite rule key. The full rule key contains only control, current
+random-tape symbol and current output symbol.
+
+## Correctness for arbitrary terminating paths
+
+After k forward steps, the head is at s+k and F has exactly the source's
+phase and node, until the source first terminates. Thus after T steps the
+output cell is A XOR i, the head is s+T and B stores the last target and phase.
+
+By backwards induction, after reversing T-k edges, B stores the exact source
+state after k steps, phase k modulo 156, and the head is at s+k. For k>0,
+the next left move reads a binary symbol at s+k-1. The cited inverse lemma
+recovers exactly the source state after k-1 steps. It leaves the output cell
+unchanged. At k=0 the next left move reads the delimiter at s-1 and B's state
+is the root at phase zero. The final rule erases the marker and returns to s.
+
+A root revisit at a positive multiple of 156 does not terminate reversal:
+its preceding tape cell is binary. The unique delimiter, rather than a root
+state test, distinguishes the initial visit. No numerical T survives or is
+needed during the call. The output value need not be retained in separate
+scratch because it was copied before the leaf was undone.
+
+All data symbols are read-only. The only first-tape writes are blank-to-marker
+in preparation and marker-to-blank on return. Hence arbitrary protected cells,
+the entire random string and the owned blank are restored. The output head
+never moves. This proves the stated map on every terminating path.
+
+The local rules are also one-step injective as a partial machine on arbitrary
+configurations. Every destination control has a unique incoming head direction.
+Given that direction, the written symbol and output symbol identify a unique
+incoming rule. Forward injectivity is the cited phase-and-coin inverse. Reverse
+injectivity is forward determinism. The marker/preparation ranges are disjoint
+from binary ranges. The verifier checks these two finite injectivity predicates
+on every generated rule. Invalid configurations may have no transition; total
+behavior outside the stated entry invariant is not asserted.
+
+## Exact accounting and finite certificate
+
+Preparation costs two steps. The forward walk costs T steps, including output
+XOR. Reversal costs two steps per consumed bit and two final delimiter steps.
+The total is 3T+4. Preparation and the final marker probe each move twice;
+each data bit contributes one forward and one backward head move. Travel is
+2T+4. No per-step controller bit is allocated.
+
+There are 312 F states. The actual source edges produce 624 distinct target/
+phase pairs: 312 internal pairs and 312 leaf/phase pairs. Each has B and R
+states. Entry, prepare and return add three, giving 312+2*624+3=1,563.
+For each of four dirty output symbols, the rules contain 624 forward edges,
+1,248 B moves, 624 inverse edges, two entry rules, one prepare rule and one
+return rule. Thus 4*(624+1248+624+2+1+1)=10,000. The verifier enumerates the
+states and rules instead of inferring these finite counts from a sample run.
+
+Using the cited source mean, E[steps] = 3E[T]+4 equals
+48479692514343769953106 / 4649714690825496825793 < 43/4.
+This counts finite-alphabet machine steps. It is not a wall-clock speedup or a
+comparison with a native recursive invoice.
+
+The finite replay covers 4,088 short dirty-output runs and all 938 terminating
+prefixes through depth 470. Those longer runs contain 942 reverse root revisits.
+They corroborate the interpreter, wrap handling and exact bills. The induction,
+not the finite fixture depth, proves correctness for arbitrary finite T.
+
+## Scope and remaining cost
+
+The changed contract supplies one owned blank immediately beside the random
+segment and a stationary output head. The machine pays to mark and clear that
+blank. Providing these positions in an actual caller, fixed binary-machine
+lowering, parameter dispatch and native adaptation remain separate obligations.
+The graph and finite control are fixed before any random bits are read.
+
+The resident transcript and the random-head excursion have no finite worst-case
+bound. This is constant auxiliary control and delimiter storage, not constant
+total space. After output retention, the consumed tape is correlated with that
+output. Restoring its symbols does not make them conditionally fresh. No actual
+multiplier caller, supplier admission, new kappa, complete multiplication theorem,
+independent human acceptance or proof-kernel verification is claimed.

research/marked-tape-ddg-reversal/README.md

@@ -0,0 +1,108 @@
+# A marked resident tape removes the DDG stopping counter
+
+For the fixed `(1,1)` paired sampler, one owned blank beside the random segment
+replaces the unbounded stopping counter of [JoyboyBrian's PR #6102](https://github.com/CrocSwap/integer-mult-bounds/pull/6102).
+The new finite-state two-tape machine prepares a delimiter, copies the sampled
+two-bit output into a dirty XOR accumulator, reverses to that delimiter, clears
+it and returns both heads. For every terminating path of depth T it uses exactly
+**3T+4 finite-alphabet transitions** and **2T+4 input-head moves**.
+The controller has **1,563 states and 10,000 rules**, independent of T.
+
+This is a **scoped proof with a finite machine certificate**. It supplies a
+counterless local tape service under the stated changed boundary. The resident
+random transcript and head excursion remain unbounded. The output accumulator
+becomes A XOR i; its old value is not erased or required to be zero. The random
+tape, its owned blank and both head positions are restored.
+
+[PROOF.md](PROOF.md) states the machine model, proves the arbitrary-path
+induction and one-step injectivity, and derives the exact bill. Preparation and
+marker erasure are included. The random alphabet is `{0,1,_,#}` and the output
+cell has four symbols. The second head stays stationary. This is a concrete
+finite transition system; its rule selection does not use a RAM oracle.
+Binary-alphabet lowering and repository native paid calls have different costs.
+
+## Evidence and reproduction
+
+From the repository root, using Python 3.12 and the standard library:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/marked-tape-ddg-reversal/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/marked-tape-ddg-reversal/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/marked-tape-ddg-reversal
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/marked-tape-ddg-reversal --check-source-history
+```
+
+`PASS_MARKED_TAPE_DDG_REVERSAL` enumerates every rule and state, checks local
+injectivity and permitted writes, then runs 4,088 short dirty-output fixtures
+and all 938 terminating prefixes through depth 470. The long fixtures contain
+942 reverse root revisits. Each run checks exact steps/travel, output XOR,
+complete tape restoration, returned head and delimiter erasure. Controls reject
+wrong output, exhausted fixtures, bad input, missing marker return and premature
+halting on a wrapped root. Finite tests support the implementation; the proof's
+induction establishes arbitrary finite stopping depth.
+
+[RESULT.json](RESULT.json) is generated by the verifier and binds the proof,
+machine, verifier and retained source bytes by SHA256. The verifier writes
+nothing during ordinary replay. Its optional `--write-result` path is only for
+explicit regeneration. The Python interpreter's position and bounded observer
+counter are measurement state. They do not occur in the machine's rule keys.
+
+Using zxv's cited source expectation, the new exact bill has expected value
+`48479692514343769953106/4649714690825496825793 < 43/4` transitions.
+This is a consequence of the predecessor law, not a new sampling optimum or
+runtime benchmark. The source's probability/census suite is not rerun.
+
+## Scope and credit
+
+The changed `formal-interface-lemma` task takes the first Open next question of
+PR #6102 and supplies one local service boundary. It is not a proof-assistant
+formalization. An actual caller must provide the owned adjacent blank and the
+stationary output head; it must also preserve the random segment throughout
+cleanup. No conditional freshness of reused bits, parameter selection, binary
+gate tariff, native supplier, complete multiplier or new kappa is claimed.
+The five selected framework assumptions are not discharged.
+
+This scoped construction was produced by Nick Petalas. New work is Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+zxv's PR #6072 supplies the fixed DDG, classical sampling argument and mean.
+JoyboyBrian's PR #6102 supplies the phase-and-coin edge inverse and identifies
+physical tape/counter costs as open. Their exact sources and original credit
+are retained unchanged in `vendor/`; [vendor/ORIGIN.json](vendor/ORIGIN.json)
+records public origin heads and hashes. The new contribution is the delimiter
+construction, explicit local machine and exact counterless tariff. It does not
+claim the classical technique of reversing a recorded computation as new.
+
+The frozen card, base and source pins are in [TASK.json](TASK.json) and
+[SOURCES.json](SOURCES.json). The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241748)
+predicted a persistent delimiter; the delivered service also pays to prepare
+and erase it in one owned blank cell.
+
+## Related open work
+
+- [PR #6102](https://github.com/CrocSwap/integer-mult-bounds/pull/6102) supplies
+  the edge inverse and a counter-based logical reversal. This adds a changed
+  local tape boundary that removes its growing counter.
+- [PR #6072](https://github.com/CrocSwap/integer-mult-bounds/pull/6072) supplies
+  the graph and exact sampling law. This uses only its fixed `(1,1)` graph.
+- [PR #6096](https://github.com/CrocSwap/integer-mult-bounds/pull/6096) concerns
+  the applicability of denominator-13 sampling to actual inverse residues.
+  This service does not establish that caller applicability.
+
+- [PR #6124](https://github.com/CrocSwap/integer-mult-bounds/pull/6124) shares
+  forward graphs across parameter pairs. This machine retains the literal fixed
+  graph; the quotient's reversibility is outside this proof.
+- [PR #6068](https://github.com/CrocSwap/integer-mult-bounds/pull/6068) gives
+  finite-cap sampling obstructions. This service retains unbounded stopping.
+
+## Open next questions
+
+Can one actual nonadaptive caller supply the owned adjacent blank and stationary
+output head at the point it needs both decisions? Start with one reached residue
+pair and its tape ownership layout. The missing caller and conditionally fresh
+input randomness are the blockers; restoring consumed bits does not fund reuse.
+
+What is the explicit binary-alphabet transition constant for this fixed
+finite-control machine? Start by encoding each four-symbol cell by two bits and
+lowering every local rule while preserving head return and scratch cleanup.
+The current exact bill counts finite-alphabet two-tape steps, so the binary
+constant must be proved before comparison with a binary physical tariff.

research/marked-tape-ddg-reversal/RESULT.json

@@ -0,0 +1,28 @@
+{
+  "claim_type": "scoped proof with finite machine certificate",
+  "deepest_fixture": 470,
+  "expected_transitions": "48479692514343769953106/4649714690825496825793",
+  "expected_transitions_upper": "43/4",
+  "finite_control_states": 1563,
+  "head_moves": "2*T+4",
+  "marker_writes": 2,
+  "owned_delimiter_cells": 1,
+  "reverse_targets": 624,
+  "root_revisits": 942,
+  "rules": 10000,
+  "scope": "marked resident tape; fixed pair; no caller, freshness or new kappa",
+  "short_dirty_output_runs": 4088,
+  "source_sha256": {
+    "PROOF.md": "a182430c3360c6c89daa49141a9233a566fd425d1a869a4686382323c0cdaf19",
+    "machine.py": "34be31b9322fffd854ad7fec554762c1c551abebaa61650e83259da25c64db78",
+    "vendor/ORIGIN.json": "c812c46103220bdbbfef592f7112997179508597128c7b6af6a3e2750a78fa48",
+    "vendor/PROOF.reversal.md": "ed1bd5b54af0c1ab7f8208bb474bdb5e5b5ae073d62c2dad840349942caea88e",
+    "vendor/README.reversal.md": "6ca82d87d1dbaf11199419393c1782ea8ff9ff9efba1648a15c0ce65db79bb4b",
+    "vendor/README.sampler.md": "4a8d35da8cde11b127b490abdcaf0f085643313603d8b93d5773968a2e81a695",
+    "vendor/paired_sampler.py": "a3f14b87169b934489fc7d01d82ff36f6a671bc6c38e4761443f5481e36c2f63",
+    "verify.py": "f3cb2dd82c1c62ad6cf6380b6c6d8bcd32fc0ece0d6c04699917d66a136e447f"
+  },
+  "status": "PASS_MARKED_TAPE_DDG_REVERSAL",
+  "terminating_wrap_paths": 938,
+  "transitions": "3*T+4"
+}

research/marked-tape-ddg-reversal/SOURCES.json

@@ -0,0 +1,53 @@
+{
+  "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/marked-tape-ddg-reversal/vendor/ORIGIN.json",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/ORIGIN.json",
+      "git_blob": "db79b8b81a00971494a0233c6fc1defa97b81bf8",
+      "sha256": "c812c46103220bdbbfef592f7112997179508597128c7b6af6a3e2750a78fa48"
+    },
+    {
+      "path": "research/marked-tape-ddg-reversal/vendor/PROOF.reversal.md",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/PROOF.reversal.md",
+      "git_blob": "05c37b0a6e2267aefda26b129c618ca376999f06",
+      "sha256": "ed1bd5b54af0c1ab7f8208bb474bdb5e5b5ae073d62c2dad840349942caea88e"
+    },
+    {
+      "path": "research/marked-tape-ddg-reversal/vendor/README.reversal.md",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/README.reversal.md",
+      "git_blob": "799f80fb0f3d1952d4107d18a1beaf8623d9fe8a",
+      "sha256": "6ca82d87d1dbaf11199419393c1782ea8ff9ff9efba1648a15c0ce65db79bb4b"
+    },
+    {
+      "path": "research/marked-tape-ddg-reversal/vendor/README.sampler.md",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/README.sampler.md",
+      "git_blob": "615c4890ec797561fd4287445ceb1019905175bc",
+      "sha256": "4a8d35da8cde11b127b490abdcaf0f085643313603d8b93d5773968a2e81a695"
+    },
+    {
+      "path": "research/marked-tape-ddg-reversal/vendor/paired_sampler.py",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/paired_sampler.py",
+      "git_blob": "eda448fbda7b6a78f340086fcaac6e7556bf1383",
+      "sha256": "a3f14b87169b934489fc7d01d82ff36f6a671bc6c38e4761443f5481e36c2f63"
+    }
+  ]
+}