From cd8413d796ec867faec9077483aad708c2ce7fb6 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Wed, 11 Nov 2026 10:42:25 +0000 Subject: [PATCH] Record that two moved corrections do not emit on length-7 G20 intervals. Exhaustive census of all 79 length-7 A2 intervals on the emitted #5708 word: 668,950,275 two-move assignments, none emitted. No kappa change. Prepared by unpaidmoon with substantial Cursor Grok assistance. Co-authored-by: unpaidmoon --- research/g20-length7-two-move/PROOF.md | 192 +++++++ research/g20-length7-two-move/README.md | 129 +++++ research/g20-length7-two-move/SOURCES.json | 54 ++ research/g20-length7-two-move/TASK.json | 83 +++ research/g20-length7-two-move/VERIFY.json | 38 ++ research/g20-length7-two-move/verify.py | 624 +++++++++++++++++++++ 6 files changed, 1120 insertions(+) create mode 100644 research/g20-length7-two-move/PROOF.md create mode 100644 research/g20-length7-two-move/README.md create mode 100644 research/g20-length7-two-move/SOURCES.json create mode 100644 research/g20-length7-two-move/TASK.json create mode 100644 research/g20-length7-two-move/VERIFY.json create mode 100644 research/g20-length7-two-move/verify.py diff --git a/research/g20-length7-two-move/PROOF.md b/research/g20-length7-two-move/PROOF.md new file mode 100644 index 0000000000..a99097c7b7 --- /dev/null +++ b/research/g20-length7-two-move/PROOF.md @@ -0,0 +1,192 @@ +# Two moved corrections do not emit on length-7 G20 intervals + +## Evidence class + +This is an exhaustive finite census of one finite domain. It is not a proof +that two moved corrections fail for every length, and it is not a proof of +unrestricted nonexistence. A missing edge is a rejection on the published +route table named below. No assignment in the domain emits, so none lowers +the paid moment on `(0, 1)`. The selected conditional exponent is +`363005817/100000000000`. This argument does not change that record and does +not claim a κ change. + +## 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 A2 interval runs from one `ADD(a, b)` to a later equal `ADD(a, b)`. Its +open interior has no `ERASE` or `INIT` of `a` or `b`, and each of its +noncommuting `ADD` records (its contacts) has an A2 correction: + +- `ADD(b, s)` with `s ≠ a` contributes `ADD(a, s)`; +- `ADD(d, a)` with `d ≠ b` contributes `ADD(d, b)`. + +The constructor of `construct.py` deletes the two outer gates and writes +each contact immediately followed by its correction, both on one chosen +frame. The contact-frame word uses the contact's published frame. This is +the model of PR #6664, reused by PR #6963 and PR #7079. + +## Domain + +The census takes every interval with exactly seven contacts. There are 79 +such intervals. The same scan finds 331, 250 and 119 intervals at 2, 3 and 4 +contacts, which are PR #6664's published totals; 1,384 intervals of length +at least 5, which is PR #6923's published total; 133 intervals of length +exactly 5, which is PR #6963's published total; and 86 intervals of length +exactly 6, which is PR #7079's published total. Length 7 is 79 of the 1,165 +intervals of length at least 7. The other 1,086 have length at least 8 and +are outside this census. They are counted and not searched. + +For each length-7 interval the census takes every pair `i < j` of its seven +corrections, every frame `f_i` of the route table other than contact `i`'s +frame, and every frame `f_j` other than contact `j`'s frame. The other five +corrections stay on their contact frames. The two new frames may be equal. +The table has 636 frames, so each pair contributes `635 × 635` assignments. + +| Contacts | Intervals | Pairs | Assignments | +|---:|---:|---:|---:| +| 7 | 79 | 1,659 | 668,950,275 | + +`79 × 21 × 635 × 635 = 668,950,275`. The domain is finite, and the verifier +checks that the rejection classes below add up to this product. + +The least interval in scalar-position order is the declared first case, the +one-interval step named by PR #7079. Its outer gates are the scalar records +at indexes 2,235 and 9,308, both `ADD(482, 6)`, on frames 1 and 8. It has +the same 21 pairs and 8,467,725 assignments as every other length-7 interval. +Its classes are reported separately below, and they are included in the totals. + +## Scalar endpoint + +For a contact `C` with correction `R` and outer gate `G`, `G C G = C R`, and +`R` commutes with `C`. Noncontacts commute with `G`, and `G^2 = I`, so the +rewrite preserves the scalar map. A frame is not an operand, so moving frames +leaves that map unchanged. The verifier checks the endpoint on the published +word, on all 79 contact-frame skeletons, and on one two-move skeleton of +each interval (corrections 0 and 1 moved to the least other catalogue frame). +The expected final row is `e_i` on public roles, plus `e_(i-111)` for +`111 ≤ i < 222`, and zero on owned roles. + +## Emitter + +`PATHS.json` has 2,369 one-edge routes of integer rank 1 through 7 on 636 +frames. A live ADD (nonzero source row) routes its destination and then its +source to the record's frame. A missing edge rejects the word. A dead ADD is +skipped. At the end each public role returns to its final frame and each +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 classes are exhaustive + +The emitter is a left-to-right machine that stops at the first missing route. +Write the rewritten word as + +`P · (C_i R_i at f_i) · M · (C_j R_j at f_j) · T`, + +where `P` is the prefix before contact `i`, `M` the records between +correction `i` and contact `j` (other contacts on their contact frames), and +`T` the rest. `P` is the same for every `f_i, f_j`. The records in `M` and +the unmoved meetings inside `M` depend on `f_i` and not on `f_j`. The machine +state after a prefix is a function of that prefix. Every assignment therefore +falls into exactly one of these classes, tested in order: + +| Class | Rejection point | Assignments | +|---|---|---:| +| `prefix_fail` | inside `P` | 157,257,750 | +| `first_meet` | inside `C_i R_i` at `f_i` | 379,275,340 | +| `middle_fail` | inside `M` | 123,717,685 | +| `second_meet` | inside `C_j R_j` at `f_j` | 8,670,307 | +| `tail_missing` | inside `T` or the final return | 29,193 | +| emitted | none | 0 | + +Each class except "emitted" is a rejection of the full word, because the +machine reaches it before reading any later record. If `M` for a pair +`(i, j)` misses a route, every later second index `j' > j` misses that same +route before contact `j'`, so those assignments are middle failures as well +and their frames `f_{j'}` are not read. The verifier computes the state after +`P` once per contact, resumes from there for each `f_i`, and replays `T` for +each of the 29,193 words that pass both meetings. It asserts that the six +classes partition all 668,950,275 assignments. Every tail rejection observed +during that replay is `missing_edge`. + +No assignment emits, so no paid histogram changes and no rewritten word +lowers `Σ n_r r^t` on `(0, 1)`. + +## The first length-7 interval + +On interval `2,235..9,308` the same partition is + +| Class | Assignments | +|---|---:| +| `prefix_fail` | 1,209,675 | +| `first_meet` | 6,094,095 | +| `middle_fail` | 969,645 | +| `second_meet` | 194,300 | +| `tail_missing` | 10 | +| emitted | 0 | +| total | 8,467,725 | + +`1,209,675 + 6,094,095 + 969,645 + 194,300 + 10 = 8,467,725`. Ten assignments +reach the tail and then miss an edge. One of them moves corrections 0 and 1 +onto frame 345. The other 8,467,715 assignments miss an edge before the tail. +This is the one-interval census named as the first step. The table above it +is the same machine run on the other 78 length-7 intervals as well. + +The seven contacts, as scalar index, correction and contact frame, are +`(6042, ADD(9, 6), 1)`, `(6466, ADD(122, 6), 536)`, `(6614, ADD(9, 6), 345)`, +`(8654, ADD(253, 6), 269)`, `(8657, ADD(397, 6), 269)`, +`(8660, ADD(389, 6), 269)` and `(8664, ADD(399, 6), 269)`. + +## Controls + +- **Cold tail replays.** Each of the 29,193 words that reach `T` is rebuilt + from the published scalar program and emitted from the start. Each misses + an edge. One of them is scalar positions `2,235..9,308`, corrections 0 and + 1, both moved to frame 345. +- **Cold prefix samples.** The first 25 recorded assignments in each of + `prefix_fail`, `first_meet`, `middle_fail` and `second_meet` are rebuilt + and emitted from the start. All 100 miss an edge. +- **Enumerator lock.** Lengths 2, 3 and 4 reproduce PR #6664's 331, 250 and + 119 intervals. Length at least 5 reproduces PR #6923's 1,384 intervals. + Length 5 reproduces PR #6963's 133 intervals. Length 6 reproduces PR + #7079's 86 intervals. Length at least 7 is 1,165, of which length 7 is 79 + and length at least 8 is the remaining 1,086. +- **Positive emission control.** One published length-5 one-move assignment + from PR #6923 is replayed on this emitter and is not part of the two-move + count: scalar positions `7,337..10,919`, correction 2, contact + `ADD(340, 670)` on frame 506, moved frame 123. It emits with histogram + difference `3 H2 − H4`, which is a strict loss on `(0, 1)` by the splitting + `H4 = H2 + H2` together with one extra rank-2 payment. The two-move census + itself has no emission to which that test applies. +- **Length-6 tail control.** One published length-6 two-move rejection from + PR #7079 is replayed as a single assignment, not as that census: scalar + positions `4,067..9,218`, corrections 1 and 2, both moved to frame 369, + gate `ADD(333, 51)`. It misses an edge. +- **Sign-classifier fixture.** `2 H1 − H2` is a strict loss. `H1 − 2 H2 + H3` + is left unsigned. The classifier is not used to sign a two-move histogram, + because no two-move word emits. + +A local calibration, not part of the registered command and not a new +length-6 result, ran this prefix classification on all 86 length-6 intervals +before the contact count was fixed at 7. It matched the partition published +by PR #7079, including zero emissions. The registered command does not +repeat that census. It replays only the single tail example above. + +## What remains outside this census + +The census moves exactly two corrections, on intervals of exactly seven +contacts, on the published one-edge route table. A missing edge is a +rejection on this table. It is an exhaustive finite census of that domain. +It is not a proof that two moved corrections fail at every length, and it is +not a proof that three or more moved corrections fail at length 7. Intervals +of length at least 8, a third moved correction on one of the 29,193 tail +words, and any added route are separate finite questions. They are stated in +the package README. Ordinary admission, the 18-call caller, adjoint columns, +moduli 101 and 10201, and the selected frontier are untouched. diff --git a/research/g20-length7-two-move/README.md b/research/g20-length7-two-move/README.md new file mode 100644 index 0000000000..db7d5781e2 --- /dev/null +++ b/research/g20-length7-two-move/README.md @@ -0,0 +1,129 @@ +# Two moved corrections do not emit on length-7 G20 intervals + +**Exhaustive finite census. No new κ.** The selected conditional exponent stays +`363005817/100000000000` (`0.00363005817`) in +[certificates/selected-result.json](../../certificates/selected-result.json). +This package does not edit that record and does not claim a κ change. + +On the emitted local word of +[PR #5708](https://github.com/CrocSwap/integer-mult-bounds/pull/5708), +every A2 conjugation with exactly seven contacts was tested with every pair of +corrections moved onto other frames of the published one-edge route table. +All 668,950,275 such assignments miss a published edge. None emits, so none +lowers the paid-query moment on `(0, 1)`. The argument is in +[PROOF.md](PROOF.md). + +This is a census of length exactly 7. It does not say that two moved +corrections fail at length 8 or above. + +## Task and overlap + +Base `e54523517d0f03e58352e647c403a5af3e525a57`, 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 open question 1 of +[#7079](https://github.com/CrocSwap/integer-mult-bounds/pull/7079). +The named first step is one length-7 interval. The same finite machine +classifies every length-7 interval, so the census covers all 79 rather than +a sample. Length 8 and above stays open. + +[#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. +[#6633](https://github.com/CrocSwap/integer-mult-bounds/pull/6633) moves one +correction at length 4. +[#6664](https://github.com/CrocSwap/integer-mult-bounds/pull/6664) moves two +corrections at lengths 2..4. +[#6923](https://github.com/CrocSwap/integer-mult-bounds/pull/6923) moves one +correction at length 5 or more. +[#6963](https://github.com/CrocSwap/integer-mult-bounds/pull/6963) moves two +corrections at length exactly 5. +[#7079](https://github.com/CrocSwap/integer-mult-bounds/pull/7079) moves two +corrections at length exactly 6 and leaves length at least 7 open. No open +PR enumerates length-7 two-move pairs on this word and route table. +[#7095](https://github.com/CrocSwap/integer-mult-bounds/pull/7095) is the +three-or-more census at length 5. [#7074](https://github.com/CrocSwap/integer-mult-bounds/pull/7074) +adds a route. This census does neither. + +## Census + +The route table has 636 frames, so each correction has 635 legal moves. +Each of the 79 intervals has `C(7, 2) = 21` correction pairs. + +| Class | Assignments | Outcome | +|---|---:|---| +| Prefix already missing | 157,257,750 | missing edge | +| First moved meeting rejects the new frame | 379,275,340 | missing edge | +| Records between the two meetings missing | 123,717,685 | missing edge | +| Second moved meeting rejects the new frame | 8,670,307 | missing edge | +| Tail or final return missing | 29,193 | missing edge | +| Emitted | 0 | — | +| Total | 668,950,275 | no saving | + +The declared first interval is the least pair of scalar positions, +`2,235..9,308`, outer gate `ADD(482, 6)`. Its 8,467,725 assignments are +1,209,675 prefix failures, 6,094,095 first-meeting failures, 969,645 middle +failures, 194,300 second-meeting failures and 10 tail failures. None emits. + +## Reproduce + +Python 3.12 and the standard library, from the repository root. The census +and the cold replays finish in about two minutes here. + +```sh +python3 -I -B research/g20-length7-two-move/verify.py +python3 -I -O -B research/g20-length7-two-move/verify.py +python3 -B scripts/research_package.py --package research/g20-length7-two-move +``` + +The direct verifier prints + +```text +PASS_G20_LENGTH7_TWO_MOVE intervals=79 pairs=1659 assignments=668950275 prefix_fail=157257750 first_meet=379275340 middle_fail=123717685 second_meet=8670307 full_replays=29193 tail_missing=29193 emitted=0 savings=0 first_interval=2235-9308/8467725/10 cold_replays=29293 one_move_control=3H2-H4 tail_example=2235-9308/0,1/345,345 length6_tail_control=4067-9218/1,2/369,369 length8_open=1086 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 frontier7000-verify`. +The 1,086 intervals of length at least 8 were not enumerated. + +## Open next questions + +1. Can two corrections in one interval of length at least 8 lower the paid + moment when both frames move? Length at least 7 has 1,165 intervals on + this word. This census settles the 79 of length exactly 7 and leaves + 1,086. Length 8 has 124 of them. #6664 stops at four contacts, #6963 + stops at five, #7079 stops at six, and this census stops at seven. The + first step is one length-8 interval's two-move pairs on this route table. + No length-7 assignment emits, so none supplies a saving seed. +2. Can a third moved correction on one of the 29,193 length-7 words that + survive both meetings, and then miss a later edge, make that word emit + and lower the paid moment? Those words are rejections. A partial + third-move search would not by itself be a census. This is not the + length-6 third-move question left by #7079, and it is not the length-5 + three-or-more census of #7095. + +[#7079](https://github.com/CrocSwap/integer-mult-bounds/pull/7079) question 2 +stays on that package. [#7095](https://github.com/CrocSwap/integer-mult-bounds/pull/7095) +stays on that package. +[#7074](https://github.com/CrocSwap/integer-mult-bounds/pull/7074) question, +adding the second missing edge of a dirty one-move failure, stays on that +package. This census holds the published route table fixed. + +## 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-4-and-above contact-frame obstruction is Nick Petalas's #6305. The +two-move classification at lengths 2..4, and the prefix machine this census +reimplements, are Nick Petalas's #6664. The length-1..3 one-move obstruction +is unpaidmoon's #6337. The length-4 one-move obstruction is unpaidmoon's +#6633. The length-at-least-5 one-move obstruction, including the length-5 +emission replayed here as a positive control, is unpaidmoon's #6923. The +length-5 two-move census is unpaidmoon's #6963. The length-6 two-move census +this package continues, including the single tail rejection replayed here as +a control, is unpaidmoon's #7079. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/g20-length7-two-move/SOURCES.json b/research/g20-length7-two-move/SOURCES.json new file mode 100644 index 0000000000..c01d82b4c5 --- /dev/null +++ b/research/g20-length7-two-move/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "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" + } + ] +} diff --git a/research/g20-length7-two-move/TASK.json b/research/g20-length7-two-move/TASK.json new file mode 100644 index 0000000000..e88ca8316e --- /dev/null +++ b/research/g20-length7-two-move/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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 PR #5708 word and its published one-edge route table, move exactly two corrections of each A2 conjugation with exactly seven contacts onto other frames, leave the other corrections on their contact frames, and decide whether any such assignment lowers the paid-query moment 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. Open question 1 of PR #7079 asks whether two moved corrections on one interval of length at least 7 can lower the paid moment. This package answers that question on the finite length-exactly-7 slice: every such interval on the emitted #5708 word and the published one-edge route table, not a single sample. Length at least 8 stays open.", + "bottleneck_link": "A paid-moment obstruction on this exact word says the length-7 two-move conjugation domain does not raise the ordinary BIT component. It does not change the selected exponent 363005817/100000000000.", + "budget_minutes": 60, + "stop_rule": "Stop when every two-move frame pair on the 79 intervals of length exactly 7 is classified. Do not open a length-8 search or a three-move search in this package.", + "outcome": "negative-result", + "evidence": "python3 -I -B research/g20-length7-two-move/verify.py prints PASS_G20_LENGTH7_TWO_MOVE with assignments=668950275, tail_missing=29193, emitted=0 and savings=0.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Can two corrections in one interval of length at least 8 lower the paid moment when both frames move?", + "why_it_matters": "This census classifies every two-move pair at exactly seven contacts. PR #7079 stops at six contacts, so length 8 and above is the remaining two-move clause on this word and route table.", + "first_step": "Enumerate one length-8 interval's two-move pairs on this word and one-edge route table. The length scan records 124 such intervals, and 1,086 intervals of length at least 8.", + "blocked_by": "No favorable witness is supplied. None of the 668,950,275 length-7 assignments emits, and a length-8 interval is a different finite domain." + }, + { + "question": "Can a third moved correction on one of the 29,193 length-7 words that survive both meetings, and then miss a later edge, make that word emit and lower the paid moment?", + "why_it_matters": "Exactly two corrections move in this census. A third moved frame can change a tail that currently misses an edge. This is not the length-6 third-move question left by PR #7079 and not the length-5 three-or-more census of PR #7095.", + "first_step": "On one of the 29,193 length-7 words that survive both moved meetings and then miss a later edge, move one further correction and price that word. One such word is interval 2,235..9,308 with corrections 0 and 1 both on frame 345.", + "blocked_by": "Those 29,193 words are rejections, not saving seeds. A search that moves a third correction on some of them would be a partial search unless its domain is finite and fully enumerated." + } + ] +} diff --git a/research/g20-length7-two-move/VERIFY.json b/research/g20-length7-two-move/VERIFY.json new file mode 100644 index 0000000000..397f0d0fcd --- /dev/null +++ b/research/g20-length7-two-move/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/g20-conjugation-admission/LOCAL-RESULT.json", + "research/g20-conjugation-admission/PATHS.json", + "research/g20-conjugation-admission/PROOF.md", + "research/g20-conjugation-admission/README.md", + "research/g20-conjugation-admission/WORD.json.gz", + "research/g20-conjugation-admission/construct.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Hashes, one-edge routes, scalar endpoints, the A2 length histogram against the #6664, #6923, #6963 and #7079 interval totals, exhaustive two-move classification of every length-7 interval, cold replay of every tail word and of 25 words from each earlier rejection class, one published length-5 one-move emission as a positive control, one published length-6 two-move tail rejection as a single-assignment control, and strict-loss sign controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same census under optimized bytecode. Checks raise exceptions, so they stay active." + } + ] +} diff --git a/research/g20-length7-two-move/verify.py b/research/g20-length7-two-move/verify.py new file mode 100644 index 0000000000..ac7a472a5c --- /dev/null +++ b/research/g20-length7-two-move/verify.py @@ -0,0 +1,624 @@ +#!/usr/bin/env python3 +"""Length-7 G20 conjugations with two corrections moved off their contact frames. + +The A2 identity, the constructor and the one-edge emitter are the #5708 +contract, as restated by PR #6664 and reused by PR #6963 and PR #7079. This +file reimplements that emitter. It imports no predecessor verifier. + +Domain: every A2 interval of the emitted #5708 word with exactly 7 contacts, +every pair i < j of its corrections, and every pair of frames (f_i, f_j) of +the route table with f_i different from contact i's frame and f_j different +from contact j's frame. The other five corrections stay on their contact +frames. f_i may equal f_j. + +Every assignment is classified by an exact prefix replay: + + prefix_fail the shared prefix up to contact i misses a route; + first_meet the moved pair (contact i, correction i) at f_i misses a route; + middle_fail the records between correction i and contact j miss a route; + second_meet the moved pair (contact j, correction j) at f_j misses a route; + tail_missing the full replay misses a later route; + neutral / loss / saving the full replay emits with that paid change + (no assignment reaches these classes). + +The first four classes depend only on a prefix of the rewritten word, and the +emitter rejects at the first missing route, so each is a rejection of the full +word. The 29,193 tail words are rebuilt and emitted from scratch. Twenty-five +words from each earlier class are rebuilt the same way. One published +length-5 one-move emission is replayed as a positive control that this emitter +can see a paid-histogram change. That control is one assignment, not a +length-5 census and not part of the two-move count. One published length-6 +two-move tail rejection from PR #7079 is replayed the same way: one +assignment, not the length-6 census. +""" + +from collections import Counter, defaultdict +from hashlib import sha256 +from pathlib import Path +import gzip +import json + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +BASE_PAID = {1: 1281, 2: 1338, 3: 58, 4: 57, 5: 102, 6: 10} +KAPPA = "363005817/100000000000" +ROUTES = 2369 +FRAMES = 636 +ALTERNATES = FRAMES - 1 +CONTACTS = 7 +PAIR_CHOICES = CONTACTS * (CONTACTS - 1) // 2 +INTERVALS = 79 +PAIRS = INTERVALS * PAIR_CHOICES +ASSIGNMENTS = PAIRS * ALTERNATES * ALTERNATES +EXPECTED_COUNTS = { + "pairs": PAIRS, + "assignments": ASSIGNMENTS, + "prefix_fail": 157257750, + "first_meet": 379275340, + "first_hosts": 41533, + "middle_fail": 123717685, + "second_meet": 8670307, + "full_replays": 29193, + "tail_missing": 29193, +} +FIRST_INTERVAL = (2235, 9308) +FIRST_COUNTS = { + "pairs": PAIR_CHOICES, + "assignments": PAIR_CHOICES * ALTERNATES * ALTERNATES, + "prefix_fail": 1209675, + "first_meet": 6094095, + "first_hosts": 306, + "middle_fail": 969645, + "second_meet": 194300, + "full_replays": 10, + "tail_missing": 10, +} +FIRST_CONTACTS = ( + (6042, ("ADD", 9, 6), 1), + (6466, ("ADD", 122, 6), 536), + (6614, ("ADD", 9, 6), 345), + (8654, ("ADD", 253, 6), 269), + (8657, ("ADD", 397, 6), 269), + (8660, ("ADD", 389, 6), 269), + (8664, ("ADD", 399, 6), 269), +) +# One tail word of the least length-7 interval. It passes both moved +# meetings and then misses an edge. The cold replay checks it again. +TAIL_EXAMPLE = (2235, 9308, 0, 1, 345, 345) +# One published length-6 tail rejection from PR #7079. One assignment only. +LENGTH6_TAIL = (4067, 9218, 1, 2, 369, 369) +# Lengths 2..4 are PR #6664. Length at least 5 is PR #6923's 1,384. +# Length 5 is PR #6963's 133. Length 6 is PR #7079's 86. +# Length 7 is the domain censused here. +LENGTHS = { + 0: 2, 1: 184, 2: 331, 3: 250, 4: 119, 5: 133, 6: 86, 7: 79, 8: 124, + 9: 95, 10: 129, 11: 100, 12: 151, 13: 69, 14: 102, 15: 47, 16: 73, + 17: 47, 18: 48, 19: 29, 20: 23, 21: 9, 22: 9, 23: 8, 24: 3, 25: 2, + 26: 4, 27: 4, 28: 1, 29: 2, 30: 2, 31: 3, 33: 2, +} +ONE_MOVE = (7337, 10919, 2, 123, ((2, 3), (4, -1))) +REJECTION = ("prefix_fail", "first_meet", "middle_fail", "second_meet", "tail_missing") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_pinned(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + blobs = {} + for row in sources["files"]: + if row["usage"] != "input": + continue + data = (ROOT / row["path"]).read_bytes() + need(sha256(data).hexdigest() == row["sha256"], "input hash mismatch " + row["path"]) + blobs[row["path"]] = data + source = blobs["research/g20-conjugation-admission/construct.py"].decode() + need("out.extend([e[:3] + [f], extra[:3] + [f]])" in source, + "constructor no longer puts the contact and correction on one chosen frame") + word = json.loads(gzip.decompress(blobs["research/g20-conjugation-admission/WORD.json.gz"])) + paths = json.loads(blobs["research/g20-conjugation-admission/PATHS.json"]) + local = json.loads(blobs["research/g20-conjugation-admission/LOCAL-RESULT.json"]) + selected = json.loads(blobs["certificates/selected-result.json"]) + return word, paths, local, selected + + +def load_edges(paths): + edges = {} + frames = set() + for key, value in paths.items(): + left, right = key.split(":") + need(len(value) == 1, "route " + key + " is not one edge") + start, end, rank = value[0] + need(start == int(left) and end == int(right), "route endpoints disagree with " + key) + need(type(rank) is int and 1 <= rank <= 7, "route rank outside 1..7") + edges[(start, end)] = rank + frames.update((start, end)) + need(len(edges) == ROUTES, "route count changed") + need(len(frames) == FRAMES, "frame count changed") + return edges, sorted(frames) + + +def expected_rows(width, owned): + rows = [] + for index in range(width): + if index in owned: + rows.append(0) + continue + row = 1 << index + if 111 <= index < 222: + row ^= 1 << (index - 111) + rows.append(row) + return rows + + +def endpoint_ok(records, width, owned, expected): + rows = [1 << index for index in range(width)] + for event in records: + op, dest = event[0], event[1] + if op == "ADD": + rows[dest] ^= rows[event[2]] + elif op == "ERASE": + if dest not in owned: + return False + rows[dest] = 0 + elif op == "INIT": + if dest not in owned or rows[dest]: + return False + else: + return False + return rows == expected + + +class Machine: + """The one-edge emitter: rows, wire frames and the paid histogram.""" + + def __init__(self, rows, state, paid, edges, owned): + self.rows, self.state, self.paid = rows, state, paid + self.edges, self.owned = edges, owned + + def copy(self): + return Machine(self.rows[:], self.state[:], Counter(self.paid), self.edges, self.owned) + + def step(self, event): + """Apply one record; return None or a rejection reason.""" + op, dest = event[0], event[1] + rows, state = self.rows, self.state + if op in ("ERASE", "INIT"): + if dest not in self.owned or (op == "INIT" and rows[dest]): + return "owned_op" + rows[dest] = 0 + state[dest] = event[2] + return None + if op != "ADD": + return "opcode" + source, frame = event[2], event[3] + if not rows[source]: + return None + for wire in (dest, source): + origin = state[wire] + if origin == frame: + continue + rank = self.edges.get((origin, frame)) + if rank is None: + return "missing_edge" + if rows[wire]: + self.paid[rank] += 1 + state[wire] = frame + rows[dest] ^= rows[source] + return None + + def run(self, records): + for event in records: + reason = self.step(event) + if reason is not None: + return reason + return None + + def finish(self, final): + rows, state = self.rows, self.state + for dest, frame in enumerate(final): + if dest in self.owned: + if rows[dest]: + return "owned_live" + state[dest] = frame + continue + origin = state[dest] + if origin == frame: + continue + rank = self.edges.get((origin, frame)) + if rank is None: + return "missing_edge" + if rows[dest]: + self.paid[rank] += 1 + state[dest] = frame + return None if state == final else "final_state" + + +def fresh(width, start, edges, owned): + return Machine([1 << index for index in range(width)], start[:], Counter(), edges, owned) + + +def emit(records, width, start, final, edges, owned): + machine = fresh(width, start, edges, owned) + reason = machine.run(records) or machine.finish(final) + return reason, (None if reason else machine.paid) + + +def correction(event, gate_dest, gate_source): + dest, source = event[1], event[2] + if dest == gate_source and source != gate_dest: + return ["ADD", gate_dest, source] + if source == gate_dest and dest != gate_source: + return ["ADD", dest, gate_source] + return None + + +def scan_intervals(scalars, lengths, cap): + """Every A2 interval whose contact count is in `lengths`. + + An interval that grows past `cap` contacts is rejected and counted in the + cap total. Callers that want the true length histogram pass a cap above + every interval the word contains. + """ + groups = defaultdict(list) + for index, event in enumerate(scalars): + if event[0] == "ADD": + groups[(event[1], event[2])].append(index) + found = [] + capped = 0 + for (gate_dest, gate_source), positions in groups.items(): + for left_at, left in enumerate(positions): + for right in positions[left_at + 1:]: + changes = [] + rejected = False + for index in range(left + 1, right): + event = scalars[index] + if event[0] in ("ERASE", "INIT") and event[1] in (gate_dest, gate_source): + rejected = True + break + if event[0] == "ADD" and (event[1] == gate_source or event[2] == gate_dest): + extra = correction(event, gate_dest, gate_source) + if extra is None or len(changes) == cap: + if extra is not None and len(changes) == cap: + capped += 1 + rejected = True + break + changes.append((index, extra, event[3])) + if rejected or len(changes) not in lengths: + continue + found.append((left, right, changes, gate_dest, gate_source)) + return sorted(found, key=lambda item: (item[0], item[1], item[3], item[4])), capped + + +def length_histogram(scalars): + groups = defaultdict(list) + for index, event in enumerate(scalars): + if event[0] == "ADD": + groups[(event[1], event[2])].append(index) + counts = Counter() + capped = 0 + cap = 64 + for (gate_dest, gate_source), positions in groups.items(): + for left_at, left in enumerate(positions): + for right in positions[left_at + 1:]: + changes = 0 + rejected = False + for index in range(left + 1, right): + event = scalars[index] + if event[0] in ("ERASE", "INIT") and event[1] in (gate_dest, gate_source): + rejected = True + break + if event[0] == "ADD" and (event[1] == gate_source or event[2] == gate_dest): + extra = correction(event, gate_dest, gate_source) + if extra is None or changes == cap: + if extra is not None and changes == cap: + capped += 1 + rejected = True + break + changes += 1 + if not rejected: + counts[changes] += 1 + return counts, capped + + +def skeleton(scalars, left, right, changes, override): + """The rewritten word plus the skeleton position of each contact.""" + replaced = {index: (extra, override.get(number, frame0)) + for number, (index, extra, frame0) in enumerate(changes)} + out, contacts = [], [] + for index, event in enumerate(scalars): + if index in (left, right): + continue + if index in replaced: + extra, frame = replaced[index] + contacts.append(len(out)) + out.append(event[:3] + [frame]) + out.append(extra + [frame]) + else: + out.append(event) + return out, contacts + + +def delta_of(paid, base): + ranks = set(paid) | set(base) + return tuple(sorted( + (rank, paid[rank] - base[rank]) for rank in ranks if paid[rank] != base[rank])) + + +def clean(counter): + return Counter({rank: count for rank, count in counter.items() if count}) + + +def strict_loss(delta): + """Positive by nonnegative terms or by repeated strict rank splits.""" + pos, neg = Counter(), Counter() + for rank, count in delta: + if count > 0: + pos[rank] += count + elif count < 0: + neg[rank] += -count + used_split = False + while True: + pos, neg = clean(pos), clean(neg) + if not neg: + return bool(pos) or used_split + rank = min(neg) + items = [] + for part, count in pos.items(): + items.extend([part] * count) + if len(items) > 14: + return False + found = None + for mask in range(1, 1 << len(items)): + bits = [items[i] for i in range(len(items)) if mask >> i & 1] + if len(bits) >= 2 and sum(bits) == rank: + found = bits + break + if found is None: + return False + for part in found: + pos[part] -= 1 + neg[rank] -= 1 + used_split = True + + +def moved(record, frame): + return record[:3] + [frame] + + +def remember(bucket, sample, limit=25): + if len(bucket) < limit: + bucket.append(sample) + + +def census(scalars, edges, frames, width, owned, start, final, base, expected): + """Resume each assignment from cached prefix states of the same word.""" + frame_set = set(frames) + items = scan_intervals(scalars, frozenset((CONTACTS,)), CONTACTS)[0] + need(len(items) == INTERVALS, "length-7 interval count changed") + need(len({(item[0], item[1]) for item in items}) == INTERVALS, "length-7 gates are not unique") + need(min((item[0], item[1]) for item in items) == FIRST_INTERVAL, + "the first length-7 interval moved") + counts = Counter() + first = Counter() + samples = defaultdict(list) + tails = [] + emitted = [] + block = ALTERNATES * ALTERNATES + for left, right, changes, gate_dest, gate_source in items: + track = (left, right) == FIRST_INTERVAL + need(len(changes) == CONTACTS, "a length-7 interval has another contact count") + if track: + need(scalars[left] == ["ADD", 482, 6, 1], "first left gate changed") + need(scalars[right] == ["ADD", 482, 6, 8], "first right gate changed") + need((gate_dest, gate_source) == (482, 6), "first gate operands changed") + observed = tuple((index, tuple(extra), frame) for index, extra, frame in changes) + need(observed == FIRST_CONTACTS, "first length-7 contacts changed") + fixed, contacts = skeleton(scalars, left, right, changes, {}) + need(endpoint_ok(fixed, width, owned, expected), "contact-frame endpoint failed") + others = [] + for change in changes: + need(change[2] in frame_set, "contact frame is outside the route table") + alts = [frame for frame in frames if frame != change[2]] + need(len(alts) == ALTERNATES, "alternate-frame count changed") + others.append(alts) + alternate = {0: others[0][0], 1: others[1][0]} + moved_word, _ = skeleton(scalars, left, right, changes, alternate) + need(endpoint_ok(moved_word, width, owned, expected), "two-move endpoint failed") + snaps = [] + machine = fresh(width, start, edges, owned) + cursor = 0 + alive = True + for position in contacts: + if alive and machine.run(fixed[cursor:position]) is not None: + alive = False + snaps.append(machine.copy() if alive else None) + cursor = position + for i in range(CONTACTS): + later = range(i + 1, CONTACTS) + for j in later: + counts["pairs"] += 1 + counts["assignments"] += block + if track: + first["pairs"] += 1 + first["assignments"] += block + if snaps[i] is None: + for j in later: + counts["prefix_fail"] += block + if track: + first["prefix_fail"] += block + remember(samples["prefix_fail"], + (left, right, i, j, others[i][0], others[j][0])) + continue + for f_i in others[i]: + at = snaps[i].copy() + c_i = contacts[i] + if at.run([moved(fixed[c_i], f_i), moved(fixed[c_i + 1], f_i)]) is not None: + for j in later: + counts["first_meet"] += ALTERNATES + if track: + first["first_meet"] += ALTERNATES + remember(samples["first_meet"], (left, right, i, j, f_i, others[j][0])) + continue + counts["first_hosts"] += 1 + if track: + first["first_hosts"] += 1 + cursor = c_i + 2 + for j in later: + c_j = contacts[j] + if at is None or at.run(fixed[cursor:c_j]) is not None: + at = None + counts["middle_fail"] += ALTERNATES + if track: + first["middle_fail"] += ALTERNATES + remember(samples["middle_fail"], + (left, right, i, j, f_i, others[j][0])) + continue + for f_j in others[j]: + tail = at.copy() + pair = [moved(fixed[c_j], f_j), moved(fixed[c_j + 1], f_j)] + if tail.run(pair) is not None: + counts["second_meet"] += 1 + if track: + first["second_meet"] += 1 + remember(samples["second_meet"], (left, right, i, j, f_i, f_j)) + continue + counts["full_replays"] += 1 + if track: + first["full_replays"] += 1 + reason = tail.run(fixed[c_j + 2:]) or tail.finish(final) + if reason is not None: + need(reason == "missing_edge", "moved word failed as " + reason) + counts["tail_missing"] += 1 + if track: + first["tail_missing"] += 1 + tails.append((left, right, i, j, f_i, f_j)) + continue + delta = delta_of(tail.paid, base) + emitted.append((left, right, i, j, f_i, f_j, delta)) + if at.run(fixed[c_j:c_j + 2]) is not None: + at = None + cursor = c_j + 2 + return items, counts, first, samples, tails, emitted + + +def one_move_control(scalars, edges, width, owned, start, final, base, expected): + """Replay the published length-5 one-move emission. One assignment only.""" + left, right, index, frame, shape = ONE_MOVE + items = scan_intervals(scalars, frozenset((5,)), 5)[0] + matches = [item for item in items if item[0] == left and item[1] == right] + need(len(matches) == 1, "the length-5 one-move witness interval is missing") + _left, _right, changes, gate_dest, gate_source = matches[0] + need(len(changes) == 5, "the length-5 control interval changed length") + need((gate_dest, gate_source) == (349, 340), "witness gate operands changed") + need(scalars[left][:3] == ["ADD", 349, 340] and scalars[right][:3] == ["ADD", 349, 340], + "witness outer gates changed") + contact_at, extra, contact_frame = changes[index] + need(contact_at == 7343, "witness contact index changed") + need(scalars[contact_at][:3] == ["ADD", 340, 670], "witness contact changed") + need(extra == ["ADD", 349, 670] and contact_frame == 506, "witness correction changed") + need(frame != contact_frame, "the control frame is the contact frame") + words, _contacts = skeleton(scalars, left, right, changes, {index: frame}) + need(endpoint_ok(words, width, owned, expected), "one-move control misses its endpoint") + reason, paid = emit(words, width, start, final, edges, owned) + need(reason is None, "published length-5 one-move witness no longer emits") + need(delta_of(paid, base) == shape, "published length-5 one-move shape changed") + need(strict_loss(shape), "published length-5 one-move shape is not a strict loss") + + +def length6_tail_control(scalars, edges, width, owned, start, final): + """Replay one published length-6 two-move rejection. One assignment only.""" + left, right, index_i, index_j, frame_i, frame_j = LENGTH6_TAIL + items = scan_intervals(scalars, frozenset((6,)), 6)[0] + matches = [item for item in items if item[0] == left and item[1] == right] + need(len(matches) == 1, "the length-6 tail-example interval is missing") + _left, _right, changes, gate_dest, gate_source = matches[0] + need(len(changes) == 6, "the length-6 tail example changed length") + need((gate_dest, gate_source) == (333, 51), "length-6 tail gate operands changed") + words, _contacts = skeleton( + scalars, left, right, changes, {index_i: frame_i, index_j: frame_j}) + reason, _paid = emit(words, width, start, final, edges, owned) + need(reason == "missing_edge", "published length-6 tail example no longer misses an edge") + + +def control_samples(scalars, items, samples, tails, width, start, final, edges, owned): + """Cold replays: 25 words from each prefix class, and every tail word.""" + by_key = {(left, right): changes for left, right, changes, _gate_dest, _gate_source in items} + checked = 0 + for kind in REJECTION[:-1]: + need(len(samples[kind]) == 25, kind + " sample count changed") + for left, right, i, j, f_i, f_j in samples[kind]: + words, _contacts = skeleton(scalars, left, right, by_key[(left, right)], {i: f_i, j: f_j}) + reason, _paid = emit(words, width, start, final, edges, owned) + need(reason == "missing_edge", kind + " sample emitted or failed as " + str(reason)) + checked += 1 + need(len(tails) == EXPECTED_COUNTS["tail_missing"], "tail list does not match the census") + need(TAIL_EXAMPLE in tails, "the named tail example left the tail class") + for left, right, i, j, f_i, f_j in tails: + words, _contacts = skeleton(scalars, left, right, by_key[(left, right)], {i: f_i, j: f_j}) + reason, _paid = emit(words, width, start, final, edges, owned) + need(reason == "missing_edge", "tail sample emitted or failed as " + str(reason)) + checked += 1 + return checked + + +def main(): + word, paths, local, selected = load_pinned() + need(selected["kappa"] == KAPPA, "selected kappa changed") + published = {int(rank): count for rank, count in local["stats"]["paid"].items()} + need(published == BASE_PAID, "LOCAL-RESULT paid histogram drifted") + edges, frames = load_edges(paths) + scalars = [event[:] for event in word["records"] if event[0] not in ("Q", "ZERO_Q")] + width = len(word["start"]) + need(len(scalars) == 11930 and width == 685, "scalar program shape changed") + owned = set(word["owned"]) + start, final = word["start"][:], word["final"][:] + expected = expected_rows(width, owned) + need(endpoint_ok(scalars, width, owned, expected), "published word misses its scalar endpoint") + reason, base = emit(scalars, width, start, final, edges, owned) + need(reason is None and dict(base) == BASE_PAID, "published word does not emit its histogram") + histogram, capped = length_histogram(scalars) + need(capped == 0, "the length scan hit its cap") + need(dict(histogram) == LENGTHS, "A2 length histogram changed " + str(dict(histogram))) + need(sum(count for length, count in histogram.items() if length >= 5) == 1384, + "length-at-least-5 interval total changed") + need(histogram[5] == 133 and histogram[6] == 86 and histogram[7] == 79, + "length-5, length-6 or length-7 interval total changed") + need(sum(count for length, count in histogram.items() if length >= 7) == 1165, + "length-at-least-7 interval total changed") + need(sum(count for length, count in histogram.items() if length >= 8) == 1086, + "length-at-least-8 interval total changed") + need(histogram[2] == 331 and histogram[3] == 250 and histogram[4] == 119, + "short-interval control disagrees with PR6664") + items, counts, first, samples, tails, emitted = census( + scalars, edges, frames, width, owned, start, final, base, expected) + need(dict(counts) == EXPECTED_COUNTS, "two-move census changed " + str(dict(counts))) + need({key: first[key] for key in FIRST_COUNTS} == FIRST_COUNTS, + "first-interval census changed " + str(dict(first))) + rejected = sum(counts[kind] for kind in REJECTION) + need(rejected == counts["assignments"] == ASSIGNMENTS, + "rejection classes do not partition the assignments") + need(not emitted, "a two-move assignment emitted " + str(emitted[:1])) + one_move_control(scalars, edges, width, owned, start, final, base, expected) + length6_tail_control(scalars, edges, width, owned, start, final) + checked = control_samples(scalars, items, samples, tails, width, start, final, edges, owned) + need(checked == 100 + EXPECTED_COUNTS["tail_missing"], "cold-replay count changed") + need(strict_loss(((1, 2), (2, -1))) and not strict_loss(((1, 1), (2, -2), (3, 1))), + "strict-loss classifier control failed") + print( + "PASS_G20_LENGTH7_TWO_MOVE" + " intervals=79 pairs={pairs} assignments={assignments}" + " prefix_fail={prefix_fail} first_meet={first_meet} middle_fail={middle_fail}" + " second_meet={second_meet} full_replays={full_replays} tail_missing={tail_missing}" + " emitted=0 savings=0" + " first_interval=2235-9308/8467725/10" + " cold_replays={checked} one_move_control=3H2-H4" + " tail_example=2235-9308/0,1/345,345" + " length6_tail_control=4067-9218/1,2/369,369" + " length8_open=1086 no_new_kappa=true".format(checked=checked, **counts)) + + +if __name__ == "__main__": + main()