From 086722ff6feb3a0e368f83c77ac698c3611c360b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 10 Nov 2026 21:26:46 +0000 Subject: [PATCH] feat(research): record a 21-shear one-scale helper-462 word The pinned helper-462 matcher has a zero-swap word with one scale of -16 and 21 rational shears, below the 26 recorded in open PR #7054. One exact word per scale row is recorded as well. The lengths are upper bounds from a heuristic search, not minima. No new kappa. --- .../helper462-one-scale-21-shear/README.md | 151 +++ .../ROW_WORDS.json | 1135 +++++++++++++++++ .../helper462-one-scale-21-shear/SOURCES.json | 24 + .../helper462-one-scale-21-shear/TASK.json | 103 ++ .../helper462-one-scale-21-shear/VERIFY.json | 20 + .../helper462-one-scale-21-shear/WORD.json | 147 +++ .../helper462-one-scale-21-shear/search.py | 154 +++ .../helper462-one-scale-21-shear/verify.py | 176 +++ 8 files changed, 1910 insertions(+) create mode 100644 research/helper462-one-scale-21-shear/README.md create mode 100644 research/helper462-one-scale-21-shear/ROW_WORDS.json create mode 100644 research/helper462-one-scale-21-shear/SOURCES.json create mode 100644 research/helper462-one-scale-21-shear/TASK.json create mode 100644 research/helper462-one-scale-21-shear/VERIFY.json create mode 100644 research/helper462-one-scale-21-shear/WORD.json create mode 100644 research/helper462-one-scale-21-shear/search.py create mode 100644 research/helper462-one-scale-21-shear/verify.py diff --git a/research/helper462-one-scale-21-shear/README.md b/research/helper462-one-scale-21-shear/README.md new file mode 100644 index 0000000000..38f9e3b4f6 --- /dev/null +++ b/research/helper462-one-scale-21-shear/README.md @@ -0,0 +1,151 @@ +# helper462-one-scale-21-shear + +**Constructive witness. No new κ and no selected-frontier change.** + +## Result + +For the pinned helper-462 matcher `S` +(`research/bit-completed-backend-api/science/RESULT.json#matcher`, an 8 by 8 +integer matrix of determinant `-16`), the alphabet of axis swaps, +single-coordinate rational scales and rational shears contains a zero-swap +word with exactly one scale and **21 shears**. The scale is the last letter, +on row 0, with coefficient `-16`. The shear denominators are `1, 2, 4, 8, 16`. + +The shortest one-scale zero-swap word recorded before this package has 26 +shears (unpaidmoon, open PR #7054), on the same matrix with the same scale. +The lower bound is 9 shears (unpaidmoon, open PR #7055). The open interval for +the one-scale shear length therefore moves from 9 through 26 to **9 through 21**. + +Twenty-one is the length of this witness. It is not claimed to be minimal. + +### The word + +Letters apply first to last as row operations on the identity. +`t += a*s` means row `t` gains `a` times row `s`. This is the content of +[WORD.json](WORD.json). + +| # | letter | # | letter | # | letter | +|---:|---|---:|---|---:|---| +| 1 | `7 += -1*2` | 8 | `0 += 3/4*1` | 15 | `5 += 1/2*1` | +| 2 | `1 += 1*3` | 9 | `1 += 4*0` | 16 | `4 += 1*7` | +| 3 | `5 += 1*3` | 10 | `0 += -3/16*1` | 17 | `4 += 16*0` | +| 4 | `3 += -2*1` | 11 | `2 += -8*0` | 18 | `6 += -1*3` | +| 5 | `5 += 2*0` | 12 | `0 += 1/8*2` | 19 | `3 += 1*6` | +| 6 | `0 += -1/2*5` | 13 | `0 += -1/16*4` | 20 | `6 += -1*3` | +| 7 | `4 += 2*2` | 14 | `1 += 2*3` | 21 | `1 += 1*2` | + +Letter 22 is the scale: row 0 times `-16`. + +### One word per scale row + +A zero-swap word with one scale `c` on row `r` has determinant `c`, so `c = -16` +and the shears multiply to `D_r^{-1} S`. Conjugating by the scale moves it to +either end without changing the shear count, so only the row `r` matters. +[ROW_WORDS.json](ROW_WORDS.json) records one exact word for each row: + +| scale row | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | +|---|---:|---:|---:|---:|---:|---:|---:|---:| +| shears | 21 | 21 | 24 | 21 | 21 | 21 | 21 | 23 | + +Each count is an upper bound for that row. The larger counts on rows 2 and 7 +are a search outcome. They are not a proof that those rows need more shears. + +## Claim type and limits + +- **Finite certificate.** Each frozen word multiplies exactly to `S` over the + rationals. That is the whole proof of the upper bounds. +- **Not a minimum.** The words came from a beam search, which is a heuristic + and not a census of rational words. Lengths 9 through 20 stay open. +- **Lower bound cited, not replayed.** The floor of 9 is the statement of open + PR #7055. This package does not recheck it. +- No supplier admission, no P2 ordinary bill, no tariff, and no + integer-coefficient claim. With integer shears no one-scale zero-swap word + exists (merged PR #6954); this word uses the denominator 16. + +## Evidence + +`verify.py` uses the Python 3.12 standard library and exact fractions. It checks: + +1. the pinned matcher is 8 by 8 with determinant `-16`; +2. the 21 shears followed by the scale reproduce `S`, by row operations on the + identity and by an independent product of elementary matrices; +3. the shear part has determinant 1, and no two adjacent shears share a + position, so no pair merges into one letter; +4. the same checks for the eight words of `ROW_WORDS.json`, whose row-0 entry + equals `WORD.json`; +5. 406 failure controls: for the primary word and each row word, deleting any + single letter misses `S`, and adding 1 to any single coefficient misses `S`. + +Failures use an explicit exit, so the controls stay active under `-O`. + +## Reproduce + +From the repository root, with CPython 3.12: + +```sh +python3.12 -B research/helper462-one-scale-21-shear/verify.py +python3.12 -O -B research/helper462-one-scale-21-shear/verify.py +python3.12 -B scripts/research_package.py --package research/helper462-one-scale-21-shear +python3.12 -B scripts/check_research_commit.py --package research/helper462-one-scale-21-shear --check-source-history +``` + +Expected first line: `PASS_HELPER462_ONE_SCALE_21_SHEAR`. The verifier runs in +well under a second. + +### Search provenance (not a registered check) + +`search.py` is the beam search that proposed the words. It reduces +`D_r^{-1} S` to the identity by row and column shears whose coefficient clears +one entry or sets one diagonal entry to 1, and keeps the matrices with the +fewest entries differing from the identity. It writes its output to a +directory outside the checkout: + +```sh +python3.12 -B research/helper462-one-scale-21-shear/search.py "$OUT" 4000 1 0 "" 24 +python3.12 -B research/helper462-one-scale-21-shear/search.py "$OUT" 300 1 0 "" 30 2,7 +``` + +The first command took about 11 seconds on ten cores and returns the recorded +21-shear words for rows 0, 1, 3, 4, 5 and 6; it returns nothing for rows 2 +and 7 within depth 24. The second returns the recorded 24-shear word for row 2. +The row-7 word came from +`search.py "$OUT" 1500 2 1.5 "1,-1,2,-2,0.5,-0.5" 23`, seed 1, a run of about +three minutes that was not repeated. The frozen words do not depend on the +search: the exact products are the certificate. + +## Open next questions + +Structured copies are in [TASK.json](TASK.json). + +1. **What is the minimal one-scale shear length?** The interval is now 9 + through 21. First step: run `search.py` with a wider beam and depth cap 20 + on rows 0, 1, 3, 4, 5 and 6, and separately try to raise the rank-drop floor + of PR #7055 from 9 to 10. A search that returns nothing is not a lower bound. +2. **Do scale rows 2 and 7 admit 21 shears?** The recorded words have 24 and + 23. First step: a wider or noisier beam on those rows, or an invariant of + `D_r^{-1} S` that separates them from the other six rows. +3. **Does the 21-shear word help on the P2 ordinary bill?** Letter counts do + not determine the signed moment, and this word has denominators up to 16. + First step: evaluate it under the tariff model of merged + `research/helper462-p2-ordinary-bill`. + +## Credit + +This package was produced by Nick Petalas. New work is Apache-2.0. + +Predecessors, none of which is replayed here: + +- The matcher and its five-swap elimination are from + `research/bit-completed-backend-api` (Chris R / Clear1nsight, PR #4957), + using the helper-462 witness of ai-nanachi #4760/#4814. +- unpaidmoon, merged PR #6954: a one-scale zero-swap word (53 shears), + the determinant identity that forces the scale `-16`, and the integer-shear + obstruction. +- unpaidmoon, open PR #7030 (head `98238eeed3faca9f0a5f1d4060db5d5da524a192`): + a 29-shear one-scale word and the rank lower bound 8. +- unpaidmoon, open PR #7054 (head `ae1cf2af174cd4f8c89089a27fc58e470b5452bd`): + the 26-shear one-scale word this package shortens. Its word format and + application order are reused in `WORD.json`. +- unpaidmoon, open PR #7055 (head `0a6361ec1b63621ca5f985218892e0cdc79502ae`): + the lower bound of 9 shears, which poses the open interval answered in part + here. diff --git a/research/helper462-one-scale-21-shear/ROW_WORDS.json b/research/helper462-one-scale-21-shear/ROW_WORDS.json new file mode 100644 index 0000000000..e67fe09c8d --- /dev/null +++ b/research/helper462-one-scale-21-shear/ROW_WORDS.json @@ -0,0 +1,1135 @@ +{ + "schema_version": 1, + "claim_type": "constructive-witnesses", + "note": "One zero-swap one-scale word per scale row, same application order as WORD.json. Lengths are upper bounds from a heuristic search, not minima.", + "shear_counts": [ + 21, + 21, + 24, + 21, + 21, + 21, + 21, + 23 + ], + "words": [ + { + "scale_row": 0, + "letters": [ + { + "op": "add", + "target": 7, + "source": 2, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 5, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "-2" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 4, + "source": 2, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "3/4" + }, + { + "op": "add", + "target": 1, + "source": 0, + "coefficient": "4" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "-3/16" + }, + { + "op": "add", + "target": 2, + "source": 0, + "coefficient": "-8" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "1/8" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "-1/16" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "2" + }, + { + "op": "add", + "target": 5, + "source": 1, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "16" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 2, + "coefficient": "1" + }, + { + "op": "scale", + "target": 0, + "coefficient": "-16" + } + ] + }, + { + "scale_row": 1, + "letters": [ + { + "op": "add", + "target": 7, + "source": 2, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 5, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "-2" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 4, + "source": 2, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "5" + }, + { + "op": "add", + "target": 1, + "source": 0, + "coefficient": "-1/4" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "20" + }, + { + "op": "add", + "target": 2, + "source": 0, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "-2" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "-1/8" + }, + { + "op": "add", + "target": 5, + "source": 1, + "coefficient": "-8" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "-1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 2, + "coefficient": "-1/16" + }, + { + "op": "scale", + "target": 1, + "coefficient": "-16" + } + ] + }, + { + "scale_row": 2, + "letters": [ + { + "op": "add", + "target": 7, + "source": 2, + "coefficient": "-1" + }, + { + "op": "add", + "target": 0, + "source": 3, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 3, + "source": 2, + "coefficient": "17" + }, + { + "op": "add", + "target": 4, + "source": 2, + "coefficient": "2" + }, + { + "op": "add", + "target": 2, + "source": 3, + "coefficient": "-1/16" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 6, + "source": 1, + "coefficient": "2" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 0, + "source": 3, + "coefficient": "-1/8" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "-2" + }, + { + "op": "add", + "target": 1, + "source": 0, + "coefficient": "4" + }, + { + "op": "add", + "target": 1, + "source": 5, + "coefficient": "-2" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "-2" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 6, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 5, + "source": 1, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "-1" + }, + { + "op": "add", + "target": 2, + "source": 1, + "coefficient": "1/32" + }, + { + "op": "add", + "target": 1, + "source": 2, + "coefficient": "-16" + }, + { + "op": "scale", + "target": 2, + "coefficient": "-16" + } + ] + }, + { + "scale_row": 3, + "letters": [ + { + "op": "add", + "target": 7, + "source": 2, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "-15/2" + }, + { + "op": "add", + "target": 5, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "1/8" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 4, + "source": 2, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "-5/16" + }, + { + "op": "add", + "target": 1, + "source": 0, + "coefficient": "4" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "-5/4" + }, + { + "op": "add", + "target": 2, + "source": 0, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "-2" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "2" + }, + { + "op": "add", + "target": 5, + "source": 1, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "-1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "16" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "-1/16" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "16" + }, + { + "op": "add", + "target": 1, + "source": 2, + "coefficient": "1" + }, + { + "op": "scale", + "target": 3, + "coefficient": "-16" + } + ] + }, + { + "scale_row": 4, + "letters": [ + { + "op": "add", + "target": 7, + "source": 2, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 5, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "-2" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 4, + "source": 2, + "coefficient": "-1/8" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "3/4" + }, + { + "op": "add", + "target": 1, + "source": 0, + "coefficient": "4" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "-3/16" + }, + { + "op": "add", + "target": 2, + "source": 0, + "coefficient": "-8" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "1/8" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "2" + }, + { + "op": "add", + "target": 5, + "source": 1, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "-1/16" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "-1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 2, + "coefficient": "1" + }, + { + "op": "scale", + "target": 4, + "coefficient": "-16" + } + ] + }, + { + "scale_row": 5, + "letters": [ + { + "op": "add", + "target": 7, + "source": 2, + "coefficient": "-1" + }, + { + "op": "add", + "target": 0, + "source": 3, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "-2" + }, + { + "op": "add", + "target": 5, + "source": 1, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 4, + "source": 2, + "coefficient": "2" + }, + { + "op": "add", + "target": 2, + "source": 5, + "coefficient": "4" + }, + { + "op": "add", + "target": 1, + "source": 5, + "coefficient": "-2" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "8" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "-1/8" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "-2" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "1" + }, + { + "op": "add", + "target": 2, + "source": 1, + "coefficient": "3/2" + }, + { + "op": "add", + "target": 2, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "8" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "-1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 2, + "coefficient": "1" + }, + { + "op": "scale", + "target": 5, + "coefficient": "-16" + } + ] + }, + { + "scale_row": 6, + "letters": [ + { + "op": "add", + "target": 7, + "source": 2, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "-15/2" + }, + { + "op": "add", + "target": 5, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "1/8" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 4, + "source": 2, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "-5/16" + }, + { + "op": "add", + "target": 1, + "source": 0, + "coefficient": "4" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "-5/4" + }, + { + "op": "add", + "target": 2, + "source": 0, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "-2" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "2" + }, + { + "op": "add", + "target": 5, + "source": 1, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "-1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 2, + "coefficient": "1" + }, + { + "op": "scale", + "target": 6, + "coefficient": "-16" + } + ] + }, + { + "scale_row": 7, + "letters": [ + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 5, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "-2" + }, + { + "op": "add", + "target": 2, + "source": 0, + "coefficient": "-2" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "3/2" + }, + { + "op": "add", + "target": 1, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "-3/8" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "1/8" + }, + { + "op": "add", + "target": 1, + "source": 5, + "coefficient": "-1" + }, + { + "op": "add", + "target": 2, + "source": 5, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "-1" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "2" + }, + { + "op": "add", + "target": 7, + "source": 4, + "coefficient": "-9" + }, + { + "op": "add", + "target": 1, + "source": 4, + "coefficient": "-8" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "1" + }, + { + "op": "add", + "target": 7, + "source": 4, + "coefficient": "-17/16" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "scale", + "target": 7, + "coefficient": "-16" + } + ] + } + ] +} diff --git a/research/helper462-one-scale-21-shear/SOURCES.json b/research/helper462-one-scale-21-shear/SOURCES.json new file mode 100644 index 0000000000..5f7bfe6f8f --- /dev/null +++ b/research/helper462-one-scale-21-shear/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-completed-backend-api/science/RESULT.json", + "usage": "input", + "git_blob": "55dca30281e3375d63a128c3de041e46c8a3c5ba", + "sha256": "965b650c0e49572e028f89a60943c64ad8dff9032fc93272b86cd1f9715a77b7" + } + ] +} diff --git a/research/helper462-one-scale-21-shear/TASK.json b/research/helper462-one-scale-21-shear/TASK.json new file mode 100644 index 0000000000..ddaaaea0a0 --- /dev/null +++ b/research/helper462-one-scale-21-shear/TASK.json @@ -0,0 +1,103 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "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" + ], + "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": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "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": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "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": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "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": "For the pinned helper-462 matcher, the rational elementary alphabet of shears, single-coordinate scales and axis swaps contains a zero-swap word with exactly one scale and 21 shears. The scale is the last letter, on row 0, with coefficient -16. One further exact word is recorded for each scale row, with 21, 21, 24, 21, 21, 21, 21 and 23 shears on rows 0 through 7. These are upper bounds from a heuristic search, not minima. No supplier admission, tariff comparison, or new kappa.", + "scope_change_reason": "The card asks for supplier admission coverage. This package answers one narrower open question posed by unpaidmoon's open PRs #7030, #7054 and #7055: whether a one-scale zero-swap word for this matcher exists with fewer than 26 shears. It audits no supplier and prices no tariff.", + "bottleneck_link": "Side result on a route ledger. The letter count of the helper-462 matcher is one charged part of the missing physical generator named in the predecessor packages. A shorter word lowers the best known shear count at one scale from 26 to 21 and narrows the open interval to 9 through 20. Letter counts do not determine the ordinary bill, so this is not a supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact one-scale zero-swap word with fewer than 26 shears, its per-row companions and the failure controls. Do not raise the lower bound, price P2 tariffs, or run an exhaustive census.", + "outcome": "completed", + "evidence": "Exact rational product of the frozen 0-swap, 1-scale, 21-shear word equals the pinned matcher, by row operations and by an independent product of elementary matrices. The same holds for one word per scale row with shear counts (21, 21, 24, 21, 21, 21, 21, 23). All 406 single-letter deletions and coefficient mutations miss the matcher. The lower bound of 9 shears is cited from open PR #7055 and was not replayed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the minimal number of shears in a one-scale zero-swap word for the helper-462 matcher? The known interval is now 9 through 21.", + "why_it_matters": "The word here came from a beam search that only tries coefficients clearing one entry or setting one diagonal entry to 1. A gap of twelve remains between the cited floor and this witness, so neither bound is known to be near the truth.", + "first_step": "Run research/helper462-one-scale-21-shear/search.py with a wider beam and a depth cap of 20 on scale rows 0, 1, 3, 4, 5 and 6, and separately try to raise the rank-drop floor of PR #7055 from 9 to 10.", + "blocked_by": "The search is heuristic. A run that returns nothing is a search failure, not a lower bound, and no exhaustive census of rational words is known." + }, + { + "question": "Do scale rows 2 and 7 admit a one-scale zero-swap word with 21 shears?", + "why_it_matters": "The recorded words have 24 shears on row 2 and 23 on row 7, against 21 on the other six rows. If the gap is real, the choice of scale row is a charged decision for any later generator.", + "first_step": "Run search.py on rows 2 and 7 with a beam of at least 4000 and a nonzero tie-breaking noise, or look for an invariant of D_r^{-1} S that separates rows 2 and 7 from the rest.", + "blocked_by": "At beam 4000 without noise the search returns nothing within depth 24 on these two rows. That is a search failure, not an exclusion." + }, + { + "question": "With the inherited P2 tariffs, does the 21-shear word beat the published five-swap pair or the seven-scale route on the completed ordinary bill?", + "why_it_matters": "Letter counts do not determine the signed moment. The 21-shear word uses coefficients with denominators up to 16, and the ordinary bill may charge those differently from unit shears.", + "first_step": "Evaluate this word under the tariff model of merged research/helper462-p2-ordinary-bill, which prices the seven-scale 27-shear route.", + "blocked_by": "That comparison needs the primitive tariffs pinned by the P2 package. This package records no bill." + } + ] +} diff --git a/research/helper462-one-scale-21-shear/VERIFY.json b/research/helper462-one-scale-21-shear/VERIFY.json new file mode 100644 index 0000000000..657c663d88 --- /dev/null +++ b/research/helper462-one-scale-21-shear/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-completed-backend-api/science/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Pinned matcher has determinant -16; the frozen 0-swap 1-scale 21-shear word equals it by exact row operations and by an independent elementary-matrix product; the shear part has determinant 1 and no adjacent mergeable pair; one exact word per scale row with shear counts (21, 21, 24, 21, 21, 21, 21, 23); 406 dropped-letter and mutated-coefficient failure controls." + } + ] +} diff --git a/research/helper462-one-scale-21-shear/WORD.json b/research/helper462-one-scale-21-shear/WORD.json new file mode 100644 index 0000000000..cb3fc49d0f --- /dev/null +++ b/research/helper462-one-scale-21-shear/WORD.json @@ -0,0 +1,147 @@ +{ + "schema_version": 1, + "claim_type": "constructive-witness", + "matcher": "research/bit-completed-backend-api/science/RESULT.json#matcher", + "scale_row": 0, + "scale_coefficient": "-16", + "application_order": "Apply letters from first to last as row operations on I. The 21 shears come first and the unique scale is last.", + "letter_counts": { + "swap": 0, + "scale": 1, + "add": 21 + }, + "not_a_minimum": true, + "letters": [ + { + "op": "add", + "target": 7, + "source": 2, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 5, + "source": 3, + "coefficient": "1" + }, + { + "op": "add", + "target": 3, + "source": 1, + "coefficient": "-2" + }, + { + "op": "add", + "target": 5, + "source": 0, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 5, + "coefficient": "-1/2" + }, + { + "op": "add", + "target": 4, + "source": 2, + "coefficient": "2" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "3/4" + }, + { + "op": "add", + "target": 1, + "source": 0, + "coefficient": "4" + }, + { + "op": "add", + "target": 0, + "source": 1, + "coefficient": "-3/16" + }, + { + "op": "add", + "target": 2, + "source": 0, + "coefficient": "-8" + }, + { + "op": "add", + "target": 0, + "source": 2, + "coefficient": "1/8" + }, + { + "op": "add", + "target": 0, + "source": 4, + "coefficient": "-1/16" + }, + { + "op": "add", + "target": 1, + "source": 3, + "coefficient": "2" + }, + { + "op": "add", + "target": 5, + "source": 1, + "coefficient": "1/2" + }, + { + "op": "add", + "target": 4, + "source": 7, + "coefficient": "1" + }, + { + "op": "add", + "target": 4, + "source": 0, + "coefficient": "16" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 3, + "source": 6, + "coefficient": "1" + }, + { + "op": "add", + "target": 6, + "source": 3, + "coefficient": "-1" + }, + { + "op": "add", + "target": 1, + "source": 2, + "coefficient": "1" + }, + { + "op": "scale", + "target": 0, + "coefficient": "-16" + } + ] +} diff --git a/research/helper462-one-scale-21-shear/search.py b/research/helper462-one-scale-21-shear/search.py new file mode 100644 index 0000000000..19a2f53f95 --- /dev/null +++ b/research/helper462-one-scale-21-shear/search.py @@ -0,0 +1,154 @@ +#!/usr/bin/env python3 +"""Heuristic beam search that proposed the words in this package. + +Provenance only: this is not a registered check and not a census. It reduces +D_r^{-1} S to the identity by row and column shears whose coefficient clears +one entry or sets one diagonal entry to 1, keeps the `beam` matrices closest +to the identity at each depth, and rebuilds a row-operation word. Arithmetic +is binary floating point restricted to a dyadic grid, so every accepted step +is exact; each returned word is rechecked with exact fractions. A run that +returns nothing proves nothing. + +Usage: search.py OUTDIR BEAM SEEDS NOISE [EXTRA_COEFFICIENTS [MAXDEPTH [ROWS]]] +""" +import json +import random +import sys +from fractions import Fraction +from multiprocessing import Pool +from pathlib import Path + +RESULT = Path(__file__).resolve().parents[2] / "research/bit-completed-backend-api/science/RESULT.json" +S = [[int(entry) for entry in row] for row in json.loads(RESULT.read_text())["matcher"]] +N = 8 +GRID = 4096.0 +BOUND = 1024.0 + + +def transpose(m): + return tuple(zip(*m)) + + +def nnz(m): + return sum(1 for i in range(N) for j in range(N) if m[i][j] != (1.0 if i == j else 0.0)) + + +def row_score(row, t): + return sum(1 for j in range(N) if row[j] != (1.0 if j == t else 0.0)) + + +def children(m, score, extra): + """Yield (child, child_score, (t, s, a)) for row operations row_t += a*row_s.""" + for t in range(N): + rt = m[t] + base = score - row_score(rt, t) + for s in range(N): + if s == t: + continue + rs = m[s] + coefs = set(extra) + for c in range(N): + y = rs[c] + if y == 0.0: + continue + v = rt[c] + if v != 0.0: + coefs.add(-v / y) + if c == t and v != 1.0: + coefs.add((1.0 - v) / y) + for a in coefs: + if a == 0.0 or abs(a) > BOUND or (a * GRID) != int(a * GRID): + continue + new = tuple(rt[c] + a * rs[c] for c in range(N)) + ok = True + for x in new: + if abs(x) > BOUND or (x * GRID) != int(x * GRID): + ok = False + break + if not ok: + continue + yield m[:t] + (new,) + m[t + 1:], base + row_score(new, t), (t, s, a) + + +def search(args): + r, beam, seed, noise, extra, maxdepth = args + rng = random.Random(seed) + start = tuple(tuple(float(Fraction(x, -16 if i == r else 1)) for x in row) for i, row in enumerate(S)) + ident = tuple(tuple(1.0 if i == j else 0.0 for j in range(N)) for i in range(N)) + layers = [{start: None}] + frontier = [(nnz(start), start)] + seen = {start} + for depth in range(1, maxdepth + 1): + cand = {} + for score, m in frontier: + for child, cs, mv in children(m, score, extra): + if child not in seen and child not in cand: + cand[child] = (cs, m, ("R",) + mv) + mt = transpose(m) + for child, cs, mv in children(mt, score, extra): + ch = transpose(child) + if ch not in seen and ch not in cand: + cand[ch] = (cs, m, ("C",) + mv) + if not cand: + return r, seed, None + if ident in cand: + layers.append({ident: cand[ident][1:]}) + path = [] + cur = ident + for layer in reversed(layers[1:]): + parent, mv = layer[cur] + path.append(mv) + cur = parent + path.reverse() + return r, seed, path + items = sorted(cand.items(), key=lambda kv: kv[1][0] + (rng.random() * noise if noise else 0.0))[:beam] + layers.append({k: v[1:] for k, v in items}) + frontier = [(v[0], k) for k, v in items] + seen.update(k for k, _ in items) + return r, seed, None + + +def to_word(path): + """Row-op letters, first to last on I, whose product is D_r^{-1} S.""" + rights = [mv for mv in path if mv[0] == "C"] + lefts = [mv for mv in path if mv[0] == "R"] + word = [] + for _, t, s, a in rights: # col_t += a col_s == M (I + a E_{s,t}) + word.append((s, t, -Fraction(a))) + for _, t, s, a in reversed(lefts): + word.append((t, s, -Fraction(a))) + return word + + +def check(word, r): + m = [[Fraction(int(i == j)) for j in range(N)] for i in range(N)] + for t, s, a in word: + assert t != s and a != 0 + m[t] = [m[t][c] + a * m[s][c] for c in range(N)] + m[r] = [x * -16 for x in m[r]] + return m == [[Fraction(x) for x in row] for row in S] + + +if __name__ == "__main__": + outdir = Path(sys.argv[1]) + beam = int(sys.argv[2]) + seeds = int(sys.argv[3]) + noise = float(sys.argv[4]) + extra = tuple(float(x) for x in sys.argv[5].split(",")) if len(sys.argv) > 5 and sys.argv[5] else () + maxdepth = int(sys.argv[6]) if len(sys.argv) > 6 else 30 + rows = [int(x) for x in sys.argv[7].split(",")] if len(sys.argv) > 7 else list(range(N)) + jobs = [(r, beam, seed, noise, extra, maxdepth) for seed in range(seeds) for r in rows] + best = {} + with Pool() as pool: + for r, seed, path in pool.imap_unordered(search, jobs): + if path is None: + print("row", r, "seed", seed, "none", flush=True) + continue + word = to_word(path) + ok = check(word, r) + print("row", r, "seed", seed, "len", len(word), "exact", ok, flush=True) + if ok and (r not in best or len(word) < len(best[r])): + best[r] = word + target = outdir / ("best_row%d_len%d.json" % (r, len(word))) + target.write_text(json.dumps([[t, s, str(a)] for t, s, a in word]) + "\n") + print({r: len(w) for r, w in sorted(best.items())}) diff --git a/research/helper462-one-scale-21-shear/verify.py b/research/helper462-one-scale-21-shear/verify.py new file mode 100644 index 0000000000..687d9aceba --- /dev/null +++ b/research/helper462-one-scale-21-shear/verify.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +"""A 21-shear one-scale zero-swap word for the pinned helper-462 matcher. + +The certificate is the exact rational product of the frozen words. Twenty-one +is an upper bound from a heuristic search, not a minimum. No new kappa. +""" +from fractions import Fraction +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +RESULT = ROOT / "research/bit-completed-backend-api/science/RESULT.json" +N = 8 +SCALE = Fraction(-16) +PRIMARY_SHEARS = 21 +ROW_SHEARS = (21, 21, 24, 21, 21, 21, 21, 23) +TOKEN = "PASS_HELPER462_ONE_SCALE_21_SHEAR" + + +def need(condition, message): + """Fail closed. A plain assert would vanish under python -O.""" + if not condition: + raise SystemExit("FAIL: " + message) + + +def identity(): + return [[Fraction(int(i == j)) for j in range(N)] for i in range(N)] + + +def matmul(left, right): + return [[sum(left[i][k] * right[k][j] for k in range(N)) for j in range(N)] + for i in range(N)] + + +def determinant(matrix): + work = [row[:] for row in matrix] + value = Fraction(1) + for column in range(N): + pivot = next((row for row in range(column, N) if work[row][column] != 0), None) + if pivot is None: + return Fraction(0) + if pivot != column: + work[column], work[pivot] = work[pivot], work[column] + value = -value + value *= work[column][column] + for row in range(column + 1, N): + factor = work[row][column] / work[column][column] + for index in range(column, N): + work[row][index] -= factor * work[column][index] + return value + + +def parse_letter(raw): + """Return ("add", target, source, coefficient) or ("scale", target, coefficient).""" + need(isinstance(raw, dict), "a letter must be an object") + kind = raw.get("op") + target = raw.get("target") + need(isinstance(target, int) and not isinstance(target, bool) and 0 <= target < N, + "a letter target must be a row index") + need(isinstance(raw.get("coefficient"), str), "a coefficient must be a string") + coefficient = Fraction(raw["coefficient"]) + if kind == "add": + source = raw.get("source") + need(isinstance(source, int) and not isinstance(source, bool) and 0 <= source < N, + "a shear source must be a row index") + need(source != target, "a shear must be off-diagonal") + need(coefficient != 0, "a shear coefficient must be nonzero") + need(set(raw) == {"op", "target", "source", "coefficient"}, "unexpected shear key") + return ("add", target, source, coefficient) + need(kind == "scale", "the alphabet here is shears and scales; swaps are excluded") + need(coefficient not in (0, 1), "a scale must be a non-identity coefficient") + need(set(raw) == {"op", "target", "coefficient"}, "unexpected scale key") + return ("scale", target, coefficient) + + +def apply_rows(letters): + """Apply the letters first to last as row operations on the identity.""" + matrix = identity() + for letter in letters: + if letter[0] == "add": + _, target, source, coefficient = letter + matrix[target] = [matrix[target][c] + coefficient * matrix[source][c] + for c in range(N)] + else: + _, target, coefficient = letter + matrix[target] = [coefficient * entry for entry in matrix[target]] + return matrix + + +def elementary(letter): + matrix = identity() + if letter[0] == "add": + matrix[letter[1]][letter[2]] = letter[3] + else: + matrix[letter[1]][letter[1]] = letter[2] + return matrix + + +def multiply_out(letters): + """Independent route: the product E_last ... E_first of elementary matrices.""" + matrix = identity() + for letter in letters: + matrix = matmul(elementary(letter), matrix) + return matrix + + +def check_word(raw_letters, matcher, scale_row, shear_count): + """One-scale zero-swap word: shear_count shears, then the scale -16 on scale_row.""" + letters = [parse_letter(raw) for raw in raw_letters] + need(len(letters) == shear_count + 1, "wrong letter count for scale row %d" % scale_row) + shears, scale = letters[:-1], letters[-1] + need(all(letter[0] == "add" for letter in shears), "the scale must be the last letter") + need(scale == ("scale", scale_row, SCALE), "the unique scale must be -16 on its row") + need(apply_rows(letters) == matcher, "row operations miss the matcher") + need(multiply_out(letters) == matcher, "elementary-matrix product misses the matcher") + need(determinant(apply_rows(shears)) == 1, "the shear part must have determinant 1") + for first, second in zip(shears, shears[1:]): + need(first[1:3] != second[1:3], "adjacent shears on one position would merge") + return letters + + +def failure_controls(letters, matcher): + """Every single-letter deletion and every mutated coefficient must miss.""" + count = 0 + for index, letter in enumerate(letters): + dropped = letters[:index] + letters[index + 1:] + need(apply_rows(dropped) != matcher, "dropping letter %d still matches" % index) + mutated = letters[:] + mutated[index] = letter[:-1] + (letter[-1] + 1,) + need(apply_rows(mutated) != matcher, "mutating letter %d still matches" % index) + count += 2 + return count + + +def main(): + matcher_raw = json.loads(RESULT.read_text())["matcher"] + need(len(matcher_raw) == N and all(len(row) == N for row in matcher_raw), + "the pinned matcher must be 8 by 8") + matcher = [[Fraction(entry) for entry in row] for row in matcher_raw] + need(determinant(matcher) == SCALE, "the matcher determinant must be -16") + + word = json.loads((PACKAGE / "WORD.json").read_text()) + need(word["letter_counts"] == {"swap": 0, "scale": 1, "add": PRIMARY_SHEARS}, + "WORD.json letter counts") + need(word["scale_row"] == 0 and Fraction(word["scale_coefficient"]) == SCALE, + "WORD.json scale header") + primary = check_word(word["letters"], matcher, 0, PRIMARY_SHEARS) + controls = failure_controls(primary, matcher) + denominators = sorted({letter[3].denominator for letter in primary[:-1]}) + need(denominators == [1, 2, 4, 8, 16], "primary shear denominators") + need(PRIMARY_SHEARS < 26, "the word must be shorter than the 26 shears of PR #7054") + + rows = json.loads((PACKAGE / "ROW_WORDS.json").read_text()) + need(tuple(rows["shear_counts"]) == ROW_SHEARS, "ROW_WORDS.json shear counts") + need(len(rows["words"]) == N, "ROW_WORDS.json must hold one word per scale row") + for scale_row, entry in enumerate(rows["words"]): + need(entry["scale_row"] == scale_row, "ROW_WORDS.json row order") + letters = check_word(entry["letters"], matcher, scale_row, ROW_SHEARS[scale_row]) + controls += failure_controls(letters, matcher) + need(rows["words"][0]["letters"] == word["letters"], "row 0 must equal WORD.json") + + print(TOKEN) + print(json.dumps({ + "matcher_determinant": str(SCALE), + "primary_word": {"swaps": 0, "scales": 1, "shears": PRIMARY_SHEARS, + "scale_row": 0, "shear_denominators": denominators}, + "shears_by_scale_row": list(ROW_SHEARS), + "failure_controls": controls, + "minimum_claimed": False, + "new_kappa": False, + }, sort_keys=True)) + + +if __name__ == "__main__": + main()