Record that length-4 G20 conjugations do not emit after one moved cor…

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

@@ -0,0 +1,118 @@
+# Length-4 G20 conjugations do not emit after one moved correction
+
+## Object
+
+The word is the emitted local scalar program in
+`research/g20-conjugation-admission/WORD.json.gz`, the output of PR #5708.
+Drop `Q` and `ZERO_Q`. What remains is 11,930 scalar records on 685 roles.
+`ADD(a, b)` is the characteristic-2 update `x_a <- x_a + x_b`.
+
+An interval from one `ADD(a, b)` to a later equal `ADD(a, b)` is an **A2
+conjugation of length 4** when the open interval contains no `ERASE` or
+`INIT` of `a` or `b`, contains exactly four 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. The constructor deletes the two
+outer gates and writes each contact immediately followed by its correction.
+On the contact-frame word every correction keeps the contact's published
+frame. This proof moves **exactly one** of the four corrections onto a
+different frame of the published one-edge route table and leaves the other
+three on their contact frames.
+
+There are 119 such intervals. PR #6305 already classifies every length of
+four or more while every correction stays on its contact frame. PR #6337
+moves one correction only for lengths one through three. Neither statement
+covers a length-4 word with one moved frame.
+
+## Scalar endpoint
+
+For a contact `C` with correction `R`, the elementary identity is
+`G C G = C R`, and `R` commutes with `C`. Every noncontact commutes with the
+outer gate `G`, and `G^2 = I`, so deleting the two outer gates and replacing
+each contact by `C R` preserves the scalar map at every contact count. A
+frame is not an operand, so the same skeleton with one correction frame
+changed has the same scalar map.
+
+The verifier checks that map on the published word, on all 119 contact-frame
+skeletons, and on every moved skeleton that passes the local meeting test.
+Each row is a 685-bit mask, initially `e_i`. ADD is exact XOR. Only an owned
+role may be erased, and INIT requires that role's row to be zero. The
+expected final row is zero on owned roles. On every other role it is `e_i`,
+with the extra term `e_(i-111)` for `111 ≤ i < 222`.
+
+## Routes
+
+`PATHS.json` has 2,369 routes and 636 frames. Every route is one edge of
+integer rank 1 through 7. A live ADD, meaning its source row is nonzero,
+routes its destination and then its source to its frame before the sum. A
+missing edge rejects the word, including when the moved row is zero. A dead
+ADD is omitted and does not read its frame. At the end every public role
+returns to its final frame, and every owned role must be zero. The paid
+moment at exponent `t` is `Σ_r n_r r^t`. The published word pays
+
+```text
+{1: 1281, 2: 1338, 3: 58, 4: 57, 5: 102, 6: 10}.
+```
+
+## Why the meeting filter is exhaustive
+
+Fix one correction and a candidate frame `f` other than its contact frame.
+The snapshot is the row masks and wire frames immediately before that
+contact on the contact-frame skeleton. Earlier corrections stay on their
+contact frames, so this snapshot is the pre-contact state of the one-move
+word. The contact and its correction are the next two ADD records, both at
+`f`.
+
+Every wire that the contact or the correction must move is therefore a wire
+that has to reach `f` from its snapshot frame. Those wires' reachable frames
+are the snapshot frame itself and the heads of the published edges out of
+that frame. Any `f` outside the intersection fails on this pair, so the full
+word fails. The verifier compares that intersection with an independent
+two-event replay on all 635 other catalogue frames. The two tests agree on
+every one of the 476 corrections: 301,756 frames fail the meeting, and 504
+lie in the intersection.
+
+## Census
+
+| Domain | Count | Outcome |
+|---|---:|---|
+| Length-4 intervals | 119 | 118 missing routes, 1 unchanged histogram |
+| Other catalogue frames | 302,260 | 301,756 fail the meeting, 504 miss a later edge |
+| Emitted moved frames | 0 | no paid-moment change is defined |
+
+The one contact-frame emission is the length-4 neutral word already named by
+PR #6305: zero-based scalar positions 9,399 and 10,815, gate `ADD(560, 315)`.
+Its histogram equals the published histogram, so it is not a saving. Every
+moved assignment fails to emit. None lowers `Σ n_r r^t` on `(0, 1)`.
+
+As a control, the same enumerator and emitter recount every length of four
+or more at the contact frame. The totals are 1,503 intervals, 1,450 missing
+routes, 14 unchanged histograms and 39 strict losses, with the same seven
+signed shapes published by PR #6305. That recount is a consistency check. It
+is not a new proof of the fixed-frame theorem.
+
+## Sign control for those seven shapes
+
+Write `Hr` for a job of rank `r`. A shape with every coefficient positive is
+positive for `0 < t < 1`. Otherwise each negative job of rank `R` is replaced
+by at least two positive jobs whose ranks sum to `R`. For positive `a, b`
+and `0 < t < 1`, `(a+b)^t < a^t + b^t`, because
+`(a/(a+b))^t > a/(a+b)` and the same holds for `b`. Iteration leaves a
+nonnegative remainder, so the shape is a strict loss on the whole interval.
+The seven shapes are `2H1 − H2`, `3H1 + 2H2`, `2H2 − H4`, `2H1 + H2 + H3`,
+`H1 + 3H2`, `H1 + 2H2 − H5` and `H1 + H3 − H4`. The same rule rejects
+`H1 − 2H2 + H3`. No moved length-4 word produces a shape, because none emits.
+
+## What this does not say
+
+The screen does not move two corrections in one interval, does not move a
+frame at length five or more, and does not add a route. A missing edge is a
+rejection on this table, not a proof that another native path is impossible.
+The six neutral one-step neighbors and the 645 common-frame expansions named
+in the #5708 README still have no executable search record in that package.
+Ordinary admission, the 18-call caller, adjoint columns, moduli 101 and
+10201, and the selected frontier are untouched. The selected conditional
+exponent remains `781451/250000000`.

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

@@ -0,0 +1,124 @@
+# Length-4 G20 conjugations do not emit after one moved correction
+
+**Negative result. No new κ.** The selected conditional exponent stays
+`781451/250000000` (`0.003125804`) in
+[certificates/selected-result.json](../../certificates/selected-result.json).
+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 length-4 A2 conjugation keeps its scalar endpoint when exactly one of
+its four corrections is moved onto a different frame of the published
+one-edge route table. All 302,260 such assignments fail to emit: 301,756
+fail at the contact-correction meeting, and 504 meet and then miss a later
+published edge. No assignment lowers the paid-query moment on `(0, 1)`.
+The argument is in [PROOF.md](PROOF.md).
+
+## Task and overlap
+
+Base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, 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 length-4 one-move clause left open by the
+length-1..3 moved-frame screen.
+
+Ordered eligible list for session r89, rebuilt on 2026-11-03 against that
+main. The 19 October handoff-index items are already delivered or closed, as
+recorded by the length-1..3 package. Discussion #1166 through 2026-11-03 has
+no newer finite handoff index. The newest posts are completed claims and
+three individual handoffs (compressed-word drops, a stopped modular-inverse
+draft, and a review request for open PR #6551). Those do not replace the
+priority table. The 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, in catalogue order. 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.
+
+1. Complex helpers (`p104-side-correction`, `coverage-law-change`).
+2. **This package.** BIT (`bit-helper-contract`): one correction of a
+   #5708 length-4 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`.
+
+[#6305](https://github.com/CrocSwap/integer-mult-bounds/pull/6305) keeps
+every correction on its contact frame for length 4 and above.
+[#6337](https://github.com/CrocSwap/integer-mult-bounds/pull/6337) moves one
+correction only for lengths 1..3.
+`research/g20-one-contact-free-frame` allows catalogue paths, and only for
+one contact. `research/g20-neutral-two-step-obstruction` keeps correction
+frames fixed. The local overlap search does not find a replay of this
+length-4 one-move domain.
+
+## Census
+
+| Domain | Missing meeting | Later missing edge | Emitted | Saving |
+|---|---:|---:|---:|---:|
+| One moved correction, length 4 | 301,756 | 504 | 0 | 0 |
+
+The contact-frame slice of the same 119 intervals is 118 missing routes and
+one unchanged histogram, at zero-based scalar positions 9,399 and 10,815 of
+`ADD(560, 315)`. A separate control recounts all 1,503 lengths of four or
+more at the contact frame and matches the published #6305 totals: 1,450
+missing, 14 unchanged, and 39 strict losses in the seven published shapes.
+That control does not replace the #6305 proof.
+
+## Reproduce
+
+Python 3.12 and the standard library, from the repository root. The census
+finishes in about ten seconds here.
+
+```sh
+python3 -I -B research/g20-length4-moved-frame/verify.py
+python3 -I -O -B research/g20-length4-moved-frame/verify.py
+python3 -B scripts/research_package.py --package research/g20-length4-moved-frame --check-only
+python3 -B scripts/research_package.py --package research/g20-length4-moved-frame
+```
+
+The direct verifier prints
+
+```text
+PASS_G20_LENGTH4_MOVED_FRAME intervals=119 fixed_missing=118 fixed_neutral=1 moved_assignments=302260 local_fail=301756 local_feasible=504 missing_edge=504 emitted=0 savings=0 long_control=1503/1450/14/39 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` needs full Git history.
+This checkout's upstream pin is shallow, so that ancestry check was not run.
+The pinned input blobs are objects of the recorded base commit.
+
+## Open next questions
+
+1. Can two corrections in one length-2, length-3 or length-4 interval lower
+   the paid moment when both frames move? This certificate moves exactly one
+   correction. The first step is one two-move pair on this word and route
+   table. No saving seed is supplied by the one-move census.
+2. Can one moved correction at length 5 or more lower the paid moment?
+   #6305 excludes those lengths only while every correction stays on its
+   contact frame. The first step is one length-5 interval with one moved
+   frame. The length-4 assignments do not provide a seed that emits.
+3. 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 blocker is that the published package does not contain
+   the search.
+
+## Credit
+
+The emitted word, route table, A2 relation, and the local-only conjugation
+count are Ali Romman's `research/g20-conjugation-admission`, following
+Dugongue, ai-nanachi, and the retained G20 lineage named there. The
+length-1..3 contact-frame census is unpaidmoon's #6290. The length-4-and-above
+contact-frame obstruction is Nick Petalas's #6305. The length-1..3 one-move
+obstruction is unpaidmoon's #6337. The one-contact free-frame obstruction
+and the fixed-frame neutral two-step obstruction are separate packages and
+are not imported.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

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

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/g20-conjugation-admission/LOCAL-RESULT.json",
+      "usage": "input",
+      "git_blob": "29cd42b8baa531f2598b9b8894fd514c754ed17c",
+      "sha256": "ec37bf5ddf743caf6a415bd4ce6fcd9c0f40922f0066ea79f6d2321ee0f18e96"
+    },
+    {
+      "path": "research/g20-conjugation-admission/PATHS.json",
+      "usage": "input",
+      "git_blob": "efbdf632746a971f9a593f57ccbb7d2cc67a6760",
+      "sha256": "f4dd58b78121040b1f054c0f7a626b25f6ef8d39f3de044d3456ea7dea8a6a5e"
+    },
+    {
+      "path": "research/g20-conjugation-admission/PROOF.md",
+      "usage": "input",
+      "git_blob": "b5147598224b8e164e7956e44c6e0fd76b7dc1ef",
+      "sha256": "8679c50955912242b9c98c6d8625ac9ca8f83660e50337cd16465ad71e507154"
+    },
+    {
+      "path": "research/g20-conjugation-admission/README.md",
+      "usage": "input",
+      "git_blob": "b1655b59134ae7a5734628ba1efef6611b2dcd31",
+      "sha256": "e443b2fd7b988316953bfc7d21045690ea0d3ce9069ce1a06880f6ccfc7ec054"
+    },
+    {
+      "path": "research/g20-conjugation-admission/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "3877a72d8a15adb03f6492f7d2fd8fa902ecb639",
+      "sha256": "8dd441fdb9c8923df06eb5ebfda37d03e4539f2305763e688d8c7025d196c4b1"
+    },
+    {
+      "path": "research/g20-conjugation-admission/construct.py",
+      "usage": "input",
+      "git_blob": "c0fe9d080b76171d8ed967cbad337c596d250a23",
+      "sha256": "2922052092d9323de2c715afb66dbd33fb58c7d0eeb3b9298bab5f7b2a930cb1"
+    }
+  ]
+}