Price the closed six-tape head moves of L546 -= L561.

research/qq16-l546-head-move/PROOF.md

@@ -0,0 +1,78 @@
+# Closed head-move bill for one six-tape subtraction
+
+The tape rules are the pinned `Tape` object in
+`research/qq16-gaussian-axis-tapes/tapes.py`: a head reads or writes only the
+cell it occupies, a move changes that head by exactly one cell, and the cell
+one past the owned interval may be occupied but not read or written. Finite
+control may hold a borrow in `{0,1}`. No second head, random access, or free
+relocation is available.
+
+## Placement
+
+Let \(N=2^n\) with \(n\ge 1\) and let \(W\ge 1\). Write \(L=NW\). The six
+lengths are the kernel's lengths \((L,L,L/2,L/2,L/2,L/2)\).
+
+| Tape | Contents | Cells |
+| --- | --- | ---: |
+| data0 | real part of L546, coordinates \(0..N-1\), little-endian | \(L\) |
+| data1 | imaginary part of L546 | \(L\) |
+| scratch0 | real part of L561, coordinates \(0..N/2-1\) | \(L/2\) |
+| scratch1 | imaginary part of L561, coordinates \(0..N/2-1\) | \(L/2\) |
+| scratch2 | real part of L561, coordinates \(N/2..N-1\) | \(L/2\) |
+| scratch3 | imaginary part of L561, coordinates \(N/2..N-1\) | \(L/2\) |
+
+Every cell is a payload bit. The two complex registers occupy \(4L\) cells and
+the six tapes have exactly \(4L\) cells, so this is a capacity-tight packing
+of those lengths. Heads start at the origin of each interval, which is cell 0.
+
+## Program
+
+On each coordinate, subtract the \(W\)-bit two's-complement integer on the
+source tape from the integer on the destination tape. The borrow resets at
+every coordinate boundary, so it does not cross from scratch0 to scratch2.
+Process the first \(N/2\) coordinates, step each data head one cell onto the
+second half, process the remaining coordinates, then walk every head back to
+its origin. Source cells are read and not written.
+
+The forward scan of a tape of length \(L_t\) makes \(L_t-1\) moves and finishes
+on the last cell. The return makes another \(L_t-1\) moves. Data tapes are one
+interval of length \(L\), so the single step between the halves is one of those
+\(L-1\) forward moves, not an extra crossing. The move total is
+
+\[
+\sum_t 2(L_t-1) = 2\bigl(2(L-1)+4(L/2-1)\bigr) = 8L-12 = 8NW-12.
+\]
+
+Each of the \(4L\) payload cells is read once, and each of the \(2L\)
+destination cells is written once. So READ \(=4NW\), WRITE \(=2NW\), and the
+cell-action total is \(14NW-12\).
+
+## Matching lower bound
+
+Work in the model above, with heads required to start and end at cell 0.
+
+Changing any one payload bit changes the coordinatewise difference in
+\((\mathbb{Z}/2^W\mathbb{Z})^2\). A cell that is never read cannot affect a
+later write, so every payload cell is read. The output bit string is not a
+function of the minuend alone, so every destination cell must be written:
+otherwise that cell would keep a bit that is not always the difference bit.
+Therefore every cell of every tape is visited.
+
+On one tape the farthest cell is \(L_t-1\). A unit-step walk from 0 to \(L_t-1\)
+and back to 0 has length at least \(2(L_t-1)\), and that shortest walk already
+visits every earlier cell. Summing over the six lengths gives at least
+\(8NW-12\) moves. The program meets the bound, so the closed-return move count
+is sharp for this placement.
+
+The same counting gives READ at least \(4NW\) and WRITE at least \(2NW\). Both
+are achieved. Stepping one past the last cell, as the axis kernel does, would
+add two moves per tape and is not required here.
+
+## What is not charged
+
+Copying L561 onto the scratch windows, returning those bits to a native home,
+zeroing scratch for a later kernel, the preceding axis factor (MOVE \(=20NW\)
+in the pinned kernel), frame climbs, and the four scalar-work steps of the
+same-frame coefficient count are outside this bill. \(W\) is the component
+width of the placement. This note does not claim that event 9895 uses a
+particular \(W\), including the \(W=5\) kernel fixture.

research/qq16-l546-head-move/README.md

@@ -0,0 +1,141 @@
+# Sharp six-tape head moves for `L546 -= L561`
+
+**Scoped tariff. No new κ.** The selected conditional exponent stays
+`60403/20000000`. Same-frame legality of this ADD does not make its tape-head
+bill zero.
+
+## Result
+
+After both complex registers already occupy the six tapes of the pinned axis
+kernel, the coordinatewise subtraction `L546 -= L561` has the closed-return
+cell-action bill
+
+| | count |
+| --- | ---: |
+| READ | \(4NW\) |
+| WRITE | \(2NW\) |
+| MOVE | \(8NW-12\) |
+
+Here \(N=2^n\) with \(n\ge 1\), \(W\ge 1\) is the signed component width, and
+every head starts and ends at its interval origin. The move count equals
+\(\sum 2(L_t-1)\) over the six kernel lengths
+\((NW, NW, NW/2, NW/2, NW/2, NW/2)\), so it is sharp for that placement.
+L561's cells are unchanged. The argument is in [PROOF.md](PROOF.md).
+
+data0 and data1 hold L546. The four half-length scratch tapes hold L561, split
+after coordinate \(N/2\). Those six lengths have exactly the \(4NW\) cells the
+two registers need. Borrow stays in finite control and resets on each
+coordinate. The schedule never steps one past the last cell.
+
+For the kernel fixture size \(N=512\), \(W=5\), the formula gives
+MOVE \(=20468\), READ \(=10240\), WRITE \(=5120\). That width is the kernel
+fixture's width, not a measured width of native event 9895.
+
+## Scope
+
+Task card `joint-query-controller`, priority revision 7, base
+`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. Scope status is **refined**.
+
+This is item 2 of the eligible list below. It answers open question 1 of
+`research/qq16-adjacent-add-bill` and the layout half of discussion comment
+19030049 that remains after `research/qq16-f0-first-caller` bound event 9894.
+It does not repeat #4162's four scalar-work steps, and it does not price the
+matched park/restore comparison left by #4166.
+
+Ordered eligible list for session r24. Dropped first: work this account
+already delivered, results closed on current main, questions covered by an
+open pull request, and topics already on a fork `cursor/*` branch. Open
+handoffs from the 19 October index come first, with a closed smallest task
+removed and a still-open remainder kept when it is distinct. Priority-table
+rows whose stated next decision is still open come next. Catalogue cards that
+are not already one of those rows follow.
+
+1. A caller that accepts `(w, q, v_N)` without restoring the original source
+   slots and without repaying the saving (discussion comment 19030045). The
+   q-field cleanup in `research/p104-residual-consumer` and the 192-transport
+   return in `research/p104-role-exchange-caller-audit` leave that caller open.
+   Distinct from the encoded-exit standard-Y consumer and from `(N-P)⊗M`.
+2. This package.
+3. Four-provider ordinary/outer rebind (`supplier-boundary-audit`; open
+   question 1 of `research/staged544-mixed-fourth-entry`). The idle-cost block
+   is recorded; the four-id rebind is not.
+4. Matched park/restore bill for the #4166 caller (`joint-query-controller`
+   as stated in the priority table; open question of
+   `research/qq16-caller-install`). Open #4167 and #4172 do not price it.
+5. R437 fixed-tape preparation and parking bill (open question 1 of
+   `research/r437-carrier-integration`). The reverse coefficient is already
+   covered.
+6. `#4091` model equivalence on the later 1090-call fill
+   (`independent-moment`).
+7. The PR2809 encoded-stack visited-space bound left by
+   `research/bit-stock-recurrence-audit`. The algebraic BIT.md induction is
+   closed there. CRT join, row-field movement, the half-gap budget and the
+   uniform evaluator are already on fork `cursor/*` branches or in the listed
+   unpaidmoon PRs.
+
+Excluded before this cut: the fresh T385 wrapper (comment 19030047), closed
+by `research/t385-r437-copy-audit`; the retiming handoff (comment 19030053),
+already covered by #4122, #4128 and later shear work; `p104-side-correction`
+as its own row, because the slot, chart, encoding, fiber and standard-Y
+pieces are already certified; `formal-interface-lemma`, because #4321 audited
+the compact-switch contract and a fork branch holds the sharp-window density.
+
+## Not charged
+
+- Moving L561 from its native home onto these scratch windows.
+- Copying it back, or clearing scratch for a later kernel.
+- The preceding axis kernel (MOVE \(=20NW\) on its own contract) and the
+  frame climb of event 9894.
+- A native component width for event 9895. The formula keeps \(W\).
+- Park/restore, F17 consumption, and any change to κ.
+
+Unknown placement cost is not zero. This is a conditional tariff for one
+stated packing, not a physical embedding extracted from the native word.
+
+## Reproduce
+
+From the repository root, CPython 3.12, standard library only:
+
+```sh
+python3 scripts/research_package.py --package research/qq16-l546-head-move --check-only
+python3.12 -B scripts/research_package.py --package research/qq16-l546-head-move
+```
+
+Directly:
+
+```sh
+python3 -B research/qq16-l546-head-move/verify.py
+```
+
+Expected:
+
+```text
+PASS_QQ16_L546_HEAD_MOVE move=8*N*W-12 read=4*N*W write=2*N*W bound=sum_2(L_t-1) sharp=yes placement=data_full_scratch_halves heads=origin L561=preserved no_new_kappa
+```
+
+The verifier loads the pinned tape object, checks the bill on every
+\(N=2^1..2^7\) and \(W=1..5\), checks signed fixtures including \(N=512\),
+\(W=5\), rejects a non-unit move, and flips every payload cell of one
+\(N=2\), \(W=2\) instance.
+
+## Open next questions
+
+1. What does it cost to place L561 onto the four scratch windows before this
+   subtraction? The move bill above starts only after that placement. The
+   first step is to name the intervals that actually hold L561 at event 9895.
+   PR #3932 leaves those intervals unbound.
+2. If the next kernel needs zero scratch, L561 must be copied out before that
+   clear. The first step is to bind the next tape-using event after 9895 to
+   these six windows. No such binding is in the forward word's frame bill.
+
+## Credit
+
+The six-tape rules and the axis-kernel lengths are Clear1nsight's
+`research/qq16-gaussian-axis-tapes` (PR #3884). The first-caller cut at event
+9894 is PR #3932. The same-frame scalar price of event 9895 is unpaidmoon's
+#4162 (`research/qq16-adjacent-add-bill`), whose open question 1 is the
+question answered here. Ali Romman's QQ16 lineage and Nick Petalas's numerical
+formats are the retained background; they are not re-proved.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human or formal-kernel review.

research/qq16-l546-head-move/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/qq16-gaussian-axis-tapes/tapes.py",
+      "usage": "input",
+      "git_blob": "661aafb229dbc280bc667fdc0f22b438b85c634b",
+      "sha256": "a3ad668b94d44ff1b9d7093e95c5af3ea0d80cdb798365ea7631c0e2a3dcae10"
+    }
+  ]
+}

research/qq16-l546-head-move/TASK.json

@@ -0,0 +1,96 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "joint-query-controller",
+    "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/qq16-caller-install/README.md"
+    ],
+    "methods": [
+      "Derive the matched whole-caller physical bill for installed and baseline protocols.",
+      "Change the actual demanded observations and prove a cheaper legal producer/consumer contract."
+    ],
+    "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.",
+    "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.",
+    "allowed_variations": [
+      "One paid query, one changed first pair, or one precisely specified affine helper state.",
+      "A counterexample or lower bound for that exact proposed repair.",
+      "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain."
+    ],
+    "scope_change_triggers": [
+      "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.",
+      "Treating cover-map counts as zero-cost physical address operations.",
+      "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.",
+      "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.",
+      "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.",
+      "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving."
+    ],
+    "overlap_terms": [
+      "QQ16",
+      "joint-query",
+      "changing-chart controller",
+      "selected observation",
+      "1969",
+      "2540",
+      "early record",
+      "output-bank retention",
+      "complete native decoder",
+      "2965",
+      "producer defect",
+      "dirty-helper range",
+      "F17 consumer",
+      "4166",
+      "qq16-caller-install"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.",
+        "evidence": "research/qq16-caller-install/README.md",
+        "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.",
+        "status": "author-checked",
+        "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Once L546 and L561 occupy the six kernel tapes, what is the exact closed-return head-move bill of the coordinatewise subtraction L546 -= L561?",
+  "scope_change_reason": "The card asks for a matched whole-caller bill or a cheaper demand. Open question 1 of research/qq16-adjacent-add-bill, continuing discussion comment 19030049, asks only for the head moves of this one ADD after the registers are already on the six-tape windows. The same-frame scalar price is already #4162. This package answers that head-move question and stops. It does not compare park/restore protocols or change the demanded observations.",
+  "bottleneck_link": "The first rank-positive F0 climb is already followed by a legal same-frame ADD. A zero frame delta does not make the physical layout bill zero. The sharp six-tape move count is the missing local charge for that pair; it is not a supplier admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop when the closed-return subtraction matches the line-tour lower bound on the kernel's six lengths. Do not price copying L561 onto those windows, the preceding axis kernel, later cleanup, or the matched parent park/restore bill.",
+  "outcome": "partial",
+  "evidence": "verify.py prints PASS_QQ16_L546_HEAD_MOVE with MOVE=8NW-12, READ=4NW, WRITE=2NW. The count meets sum 2(L_t-1) over the six kernel lengths, and random signed fixtures reproduce coordinatewise two's-complement subtraction while restoring every head and leaving L561 unchanged.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok 4.7 wrote the scan, the lower-bound note and this card. The tape object is the pinned predecessor module. No independent human or formal-kernel review.",
+  "open_questions": [
+    {
+      "question": "What is the head-move cost of placing L561 onto the four half-length scratch windows from its native home, with heads returned, before this subtraction starts?",
+      "why_it_matters": "The bill above assumes that placement is already paid. If the copy is longer than the subtraction, it dominates this pair.",
+      "first_step": "Name the source intervals and origins that actually hold L561 at event 9895, then scan-copy each component into scratch0/scratch2 or scratch1/scratch3 and return those heads.",
+      "blocked_by": "PR #3932 and research/qq16-f0-first-caller leave L546 and L561 physical intervals unbound."
+    },
+    {
+      "question": "Does the next kernel on these same six tapes require the scratch windows to be zero, and what extra closed scan does that clear cost?",
+      "why_it_matters": "This subtraction leaves L561's bits in scratch. A later axis kernel in research/qq16-gaussian-axis-tapes demands scratch it may destroy, but a live L561 cannot be wiped without a copy-out.",
+      "first_step": "Find the next tape-using event after 9895 that needs these four scratch windows and decide whether L561 still occupies them.",
+      "blocked_by": "No native event after 9895 is bound to these six physical tapes."
+    }
+  ]
+}

research/qq16-l546-head-move/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/qq16-gaussian-axis-tapes/tapes.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Closed-return coordinatewise subtraction on the six kernel tape lengths: MOVE=8NW-12 equals the line-tour lower bound, READ=4NW, WRITE=2NW, heads and L561 cells restored, signed fixtures match, and every payload cell on a small instance is necessary."
+    }
+  ]
+}