Record that the #5718 boundary functionals differ and force cleanup o…

research/p104-boundary-functional-review/PROOF.md

@@ -0,0 +1,53 @@
+# The #5718 boundary functionals differ, and cleanup order is forced
+
+## Pinned objects
+
+The source word is the `WORD.json.gz` member
+`research/p104-temporal-updates/WORD.json.gz` inside
+`research/p104-two-boundary-helper-split/inputs/pr5713-source.tar`.
+Its canonical JSON SHA256 is
+`32adce6656e49aa020d3e6317f1c45c11fccadeeb67a8d506172d101703d2138`.
+The published candidate is
+`research/p104-two-boundary-helper-split/WORD.json.gz`, canonical SHA256
+`a1c8277189a811546bdc7b147d72e6a594504ff9585c9bf59a5681aa873abb01`.
+Neither file is modified. The predecessor constructor is not imported.
+
+## Two functionals
+
+Replay the source through event 14330, the pinned move
+`MOVE 119 602 -> 684`. Rows start at the identity. Write `a` for row 708
+and let `c` be half of row 154. The input carrier is `h = a + c`. It has 88
+terms, coefficient 1 on register 708, and its only live main-input terms are
+`(x154 + x217) / 4`. The input nuisance is `k = h - e708`, with 87 terms.
+
+On the published word, event 17523 is the unique
+`743 += 146/2` at frame 127. Let `t` be row 743 immediately after that
+event. The output nuisance is `g = e743 - t`. Direct replay gives
+`g = k - c`. The partner covector `c` is nonzero, so `g ≠ k`. The frame-3
+prefix of the published word is exactly the instruction list for `-k`,
+followed by `126 -= 2·708` and `188 += 2·708`. Thus the input side really
+is `k`, while the live 146 correction removes `g`.
+
+## Order
+
+The next three instructions are, in order,
+`126 += 2·743`, `188 -= 2·743`, and `743 -= 146/2`.
+No later instruction reads 126, 188 or 743. Later writes of 126 and 188 are
+ADDs at frame 127, so they commute with the first two restorations. The third
+instruction replaces `t` by `e743`, and `t - e743 = -g`.
+
+Doing that replacement first and then adding `±2·e743` instead of `±2·t`
+changes the 126 row by `2(t - e743) = -2g` and the 188 row by `2g`. Both
+differences are nonzero. The full scalar endpoint walk accepts the published
+order on every public and owned row. The same walk on the swapped triple
+fails exactly rows 126 and 188. Changing only the last coefficient from
+`-1/2` to `+1/2` leaves 126 and 188 corrected, because those restorations
+already used `t`, and fails exactly row 743. The order is what couples the
+three registers; the sign repairs only the new helper.
+
+## What this does not say
+
+The paid histogram is untouched by this audit, and no new conditional
+exponent is computed. Native maps, the physical caller, compiler closure,
+precision and the outer ledger stay on the predecessor's obligations.
+Unknown costs there are not zero. The selected frontier is unchanged.

research/p104-boundary-functional-review/README.md

@@ -0,0 +1,95 @@
+# Independent review of the #5718 boundary functionals
+
+**Scoped verification. No new κ.** The selected conditional exponent stays
+`781451/250000000` (`0.003125804`) in
+[certificates/selected-result.json](../../certificates/selected-result.json).
+
+On the pinned PR5718 word, the input nuisance `k` and the output nuisance
+`g = k - c` are different covectors. The three early cleanup operations
+restore every scalar endpoint only in the published order. Moving
+`743 -= 146/2` ahead of the 126 and 188 restorations fails exactly those
+two rows. [PROOF.md](PROOF.md) records the identities. The checker replays
+the pinned source and final words and does not import the predecessor
+constructor.
+
+## Task and overlap
+
+Base commit `626e936ce4d61f2584316914fc71baf96940c512` on canonical
+`CrocSwap/integer-mult-bounds` main. Priority revision 8. Catalogue card
+`p104-side-correction`. Scope status: **refined**.
+
+The card asks whether a legal helper split improves the complete invoice.
+This package does not search for another split. It answers the first open
+question of `research/p104-two-boundary-helper-split`: a separate reviewer
+checks the two boundary functionals and the early cleanup order.
+
+Session selection, in first-mention order of `open_questions` from the
+`TASK.json` files of packages named by PR number in revision-8
+`docs/research/current-priorities.md`, skipping #5599 because that PR is
+the selected frontier rather than an open assignment. Questions answered
+by a later merged package are dropped:
+
+1. #5679: Can a cut use a different physical role for the early output?
+2. #5679: Can the changed split word enable another paid-query removal?
+3. #5679: Can a stronger Gaussian caller consume the completed BIT component?
+4. #5708: Can noncoordinate public input contracts give another split?
+5. #5708: Can a stronger Gaussian caller consume this BIT component?
+6. #5718: Can a separate reviewer verify the different input/output bases and early cleanup order?
+7. #5718: Do other pairs of legal boundary functionals support profitable helper splits?
+8. #5718: Can the retained framework assumptions be resolved?
+9. #5615: Does a current source cut gain a channel under the full dyadic criterion?
+10. #5717: Can the same explicit-inventory audit be rebound to a successor with a changed caller or helper ABI?
+
+Item 6 is this package. Dropped before this list: #5708's longer-identity
+question, answered for one-to-three contacts by #6290 and for four or more
+fixed-frame contacts by #6305, and #5611's physical-target question,
+answered by #6297. The 19 October handoff index in discussion #1166 is
+already closed. The later H25 serializer handoffs are open engineering
+lanes on their own draft PRs and are not this finite scalar question.
+
+The phrase "early cleanup order" occurs only in the #5718 README and task
+file. #5844 checks a different claim: the #5719 causal certificate does not
+transfer onto this word.
+
+## Validation
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B scripts/research_package.py --package research/p104-boundary-functional-review --check-only
+python3 -I -B research/p104-boundary-functional-review/verify.py
+python3 -I -O -B research/p104-boundary-functional-review/verify.py
+python3 -B scripts/research_package.py --package research/p104-boundary-functional-review
+```
+
+The direct runs and the registered replay print
+`PASS_P104_BOUNDARY_FUNCTIONALS_DIFFER_AND_CLEANUP_ORDER` with term counts
+`carrier=88 input=87 output=118 partner=171`, then
+`PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+Controls: the published order has no endpoint failure; inverse-first cleanup
+fails exactly rows 126 and 188; the opposite 146 sign fails only row 743;
+the recorded witness carrier, cleanup triple and 118-term output functional
+must match the replay. A zero partner covector would make the two
+functionals equal and fail the difference check.
+
+Not run: the #5718 native maps, physical caller, pricing adapter, ordinary
+admission, Lean, Docker, and `scripts/research_selected_baseline.py` beyond
+reading the selected record.
+
+## Credit
+
+The word, witness and source archive are flyingviper's
+`research/p104-two-boundary-helper-split`, following Ali Romman's PR5713
+and Joel Pulikkan / GamingPuzzled's PR5684. No predecessor file is modified.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+## Open next questions
+
+1. Do other legal boundary pairs at another coframed cut improve the signed
+   bill? The first step is one new cut whose input and output functionals
+   are written down before any search. This review does not supply that cut.
+2. Does the scalar order obstruction still fail after native maps and the
+   physical caller? The first step is to replay the predecessor caller on
+   the three-instruction swap alone. Those engines were not run here.

research/p104-boundary-functional-review/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "626e936ce4d61f2584316914fc71baf96940c512",
+  "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/p104-two-boundary-helper-split/PROOF.md",
+      "usage": "input",
+      "git_blob": "0eeb4ce7ecb8a558cf62f3052ed4e80c5da198a2",
+      "sha256": "83c86475a632a92497d2c7a149cca189b08412dfbb59efeac5a0967326ef567e"
+    },
+    {
+      "path": "research/p104-two-boundary-helper-split/WITNESS.json",
+      "usage": "input",
+      "git_blob": "88d25590010052ebe4da2b575803f618241500eb",
+      "sha256": "0e78b2fbc34b52662f7b05733e3a3132599c55486dd215d7b96aaaf0c1bff804"
+    },
+    {
+      "path": "research/p104-two-boundary-helper-split/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "4db015aca34ea957dd8b3b4d7ae4fa12b89934f8",
+      "sha256": "cff7196f8b168c4ebf8227185eed98387b66ec5db0179108adfea4045775cc31"
+    },
+    {
+      "path": "research/p104-two-boundary-helper-split/inputs/pr5713-source.tar",
+      "usage": "input",
+      "git_blob": "ec8f4bccaca147bc80cec078147fb95bc515036e",
+      "sha256": "c4d8d0bcd6231eb4539a76d66b0dbd465313cbc50d279ca974a55fecb935d544"
+    }
+  ]
+}

research/p104-boundary-functional-review/TASK.json

@@ -0,0 +1,123 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 8,
+  "base_commit": "626e936ce4d61f2584316914fc71baf96940c512",
+  "original_card": {
+    "id": "p104-side-correction",
+    "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "research/p104-helper-subspace-splits/README.md",
+      "research/dyadic-helper-channel-capacity/README.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "P104",
+      "helper basis",
+      "helper split",
+      "5718",
+      "dyadic capacity"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4133: literal-slot defect",
+        "evidence": "research/p104-literal-slot-defect/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4136: uniform commutation gap",
+        "evidence": "research/p104-uniform-commutation-gap/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4140: uniform encoding gap",
+        "evidence": "research/p104-uniform-encoding-gap/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance",
+        "evidence": "research/p104-source-chart-shortcut/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4154: fiber-tag seam mismatch",
+        "evidence": "research/p104-fiber-tag-seam/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "On the pinned PR5718 word, show that the input nuisance k and the output nuisance g=k-c differ, and that moving the 146 inverse ahead of the 126/188 restorations fails exactly those two scalar endpoints.",
+  "scope_change_reason": "The card asks for a legal split that improves the invoice. This package does not search for another split. It answers the first open question of PR5718: an independent check of the two boundary functionals and the early cleanup order.",
+  "bottleneck_link": "The #5718 gain replaces one H9 target by H2+H7 only if these two different functionals and this cleanup order are legal. Reversing the order loses the endpoint identity, so the split is not available under a same-functional or swapped-order contract.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one source-bound verification of these two functionals and the three-instruction order. Do not search for another cut or rerun the caller.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and the verifier's endpoint and order controls",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance for the independent replay, writing and checks. Not independent human or formal acceptance.",
+  "open_questions": [
+    {
+      "question": "Do other legal boundary pairs at another coframed cut improve the signed bill?",
+      "why_it_matters": "The reviewed split is one cut. A second pair would be a different construction.",
+      "first_step": "Write one new cut's input and output functionals before searching.",
+      "blocked_by": "No second cut is supplied here."
+    },
+    {
+      "question": "Does the scalar order obstruction still fail after native maps and the physical caller?",
+      "why_it_matters": "Endpoint failure on the scalar word does not by itself price native or caller repairs.",
+      "first_step": "Replay the predecessor caller on the three-instruction swap alone.",
+      "blocked_by": "Those engines were not run."
+    }
+  ]
+}

research/p104-boundary-functional-review/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-two-boundary-helper-split/PROOF.md",
+    "research/p104-two-boundary-helper-split/WITNESS.json",
+    "research/p104-two-boundary-helper-split/WORD.json.gz",
+    "research/p104-two-boundary-helper-split/inputs/pr5713-source.tar"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 90,
+      "checks": "Source and final hashes, distinct input and output nuisances, published endpoints, inverse-first failure on rows 126 and 188, opposite-sign failure on row 743 only, and witness agreement."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 90,
+      "checks": "The same identities under optimized bytecode. Failures are exceptions, so they stay active."
+    }
+  ]
+}