Cursor/g20 moved correction frame 9d0c

research/g20-moved-correction-frame/PROOF.md

@@ -0,0 +1,105 @@
+# Moving one G20 correction frame does not lower the paid moment
+
+## Object
+
+The word is the emitted local scalar program in
+`research/g20-conjugation-admission/WORD.json.gz`, the output of PR #5708.
+Its scalar skeleton is the record list with `Q` and `ZERO_Q` removed.
+`ADD(a, b)` means the characteristic-2 update `x_a <- x_a + x_b`. Two such
+maps fail to commute when one destination is the other source.
+
+An interval from one `ADD(a, b)` to a later equal `ADD(a, b)` is an **A2
+conjugation of length k** when the open interval contains no `ERASE` or
+`INIT` of `a` or `b`, contains exactly `k` noncommuting `ADD` records, and
+each of those records has an A2 correction:
+
+- `ADD(b, s)` with `s ≠ a` contributes `ADD(a, s)`;
+- `ADD(d, a)` with `d ≠ b` contributes `ADD(d, b)`.
+
+`ADD(b, a)` has no correction of this form. There are 765 such intervals
+with `k ∈ {1, 2, 3}`. The constructor in #5708 places each contact and its
+correction on one common frame `f`. The contact-frame case `f` equal to the
+contact's published frame is the census in
+`research/g20-short-conjugation-screen`. This proof moves **exactly one**
+correction to a different frame and leaves every other correction on its
+contact frame.
+
+## Routes and endpoint
+
+`PATHS.json` has 2,369 routes, and every route is one edge whose third
+component is an integer rank from 1 through 7. A wire moves from its current
+frame `u` to a frame `v` only along that edge. A missing edge means the
+candidate does not emit. A nonzero scalar row pays one query of that rank;
+a zero row pays nothing and still needs the edge when it moves. The paid
+moment at exponent `t` is `Σ_r n_r r^t`.
+
+The scalar endpoint ignores frames. Every non-owned column `i` must finish
+as `e_i`, xor `e_{i-111}` when `111 ≤ i < 222`, and every owned column must
+finish at zero. The published skeleton meets that identity, and so does
+every one of the 765 corrected skeletons, because a frame change does not
+alter an ADD's operands.
+
+## Which frames can emit
+
+Fix one correction and a candidate frame `f`. The emitter writes the contact
+first and the correction immediately after it, both at `f`. A live ADD,
+meaning its source row is nonzero, routes its destination and its source to
+`f` before applying the sum. A dead ADD is omitted and does not read `f`.
+
+The contact can change only the frames of its own two operands. Therefore a
+correction operand that is not one of those two operands must already be
+able to reach `f` from its pre-contact frame, and so must each contact
+operand when the contact itself is live. The reachable frames of a wire are
+its current frame and the heads of the published edges out of that frame.
+Any `f` outside the intersection of those sets fails on the contact pair.
+The verifier tests that necessity against an independent two-event replay
+on every catalogue frame, for every contact of every interval. It then
+replays the whole word, including later routes and the final return, for
+every frame inside the intersection.
+
+## Census
+
+The fixed-frame screen reproduces the earlier count: 605 missing edges,
+153 losses `2H1 − H2`, one loss `H1 + H2 + H4`, and 6 neutral words.
+None of those 160 emitted words has a negative moment change on `(0, 1)`.
+
+The one-move screen examines 28,149 frames in the intersections above.
+28,123 do not emit. The other 26 emit, all from length-3 intervals:
+
+| Paid change | Count | Sign on `(0, 1)` |
+|---|---:|---|
+| `H4` | 2 | `4^t > 0` |
+| `5 H2 − 2 H4` | 24 | positive, proved below |
+
+No emitted change is empty or equal to the known saving `H1 − 2H2 + H3`.
+On every interval that emits at least one moved frame, a second replay tries
+every catalogue frame, not only the intersection, and obtains the same
+multiset of changes.
+
+## Sign of `5 H2 − 2 H4`
+
+Let `x = 2^t`. For `0 < t < 1`, the map `t ↦ 2^t` is strictly increasing and
+`2^0 = 1`, `2^1 = 2`, so `1 < x < 2`. The change is
+
+```text
+5·2^t − 2·4^t = 5x − 2x^2 = x(5 − 2x).
+```
+
+Here `x > 1 > 0`. Also `2x < 4`, so `5 − 2x > 1 > 0`. The product is
+therefore positive. The same bound at the closed edge `x = 2` is
+`2·2 − 5 = −1 < 0` for the factor `2x − 5`, which is the integer check
+recorded by the verifier; the open interval stays strictly above that edge.
+
+## What this does not say
+
+The screen does not rebuild the 18-call caller, the adjoint, the moduli
+101 and 10201, or the ordinary-admission arithmetic. It does not move two
+corrections in the same interval, add a route, or accept a length of four
+or more. Length four and above at the original contact frames is the
+separate result of PR #6305. Paths through neutral rewrites with correction
+frames held fixed are the separate neutral two-step obstruction. The six
+neutral one-step neighbors and the 645 common-frame expansions named in the
+#5708 README still have no executable definition in that package. No
+selected-frontier update follows. The selected conditional exponent remains
+`781451/250000000`. Full-history source preflight was not run in this
+shallow checkout; the recorded base commit and input hashes are the pins.

research/g20-moved-correction-frame/README.md

@@ -0,0 +1,128 @@
+# One moved G20 correction frame does not lower the paid moment
+
+**Negative result. No new κ.** The selected conditional exponent stays
+`781451/250000000` (`0.003125804`) in
+[certificates/selected-result.json](../../certificates/selected-result.json).
+Admitted BIT saving on this base is `17/5000`. The baseline binding check
+returned `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. That command is not a
+supplier replay.
+
+On the emitted local word of
+[PR #5708](https://github.com/CrocSwap/integer-mult-bounds/pull/5708),
+every one-to-three-contact A2 conjugation keeps its scalar endpoint when
+exactly one correction is moved onto a different frame of the published
+one-edge route table. Of the 28,149 frames that can host that meeting,
+28,123 do not emit. The 26 that emit raise the paid-query moment on the
+whole interval `(0, 1)`, by `H4` or by `5 H2 − 2 H4`. The argument is in
+[PROOF.md](PROOF.md).
+
+## Task and overlap
+
+Base `626e936ce4d61f2584316914fc71baf96940c512`, priority revision 8. Card
+`bit-helper-contract`, scope **refined**. The card says to review the
+#5679/#5708 chain and stop when a proposed cut does not improve the paid
+moment. This package is the moved-frame clause those earlier screens left
+open.
+
+Ordered eligible list for session r69, rebuilt on 2026-11-01 against that
+main. Open handoffs from the 19 October index (discussion comments
+19030045, 19030047, 19030049, and 19030053) come first and are dropped: the
+`(w, q, v_N)` consumer, the fresh T385 wrapper, the L546 six-tape bill, and
+the single-ADD retiming class are already delivered by this account or
+closed on main. Discussion #1166 through 2026-11-01 has no newer finite
+handoff index. The newest posts are H25 serializer handoffs and completed
+claims, not a replacement of the priority table. The priority table is the
+revision-8 "Next bounded decisions" table. A row stays while that table
+still states the decision. Catalogue cards not named by the table follow.
+Dropped before the cut: 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, including the port-0 G20 tariff and
+the one-to-three-contact screen.
+
+1. Complex helpers (`p104-side-correction`, `coverage-law-change`).
+2. **This package.** BIT (`bit-helper-contract`): one correction of a
+   #5708 one-to-three-contact conjugation, moved off its contact frame.
+3. New decoders and interfaces.
+4. Supplier audit (`supplier-boundary-audit`).
+5. All-size audit (`uniform-transfer-audit`).
+6. Verification tooling (`replay-runtime`).
+7. `bit-new-register-model`.
+8. `r437-carrier-integration`.
+9. `complex-rank-shape-decoder`.
+10. `complex-new-helper-inventory`.
+
+[#6290](https://github.com/CrocSwap/integer-mult-bounds/pull/6290) certified
+the 765 contact-frame conjugations. [#6305](https://github.com/CrocSwap/integer-mult-bounds/pull/6305)
+certified four or more contacts with corrections kept on the contact frame.
+`research/g20-neutral-two-step-obstruction` allows catalogue routes after a
+neutral first move and states that changed correction frames stay outside
+its quantifier. The local overlap search finds the moved-frame question in
+those three write-ups and does not find a replay of this one-move domain.
+
+## Census
+
+| Domain | Missing route | `H4` loss | `5 H2 − 2 H4` loss | Saving |
+|---|---:|---:|---:|---:|
+| One moved correction, length 1..3 | 28,123 | 2 | 24 | 0 |
+
+The fixed-frame control reproduces 605 missing routes, 153 losses
+`2H1 − H2`, one loss `H1 + H2 + H4`, and 6 neutral words. For `0 < t < 1`
+and `x = 2^t`,
+
+```text
+5·2^t − 2·4^t = x(5 − 2x) > 0
+```
+
+because `1 < x < 2`. `4^t` is positive. The verifier rejects every other
+shape, and on each interval that emits a moved frame it replays every
+catalogue frame, not only the one-edge meeting set.
+
+## Reproduce
+
+Python 3.12 and the standard library, from the repository root. The census
+finishes in about one minute here.
+
+```sh
+python3 -I -B research/g20-moved-correction-frame/verify.py
+python3 -I -O -B research/g20-moved-correction-frame/verify.py
+python3 -B scripts/research_package.py --package research/g20-moved-correction-frame --check-only
+python3 -B scripts/research_package.py --package research/g20-moved-correction-frame
+```
+
+The direct verifier prints
+
+```text
+PASS_G20_MOVED_CORRECTION_FRAME candidates=765 moved_trials=28149 missing_edge=28123 emitted_h4=2 emitted_5h2_minus_2h4=24 savings=0 no_new_kappa=true
+```
+
+Checks raise exceptions, so `-O` does not disable them. Not run: the #5708
+integration replay, the 18-call caller, adjoint columns, moduli 101 and
+10201, ordinary admission, Lean, Docker, and `make frontier6030-verify`.
+`check_research_commit.py --check-source-history` was not run: this checkout
+does not have full Git history. The pinned blobs are objects of the recorded
+base commit in this clone.
+
+## Open next questions
+
+1. Can two corrections in one interval, or one length-4 conjugation with a
+   moved frame, lower the paid moment? #6305 already excludes length 4 and
+   above when every correction stays on its contact frame. The first step is
+   one two-move pair, or one length-4 interval with one moved frame, on this
+   word and route table. No saving seed is supplied by the one-move census.
+2. Do the six neutral one-step neighbors and the 645 common-frame expansions
+   in the #5708 README have an executable rule? That sentence is still
+   local-only. The first step is to recover the search or to show that the
+   phrases name domains already certified. The published package does not
+   contain the search.
+
+## Credit
+
+The emitted word, route table, A2 relation, and the local-only 765 count are
+Ali Romman's `research/g20-conjugation-admission`, following Dugongue,
+ai-nanachi, and the retained G20 lineage named there. The contact-frame
+length-1..3 census is unpaidmoon's #6290. The length-4-and-above contact-frame
+obstruction is Nick Petalas's #6305. The fixed-frame neutral two-step
+obstruction is the package prepared for @CubeJerry. This package only moves
+one correction frame inside the length-1..3 domain.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

research/g20-moved-correction-frame/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "626e936ce4d61f2584316914fc71baf96940c512",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "research/g20-conjugation-admission/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "3877a72d8a15adb03f6492f7d2fd8fa902ecb639",
+      "sha256": "8dd441fdb9c8923df06eb5ebfda37d03e4539f2305763e688d8c7025d196c4b1"
+    },
+    {
+      "path": "research/g20-conjugation-admission/PATHS.json",
+      "usage": "input",
+      "git_blob": "efbdf632746a971f9a593f57ccbb7d2cc67a6760",
+      "sha256": "f4dd58b78121040b1f054c0f7a626b25f6ef8d39f3de044d3456ea7dea8a6a5e"
+    },
+    {
+      "path": "research/g20-conjugation-admission/LOCAL-RESULT.json",
+      "usage": "input",
+      "git_blob": "29cd42b8baa531f2598b9b8894fd514c754ed17c",
+      "sha256": "ec37bf5ddf743caf6a415bd4ce6fcd9c0f40922f0066ea79f6d2321ee0f18e96"
+    },
+    {
+      "path": "research/g20-conjugation-admission/README.md",
+      "usage": "input",
+      "git_blob": "b1655b59134ae7a5734628ba1efef6611b2dcd31",
+      "sha256": "e443b2fd7b988316953bfc7d21045690ea0d3ce9069ce1a06880f6ccfc7ec054"
+    },
+    {
+      "path": "research/g20-conjugation-admission/PROOF.md",
+      "usage": "input",
+      "git_blob": "b5147598224b8e164e7956e44c6e0fd76b7dc1ef",
+      "sha256": "8679c50955912242b9c98c6d8625ac9ca8f83660e50337cd16465ad71e507154"
+    },
+    {
+      "path": "research/g20-conjugation-admission/construct.py",
+      "usage": "input",
+      "git_blob": "c0fe9d080b76171d8ed967cbad337c596d250a23",
+      "sha256": "2922052092d9323de2c715afb66dbd33fb58c7d0eeb3b9298bab5f7b2a930cb1"
+    }
+  ]
+}

research/g20-moved-correction-frame/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "626e936ce4d61f2584316914fc71baf96940c512",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "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/g20-helper-split/README.md",
+      "research/g20-conjugation-admission/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": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.",
+    "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": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "existing_checks": [
+      {
+        "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 emitted PR5708 word, move exactly one correction of each one-to-three-contact A2 conjugation onto a different frame of the published one-edge route table and decide whether the paid-query moment falls on (0,1).",
+  "scope_change_reason": "The card says to review the #5679/#5708 chain and stop when a proposed cut does not improve the paid moment. #6290 certified contact-frame conjugations of length 1..3, #6305 certified length 4 and above at the contact frame, and the neutral two-step obstruction kept correction frames fixed. This package takes the remaining moved-frame clause on the same 765 intervals.",
+  "bottleneck_link": "A paid-moment obstruction on this exact word says the moved-frame conjugation domain does not raise the ordinary BIT component. It does not change the selected exponent.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop when every one-move frame on the 765 intervals is classified. Do not open a two-move search, a new route, or a four-contact moved-frame search in this package.",
+  "outcome": "negative-result",
+  "evidence": "python3 -I -B research/g20-moved-correction-frame/verify.py prints PASS_G20_MOVED_CORRECTION_FRAME with moved_trials=28149 and savings=0.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "Can two corrections in one interval, or one four-or-more-contact conjugation, lower the paid moment when a correction frame moves?",
+      "why_it_matters": "This certificate moves exactly one correction and stops at three contacts. #6305 already shows that four or more contacts do not save when every correction stays on its contact frame.",
+      "first_step": "Enumerate one two-move pair, or one length-4 interval with one moved frame, on the same word and route table.",
+      "blocked_by": "No such witness is supplied, and the one-move length-1..3 domain does not provide a seed that saves."
+    },
+    {
+      "question": "Do the six neutral one-step neighbors and the 645 common-frame expansions named beside the 765 conjugations have an executable rule?",
+      "why_it_matters": "The #5708 README still marks those two checks as local-only, and this package does not define them.",
+      "first_step": "Recover the search record or show that the phrases name the six paid-neutral words and the 645 frame classes already certified elsewhere.",
+      "blocked_by": "The published #5708 package does not contain that search."
+    }
+  ]
+}