Record that the R437 parent blank-return exceeds the 972-bit child.

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

@@ -0,0 +1,85 @@
+# The 972-bit R437 child does not pay the parent spectator blank-return
+
+No new κ. The selected conditional exponent stays `60403/20000000`.
+
+## What is taken as stated
+
+These integers are the ones written in `research/r437-carrier-integration`,
+pinned at the base commit. This note does not execute `physical.py` or
+`Layout.child_extents`.
+
+From NUMERICAL.md §5, the live-symbol constant is `269241600`, and a parent
+split divides that constant by `W = 28416`:
+
+```text
+269241600 / 28416 = 9475.
+```
+
+The same section writes `K = lcm(28416, 28425) * N * H_lifts = 269241600 * N * H_lifts`,
+so the lcm claim being checked is `lcm(28416, 28425) = 269241600`. The unused-row
+multiplier on the child is `U = t * 9475 * K^{D(n)-1}`.
+
+From PHYSICAL.md, the source rank-two plan has extents
+
+```text
+B = 2,
+G = 3 * 3^124,
+S = 2,
+U_parent = 9475,
+V_parent = U_parent * B * G * S * 3^4 = 9475 * 12 * 3^128.
+```
+
+The executed child uses one row and gap `3`, and `physical.py` allocates a
+tape of `972` bits for extents `(2, 3, 2)`.
+
+## Arithmetic
+
+`gcd(28416, 28425) = 3`, because `28425 - 28416 = 9` and `28416 = 3 * 9472`
+with `9472` not divisible by `3`. Therefore
+
+```text
+lcm(28416, 28425) = 9472 * 28425 = 269241600,
+269241600 = 28416 * 9475.
+```
+
+The four-atom factor in the parent formula is `3^4 = 81`. The executed gap is
+the parent gap with the `124` omitted atom coordinates removed:
+
+```text
+E = 2 * 3 * 2 * 3^4 = 972,
+V = 9475 * 2 * (3 * 3^124) * 2 * 3^4 = 9475 * 12 * 3^128.
+```
+
+The second expression equals `4 * 3^129 * 9475`, and `4 * 3^129 = 12 * 3^128`.
+Canceling `E` gives the exact ratio
+
+```text
+V / E = 9475 * 3^124.
+```
+
+Both factors are greater than `1`. Dropping the unused rows leaves `3^124`.
+Dropping the `124` coordinates leaves `9475`. Neither witness is the parent
+payload.
+
+## Blank-return comparison
+
+Comparison model, stated here and not claimed as a theorem of the predecessor:
+a fixed-tape blank-return charges at least one visit per payload symbol, and
+the executed child is charged at most once per bit of its `972`-bit packet.
+
+Under that model the parent blank-return is at least `V` and the executed
+packet's blank-return is at most `972`. Since `V = 972 * 9475 * 3^124`, the
+executed packet does not pay the parent blank-return. The local action-lane
+decreases inside the `972`-bit boundary, recorded in BILL.md, are not a
+payment of this term.
+
+NUMERICAL.md §5 already says that the live-symbol inequality does not discharge
+physical blank-return. The new content is the exact factor separating the
+executed packet from the parent payload those pages name.
+
+## Scope
+
+This does not price gather, routing, checkpointing, table setup, or the
+reverse-row coefficient. It does not assign zero to any unpaid term of
+BILL.md's C/D inequality. It does not admit the carrier and it does not change
+the selected frontier.

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

@@ -0,0 +1,120 @@
+# The 972-bit R437 child does not pay the parent spectator blank-return
+
+**Partial negative result. No new κ.** The selected conditional exponent stays
+`60403/20000000` (`0.00302015`, #4470).
+
+## Result
+
+On the source-entry identities in `research/r437-carrier-integration`, the
+full parent payload is exactly `9475 * 3^124` times the executed `972`-bit
+child packet. A fixed-tape blank-return that charges at least one visit per
+payload symbol is therefore not paid by that execution.
+
+The checked arithmetic is:
+
+```text
+lcm(28416, 28425) = 269241600 = 28416 * 9475,
+E = 2 * 3 * 2 * 3^4 = 972,
+V = 9475 * 2 * (3 * 3^124) * 2 * 3^4 = 9475 * 12 * 3^128,
+V / E = 9475 * 3^124.
+```
+
+`9475` is the unused-row multiplier in NUMERICAL.md §5. The factor `3^124`
+is the `124` atom coordinates present in the parent gap and absent from the
+executed gap `3`. Both factors are required: either one alone is a strictly
+smaller comparison. The argument is in [PROOF.md](PROOF.md). `verify.py`
+recomputes the lcm, the two extent products and the ratio. It does not import
+the carrier-integration package.
+
+## Scope
+
+Task card `r437-carrier-integration`, priority revision 7, base
+`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. Scope status is **refined**.
+
+The card asks whether the paid two-window carrier is admitted by the pooled
+compiler and the physical caller. This package takes open question 1 of
+`research/r437-carrier-integration`: bind the checked source entry's parent
+spectator multiplicity to the uniform fixed-tape blank-return. The multiplicity
+is certified, and the `972`-bit execution does not pay it. Gather, routing,
+checkpointing, table setup and the reverse coefficient stay unresolved, so
+this is not a global admission and not a supplier.
+
+Ordered eligible list for session r27, after dropping work this account
+already delivered, results on current main, questions covered by an open pull
+request, and topics already on a fork `cursor/*` branch. Open handoffs in the
+19 October index (discussion comment 19029944) come first. Priority-table rows
+whose stated next decision is still open come next.
+
+1. Downstream consumer of `(w, q, v_N)` (comment 19030045). The role-exchange
+   caller audit still has no favorable caller for that triple.
+2. Fresh T385 full-wrapper completion (comment 19030047). The admission audit
+   still records the 780-second timeout as unfinished.
+3. Six-tape head-move bill at the L546 F0 event (comment 19030049), distinct
+   from the adjacent-ADD price in #4162.
+4. `BIT.md` weighted-leaf and fixed-tape induction, the remaining shortest
+   unaudited #4100 obligation not already delivered by this account.
+5. **This package.** Parent spectator blank-return for the R437 carrier.
+
+Excluded before this cut: the retiming handoff (comment 19030053), already
+covered by #4122, #4128 and open #4567; the four-provider rebind, already on
+main in `research/mixed-provider-admission`; the QQ16 park/restore comparison,
+in open #4167 and #4172; the P104 slot, chart, encoding, fiber and port-chart
+packages, including the helper-chart half as a refinement of that row; the
+compact-switch audit #4321; the rank-8/16-child producer, already in
+unpaidmoon PRs #4151, #4156 and #4158 and in fork `cursor/rank8-*` branches;
+and the `F_2^6` difference basis, on main in `research/f2-six-difference-basis`.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 scripts/research_package.py --package research/r437-parent-spectator-blank --check-only
+python3.12 -B scripts/research_package.py --package research/r437-parent-spectator-blank
+```
+
+Direct checks:
+
+```sh
+python3 -B research/r437-parent-spectator-blank/verify.py
+python3 -B research/r437-parent-spectator-blank/test_verify.py
+```
+
+Expected marker:
+
+```text
+PASS_R437_PARENT_SPECTATOR_BLANK rows=9475 omitted_coordinates=124 executed_bits=972 parent_over_executed=9475*3^124 parent_over_executed_digits=64 lcm=269241600 blank_return_discharged=false no_new_kappa
+```
+
+`test_verify.py` prints `PASS_R437_PARENT_SPECTATOR_BLANK_CONTROLS`.
+
+Not run: Lean, Docker, the selected cold replay, `physical.py`, the pooled
+compiler, and any execution of the 9475-row parent packet.
+
+## Open next questions
+
+1. What is the exact fixed-tape visit count of one blank-return of the
+   `9475`-row parent, including cursor motion across the `124` omitted
+   coordinates, at this same source entry? The factor above is a payload
+   lower bound, not that machine's invoice. First step: one source-bound
+   cursor trace on the parent extents. Blocker: the published child bridge
+   does not allocate that parent.
+2. Can the remaining terms of BILL.md's C/D inequality be instantiated at the
+   original root without setting gather, checkpoint or table setup to zero?
+   A blank-return lower bound does not sign the whole inequality. First step:
+   name one of `G`, `C` or `F` and pin its tariff. Blocker: those tariffs are
+   not inputs here.
+
+## Credit
+
+The extents, the constant `269241600`, the quotient `9475`, the executed
+`972`-bit tape and the statement that blank-return stays charged are Chris R
+/ Clear1nsight, `research/r437-carrier-integration`, from the paid carrier in
+PR #4067 and the reverse-coefficient distinction in unpaidmoon PR #4147.
+Constructor traffic inside preparation is unpaidmoon PR #4160 and is not this
+ratio. Predecessor lineage named in the carrier package remains theirs,
+including 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-spectator-blank/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/r437-carrier-integration/PHYSICAL.md",
+      "usage": "provenance",
+      "git_blob": "ec85739460fb61c6505f9b1179f3bb3dc86cc079",
+      "sha256": "c7689d458e03853f5487a27707003698d04cbca086a503af47cd95d78cb14864"
+    },
+    {
+      "path": "research/r437-carrier-integration/NUMERICAL.md",
+      "usage": "provenance",
+      "git_blob": "1001480b0ba8da8bae4ae8f53c18d8c6aa9d7b57",
+      "sha256": "e2303eec688d963390f5df4440300bee75840c2c485d94d7342a7d2ef1430438"
+    },
+    {
+      "path": "research/r437-carrier-integration/BILL.md",
+      "usage": "provenance",
+      "git_blob": "21dedc3beab41eb66d60f4a3ddf9f4fe9d77f184",
+      "sha256": "21b81fc33d9de49a3b5abd7cb53958cc241e6cbd4374dd3996c585c7bf5e82a8"
+    },
+    {
+      "path": "research/r437-carrier-integration/physical.py",
+      "usage": "provenance",
+      "git_blob": "e314799b5c6deeb45a790534539d846a27d2d60c",
+      "sha256": "d41ea48bc8fd6e449ef17f122dfbea05adf06e7ab448063e4afd06add1152cf0"
+    }
+  ]
+}

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

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "r437-carrier-integration",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #4067 paid profile and open integration obligations; #4147 covers the reverse row coefficient. Three additional ADDs per call and all helpers remain charged. This is not a selected supplier.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "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 r437-carrier-integration source entry, certify that the parent payload is exactly 9475*3^124 times the executed 972-bit child, so a one-visit-per-symbol fixed-tape blank-return of the parent is not paid by that execution.",
+  "scope_change_reason": "Open question 1 of research/r437-carrier-integration asks to bind the checked source entry and the full parent spectator multiplicity to the uniform fixed-tape blank-return. This package certifies that multiplicity and shows the executed child does not pay it. It does not rerun the pooled compiler, rederive the reverse coefficient, or admit the carrier.",
+  "bottleneck_link": "The paid R437 exchange cannot raise the selected exponent until its parent blank-return and the other unpaid C/D terms are charged. This separates the executed packet from the parent payload by an exact factor instead of treating the local lane decreases as that charge.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop when the lcm, unused-row quotient and parent/executed ratio are certified, or when one of those stated identities fails. Do not execute physical.py, the pooled compiler, or the 9475-row parent.",
+  "outcome": "partial",
+  "evidence": "verify.py prints PASS_R437_PARENT_SPECTATOR_BLANK with rows 9475, omitted_coordinates 124, executed_bits 972, parent_over_executed 9475*3^124 and blank_return_discharged false. test_verify.py prints PASS_R437_PARENT_SPECTATOR_BLANK_CONTROLS. PROOF.md records the gcd and the extent cancellation. No new kappa.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "What is the exact fixed-tape visit count of one blank-return of the 9475-row parent, including cursor motion across the 124 omitted coordinates, at this same source entry?",
+      "why_it_matters": "The certified factor is a payload lower bound. A real cursor trace could be larger, and only that invoice can be subtracted in the C/D inequality.",
+      "first_step": "Pin one source-bound cursor trace on the parent extents B=2, G=3*3^124, S=2 and the 9475 unused rows.",
+      "blocked_by": "The published child bridge allocates the 972-bit packet and does not allocate that parent."
+    },
+    {
+      "question": "Can one of the remaining BILL.md terms G, C or F be instantiated at the original root without setting the others to zero?",
+      "why_it_matters": "A blank-return lower bound does not sign the whole C/D inequality, and the selected supplier is still complex-bound.",
+      "first_step": "Name one of gather/route, checkpoint/disposal or table-setup and pin its tariff on both arms.",
+      "blocked_by": "Those tariffs are not inputs of this package."
+    }
+  ]
+}

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

@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": ["{python}", "-B", "{package}/verify.py"],
+      "timeout_seconds": 60,
+      "checks": "lcm(28416, 28425) equals 269241600 and divides by 28416 as 9475. The executed extents (2, 3, 2) with the four-atom factor 3^4 equal 972. The parent payload with gap 3*3^124 and 9475 rows equals 9475*12*3^128, which is 9475*3^124 times 972. Dropping either factor is a strictly smaller ratio, and the 972-bit packet does not cover the parent."
+    },
+    {
+      "argv": ["{python}", "-B", "{package}/test_verify.py"],
+      "timeout_seconds": 60,
+      "checks": "An independent subtraction gcd and a differently associated product recover the same ratio. Witnesses that drop the rows, drop the 124 coordinates, drop the four-atom factor, or treat 972 bits as the parent payload are rejected."
+    }
+  ]
+}