Record the R437 parent blank-return cursor meter.

research/r437-parent-blank-cursor/PROOF.md

@@ -0,0 +1,81 @@
+# Cursor meter for one parent-packet blank-return
+
+No new κ. The selected conditional exponent stays `781451/250000000`.
+
+## Machine
+
+The packet tape is `Tape` in
+`research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py`.
+The alphabet constants in the sibling `words.py` are `ZERO, ONE, LEFT, RIGHT, BLANK = 0, 1, 2, 3, 4`.
+A fresh tape has `cells = [LEFT]` and `head = 1`. `read` at `head >= len(cells)` returns `BLANK` and does not extend the tape. `append` reads a `BLANK`, writes one symbol and steps right. `rewind` steps left until it reads `LEFT`, then steps right once. `clear` is
+
+```text
+rewind
+while read() != BLANK:
+    write(BLANK)
+    step(+1)
+rewind
+```
+
+After `n` appends the tape is `cells = [LEFT] + payload` of length `n + 1`, and the head sits at `n + 1`. Both payload symbols `0` and `1` differ from `LEFT` and from `BLANK`, so the scan length does not depend on the bit.
+
+## Call that erases a completed packet
+
+In `packet_engine.py` the success path, after `copy_bits` has consumed a packet, is
+
+```text
+current.read() == BLANK
+current.rewind()
+current.clear()
+```
+
+The comparison read is the completeness check. It leaves the head on the trailing blank and is not part of the erasure meter below. `directory.rewind()` on the same source line is a different tape. The blank-return traced here is the following `rewind` and `clear` on `current`.
+
+`changed.clear()` and `local.clear()` in the same loop are not this call. Their heads depend on `action`, which this note does not price. The failure-path `current.clear()` at the generator's `finally` is likewise not this call: it has no preceding rewind.
+
+## Meter from the trailing blank
+
+Write `R(h)` for `rewind` starting at head `h`, and `C` for `clear` starting at head `1` on a tape whose payload cells are exactly positions `1..n`.
+
+**Rewind from `h = n + 1`.** One left step lands on cell `n`. The loop then reads cells `n, ..., 1` and steps left, then reads `LEFT` at cell `0` and steps right onto cell `1`. That is `n + 1` reads, `0` writes and `n + 2` moves. The `n = 0` case is the same arithmetic: the head is already at `1`, the left step lands on `LEFT`, and the loop body does not run.
+
+**Clear from head `1`.** Its opening rewind costs `1` read and `2` moves and returns to head `1`. The loop then reads, blanks and steps through cells `1..n`, and one further read sees the virtual blank at `n + 1`. That is `n + 1` reads, `n` writes and `n` moves. The closing rewind is the rewind already counted, from head `n + 1`: `n + 1` reads and `n + 2` moves. Adding these gives
+
+```text
+reads  = 2n + 3
+writes = n
+moves  = 2n + 4
+```
+
+and restores head `1` with `cells = [LEFT] + [BLANK] * n`.
+
+**Sum, the success-path blank-return.**
+
+```text
+reads  = (n + 1) + (2n + 3) = 3n + 4
+writes = n
+moves  = (n + 2) + (2n + 4) = 3n + 6
+```
+
+The success-path rewind, the blanking scan and `clear`'s closing rewind each walk every payload cell. None of them jumps. `clear` also opens with its own rewind. On this call the head is already on cell `1`, so that rewind only steps onto `LEFT` and back. It does not walk the payload a fourth time. Its `1` read and `2` moves are included in the `2n + 3` and `2n + 4` figures above.
+
+## Parent length
+
+`PHYSICAL.md` states the unexecuted parent geometry
+
+```text
+B = 2,  G = 3 * 3^124,  S = 2,  U = 9475,
+n = U * B * G * S * 3^4 = 9475 * 12 * 3^128.
+```
+
+The same product is `972 * 9475 * 3^124`, because the executed fibre is `2 * 3 * 2 * 3^4 = 972` and the two omitted factors are the `9475` unused rows and the `124` atom coordinates inside `G`. Those coordinates are a factor of `n`, not a side path. Each of the three walks above steps across them.
+
+Substituting this `n` is the cursor invoice of one success-path blank-return of a single packet of that length. It is not an execution of the parent: the published child bridge allocates the `972`-bit fibre and does not allocate this tape. The model is the predecessor's one-payload comparison, with the executed `Tape` operations in place of the one-visit lower bound.
+
+Under that bound the parent write count was only `≥ n` and the executed packet's write count was only `≤ 972`. The machine meets both bounds exactly, and only as write counts. The parent move count `3n + 6` is strictly larger than `n` for this `n`. The same call on the executed fibre has writes `972` and moves `3 * 972 + 6 = 2922`, which is not the parent invoice.
+
+A model that blanks only one executed fibre, or that divides `n` by `3^124` before counting, is a different machine. `clear` writes once per stored payload cell.
+
+## What this does not sign
+
+Gather, routing, parking, checkpointing, table setup and the reverse-row coefficient stay unpriced. `BILL.md`'s `G`, `C` and `F` terms are not set to zero. Splitting the parent into `9475` separate tapes would replace one sentinel pair by `9475` sentinel pairs; that layout is not the packet engine's one `current` tape, and it is not claimed here. No carrier admission and no selected-frontier change follows.

research/r437-parent-blank-cursor/README.md

@@ -0,0 +1,114 @@
+# Cursor meter for one R437 parent blank-return
+
+**Partial certificate. No new κ.** The selected conditional exponent stays
+`781451/250000000`.
+
+## Result
+
+On the success path of `packet_engine.py`, a completed packet is erased by
+`rewind` followed by `Tape.clear`, starting from the trailing blank. For a
+payload of `n` symbols that call has meter
+
+```text
+reads = 3n + 4,   writes = n,   moves = 3n + 6.
+```
+
+The parent geometry in `research/r437-carrier-integration/PHYSICAL.md` is one
+payload of length
+
+```text
+n = 9475 * 12 * 3^128 = 972 * 9475 * 3^124.
+```
+
+The same call on that length is the parent blank-return invoice. The factor
+`3^124` is the 124 omitted atom coordinates inside the gap. The opening
+rewind, the blanking scan and the closing rewind each step across every
+payload cell, so those coordinates are crossed three times. They are not
+skipped.
+
+The write count is exactly the one-visit lower bound from
+`research/r437-parent-spectator-blank`. The move count is strictly larger.
+The same call on the executed 972-bit fibre has moves `2922`, which does not
+pay the parent.
+
+The argument is in [PROOF.md](PROOF.md). `verify.py` runs the pinned
+`records.Tape` on every length through 48, on the 972-bit fibre, and on the
+two miniature parents `9475 * 12 * 3^k` for `k = 0, 1`. It does not allocate
+the `3^128` parent.
+
+## What stays open
+
+`changed.clear()` and `local.clear()` still depend on where `action` leaves
+the head. Gather, routing, parking, checkpointing and table setup are not
+priced. One tape of length `n` is the predecessor's payload model; `9475`
+separate tapes would add extra sentinel walks and are not this call. No
+supplier and no new exponent is claimed.
+
+## Task and overlap
+
+- Task: `r437-carrier-integration`, scope **refined**.
+- Base: canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+- Selected record SHA-256 `9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa`.
+
+Session r85, item 8 of the ordered eligible list. The 19 October handoffs
+(discussion comments 19030045, 19030047, 19030049, and 19030053) are already
+delivered or closed. Later handoffs whose canonical artifact is an open pull
+request, including the H25 requests and the 2026-11-02 audits of #6348
+through #6361, are excluded. The revision-8 next-decision table then supplies
+six rows, naming `p104-side-correction`, `coverage-law-change` and
+`bit-helper-contract`. Catalogue cards not named by those rows follow, in
+catalogue order. Item 8 is `r437-carrier-integration`.
+
+The card's reverse coefficient, child-constructor tapes, SOURCE87 fibre
+multiplicity and payload-ratio lower bound are already delivered by this
+account (#4147, #4160, #5277, #5276). This package answers open question 1 of
+`research/r437-parent-spectator-blank`: the exact fixed-tape visit count,
+including cursor motion across the 124 omitted coordinates. It does not
+rederive the coefficient or rerun the pooled compiler.
+
+Checked on 2026-11-02: no open pull request states this `3n+6` move count.
+The merged predecessor #5276 stops at the payload ratio.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B scripts/research_selected_baseline.py
+python3 -B research/r437-parent-blank-cursor/verify.py
+python3 -B research/r437-parent-blank-cursor/test_verify.py
+python3 -B scripts/research_package.py --package research/r437-parent-blank-cursor
+```
+
+`verify.py` prints `PASS_R437_PARENT_BLANK_CURSOR` with `writes` equal to the
+parent payload and `moves = 3 * writes + 6`. `test_verify.py` prints
+`PASS_R437_PARENT_BLANK_CURSOR_CONTROLS`.
+
+Not run: `physical.py`, the pooled compiler, Lean, Docker, and
+`make frontier6030-verify`. The universal statement for every `n` is the
+control-flow count in `PROOF.md`; the checker executes the machine on the
+lengths named above.
+
+## Open next questions
+
+1. Where does `action` leave the head of `changed` and `local` before their
+   `clear` calls? Those blank-returns are not the success-path `current`
+   call priced here. First step: one source-bound postcondition for `action`
+   on a fibre of length `n`. Blocker: `action` is outside this package.
+2. Can one of `G`, `C` or `F` in `BILL.md` be instantiated on both arms
+   without setting the others to zero? A blank-return meter still does not
+   sign the whole C/D inequality. First step: pin one tariff. Blocker: those
+   tariffs are not inputs here.
+
+## Credit
+
+The parent extents, the constants `9475` and `972`, and the statement that a
+one-visit lower bound is not the machine invoice are Chris R / Clear1nsight,
+`research/r437-carrier-integration` and the open question in
+`research/r437-parent-spectator-blank` (unpaidmoon #5276). The tape operations
+are the retained predecessor `records.Tape` loaded by the selected physical
+caller. The carrier lineage remains ai-nanachi / PR #3647, Ali Romman /
+PR #1043, and Sagar Thakrar / PR #3700 and PR #2423.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human or formal-kernel review is claimed.

research/r437-parent-blank-cursor/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "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/r437-carrier-integration/PHYSICAL.md",
+      "usage": "provenance",
+      "git_blob": "ec85739460fb61c6505f9b1179f3bb3dc86cc079",
+      "sha256": "c7689d458e03853f5487a27707003698d04cbca086a503af47cd95d78cb14864"
+    },
+    {
+      "path": "research/r437-parent-spectator-blank/README.md",
+      "usage": "provenance",
+      "git_blob": "ad16671a4cb45d13cd7c4d97b709bc53b8d89607",
+      "sha256": "009860adc553a14ad5f1f41a0e65fb0d05e6eef5cb219979e1b453513c1516d9"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/inputs/pr2753/packet_engine.py",
+      "usage": "input",
+      "git_blob": "72543f684f38fefeacc2ee66d81661f1a2439cf7",
+      "sha256": "c80fc3aa9092f91cc309b2fb2dbc3618bf96bdb9b8498503993ea161f0ae2134"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py",
+      "usage": "input",
+      "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3",
+      "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py",
+      "usage": "input",
+      "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50",
+      "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9"
+    }
+  ]
+}

research/r437-parent-blank-cursor/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "r437-carrier-integration",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "r437-carrier-integration",
+    "question": "Can the paid R437 two-window carrier improvement be admitted by the actual pooled compiler and physical caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/r437-two-window-carrier/README.md",
+      "research/r437-reverse-row-coefficient/README.md"
+    ],
+    "methods": [
+      "Close one compiler/request, caller or precision/stock implication for the pinned paid exchange.",
+      "Falsify that exact interface with an arbitrary-dirty-state or chronology counterexample."
+    ],
+    "acceptance_gate": "Pin the complete source and destination contracts, exact paid and scalar deltas, and all remaining assumptions. A local moment gain is not a physical or all-size supplier admission.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Choose one unclaimed obligation: pooled compiler codebook/request alignment, actual physical caller, or precision/stock envelope using the already reported reverse coefficient. Pin the input and receiver, preserve dirty/source windows, and test one binding with a rejection control. Stop at unresolved dependencies; do not rederive the coefficient or quote the local moment as a completed bound.",
+    "bottleneck_link": "The exchange changes the paid profile; integration must establish that its gain survives the complete caller.",
+    "allowed_variations": [
+      "One compiler rebind, one actual caller boundary, or one precision/stock implication."
+    ],
+    "scope_change_triggers": [
+      "Ignoring added ADDs, retaining an obsolete reverse coefficient, or declaring global admission from the local histogram."
+    ],
+    "overlap_terms": [
+      "R437",
+      "two-window carrier",
+      "4067",
+      "4147",
+      "pooled compiler",
+      "request alignment",
+      "reverse row coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4067: source-bound two-window carrier with (2,2) to (1,3) paid exchange and fixed OQ4 host.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Pooled compiler/request rebind, physical caller and precision/stock admission.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4147: reverse row coefficient follow-up.",
+        "evidence": "research/r437-reverse-row-coefficient/README.md",
+        "remaining": "Use the exact coefficient in a caller-bound precision/stock proof rather than repeat the arithmetic.",
+        "status": "author-checked",
+        "source_commit": "72e7bb797adf82aeb525a399f56ab8adbab8e93c",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "On the pinned packet-engine success path, certify the exact Tape rewind-then-clear meter of one parent payload of length 9475*12*3^128, including the cursor walks across the 124 omitted atom coordinates.",
+  "scope_change_reason": "The card asks for one unclaimed physical-caller obligation of the paid R437 exchange and says not to rederive the reverse coefficient. Open question 1 of research/r437-parent-spectator-blank asks for this cursor invoice. The payload ratio, fibre multiplicity and constructor tapes are already delivered and are not repeated.",
+  "bottleneck_link": "The paid R437 exchange cannot be admitted until the parent blank-return is an exact charge rather than a one-visit lower bound. This prices that cursor. It does not sign the rest of the C/D inequality or raise selected kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop when the success-path meter reads=3n+4, writes=n, moves=3n+6 is certified for the parent length, or when the pinned Tape or call site disagrees with that count. Do not allocate the 3^128 parent or rerun the pooled compiler.",
+  "outcome": "partial",
+  "evidence": "verify.py prints PASS_R437_PARENT_BLANK_CURSOR with writes equal to 9475*12*3^128 and moves=3*writes+6. test_verify.py prints PASS_R437_PARENT_BLANK_CURSOR_CONTROLS. PROOF.md counts the three walks. No new kappa.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "Where does action leave the head of changed and local before their clear calls?",
+      "why_it_matters": "Those blank-returns are a different cursor start from the success-path current tape priced here, so their meters are not yet the same formula.",
+      "first_step": "Pin one source-bound postcondition for action on a fibre of length n, then rerun rewind and clear from that head.",
+      "blocked_by": "action is outside this package."
+    },
+    {
+      "question": "Can one of BILL.md's G, C or F terms be instantiated on both arms without setting the others to zero?",
+      "why_it_matters": "An exact blank-return meter still does not sign the whole C/D inequality, and the selected supplier remains complex-bound.",
+      "first_step": "Name one of gather/route, checkpoint/disposal or table-setup and pin its tariff on C and D.",
+      "blocked_by": "Those tariffs are not inputs of this package."
+    }
+  ]
+}

research/r437-parent-blank-cursor/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/selected-bit-physical-caller/inputs/pr2753/packet_engine.py",
+    "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py",
+    "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py"
+  ],
+  "commands": [
+    {
+      "argv": ["{python}", "-B", "{package}/verify.py"],
+      "timeout_seconds": 120,
+      "checks": "The pinned Tape success-path rewind-then-clear meter is reads=3n+4, writes=n, moves=3n+6 for every n through 48, for both payload bits, for the 972-bit fibre, and for miniature parents 9475*12*3^k at k=0 and k=1. The parent length 9475*12*3^128 equals 972*9475*3^124, and the fibre move count 2922 is strictly smaller."
+    },
+    {
+      "argv": ["{python}", "-B", "{package}/test_verify.py"],
+      "timeout_seconds": 120,
+      "checks": "An independent transcription of rewind, clear's opening rewind, the blanking scan and the closing rewind agrees with Tape for n through 40. Payload-only moves, a 972-bit write count, dropping 3^124, and clear without the opening rewind are rejected for the parent length."
+    }
+  ]
+}