From e5d7e4dc31331f19fb9ee795f180e6058ccf779c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 12:50:55 +0100 Subject: [PATCH] feat(research): classify all intact-region moment minimizers --- .../intact-region-minimizer-count/README.md | 182 ++ .../intact-region-minimizer-count/RESULT.json | 2073 +++++++++++++++++ .../SOURCES.json | 36 + .../intact-region-minimizer-count/TASK.json | 78 + .../intact-region-minimizer-count/VERIFY.json | 61 + .../independent.py | 115 + .../intact-region-minimizer-count/verify.py | 201 ++ 7 files changed, 2746 insertions(+) create mode 100644 research/intact-region-minimizer-count/README.md create mode 100644 research/intact-region-minimizer-count/RESULT.json create mode 100644 research/intact-region-minimizer-count/SOURCES.json create mode 100644 research/intact-region-minimizer-count/TASK.json create mode 100644 research/intact-region-minimizer-count/VERIFY.json create mode 100644 research/intact-region-minimizer-count/independent.py create mode 100644 research/intact-region-minimizer-count/verify.py diff --git a/research/intact-region-minimizer-count/README.md b/research/intact-region-minimizer-count/README.md new file mode 100644 index 0000000000..12b9dc6dec --- /dev/null +++ b/research/intact-region-minimizer-count/README.md @@ -0,0 +1,182 @@ +# Exactly 2^43 intact-region minimizers in each orientation + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +The fixed-boundary intact-region model has exactly +**8,796,093,022,208 = 2^43 minimizing chart assignments in each orientation**. +The minimizing set is a complete Boolean cube. Of the predecessor's 203 +residual binary region choices, 160 are fixed and 43 vary independently. +The free region IDs and all fixed bits are identical forward and backward. +Every minimum has the same rank histogram throughout `0> k) & 1`, and use `fixed_bits` at every other binary region. +Choose the lower or upper basis in the predecessor witness's `bounds` row +according to that bit; all nonbinary regions keep their unique bound. +This is a bijection and an explicit enumeration without storing trillions +of assignments. Region IDs refer to #4997's contracted graph, not word offsets. + +Use CPython 3.12 and the standard library, from the worktree root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/intact-region-minimizer-count +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/intact-region-minimizer-count --check-source-history +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/intact-region-minimizer-count/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/intact-region-minimizer-count/independent.py +``` + +The manifest registers both direct commands in normal and optimized modes. +The main success marker is `PASS_INTACT_REGION_MINIMIZER_COUNT`. +`verify.py --write` explicitly regenerates only RESULT.json. Ordinary replay +compares its freshly computed receipt and writes no package files. +Controls include a coupled equality pair whose two varying marginals do not +form a cube, independent factors, contradictory relations, an unreachable +conditional tie, duplicate variables and propagated implications. + +## Scope, provenance and implementation limits + +Canonical base is `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision +7. TASK.json preserves the original `complex-rank-shape-decoder` card and +records its changed scope to this equality question. The card's decoder +synthesis experiment is replaced by equality extraction from #5024's first +working certificate, because this contribution does not propose a new paid +profile. The selected baseline metadata orientation passed separately. + +SOURCES.json pins the live compressed witness and preserves the predecessor +proof/README as Git provenance. No predecessor executable is an input. +The universal equality-extraction argument and strictness above use #5024's +proved trace semantics. The finite verifier establishes this pinned trace's +new equality class. It is not independent validation of the native graph, +absolute phases, arbitrary dirty endpoints or the predecessor optimum. +No native/all-column, compiler, stock, precision/tape, complete selected cold +replay, Lean or outer multiplication proof is run or claimed. + +All new loops have finite input or explicit iteration bounds; the source is +capped at 203 variables, separators at three bits and the decompressed witness +at one million bytes. Both algorithms are iterative. Python's managed +allocation is a Power of Ten deviation: tables have at most 16 entries, +integer counts at most 204 bits, and at most 406 elimination factors. Package +metadata checks and warning-strict normal/optimized replays supply the +available diagnostics. Assertions are not verification gates. + +## Open next questions + +Can one of the 43 independent minimum-moment chart choices reduce a concrete +routing, storage or precision cost? First attach that actual cost to the free +region IDs, retain all incident operations and absolute phases, and compare +fully charged alternatives. A physical implementation and a complete consumer +bill are the blockers. This package assigns no such improvement. + +Can splitting one source region exploit a minimum-moment choice to remove an +actual paid transition? Coordinate with the broader +[PR #4993](https://github.com/CrocSwap/integer-mult-bounds/pull/4993) before +selecting one literal split. The first test needs its exact operator, dirty +restoration, all new edges and full cost. The intact-region theorem does not +answer that changed-boundary question. + +## Credit and overlap + +Chris R / Clear1nsight #5161 and Cinna Davis #5124 retain the existing +43-zero-move family and its `2^43` invoice-preserving subsets. This submission +adds exhaustive equality classification in the intact-region model. +Krzysztof Wojt #5024 supplies the global optimum, complete elimination witness +and five strict all-exponent comparison arguments, with the first three +inequalities credited there to Cinna Davis #4997. Cinna Davis supplies the +intact-region graph/model. Dugongue #4971 supplies carried-frame swaps and the +retained native source. Cao Yifan, zxv, Jacob Alan Sussman, James Reed and all +contributors named in those predecessor packages retain their attribution. +No predecessor file or credit line is changed. + +The broader numerical domain of #5016, Clear1nsight's small-component +fixed-price result #5068 and Cinna Davis's continuing #4993 search have +different restrictions. Their minima and search results are cited, not +recomputed here. Live PR bodies, this account's recent work, handoffs, active +Discussions, merged/main-tree terms and question reservations were checked. +The overlap cache covered 331 open PRs and 4,359 Discussion records; sparse +local notes were supplemented with all-main README searches. This is bounded +overlap evidence, not a novelty certificate. Unpublished work and arbitrary +code diffs remain outside coverage. diff --git a/research/intact-region-minimizer-count/RESULT.json b/research/intact-region-minimizer-count/RESULT.json new file mode 100644 index 0000000000..268fbc41af --- /dev/null +++ b/research/intact-region-minimizer-count/RESULT.json @@ -0,0 +1,2073 @@ +{ + "artifact_sha256": { + "README.md": "47e31501e18c0906ea157da11a350a401df5b02125d81cb1e59c15f797fd1074", + "independent.py": "8d2e85d65aeb13b63b35f4aad0497b0a7680932e56b8477c42c55d4eaa9511ad", + "verify.py": "72ab0d7b647084d46be73309a7a621385ae3ca6701beccb8ff13f4b68d1753e5" + }, + "claim_type": "scoped equality-class proof", + "controls": [ + "coupled pair", + "coupled marginals", + "noncube", + "independent product", + "inconsistency", + "unreachable tie", + "duplicate variable" + ], + "orientations": { + "backward": { + "count": 8796093022208, + "fixed_bits": { + "10001": 0, + "10002": 0, + "10003": 0, + "10007": 1, + "10008": 1, + "10009": 1, + "10023": 0, + "10024": 0, + "10025": 0, + "10029": 1, + "10030": 1, + "10031": 1, + "10071": 1, + "10073": 1, + "10095": 1, + "10097": 1, + "10120": 1, + "10122": 1, + "10143": 1, + "10145": 1, + "10165": 1, + "10167": 1, + "10189": 1, + "10191": 1, + "10216": 1, + "10218": 1, + "10238": 1, + "10240": 1, + "10269": 1, + "10273": 1, + "10277": 1, + "10281": 1, + "10283": 0, + "10284": 0, + "10288": 0, + "10289": 0, + "10293": 0, + "10294": 0, + "10298": 0, + "10299": 0, + "10303": 0, + "10304": 0, + "10306": 1, + "10308": 0, + "10309": 0, + "10311": 1, + "10313": 0, + "10314": 0, + "10318": 0, + "10319": 0, + "10446": 0, + "10447": 0, + "10448": 0, + "10449": 0, + "10450": 0, + "10451": 0, + "10452": 0, + "10453": 0, + "10454": 0, + "10489": 1, + "10511": 0, + "10512": 1, + "10513": 1, + "10514": 1, + "10515": 1, + "10516": 1, + "10517": 1, + "10518": 1, + "10519": 1, + "10531": 1, + "10572": 0, + "10613": 0, + "10614": 1, + "10615": 1, + "10616": 1, + "10617": 1, + "10618": 1, + "10619": 1, + "10620": 1, + "10621": 1, + "10641": 0, + "10662": 1, + "10663": 1, + "10664": 1, + "10665": 1, + "10682": 1, + "10683": 1, + "10684": 1, + "10685": 1, + "10983": 1, + "10987": 1, + "10991": 1, + "10995": 1, + "10999": 1, + "11003": 1, + "11007": 1, + "11011": 1, + "11143": 1, + "11147": 1, + "11151": 1, + "11155": 1, + "11159": 1, + "11163": 1, + "11167": 1, + "11171": 1, + "11239": 1, + "11243": 1, + "11247": 1, + "11251": 1, + "11255": 1, + "11259": 1, + "11263": 1, + "11267": 1, + "11271": 1, + "11275": 1, + "11279": 1, + "11283": 1, + "11287": 1, + "11291": 1, + "11295": 1, + "11299": 1, + "9094": 1, + "9190": 1, + "9286": 1, + "9872": 0, + "9873": 0, + "9874": 0, + "9878": 1, + "9879": 1, + "9880": 1, + "9893": 0, + "9894": 0, + "9895": 0, + "9899": 1, + "9900": 1, + "9901": 1, + "9914": 0, + "9915": 0, + "9916": 0, + "9920": 1, + "9921": 1, + "9922": 1, + "9937": 0, + "9938": 0, + "9939": 0, + "9943": 1, + "9944": 1, + "9945": 1, + "9959": 0, + "9960": 0, + "9961": 0, + "9965": 1, + "9966": 1, + "9967": 1, + "9980": 0, + "9981": 0, + "9982": 0, + "9986": 1, + "9987": 1, + "9988": 1 + }, + "free_regions": [ + 9875, + 9876, + 9877, + 9896, + 9897, + 9898, + 9917, + 9918, + 9919, + 9940, + 9941, + 9942, + 9962, + 9963, + 9964, + 9983, + 9984, + 9985, + 10004, + 10005, + 10006, + 10026, + 10027, + 10028, + 10285, + 10286, + 10287, + 10290, + 10291, + 10292, + 10296, + 10297, + 10301, + 10302, + 10887, + 10891, + 10895, + 10899, + 10903, + 10907, + 10911, + 10915, + 11311 + ], + "local_allowed_rows": 552, + "marginals": { + "10001": [ + 8796093022208, + 0 + ], + "10002": [ + 8796093022208, + 0 + ], + "10003": [ + 8796093022208, + 0 + ], + "10004": [ + 4398046511104, + 4398046511104 + ], + "10005": [ + 4398046511104, + 4398046511104 + ], + "10006": [ + 4398046511104, + 4398046511104 + ], + "10007": [ + 0, + 8796093022208 + ], + "10008": [ + 0, + 8796093022208 + ], + "10009": [ + 0, + 8796093022208 + ], + "10023": [ + 8796093022208, + 0 + ], + "10024": [ + 8796093022208, + 0 + ], + "10025": [ + 8796093022208, + 0 + ], + "10026": [ + 4398046511104, + 4398046511104 + ], + "10027": [ + 4398046511104, + 4398046511104 + ], + "10028": [ + 4398046511104, + 4398046511104 + ], + "10029": [ + 0, + 8796093022208 + ], + "10030": [ + 0, + 8796093022208 + ], + "10031": [ + 0, + 8796093022208 + ], + "10071": [ + 0, + 8796093022208 + ], + "10073": [ + 0, + 8796093022208 + ], + "10095": [ + 0, + 8796093022208 + ], + "10097": [ + 0, + 8796093022208 + ], + "10120": [ + 0, + 8796093022208 + ], + "10122": [ + 0, + 8796093022208 + ], + "10143": [ + 0, + 8796093022208 + ], + "10145": [ + 0, + 8796093022208 + ], + "10165": [ + 0, + 8796093022208 + ], + "10167": [ + 0, + 8796093022208 + ], + "10189": [ + 0, + 8796093022208 + ], + "10191": [ + 0, + 8796093022208 + ], + "10216": [ + 0, + 8796093022208 + ], + "10218": [ + 0, + 8796093022208 + ], + "10238": [ + 0, + 8796093022208 + ], + "10240": [ + 0, + 8796093022208 + ], + "10269": [ + 0, + 8796093022208 + ], + "10273": [ + 0, + 8796093022208 + ], + "10277": [ + 0, + 8796093022208 + ], + "10281": [ + 0, + 8796093022208 + ], + "10283": [ + 8796093022208, + 0 + ], + "10284": [ + 8796093022208, + 0 + ], + "10285": [ + 4398046511104, + 4398046511104 + ], + "10286": [ + 4398046511104, + 4398046511104 + ], + "10287": [ + 4398046511104, + 4398046511104 + ], + "10288": [ + 8796093022208, + 0 + ], + "10289": [ + 8796093022208, + 0 + ], + "10290": [ + 4398046511104, + 4398046511104 + ], + "10291": [ + 4398046511104, + 4398046511104 + ], + "10292": [ + 4398046511104, + 4398046511104 + ], + "10293": [ + 8796093022208, + 0 + ], + "10294": [ + 8796093022208, + 0 + ], + "10296": [ + 4398046511104, + 4398046511104 + ], + "10297": [ + 4398046511104, + 4398046511104 + ], + "10298": [ + 8796093022208, + 0 + ], + "10299": [ + 8796093022208, + 0 + ], + "10301": [ + 4398046511104, + 4398046511104 + ], + "10302": [ + 4398046511104, + 4398046511104 + ], + "10303": [ + 8796093022208, + 0 + ], + "10304": [ + 8796093022208, + 0 + ], + "10306": [ + 0, + 8796093022208 + ], + "10308": [ + 8796093022208, + 0 + ], + "10309": [ + 8796093022208, + 0 + ], + "10311": [ + 0, + 8796093022208 + ], + "10313": [ + 8796093022208, + 0 + ], + "10314": [ + 8796093022208, + 0 + ], + "10318": [ + 8796093022208, + 0 + ], + "10319": [ + 8796093022208, + 0 + ], + "10446": [ + 8796093022208, + 0 + ], + "10447": [ + 8796093022208, + 0 + ], + "10448": [ + 8796093022208, + 0 + ], + "10449": [ + 8796093022208, + 0 + ], + "10450": [ + 8796093022208, + 0 + ], + "10451": [ + 8796093022208, + 0 + ], + "10452": [ + 8796093022208, + 0 + ], + "10453": [ + 8796093022208, + 0 + ], + "10454": [ + 8796093022208, + 0 + ], + "10489": [ + 0, + 8796093022208 + ], + "10511": [ + 8796093022208, + 0 + ], + "10512": [ + 0, + 8796093022208 + ], + "10513": [ + 0, + 8796093022208 + ], + "10514": [ + 0, + 8796093022208 + ], + "10515": [ + 0, + 8796093022208 + ], + "10516": [ + 0, + 8796093022208 + ], + "10517": [ + 0, + 8796093022208 + ], + "10518": [ + 0, + 8796093022208 + ], + "10519": [ + 0, + 8796093022208 + ], + "10531": [ + 0, + 8796093022208 + ], + "10572": [ + 8796093022208, + 0 + ], + "10613": [ + 8796093022208, + 0 + ], + "10614": [ + 0, + 8796093022208 + ], + "10615": [ + 0, + 8796093022208 + ], + "10616": [ + 0, + 8796093022208 + ], + "10617": [ + 0, + 8796093022208 + ], + "10618": [ + 0, + 8796093022208 + ], + "10619": [ + 0, + 8796093022208 + ], + "10620": [ + 0, + 8796093022208 + ], + "10621": [ + 0, + 8796093022208 + ], + "10641": [ + 8796093022208, + 0 + ], + "10662": [ + 0, + 8796093022208 + ], + "10663": [ + 0, + 8796093022208 + ], + "10664": [ + 0, + 8796093022208 + ], + "10665": [ + 0, + 8796093022208 + ], + "10682": [ + 0, + 8796093022208 + ], + "10683": [ + 0, + 8796093022208 + ], + "10684": [ + 0, + 8796093022208 + ], + "10685": [ + 0, + 8796093022208 + ], + "10887": [ + 4398046511104, + 4398046511104 + ], + "10891": [ + 4398046511104, + 4398046511104 + ], + "10895": [ + 4398046511104, + 4398046511104 + ], + "10899": [ + 4398046511104, + 4398046511104 + ], + "10903": [ + 4398046511104, + 4398046511104 + ], + "10907": [ + 4398046511104, + 4398046511104 + ], + "10911": [ + 4398046511104, + 4398046511104 + ], + "10915": [ + 4398046511104, + 4398046511104 + ], + "10983": [ + 0, + 8796093022208 + ], + "10987": [ + 0, + 8796093022208 + ], + "10991": [ + 0, + 8796093022208 + ], + "10995": [ + 0, + 8796093022208 + ], + "10999": [ + 0, + 8796093022208 + ], + "11003": [ + 0, + 8796093022208 + ], + "11007": [ + 0, + 8796093022208 + ], + "11011": [ + 0, + 8796093022208 + ], + "11143": [ + 0, + 8796093022208 + ], + "11147": [ + 0, + 8796093022208 + ], + "11151": [ + 0, + 8796093022208 + ], + "11155": [ + 0, + 8796093022208 + ], + "11159": [ + 0, + 8796093022208 + ], + "11163": [ + 0, + 8796093022208 + ], + "11167": [ + 0, + 8796093022208 + ], + "11171": [ + 0, + 8796093022208 + ], + "11239": [ + 0, + 8796093022208 + ], + "11243": [ + 0, + 8796093022208 + ], + "11247": [ + 0, + 8796093022208 + ], + "11251": [ + 0, + 8796093022208 + ], + "11255": [ + 0, + 8796093022208 + ], + "11259": [ + 0, + 8796093022208 + ], + "11263": [ + 0, + 8796093022208 + ], + "11267": [ + 0, + 8796093022208 + ], + "11271": [ + 0, + 8796093022208 + ], + "11275": [ + 0, + 8796093022208 + ], + "11279": [ + 0, + 8796093022208 + ], + "11283": [ + 0, + 8796093022208 + ], + "11287": [ + 0, + 8796093022208 + ], + "11291": [ + 0, + 8796093022208 + ], + "11295": [ + 0, + 8796093022208 + ], + "11299": [ + 0, + 8796093022208 + ], + "11311": [ + 4398046511104, + 4398046511104 + ], + "9094": [ + 0, + 8796093022208 + ], + "9190": [ + 0, + 8796093022208 + ], + "9286": [ + 0, + 8796093022208 + ], + "9872": [ + 8796093022208, + 0 + ], + "9873": [ + 8796093022208, + 0 + ], + "9874": [ + 8796093022208, + 0 + ], + "9875": [ + 4398046511104, + 4398046511104 + ], + "9876": [ + 4398046511104, + 4398046511104 + ], + "9877": [ + 4398046511104, + 4398046511104 + ], + "9878": [ + 0, + 8796093022208 + ], + "9879": [ + 0, + 8796093022208 + ], + "9880": [ + 0, + 8796093022208 + ], + "9893": [ + 8796093022208, + 0 + ], + "9894": [ + 8796093022208, + 0 + ], + "9895": [ + 8796093022208, + 0 + ], + "9896": [ + 4398046511104, + 4398046511104 + ], + "9897": [ + 4398046511104, + 4398046511104 + ], + "9898": [ + 4398046511104, + 4398046511104 + ], + "9899": [ + 0, + 8796093022208 + ], + "9900": [ + 0, + 8796093022208 + ], + "9901": [ + 0, + 8796093022208 + ], + "9914": [ + 8796093022208, + 0 + ], + "9915": [ + 8796093022208, + 0 + ], + "9916": [ + 8796093022208, + 0 + ], + "9917": [ + 4398046511104, + 4398046511104 + ], + "9918": [ + 4398046511104, + 4398046511104 + ], + "9919": [ + 4398046511104, + 4398046511104 + ], + "9920": [ + 0, + 8796093022208 + ], + "9921": [ + 0, + 8796093022208 + ], + "9922": [ + 0, + 8796093022208 + ], + "9937": [ + 8796093022208, + 0 + ], + "9938": [ + 8796093022208, + 0 + ], + "9939": [ + 8796093022208, + 0 + ], + "9940": [ + 4398046511104, + 4398046511104 + ], + "9941": [ + 4398046511104, + 4398046511104 + ], + "9942": [ + 4398046511104, + 4398046511104 + ], + "9943": [ + 0, + 8796093022208 + ], + "9944": [ + 0, + 8796093022208 + ], + "9945": [ + 0, + 8796093022208 + ], + "9959": [ + 8796093022208, + 0 + ], + "9960": [ + 8796093022208, + 0 + ], + "9961": [ + 8796093022208, + 0 + ], + "9962": [ + 4398046511104, + 4398046511104 + ], + "9963": [ + 4398046511104, + 4398046511104 + ], + "9964": [ + 4398046511104, + 4398046511104 + ], + "9965": [ + 0, + 8796093022208 + ], + "9966": [ + 0, + 8796093022208 + ], + "9967": [ + 0, + 8796093022208 + ], + "9980": [ + 8796093022208, + 0 + ], + "9981": [ + 8796093022208, + 0 + ], + "9982": [ + 8796093022208, + 0 + ], + "9983": [ + 4398046511104, + 4398046511104 + ], + "9984": [ + 4398046511104, + 4398046511104 + ], + "9985": [ + 4398046511104, + 4398046511104 + ], + "9986": [ + 0, + 8796093022208 + ], + "9987": [ + 0, + 8796093022208 + ], + "9988": [ + 0, + 8796093022208 + ] + }, + "variables": 203 + }, + "forward": { + "count": 8796093022208, + "fixed_bits": { + "10001": 0, + "10002": 0, + "10003": 0, + "10007": 1, + "10008": 1, + "10009": 1, + "10023": 0, + "10024": 0, + "10025": 0, + "10029": 1, + "10030": 1, + "10031": 1, + "10071": 1, + "10073": 1, + "10095": 1, + "10097": 1, + "10120": 1, + "10122": 1, + "10143": 1, + "10145": 1, + "10165": 1, + "10167": 1, + "10189": 1, + "10191": 1, + "10216": 1, + "10218": 1, + "10238": 1, + "10240": 1, + "10269": 1, + "10273": 1, + "10277": 1, + "10281": 1, + "10283": 0, + "10284": 0, + "10288": 0, + "10289": 0, + "10293": 0, + "10294": 0, + "10298": 0, + "10299": 0, + "10303": 0, + "10304": 0, + "10306": 1, + "10308": 0, + "10309": 0, + "10311": 1, + "10313": 0, + "10314": 0, + "10318": 0, + "10319": 0, + "10446": 0, + "10447": 0, + "10448": 0, + "10449": 0, + "10450": 0, + "10451": 0, + "10452": 0, + "10453": 0, + "10454": 0, + "10489": 1, + "10511": 0, + "10512": 1, + "10513": 1, + "10514": 1, + "10515": 1, + "10516": 1, + "10517": 1, + "10518": 1, + "10519": 1, + "10531": 1, + "10572": 0, + "10613": 0, + "10614": 1, + "10615": 1, + "10616": 1, + "10617": 1, + "10618": 1, + "10619": 1, + "10620": 1, + "10621": 1, + "10641": 0, + "10662": 1, + "10663": 1, + "10664": 1, + "10665": 1, + "10682": 1, + "10683": 1, + "10684": 1, + "10685": 1, + "10983": 1, + "10987": 1, + "10991": 1, + "10995": 1, + "10999": 1, + "11003": 1, + "11007": 1, + "11011": 1, + "11143": 1, + "11147": 1, + "11151": 1, + "11155": 1, + "11159": 1, + "11163": 1, + "11167": 1, + "11171": 1, + "11239": 1, + "11243": 1, + "11247": 1, + "11251": 1, + "11255": 1, + "11259": 1, + "11263": 1, + "11267": 1, + "11271": 1, + "11275": 1, + "11279": 1, + "11283": 1, + "11287": 1, + "11291": 1, + "11295": 1, + "11299": 1, + "9094": 1, + "9190": 1, + "9286": 1, + "9872": 0, + "9873": 0, + "9874": 0, + "9878": 1, + "9879": 1, + "9880": 1, + "9893": 0, + "9894": 0, + "9895": 0, + "9899": 1, + "9900": 1, + "9901": 1, + "9914": 0, + "9915": 0, + "9916": 0, + "9920": 1, + "9921": 1, + "9922": 1, + "9937": 0, + "9938": 0, + "9939": 0, + "9943": 1, + "9944": 1, + "9945": 1, + "9959": 0, + "9960": 0, + "9961": 0, + "9965": 1, + "9966": 1, + "9967": 1, + "9980": 0, + "9981": 0, + "9982": 0, + "9986": 1, + "9987": 1, + "9988": 1 + }, + "free_regions": [ + 9875, + 9876, + 9877, + 9896, + 9897, + 9898, + 9917, + 9918, + 9919, + 9940, + 9941, + 9942, + 9962, + 9963, + 9964, + 9983, + 9984, + 9985, + 10004, + 10005, + 10006, + 10026, + 10027, + 10028, + 10285, + 10286, + 10287, + 10290, + 10291, + 10292, + 10296, + 10297, + 10301, + 10302, + 10887, + 10891, + 10895, + 10899, + 10903, + 10907, + 10911, + 10915, + 11311 + ], + "local_allowed_rows": 552, + "marginals": { + "10001": [ + 8796093022208, + 0 + ], + "10002": [ + 8796093022208, + 0 + ], + "10003": [ + 8796093022208, + 0 + ], + "10004": [ + 4398046511104, + 4398046511104 + ], + "10005": [ + 4398046511104, + 4398046511104 + ], + "10006": [ + 4398046511104, + 4398046511104 + ], + "10007": [ + 0, + 8796093022208 + ], + "10008": [ + 0, + 8796093022208 + ], + "10009": [ + 0, + 8796093022208 + ], + "10023": [ + 8796093022208, + 0 + ], + "10024": [ + 8796093022208, + 0 + ], + "10025": [ + 8796093022208, + 0 + ], + "10026": [ + 4398046511104, + 4398046511104 + ], + "10027": [ + 4398046511104, + 4398046511104 + ], + "10028": [ + 4398046511104, + 4398046511104 + ], + "10029": [ + 0, + 8796093022208 + ], + "10030": [ + 0, + 8796093022208 + ], + "10031": [ + 0, + 8796093022208 + ], + "10071": [ + 0, + 8796093022208 + ], + "10073": [ + 0, + 8796093022208 + ], + "10095": [ + 0, + 8796093022208 + ], + "10097": [ + 0, + 8796093022208 + ], + "10120": [ + 0, + 8796093022208 + ], + "10122": [ + 0, + 8796093022208 + ], + "10143": [ + 0, + 8796093022208 + ], + "10145": [ + 0, + 8796093022208 + ], + "10165": [ + 0, + 8796093022208 + ], + "10167": [ + 0, + 8796093022208 + ], + "10189": [ + 0, + 8796093022208 + ], + "10191": [ + 0, + 8796093022208 + ], + "10216": [ + 0, + 8796093022208 + ], + "10218": [ + 0, + 8796093022208 + ], + "10238": [ + 0, + 8796093022208 + ], + "10240": [ + 0, + 8796093022208 + ], + "10269": [ + 0, + 8796093022208 + ], + "10273": [ + 0, + 8796093022208 + ], + "10277": [ + 0, + 8796093022208 + ], + "10281": [ + 0, + 8796093022208 + ], + "10283": [ + 8796093022208, + 0 + ], + "10284": [ + 8796093022208, + 0 + ], + "10285": [ + 4398046511104, + 4398046511104 + ], + "10286": [ + 4398046511104, + 4398046511104 + ], + "10287": [ + 4398046511104, + 4398046511104 + ], + "10288": [ + 8796093022208, + 0 + ], + "10289": [ + 8796093022208, + 0 + ], + "10290": [ + 4398046511104, + 4398046511104 + ], + "10291": [ + 4398046511104, + 4398046511104 + ], + "10292": [ + 4398046511104, + 4398046511104 + ], + "10293": [ + 8796093022208, + 0 + ], + "10294": [ + 8796093022208, + 0 + ], + "10296": [ + 4398046511104, + 4398046511104 + ], + "10297": [ + 4398046511104, + 4398046511104 + ], + "10298": [ + 8796093022208, + 0 + ], + "10299": [ + 8796093022208, + 0 + ], + "10301": [ + 4398046511104, + 4398046511104 + ], + "10302": [ + 4398046511104, + 4398046511104 + ], + "10303": [ + 8796093022208, + 0 + ], + "10304": [ + 8796093022208, + 0 + ], + "10306": [ + 0, + 8796093022208 + ], + "10308": [ + 8796093022208, + 0 + ], + "10309": [ + 8796093022208, + 0 + ], + "10311": [ + 0, + 8796093022208 + ], + "10313": [ + 8796093022208, + 0 + ], + "10314": [ + 8796093022208, + 0 + ], + "10318": [ + 8796093022208, + 0 + ], + "10319": [ + 8796093022208, + 0 + ], + "10446": [ + 8796093022208, + 0 + ], + "10447": [ + 8796093022208, + 0 + ], + "10448": [ + 8796093022208, + 0 + ], + "10449": [ + 8796093022208, + 0 + ], + "10450": [ + 8796093022208, + 0 + ], + "10451": [ + 8796093022208, + 0 + ], + "10452": [ + 8796093022208, + 0 + ], + "10453": [ + 8796093022208, + 0 + ], + "10454": [ + 8796093022208, + 0 + ], + "10489": [ + 0, + 8796093022208 + ], + "10511": [ + 8796093022208, + 0 + ], + "10512": [ + 0, + 8796093022208 + ], + "10513": [ + 0, + 8796093022208 + ], + "10514": [ + 0, + 8796093022208 + ], + "10515": [ + 0, + 8796093022208 + ], + "10516": [ + 0, + 8796093022208 + ], + "10517": [ + 0, + 8796093022208 + ], + "10518": [ + 0, + 8796093022208 + ], + "10519": [ + 0, + 8796093022208 + ], + "10531": [ + 0, + 8796093022208 + ], + "10572": [ + 8796093022208, + 0 + ], + "10613": [ + 8796093022208, + 0 + ], + "10614": [ + 0, + 8796093022208 + ], + "10615": [ + 0, + 8796093022208 + ], + "10616": [ + 0, + 8796093022208 + ], + "10617": [ + 0, + 8796093022208 + ], + "10618": [ + 0, + 8796093022208 + ], + "10619": [ + 0, + 8796093022208 + ], + "10620": [ + 0, + 8796093022208 + ], + "10621": [ + 0, + 8796093022208 + ], + "10641": [ + 8796093022208, + 0 + ], + "10662": [ + 0, + 8796093022208 + ], + "10663": [ + 0, + 8796093022208 + ], + "10664": [ + 0, + 8796093022208 + ], + "10665": [ + 0, + 8796093022208 + ], + "10682": [ + 0, + 8796093022208 + ], + "10683": [ + 0, + 8796093022208 + ], + "10684": [ + 0, + 8796093022208 + ], + "10685": [ + 0, + 8796093022208 + ], + "10887": [ + 4398046511104, + 4398046511104 + ], + "10891": [ + 4398046511104, + 4398046511104 + ], + "10895": [ + 4398046511104, + 4398046511104 + ], + "10899": [ + 4398046511104, + 4398046511104 + ], + "10903": [ + 4398046511104, + 4398046511104 + ], + "10907": [ + 4398046511104, + 4398046511104 + ], + "10911": [ + 4398046511104, + 4398046511104 + ], + "10915": [ + 4398046511104, + 4398046511104 + ], + "10983": [ + 0, + 8796093022208 + ], + "10987": [ + 0, + 8796093022208 + ], + "10991": [ + 0, + 8796093022208 + ], + "10995": [ + 0, + 8796093022208 + ], + "10999": [ + 0, + 8796093022208 + ], + "11003": [ + 0, + 8796093022208 + ], + "11007": [ + 0, + 8796093022208 + ], + "11011": [ + 0, + 8796093022208 + ], + "11143": [ + 0, + 8796093022208 + ], + "11147": [ + 0, + 8796093022208 + ], + "11151": [ + 0, + 8796093022208 + ], + "11155": [ + 0, + 8796093022208 + ], + "11159": [ + 0, + 8796093022208 + ], + "11163": [ + 0, + 8796093022208 + ], + "11167": [ + 0, + 8796093022208 + ], + "11171": [ + 0, + 8796093022208 + ], + "11239": [ + 0, + 8796093022208 + ], + "11243": [ + 0, + 8796093022208 + ], + "11247": [ + 0, + 8796093022208 + ], + "11251": [ + 0, + 8796093022208 + ], + "11255": [ + 0, + 8796093022208 + ], + "11259": [ + 0, + 8796093022208 + ], + "11263": [ + 0, + 8796093022208 + ], + "11267": [ + 0, + 8796093022208 + ], + "11271": [ + 0, + 8796093022208 + ], + "11275": [ + 0, + 8796093022208 + ], + "11279": [ + 0, + 8796093022208 + ], + "11283": [ + 0, + 8796093022208 + ], + "11287": [ + 0, + 8796093022208 + ], + "11291": [ + 0, + 8796093022208 + ], + "11295": [ + 0, + 8796093022208 + ], + "11299": [ + 0, + 8796093022208 + ], + "11311": [ + 4398046511104, + 4398046511104 + ], + "9094": [ + 0, + 8796093022208 + ], + "9190": [ + 0, + 8796093022208 + ], + "9286": [ + 0, + 8796093022208 + ], + "9872": [ + 8796093022208, + 0 + ], + "9873": [ + 8796093022208, + 0 + ], + "9874": [ + 8796093022208, + 0 + ], + "9875": [ + 4398046511104, + 4398046511104 + ], + "9876": [ + 4398046511104, + 4398046511104 + ], + "9877": [ + 4398046511104, + 4398046511104 + ], + "9878": [ + 0, + 8796093022208 + ], + "9879": [ + 0, + 8796093022208 + ], + "9880": [ + 0, + 8796093022208 + ], + "9893": [ + 8796093022208, + 0 + ], + "9894": [ + 8796093022208, + 0 + ], + "9895": [ + 8796093022208, + 0 + ], + "9896": [ + 4398046511104, + 4398046511104 + ], + "9897": [ + 4398046511104, + 4398046511104 + ], + "9898": [ + 4398046511104, + 4398046511104 + ], + "9899": [ + 0, + 8796093022208 + ], + "9900": [ + 0, + 8796093022208 + ], + "9901": [ + 0, + 8796093022208 + ], + "9914": [ + 8796093022208, + 0 + ], + "9915": [ + 8796093022208, + 0 + ], + "9916": [ + 8796093022208, + 0 + ], + "9917": [ + 4398046511104, + 4398046511104 + ], + "9918": [ + 4398046511104, + 4398046511104 + ], + "9919": [ + 4398046511104, + 4398046511104 + ], + "9920": [ + 0, + 8796093022208 + ], + "9921": [ + 0, + 8796093022208 + ], + "9922": [ + 0, + 8796093022208 + ], + "9937": [ + 8796093022208, + 0 + ], + "9938": [ + 8796093022208, + 0 + ], + "9939": [ + 8796093022208, + 0 + ], + "9940": [ + 4398046511104, + 4398046511104 + ], + "9941": [ + 4398046511104, + 4398046511104 + ], + "9942": [ + 4398046511104, + 4398046511104 + ], + "9943": [ + 0, + 8796093022208 + ], + "9944": [ + 0, + 8796093022208 + ], + "9945": [ + 0, + 8796093022208 + ], + "9959": [ + 8796093022208, + 0 + ], + "9960": [ + 8796093022208, + 0 + ], + "9961": [ + 8796093022208, + 0 + ], + "9962": [ + 4398046511104, + 4398046511104 + ], + "9963": [ + 4398046511104, + 4398046511104 + ], + "9964": [ + 4398046511104, + 4398046511104 + ], + "9965": [ + 0, + 8796093022208 + ], + "9966": [ + 0, + 8796093022208 + ], + "9967": [ + 0, + 8796093022208 + ], + "9980": [ + 8796093022208, + 0 + ], + "9981": [ + 8796093022208, + 0 + ], + "9982": [ + 8796093022208, + 0 + ], + "9983": [ + 4398046511104, + 4398046511104 + ], + "9984": [ + 4398046511104, + 4398046511104 + ], + "9985": [ + 4398046511104, + 4398046511104 + ], + "9986": [ + 0, + 8796093022208 + ], + "9987": [ + 0, + 8796093022208 + ], + "9988": [ + 0, + 8796093022208 + ] + }, + "variables": 203 + } + }, + "schema_version": 1, + "source_sha256": "caa0cc98b80e0032527894b913719861ea5be04fccf0ad91939496acb0fa6549" +} diff --git a/research/intact-region-minimizer-count/SOURCES.json b/research/intact-region-minimizer-count/SOURCES.json new file mode 100644 index 0000000000..565134aaba --- /dev/null +++ b/research/intact-region-minimizer-count/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/global-intact-region-optimum/PROOF.md", + "usage": "provenance", + "git_blob": "d3e9cdb85b33d534d1a6abf1a8043a3db8e44bea", + "sha256": "772e0befa248067dd763d7726614f2a490b3d32f6a9b1ed9efcbb59423230f20" + }, + { + "path": "research/global-intact-region-optimum/README.md", + "usage": "provenance", + "git_blob": "1ace822a0241b80d14d71fd2d7adc91eaf92fb4e", + "sha256": "19086980d31c5232bce8509f271defdac09ab82a4abeeccd65937a0635f0096f" + }, + { + "path": "research/global-intact-region-optimum/WITNESSES.json.gz", + "usage": "input", + "git_blob": "33038fac983fe59e151d7401dacd8531f3c29c83", + "sha256": "caa0cc98b80e0032527894b913719861ea5be04fccf0ad91939496acb0fa6549" + } + ] +} diff --git a/research/intact-region-minimizer-count/TASK.json b/research/intact-region-minimizer-count/TASK.json new file mode 100644 index 0000000000..496c657aa7 --- /dev/null +++ b/research/intact-region-minimizer-count/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Classify and count every minimum-moment intact-region chart assignment in both orientations of PR5024, using its certified optimum and trace as premises.", + "scope_change_reason": "The original card asks for a new paid decoder profile. This is an original equality-class side result answering the explicit no-uniqueness boundary of another contributor, not decoder synthesis or predecessor verification.", + "bottleneck_link": "The exact minimum-moment cube gives the domain in which future finite routing, storage or precision costs can be optimized without paying a higher recursive moment. No such physical improvement is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved exact equality class; do not extend to changed words or physical costs.", + "outcome": "completed", + "evidence": "RESULT.json; exact counting and a separate local Cartesian-product certificate; README written equality-extraction proof.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a minimum-moment chart choice lower a concrete routing, storage or precision bill?", + "why_it_matters": "There are exactly 43 independent choices with the same recursive moment.", + "first_step": "Bind one real finite cost to the named free regions and price complete alternatives.", + "blocked_by": "An actual physical implementation and complete consumer bill." + }, + { + "question": "Can a literal split of one source region exploit a minimum-moment choice to remove a paid transition?", + "why_it_matters": "This changes the intact-region hypothesis rather than repeating the completed search.", + "first_step": "Coordinate with PR4993 and specify one split, its operator and every incident edge.", + "blocked_by": "Exact dirty restoration, absolute phases and a fully charged new boundary." + } + ] +} diff --git a/research/intact-region-minimizer-count/VERIFY.json b/research/intact-region-minimizer-count/VERIFY.json new file mode 100644 index 0000000000..33685ce00f --- /dev/null +++ b/research/intact-region-minimizer-count/VERIFY.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/global-intact-region-optimum/WITNESSES.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact sum-product count, all marginals, complete cube and seven controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact sum-product count, all marginals, complete cube and seven controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent domain propagation, exhaustive local Cartesian products and three controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent domain propagation, exhaustive local Cartesian products and three controls." + } + ] +} diff --git a/research/intact-region-minimizer-count/independent.py b/research/intact-region-minimizer-count/independent.py new file mode 100644 index 0000000000..d05e4e56af --- /dev/null +++ b/research/intact-region-minimizer-count/independent.py @@ -0,0 +1,115 @@ +"""Independent domain-propagation certificate for the exact equality cube. + +No imports from the primary counter or any predecessor executable. +produced by Nick Petalas. Apache-2.0. +""" +import gzip +from hashlib import sha256 +from io import BytesIO +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +INPUT = "research/global-intact-region-optimum/WITNESSES.json.gz" + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def load(): + manifest = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + expected = [r["sha256"] for r in manifest["files"] if r["path"] == INPUT] + blob = (ROOT / INPUT).read_bytes() + check(len(blob) <= 1_000_000, "compressed budget") + check(expected == [sha256(blob).hexdigest()], "input authentication") + with gzip.GzipFile(fileobj=BytesIO(blob)) as stream: + raw = stream.read(1_000_001) + check(len(raw) <= 1_000_000, "payload budget") + return json.loads(raw) + + +def extract(trace): + check(len(trace) <= 203, "trace budget") + constraints = [] + for step in trace: + scope = (step["node"], *step["separator"]) + check(len(scope) <= 4, "scope budget") + rows = set() + for state in step["states"]: + a, b = state["candidates"] + selected = state["choice"] + if selected is None: + continue + choices = (0, 1) if a is not None and a == b else (selected,) + for choice in choices: + rows.add((choice, *state["bits"])) + constraints.append((scope, rows)) + return constraints + + +def cube(constraints): + variables = {node for scope, _ in constraints for node in scope} + check(1 <= len(variables) <= 203, "variable budget") + domains = {node: {0, 1} for node in variables} + # Each strict change removes a bit. At most 2|variables| removals are possible. + for iteration in range(2 * len(variables) + 1): + changed = False + for scope, rows in constraints: + compatible = [r for r in rows if all(b in domains[n] for n, b in zip(scope, r))] + for index, node in enumerate(scope): + supported = {row[index] for row in compatible} + new = domains[node] & supported + check(bool(new), "nonempty domain") + if new != domains[node]: + domains[node], changed = new, True + if not changed: + break + else: + raise ValueError("propagation budget exhausted") + # This is the sufficiency certificate, beyond mere arc consistency. + checked_rows = 0 + for scope, rows in constraints: + permitted = {r for r in rows if all(b in domains[n] for n, b in zip(scope, r))} + whole_box = set(product(*(sorted(domains[n]) for n in scope))) + check(permitted == whole_box, "a residual coupling prevents a free cube") + checked_rows += len(whole_box) + return domains, iteration + 1, checked_rows + + +def controls(): + equality = [((0, 1), {(0, 0), (1, 1)})] + try: + cube(equality) + except ValueError as error: + check("residual coupling" in str(error), "specific coupling rejection") + else: + raise ValueError("coupled marginals falsely accepted as cube") + independent = [((n,), {(0,), (1,)}) for n in range(3)] + domains, _, _ = cube(independent) + check(sum(len(d) == 2 for d in domains.values()) == 3, "independent cube") + domains, _, _ = cube(equality + [((1,), {(1,)})]) + check(domains == {0: {1}, 1: {1}}, "propagated implication") + return 3 + + +def main(): + witness = load() + receipt = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + for name in ("forward", "backward"): + domains, passes, rows = cube(extract(witness[name]["elimination"])) + free = sorted(n for n, d in domains.items() if len(d) == 2) + fixed = {str(n): next(iter(d)) for n, d in domains.items() if len(d) == 1} + expected = receipt["orientations"][name] + check(free == expected["free_regions"] and fixed == expected["fixed_bits"], + "independent equality-class agreement") + check(1 << len(free) == expected["count"], "independent exact count") + print(f"INDEPENDENT {name} passes={passes} local_cube_rows={rows} fixed={len(fixed)} free={len(free)}") + print(f"PASS_INDEPENDENT_INTACT_REGION_CUBE controls={controls()}") + + +if __name__ == "__main__": + main() diff --git a/research/intact-region-minimizer-count/verify.py b/research/intact-region-minimizer-count/verify.py new file mode 100644 index 0000000000..ac9bbc8ef0 --- /dev/null +++ b/research/intact-region-minimizer-count/verify.py @@ -0,0 +1,201 @@ +"""Enumerate all minimizers of the cited intact-region elimination certificate. + +produced by Nick Petalas. Apache-2.0. +""" +import argparse +import gzip +from hashlib import sha256 +from io import BytesIO +from itertools import product +import json +from math import prod +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/global-intact-region-optimum/WITNESSES.json.gz" +MAX_VARIABLES = 203 +MAX_SEPARATOR = 3 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_witness(): + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + row = next(row for row in pins["files"] if row["path"] == SOURCE) + data = (ROOT / SOURCE).read_bytes() + require(len(data) <= 1_000_000, "compressed input budget") + require(sha256(data).hexdigest() == row["sha256"], "witness source hash") + with gzip.GzipFile(fileobj=BytesIO(data)) as stream: + raw = stream.read(1_000_001) + require(len(raw) <= 1_000_000, "expanded input budget") + witness = json.loads(raw) + require(set(witness) == {"forward", "backward"}, "two orientations") + return witness, sha256(data).hexdigest() + + +def relations(trace): + """Keep both choices exactly when their certified histograms coincide.""" + require(1 <= len(trace) <= MAX_VARIABLES, "variable budget") + nodes = [step["node"] for step in trace] + require(all(type(node) is int for node in nodes), "integer region IDs") + require(len(set(nodes)) == len(nodes), "distinct elimination nodes") + position = {node: index for index, node in enumerate(nodes)} + factors = [] + for index, step in enumerate(trace): + node, separator = step["node"], tuple(step["separator"]) + require(len(separator) <= MAX_SEPARATOR, "separator budget") + require(len(set(separator)) == len(separator), "distinct separator IDs") + require(all(n in position and position[n] > index for n in separator), + "separator follows eliminated variable") + states = step["states"] + expected = set(product((0, 1), repeat=len(separator))) + require(len(states) == len(expected), "complete state table") + require({tuple(s["bits"]) for s in states} == expected, "state coverage") + table = {} + for state in states: + left, right = state["candidates"] + choice, certificate = state["choice"], state["certificate"] + if choice is None: + require(left is None and right is None, "infeasible state") + allowed = () + elif left is not None and left == right: + require(choice in (0, 1) and certificate == "equal", "equal branch") + allowed = (0, 1) + else: + require(type(choice) is int and choice in (0, 1), "chosen bit") + require((left, right)[choice] is not None, "feasible chosen bit") + require(certificate != "equal", "strict comparison is not a tie") + allowed = (choice,) + for bit in (0, 1): + table[(bit,) + tuple(state["bits"])] = int(bit in allowed) + factors.append(((node,) + separator, table)) + return nodes, factors + + +def count_assignments(nodes, factors, fixed=None): + """Exact sum-product elimination on Boolean relations, without recursion.""" + require(len(nodes) <= MAX_VARIABLES, "count variable budget") + factors = [(scope, dict(table)) for scope, table in factors] + for node, bit in (fixed or {}).items(): + require(node in nodes and bit in (0, 1), "fixed-bit domain") + factors.append(((node,), {(0,): int(bit == 0), (1,): int(bit == 1)})) + for node in nodes: + bucket = [factor for factor in factors if node in factor[0]] + factors = [factor for factor in factors if node not in factor[0]] + require(bool(bucket), "each counted variable has a factor") + separator = tuple(sorted(set().union(*(set(s) for s, _ in bucket)) - {node})) + require(len(separator) <= MAX_SEPARATOR, "count separator budget") + table = {} + for bits in product((0, 1), repeat=len(separator)): + assignment, total = dict(zip(separator, bits)), 0 + for bit in (0, 1): + assignment[node] = bit + total += prod(t[tuple(assignment[n] for n in s)] for s, t in bucket) + table[bits] = total + factors.append((separator, table)) + require(all(not scope for scope, _ in factors), "all variables eliminated") + return prod(table[()] for _, table in factors) + + +def summarize(trace): + nodes, factors = relations(trace) + total = count_assignments(nodes, factors) + require(total > 0, "nonempty minimizing set") + free, fixed, marginals = [], {}, {} + for node in sorted(nodes): + zero = count_assignments(nodes, factors, {node: 0}) + one = count_assignments(nodes, factors, {node: 1}) + require(zero + one == total, "marginal partition") + marginals[str(node)] = [zero, one] + if zero and one: + free.append(node) + else: + fixed[str(node)] = int(one > 0) + # A subset of the Boolean cube with its full cardinality is the whole cube. + require(total == 1 << len(free), "minimizers form the complete free cube") + require(all(marginals[str(n)] == [total // 2, total // 2] for n in free), + "uniform free-bit marginals") + return {"count": total, "free_regions": free, "fixed_bits": fixed, + "marginals": marginals, "variables": len(nodes), + "local_allowed_rows": sum(sum(t.values()) for _, t in factors)} + + +def controls(): + # Coupling x=y has two solutions, but both marginals vary: it is not a cube. + equality = [((0, 1), {(a, b): int(a == b) for a, b in product((0, 1), repeat=2)})] + require(count_assignments([0, 1], equality) == 2, "coupled-pair count") + for bit in (0, 1): + require(count_assignments([0, 1], equality, {0: bit}) == 1, + "coupled-pair marginal") + coupled_trace = [ + {"node": 0, "separator": [1], "states": [ + {"bits": [0], "candidates": [[0, 1], None], "choice": 0, "certificate": "forced"}, + {"bits": [1], "candidates": [None, [0, 1]], "choice": 1, "certificate": "forced"}]}, + {"node": 1, "separator": [], "states": [ + {"bits": [], "candidates": [[0, 1], [0, 1]], "choice": 0, "certificate": "equal"}]}] + try: + summarize(coupled_trace) + except ValueError as error: + require("complete free cube" in str(error), "specific noncube rejection") + else: + raise ValueError("coupled marginals falsely accepted as cube") + disconnected = [((n,), {(0,): 1, (1,): 1}) for n in range(3)] + require(count_assignments([0, 1, 2], disconnected) == 8, "independent product") + impossible = equality + [((0,), {(0,): 1, (1,): 0}), + ((1,), {(0,): 0, (1,): 1})] + require(count_assignments([0, 1], impossible) == 0, "inconsistent relations") + # The tie for x exists only at y=1, while the later step forces y=0. + conditional = [ + {"node": 0, "separator": [1], "states": [ + {"bits": [0], "candidates": [[0, 1], None], "choice": 0, "certificate": "forced"}, + {"bits": [1], "candidates": [[0, 1], [0, 1]], "choice": 0, "certificate": "equal"}]}, + {"node": 1, "separator": [], "states": [ + {"bits": [], "candidates": [[0, 1], None], "choice": 0, "certificate": "forced"}]}] + require(summarize(conditional)["count"] == 1, "unreachable tie is not freedom") + malformed = conditional + [conditional[0]] + try: + relations(malformed) + except ValueError: + pass + else: + raise ValueError("duplicate-variable rejection") + return ["coupled pair", "coupled marginals", "noncube", "independent product", + "inconsistency", "unreachable tie", "duplicate variable"] + + +def result(): + witness, digest = read_witness() + output = {"schema_version": 1, "claim_type": "scoped equality-class proof", + "source_sha256": digest, "orientations": {}, "controls": controls()} + for name in ("forward", "backward"): + output["orientations"][name] = summarize(witness[name]["elimination"]) + require(output["orientations"]["forward"] == output["orientations"]["backward"], + "same equality cube in both orientations") + output["artifact_sha256"] = { + name: sha256((HERE / name).read_bytes()).hexdigest() + for name in ("verify.py", "independent.py", "README.md")} + return output + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate RESULT.json") + args = parser.parse_args() + computed = result() + path = HERE / "RESULT.json" + if args.write: + path.write_text(json.dumps(computed, indent=2, sort_keys=True) + "\n", encoding="utf-8") + else: + require(json.loads(path.read_text(encoding="utf-8")) == computed, "generated receipt") + values = computed["orientations"]["forward"] + print("PASS_INTACT_REGION_MINIMIZER_COUNT orientations=2 " + f"fixed={len(values['fixed_bits'])} free={len(values['free_regions'])} " + f"count={values['count']} controls={len(computed['controls'])}") + + +if __name__ == "__main__": + main()