Review the staged544 fixed-frame new-gap reduction.

research/staged544-two-add-reduction-review/README.md

@@ -0,0 +1,87 @@
+# Independent review of the staged544 new-gap reduction
+
+**Negative result.** No new κ. The selected conditional κ stays
+`0.001672660197076918`. This is an audit of one reduction, not a supplier
+and not a universal two-ADD obstruction.
+
+## Scope and evidence
+
+PR #3942 certifies that a radius-one first ADD, followed by any legal second
+ADD, does not improve the raw rank moment on either pinned PR #3734 provider.
+Its released handoff asks for an independent challenge of the
+interaction/new-gap reduction and of exhaustive first-frame coverage.
+`verify.py` does not import `search.py`.
+
+On both providers the checker establishes:
+
+- Every radius-one first-move interval has quotient rank at most 3. A closed
+  quotient basis spans the upper frame, and a separate one-vector walk finds
+  exactly the Gaussian number of intermediate subspaces. There are 1292
+  intervals: 1078, 186, 3 and 25 of quotient ranks 0, 1, 2 and 3.
+- Every fixed-frame adjacent pair that shares a register has equal declared
+  frames. The 181 unequal shared pairs are nested on the trace: the later
+  gate's incoming frame is the earlier gate's frame, so they are not
+  fixed-frame swaps.
+- For every scalar-legal third ADD at the swapped interior cut:
+  - if it meets both swapped gates, its price list equals a separately coded
+    bridge formula;
+  - if it meets only the right gate, only the left gate, or neither, that
+    price equals the original-word price at the cut named in PROOF.md §3
+    (after both, before both, or the same cut).
+- The bridge rows that are not identically zero are exactly the four published
+  restore rows `(section=restore, pair=182/191/192/193, third=178, dimension=8)`
+  with delta `(0, 2, -1, 0, ...)`. Each passes the predecessor nonnegative
+  curvature certificate, so none is a raw-moment saving.
+- Counts tied to the published census: 4709 fixed pairs, 14966 scalar-legal
+  bridge gates, 14693 bridge dimensions.
+
+One published nonzero row was recomputed from `apply_move` plus a fresh trace.
+Replacing the predicted cut of an only-left gate by the interior cut changes
+the price, so the localisation test is not vacuous. Two disjoint ADDs cross
+exactly when their endpoint pairs are disjoint; that is the interaction
+reduction's crossing hypothesis, checked as algebra on `crosses`, not as the
+11.9-million-row variable census.
+
+The variable-frame second-move census and same-gate collapse are not replayed.
+Longer first displacements, illegal intermediate words, and changed native
+boundaries stay outside PR #3942 and outside this review.
+
+## Reproduce
+
+From the repository root, CPython 3.12:
+
+```sh
+python3.12 -B research/staged544-two-add-reduction-review/verify.py
+python3.12 -B scripts/research_package.py --package research/staged544-two-add-reduction-review
+```
+
+Expected marker:
+
+```text
+PASS_STAGED544_TWO_ADD_GAP_REVIEW
+```
+
+The two provider words and `vendor/retiming.py` are the bytes of PR #3942 at
+`1416f8cd6bfb2f2eb9aa5cc22f0388a85fdbac91`. `verify.py` checks their SHA256
+before use. Recorded local runtime is about 30 seconds. Not run: the
+predecessor's 11.9-million-row variable census, Lean, Docker, and the selected
+cold replay.
+
+## Open next questions
+
+1. **Disjoint second moves.** Prove or price the section-2 claim that a second
+   ADD on registers missed by the first moved gate has delta equal to its
+   original single-move delta. The crossing algebra is checked here; the
+   summed histograms are not. The blocker is the size of that census.
+2. **Same-gate collapse.** Show that choosing the moved ADD again undoes every
+   radius-one first move, not only a sample. A failed undo would be a word the
+   reduction never prices.
+
+## Credit
+
+The reduction, trace, and both provider words are Chris R / Clear1nsight, PR
+#3942, with the PR #3886 single-move rules and the PR #3734 providers from
+dataisfire. Jeremy Kothe's retiming line, Dugongue's rank-two exchange, and
+the frame-contract auditors credited in that package are unchanged. New review
+code by unpaidmoon, with substantial assistance from Cursor Grok 4.7.
+Apache-2.0. No independent human or formal-kernel review is claimed.

research/staged544-two-add-reduction-review/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/staged544-two-add-reduction-review/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "scalar-to-moment",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "scalar-to-moment",
+    "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?",
+    "starting_points": [
+      "research/r439-bsection-stars-seed01/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Derive the changed legal frame itinerary and exact child histogram.",
+      "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract."
+    ],
+    "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/r439-bsection-stars-seed01/verify.py"
+      ],
+      "expected": "PASS_R439_BSECTION_STARS",
+      "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.",
+    "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.",
+    "allowed_variations": [
+      "One existing scalar simplification and one proposed frame-path change."
+    ],
+    "scope_change_triggers": [
+      "Submitting only another scalar count as completion of a paid-profile task."
+    ],
+    "overlap_terms": [
+      "scalar simplification",
+      "paid profile",
+      "R439"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Independently check the interaction and new-gap reductions for the radius-one fixed-frame two-ADD class on both pinned PR3734 providers, including exhaustive first-frame coverage.",
+  "scope_change_reason": "The card asks for one scalar simplification's paid histogram. PR #3942 already certifies that this two-ADD class does not improve the raw rank moment, and its released handoff asks for an independent challenge of the reduction rather than another census. This package answers that review. A missed legal interior price would be a scalar move whose histogram was never tested.",
+  "bottleneck_link": "A two-ADD retiming changes the exponent only if its rank histogram improves. Confirming that every legal fixed-frame interior price is either an old single-move price or one of the four losing bridge rows blocks that scalar route from being recounted as a paid-profile gain.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after both providers' fixed-frame interior prices and radius-one frame intervals are checked. Do not replay the 11917718 variable-frame second-move rows or search a longer first displacement.",
+  "outcome": "negative-result",
+  "evidence": "Both providers: 4709 fixed pairs, 14966 scalar-legal bridge gates, 14693 bridge dimensions, max quotient rank 3, and the same four losing restore rows published by PR #3942. No omitted interior price and no bridge-formula mismatch. One-vector subspace counts match the Gaussian binomials on all 1292 intervals.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok 4.7 wrote the independent checker and the package text. The predecessor trace oracle and both provider words are unchanged bytes from PR #3942.",
+  "open_questions": [
+    {
+      "question": "Does every changed-frame first ADD, followed by every legal second ADD on a disjoint register set, have combined raw-moment delta equal to the sum of two original single-move deltas?",
+      "why_it_matters": "PROOF.md section 2 uses that identity to skip the disjoint pairs. This package checks only the crossing algebra, not the summed histograms.",
+      "first_step": "Reprice one changed-frame first word against the frozen single-move receipt, restricted to ADDs whose touched sets miss the moved gate.",
+      "blocked_by": "The variable-frame census is about 11.9 million rows and is outside this review's stop rule."
+    },
+    {
+      "question": "Does selecting the same ADD twice always collapse to an original single-ADD candidate on every radius-one first move?",
+      "why_it_matters": "That is the other half of the interaction reduction. A failed undo would be a word the census does not price.",
+      "first_step": "Apply one radius-one move and its inverse on every changed first frame, and compare the restored gate list.",
+      "blocked_by": "Needs the variable first-move list. The fixed-frame class checked here does not move a frame, so the same-gate case is a different branch."
+    }
+  ]
+}

research/staged544-two-add-reduction-review/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Both PR3734 providers: fixed-frame interior localisation, bridge-formula agreement, published nonzero rows, quotient-rank Gaussian counts, nesting of unequal shared pairs, trace oracle, and a wrong-cut sensitivity control."
+    }
+  ]
+}