From aa67983d360a7d9fd579723eec7a28fe40493bb3 Mon Sep 17 00:00:00 2001 From: woklerx Date: Tue, 13 Oct 2026 17:23:13 -0700 Subject: [PATCH 1/2] Prove the rank-six frame cover representative repair leaves13diagonals --- .../CERTIFICATE.json | 253 ++++ .../DEPENDENCY.json | 16 + .../PR-BODY.md | 5 + .../README.md | 36 + .../SOURCES.json | 24 + .../TASK.json | 60 + .../VERIFY.json | 30 + .../inputs/COVERING.json | 77 + .../inputs/MODEL.json | 1328 +++++++++++++++++ .../p112-rank6-cover-representatives/scan.py | 115 ++ .../verify.py | 5 + 11 files changed, 1949 insertions(+) create mode 100644 research/p112-rank6-cover-representatives/CERTIFICATE.json create mode 100644 research/p112-rank6-cover-representatives/DEPENDENCY.json create mode 100644 research/p112-rank6-cover-representatives/PR-BODY.md create mode 100644 research/p112-rank6-cover-representatives/README.md create mode 100644 research/p112-rank6-cover-representatives/SOURCES.json create mode 100644 research/p112-rank6-cover-representatives/TASK.json create mode 100644 research/p112-rank6-cover-representatives/VERIFY.json create mode 100644 research/p112-rank6-cover-representatives/inputs/COVERING.json create mode 100644 research/p112-rank6-cover-representatives/inputs/MODEL.json create mode 100644 research/p112-rank6-cover-representatives/scan.py create mode 100644 research/p112-rank6-cover-representatives/verify.py diff --git a/research/p112-rank6-cover-representatives/CERTIFICATE.json b/research/p112-rank6-cover-representatives/CERTIFICATE.json new file mode 100644 index 0000000000..6bfe1e18ef --- /dev/null +++ b/research/p112-rank6-cover-representatives/CERTIFICATE.json @@ -0,0 +1,253 @@ +{ + "status": "PASS_RANK6_REPRESENTATIVE_SCAN", + "parent_ranks": { + "7": 7616, + "8": 37440, + "9": 12544 + }, + "cases": 967232, + "original_missing": [ + 10, + 18, + 23, + 25, + 32, + 34, + 43, + 47, + 51, + 53, + 56, + 62, + 81, + 87, + 88, + 92, + 96, + 100, + 105, + 112, + 117 + ], + "exact": { + "missing_even_after_union": [ + 18, + 47, + 53, + 62, + 88, + 92, + 96, + 100, + 112, + 117 + ], + "counts": [ + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4 + ], + "diagonal_union_sizes": [ + 24, + 24, + 24, + 24, + 24, + 24, + 24, + 24, + 24, + 24 + ], + "candidates_sha256": "679557b05f309b109ee1f9cfdca493bbb041937161f8fc18d2921e2b1bcd8e1a", + "distinct_final_unions": 903, + "maximum_diagonals": 99, + "best_terms": [ + [ + 7, + 55, + "0x187100008e18000000000560009590" + ], + [ + 29, + 1, + "0x187100000000187100000562a60004" + ], + [ + 19, + 91, + "0x80c8048004804c0424008040102464" + ], + [ + 105, + 91, + "0xaa00550a00a50050c000cc0000000" + ], + [ + 207, + 55, + "0x6801168001018080044402a1012020" + ], + [ + 215, + 111, + "0xa42180a0084210020848840480840" + ], + [ + 183, + 3, + "0x88a04452008100404820890408804" + ], + [ + 213, + 111, + "0x9422409004422000a018241082040" + ], + [ + 229, + 53, + "0x490404200420209221080802000668" + ], + [ + 135, + 109, + "0x81008100810618604816802006004" + ] + ], + "best_missing": [ + 18, + 47, + 53, + 56, + 62, + 68, + 88, + 92, + 96, + 98, + 100, + 112, + 117 + ] + }, + "monotone": { + "missing_even_after_union": [ + 18, + 47, + 53, + 62, + 88, + 92, + 96, + 100, + 112, + 117 + ], + "counts": [ + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4, + 4 + ], + "diagonal_union_sizes": [ + 24, + 24, + 24, + 24, + 24, + 24, + 24, + 24, + 24, + 24 + ], + "candidates_sha256": "679557b05f309b109ee1f9cfdca493bbb041937161f8fc18d2921e2b1bcd8e1a", + "distinct_final_unions": 903, + "maximum_diagonals": 99, + "best_terms": [ + [ + 7, + 55, + "0x187100008e18000000000560009590" + ], + [ + 29, + 1, + "0x187100000000187100000562a60004" + ], + [ + 19, + 91, + "0x80c8048004804c0424008040102464" + ], + [ + 105, + 91, + "0xaa00550a00a50050c000cc0000000" + ], + [ + 207, + 55, + "0x6801168001018080044402a1012020" + ], + [ + 215, + 111, + "0xa42180a0084210020848840480840" + ], + [ + 183, + 3, + "0x88a04452008100404820890408804" + ], + [ + 213, + 111, + "0x9422409004422000a018241082040" + ], + [ + 229, + 53, + "0x490404200420209221080802000668" + ], + [ + 135, + 109, + "0x81008100810618604816802006004" + ] + ], + "best_missing": [ + 18, + 47, + 53, + 56, + 62, + 68, + 88, + 92, + 96, + 98, + 100, + 112, + 117 + ] + }, + "controls": [ + "frame hits imply diagonal coverage", + "any hit-preserving representatives can repair all diagonals", + "restoring removed rows preserves rank six" + ] +} diff --git a/research/p112-rank6-cover-representatives/DEPENDENCY.json b/research/p112-rank6-cover-representatives/DEPENDENCY.json new file mode 100644 index 0000000000..e0e5c25931 --- /dev/null +++ b/research/p112-rank6-cover-representatives/DEPENDENCY.json @@ -0,0 +1,16 @@ +[ + { + "head": "64fd5f9e91961dedc16118fcc7ad71ee82efe28f", + "upstream": "research/p112-rank6-frame-coverage/COVERING.json", + "local": "inputs/COVERING.json", + "sha256": "27d567a56500f857962ddc69a9baed691a945e5a2979a26632e84c23133f1c95", + "git_blob": "b762571ef996a80ed8a16d392fc56782091ac58f" + }, + { + "head": "64fd5f9e91961dedc16118fcc7ad71ee82efe28f", + "upstream": "research/p112-rank6-frame-coverage/inputs/PR1323-MODEL.json", + "local": "inputs/MODEL.json", + "sha256": "899a5a0c604a244b06d59d1b1807927c4495cafd2eb6d581479c7f0da1d5b142", + "git_blob": "99474a0444b466fbeebd74f2bbe12c9f210c486b" + } +] diff --git a/research/p112-rank6-cover-representatives/PR-BODY.md b/research/p112-rank6-cover-representatives/PR-BODY.md new file mode 100644 index 0000000000..115e8084cb --- /dev/null +++ b/research/p112-rank6-cover-representatives/PR-BODY.md @@ -0,0 +1,5 @@ +PR1347 leaves 21 diagonals uncovered in its ten-term rank-six frame cover and warns that one representative per frame pattern may hide repairs. This successor scans all 967232 maximal slices across 7616 parents and proves that every representative choice preserving each original term frame-hit set covers at most **99 of 112 diagonals**. Arbitrary joint cuts of cost at most six reduce to this census by the supplied rank-factor argument. A 99-diagonal attaining tuple and three controls are included. + +This is a scoped support obstruction; changing frame patterns, other parent costs, coefficients and physical synthesis remain open. No new kappa or supplier. Source PR1347 is pinned at 64fd5f9e91961dedc16118fcc7ad71ee82efe28f, retaining contributor lineage. Prepared for woklerx with substantial OpenAI Codex assistance; Apache-2.0. + +Validation: Python3.12 registered normal/optimized replay, complete receipt comparison, selected-result integrity and git diff checks. diff --git a/research/p112-rank6-cover-representatives/README.md b/research/p112-rank6-cover-representatives/README.md new file mode 100644 index 0000000000..3bbd58cb4b --- /dev/null +++ b/research/p112-rank6-cover-representatives/README.md @@ -0,0 +1,36 @@ +# The rank-six frame cover cannot be repaired by changing support representatives + +PR1347 supplies ten rank-six atoms with copy bill 60 meeting each P112 orthogonal frame at least eight times, but its chosen supports leave 21 diagonals uncovered. It explicitly warns that retaining one support representative per frame-hit pattern may lose useful diagonal coverage. This package resolves that question for its **ten published term patterns**: allowing any cost-seven C/N root-star parent, arbitrary joint support trims of cost at most six, and extra frame hits, **at most 99 of 112 diagonals can be covered**. At least 13 remain impossible. + +Every original pattern has four tagged maximal representatives, two distinct diagonal supports, and no representative with a strict superset of its frame hits. The union of all alternatives still misses ten fixed diagonals; the complete multiple-choice calculation strengthens that to 13 simultaneously. An explicit support choice attaining 99 is in CERTIFICATE.json. This is a support obstruction, not a coefficient decoder or supplier. + +The independently written scan reconstructs all 1260 frames, all 57600 tagged parent pairs, 7616 cost-seven parents and 967232 maximal one-axis rank-six slices. All 903 distinct final union states of the ten binary choices are tested. The domain changes PR1347's representative choice, not its general frame-capacity theorem. Ten terms with different frame patterns, mixed ranks, other parents or punctures remain outside this result. + +## Proof + +Let a parent pairing matrix M have F2-rank 7. Factor M=XY with X of column rank 7 and Y of row rank 7. If restricting rows and columns gives rank at most 6, at least one restricted factor loses rank: left and right inverses would otherwise certify rank 7 for the product. When rows lose rank, their X-vectors lie in the kernel of a nonzero functional. The corresponding nonzero word in the full parent column code vanishes on all retained rows. Expanding the rows to its whole zero set and restoring all columns therefore dominates the joint trim. The other case is the transpose. All 127 nonzero codewords are enumerated for every parent; every maximal slice has rank 6 in this geometry. The argument includes arbitrary joint restrictions of cost below six. + +Expansion only adds frame hits and diagonal support. A replacement for term k must hit all frames hit by original term k, but may hit more. The scan retains every maximal slice satisfying that inclusion. Transposition preserves frame hits and the diagonal intersection, so column-side cuts add no diagonal choices. Exact candidate enumeration and dynamic union enumeration prove the maximum 99. A missing diagonal cannot be repaired by coefficients: all rank-one contributions there are zero while the target diagonal is 4. Cost-zero odd rectangles also have zero diagonal entries. + +The theorem retains a **per-term** frame-hit requirement. Letting one term lose hits while another repays them is outside it. No complete invoice is supplied: every other physical charge is optimistically zero for this necessary test, and no new kappa, native, all-size or supplier result is claimed. + +## Reproduce + +Python 3.12+, standard library, from the repository root: + +``` +python -I -B research/p112-rank6-cover-representatives/scan.py +python -I -O -B research/p112-rank6-cover-representatives/scan.py +python scripts/research_package.py --package research/p112-rank6-cover-representatives +``` + +Expected: `PASS_RANK6_REPRESENTATIVES ... max_diagonals=99 unavoidable_missing=13`. +Every replay compares the complete generated receipt. Controls reject the original false diagonal-coverage inference, the repaired-all-diagonals inference and an untrimmed parent priced at six. The best tuple is a positive rank-six support control. `--write` regenerates the receipt. + +## Open next questions + +Can ten rank-six terms cover every diagonal and every frame demand when frame hits may transfer between terms? Start by letting one original term lose hits and requiring the other nine to repay those deficits. Even a favorable support witness would still require exact complex coefficients and a complete physical invoice. Representative substitution alone cannot be the repair. + +## Sources and credit + +The cover and root order are copied byte-for-byte from Cinna Davis (@1337isnot1337), PR1347 at 64fd5f9e91961dedc16118fcc7ad71ee82efe28f; DEPENDENCY.json records paths, Git blobs and SHA256. Apache-2.0. Its source lineage retains Navinor PR1226, David Arias PR1236, Hanson Sun PR1242, Cinna Davis PR1323, DreamingOfClouds PR717 and themilkman216 PR968. New scan and proof prepared for woklerx with substantial OpenAI Codex assistance; no independent human review claimed. diff --git a/research/p112-rank6-cover-representatives/SOURCES.json b/research/p112-rank6-cover-representatives/SOURCES.json new file mode 100644 index 0000000000..2175c750ed --- /dev/null +++ b/research/p112-rank6-cover-representatives/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/complex-frame-pair-decoders/PROOF.md", + "usage": "input", + "git_blob": "889f3a653ed1bdbb7df61ebe3af4f2103602a1f4", + "sha256": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74" + } + ] +} diff --git a/research/p112-rank6-cover-representatives/TASK.json b/research/p112-rank6-cover-representatives/TASK.json new file mode 100644 index 0000000000..18c2ca7f8b --- /dev/null +++ b/research/p112-rank6-cover-representatives/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "refined", + "actual_scope": "Sharp diagonal cap99 for arbitrary cost<=6 descendants of cost7 C/N parents preserving each term frame-hit set.", + "scope_change_reason": "Audit the support-representative gap explicitly left by PR1347 on its ten published frame-hit patterns.", + "bottleneck_link": "Rejects a bill60 candidate before coefficient synthesis and physical realization.", + "budget_minutes": 60, + "stop_rule": "Complete967232slice census and exact choice coverage.", + "outcome": "negative-result", + "evidence": "CERTIFICATE.json and written proof in README.md", + "author": "woklerx", + "ai_assistance": "Substantial OpenAI Codex assistance", + "open_questions": [ + { + "question": "Can frame-hit redistribution between ten rank6terms cover all112diagonals?", + "why_it_matters": "Representative substitution alone cannot repair the cover.", + "first_step": "Permit one term to lose hits and demand other terms repay them.", + "blocked_by": "Full support search, coefficients and physical invoice remain open." + } + ] +} diff --git a/research/p112-rank6-cover-representatives/VERIFY.json b/research/p112-rank6-cover-representatives/VERIFY.json new file mode 100644 index 0000000000..2526ef9c8a --- /dev/null +++ b/research/p112-rank6-cover-representatives/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-frame-pair-decoders/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/scan.py" + ], + "timeout_seconds": 120, + "checks": "Complete967232slice census,source pins,sharp99bound and3controls" + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/scan.py" + ], + "timeout_seconds": 120, + "checks": "Optimized-mode full replay" + } + ] +} diff --git a/research/p112-rank6-cover-representatives/inputs/COVERING.json b/research/p112-rank6-cover-representatives/inputs/COVERING.json new file mode 100644 index 0000000000..b762571ef9 --- /dev/null +++ b/research/p112-rank6-cover-representatives/inputs/COVERING.json @@ -0,0 +1,77 @@ +{ + "scope": "Frame-demand relaxation only; arbitrary coefficients are not supplied. All helpers, source access, frame changes, copies beyond per-term rank, restoration, hosting and recursive overhead are optimistically zero.", + "terms": [ + [ + 7, + 0, + "0x187100008e18000000000560009590" + ], + [ + 29, + 0, + "0x187100000000187100000562a60004" + ], + [ + 19, + 2, + "0x80c8048004804c0424008040102464" + ], + [ + 105, + 88, + "0xaa00550a00a50050c000cc0000000" + ], + [ + 207, + 54, + "0x6801168001018080044402a1012020" + ], + [ + 215, + 90, + "0xa42180a0084210020848840480840" + ], + [ + 183, + 2, + "0x88a04452008100404820890408804" + ], + [ + 213, + 90, + "0x9422409004422000a018241082040" + ], + [ + 229, + 52, + "0x490404200420209221080802000668" + ], + [ + 135, + 54, + "0x81008100810618604816802006004" + ] + ], + "exact_check": { + "terms": 10, + "copy_bill": 60, + "minimum_hits": 8, + "hit_histogram": { + "8": 376, + "9": 648, + "10": 236 + }, + "frame_counts_sha256": "279d8390f77b13fd387f708b71988d62d021934b27a5868e7d776dc6b552327b" + }, + "diagonal_support_coverage": { + "minimum": 0, + "histogram": { + "0": 21, + "1": 41, + "2": 37, + "3": 9, + "4": 2, + "5": 2 + } + } +} diff --git a/research/p112-rank6-cover-representatives/inputs/MODEL.json b/research/p112-rank6-cover-representatives/inputs/MODEL.json new file mode 100644 index 0000000000..99474a0444 --- /dev/null +++ b/research/p112-rank6-cover-representatives/inputs/MODEL.json @@ -0,0 +1,1328 @@ +{ + "lines": [ + [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + -2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + -2, + 0, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + -2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 2 + ], + [ + 0, + 2, + 0, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + 0, + 2, + 2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + -2, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 2, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + -2, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + 2 + ], + [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + -2 + ], + [ + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + -2, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 0, + 2 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 0, + -2 + ], + [ + 0, + 0, + 0, + 0, + 2, + 2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 2 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + -2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1 + ], + [ + 1, + 1, + 1, + 1, + 1, + -1, + -1, + 1 + ], + [ + 1, + 1, + 1, + 1, + -1, + 1, + 1, + -1 + ], + [ + 1, + 1, + 1, + 1, + -1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + 1, + -1, + -1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + 1, + 1, + -1 + ], + [ + 1, + 1, + 1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 1, + 1, + 1, + -1, + 1, + -1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + 1, + 1, + -1, + -1, + -1, + -1, + 1 + ], + [ + 1, + 1, + -1, + 1, + 1, + 1, + 1, + -1 + ], + [ + 1, + 1, + -1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + 1, + -1, + 1, + 1, + -1, + 1, + 1 + ], + [ + 1, + 1, + -1, + 1, + 1, + -1, + -1, + -1 + ], + [ + 1, + 1, + -1, + 1, + -1, + 1, + 1, + 1 + ], + [ + 1, + 1, + -1, + 1, + -1, + 1, + -1, + -1 + ], + [ + 1, + 1, + -1, + 1, + -1, + -1, + 1, + -1 + ], + [ + 1, + 1, + -1, + 1, + -1, + -1, + -1, + 1 + ], + [ + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + -1, + -1, + 1, + 1, + -1, + -1 + ], + [ + 1, + 1, + -1, + -1, + 1, + -1, + 1, + -1 + ], + [ + 1, + 1, + -1, + -1, + 1, + -1, + -1, + 1 + ], + [ + 1, + 1, + -1, + -1, + -1, + 1, + 1, + -1 + ], + [ + 1, + 1, + -1, + -1, + -1, + 1, + -1, + 1 + ], + [ + 1, + 1, + -1, + -1, + -1, + -1, + 1, + 1 + ], + [ + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + 1, + 1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + -1, + 1, + 1, + 1, + -1, + 1, + 1 + ], + [ + 1, + -1, + 1, + 1, + 1, + -1, + -1, + -1 + ], + [ + 1, + -1, + 1, + 1, + -1, + 1, + 1, + 1 + ], + [ + 1, + -1, + 1, + 1, + -1, + 1, + -1, + -1 + ], + [ + 1, + -1, + 1, + 1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + 1, + 1, + -1, + -1, + -1, + 1 + ], + [ + 1, + -1, + 1, + -1, + 1, + 1, + 1, + 1 + ], + [ + 1, + -1, + 1, + -1, + 1, + 1, + -1, + -1 + ], + [ + 1, + -1, + 1, + -1, + 1, + -1, + 1, + -1 + ], + [ + 1, + -1, + 1, + -1, + 1, + -1, + -1, + 1 + ], + [ + 1, + -1, + 1, + -1, + -1, + 1, + 1, + -1 + ], + [ + 1, + -1, + 1, + -1, + -1, + 1, + -1, + 1 + ], + [ + 1, + -1, + 1, + -1, + -1, + -1, + 1, + 1 + ], + [ + 1, + -1, + 1, + -1, + -1, + -1, + -1, + -1 + ], + [ + 1, + -1, + -1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + -1, + -1, + 1, + 1, + 1, + -1, + -1 + ], + [ + 1, + -1, + -1, + 1, + 1, + -1, + 1, + -1 + ], + [ + 1, + -1, + -1, + 1, + 1, + -1, + -1, + 1 + ], + [ + 1, + -1, + -1, + 1, + -1, + 1, + 1, + -1 + ], + [ + 1, + -1, + -1, + 1, + -1, + 1, + -1, + 1 + ], + [ + 1, + -1, + -1, + 1, + -1, + -1, + 1, + 1 + ], + [ + 1, + -1, + -1, + 1, + -1, + -1, + -1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + 1, + 1, + -1, + 1 + ], + [ + 1, + -1, + -1, + -1, + 1, + -1, + 1, + 1 + ], + [ + 1, + -1, + -1, + -1, + 1, + -1, + -1, + -1 + ], + [ + 1, + -1, + -1, + -1, + -1, + 1, + 1, + 1 + ], + [ + 1, + -1, + -1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 1 + ] + ], + "punctured_frame": [ + 0, + 1, + 26, + 27, + 44, + 45, + 54, + 55 + ], + "live": [ + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111, + 112, + 113, + 114, + 115, + 116, + 117, + 118, + 119 + ] +} diff --git a/research/p112-rank6-cover-representatives/scan.py b/research/p112-rank6-cover-representatives/scan.py new file mode 100644 index 0000000000..8cb1595a06 --- /dev/null +++ b/research/p112-rank6-cover-representatives/scan.py @@ -0,0 +1,115 @@ +"""Independent support-representative screen. Apache-2.0; woklerx/Codex.""" +from pathlib import Path +from itertools import combinations,product +from collections import Counter +import argparse,hashlib,json +HERE=Path(__file__).resolve().parent + +def need(v,s): + if not v:raise ValueError(s) +def bits(v): + while v: + b=v&-v;yield b.bit_length()-1;v^=b +def basis(rows): + piv={} + for v in rows: + while v: + b=v&-v + if b in piv:v^=piv[b] + else:piv[b]=v;break + return list(piv.values()) +def run(): + for p in json.loads((HERE/'DEPENDENCY.json').read_text()): + need(hashlib.sha256((HERE/p['local']).read_bytes()).hexdigest()==p['sha256'],'dependency bytes') + data=json.loads((HERE/'inputs/MODEL.json').read_text());cover=json.loads((HERE/'inputs/COVERING.json').read_text()) + rs=data['lines'];live=data['live'];lm=sum(1<=8-len(q): + b=c&-c;c^=b;i=b.bit_length()-1;extend(q+[i],c&adj[i]) + extend([],lm);need(len(frames)==1260,'frame count') + incidence=[0]*120 + for k,f in enumerate(frames): + for i in f:incidence[i]|=1<>k&1 for p in patterns) for k in range(len(frames))] + need(min(frame_counts)==8 and hashlib.sha256(bytes(frame_counts)).hexdigest()==cover['exact_check']['frame_counts_sha256'],'original full frame demand') + need((lm&~original_diagonal).bit_count()==21,'original diagonal gap') + exact=[dict(count=0,union=0,candidates=[]) for _ in patterns] + monotone=[dict(count=0,union=0,candidates=[]) for _ in patterns] + ranks=Counter();cases=0;unique={} + for a,l in enumerate(support): + for b,r in enumerate(support): + bs=basis(pair[j]&l for j in bits(r));ranks[len(bs)]+=1 + if len(bs)!=7:continue + words=[0] + for g in bs:words += [w^g for w in words] + for w in sorted(words[1:]): + cases+=1;row=l^w;ph=hits(row)&hits(r);diag=row&r + need(len(basis(pair[i]&r for i in bits(row)))==6,'every maximal slice is rank six') + for k,target in enumerate(patterns): + if target&~ph:continue + rec=monotone[k];rec['count']+=1;rec['union']|=diag + # Transposition preserves hits and diagonal support, so it + # cannot enlarge these unions or representative classes. + rec['candidates'].append([a,b,hex(w),hex(diag)]) + if ph==target: + rec=exact[k];rec['count']+=1;rec['union']|=diag;rec['candidates'].append([a,b,hex(w),hex(diag)]) + need(cases==967232 and ranks=={7:7616,8:37440,9:12544},'complete dictionary') + result=dict(status='PASS_RANK6_REPRESENTATIVE_SCAN',parent_ranks=dict(sorted(ranks.items())),cases=cases,original_missing=list(bits(lm&~original_diagonal))) + for name,records in [('exact',exact),('monotone',monotone)]: + u=0 + for rec in records:u|=rec['union'] + result[name]=dict(missing_even_after_union=list(bits(lm&~u)),counts=[x['count'] for x in records],diagonal_union_sizes=[x['union'].bit_count() for x in records],candidates_sha256=hashlib.sha256(json.dumps([r['candidates'] for r in records],separators=(',',':')).encode()).hexdigest()) + # Complete finite multiple-choice union search. Equal union states may + # safely be merged: future unions depend only on the covered set. + states={0:[]} + for rec in records: + choices={int(v[3],16):v[:3] for v in rec['candidates']} + states={old|mask:path+[witness] for old,path in states.items() for mask,witness in choices.items()} + best=max(states,key=lambda s:(s.bit_count(),s)) + result[name]['distinct_final_unions']=len(states) + result[name]['maximum_diagonals']=best.bit_count() + result[name]['best_terms']=states[best] + result[name]['best_missing']=list(bits(lm&~best)) + controls=[] + def reject(name,condition): + need(not condition,'false claim accepted: '+name);controls.append(name) + reject('frame hits imply diagonal coverage',original_diagonal==lm) + reject('any hit-preserving representatives can repair all diagonals',result['monotone']['maximum_diagonals']==112) + a,b,cut=cover['terms'][0] + reject('restoring removed rows preserves rank six',len(basis(pair[i]&support[b] for i in bits(support[a])))==6) + # Transposition changes orientation, but never the diagonal supports or + # frame-hit incidence; all column-side cuts are therefore included. + need(all(len(basis(pair[i]&support[b] for i in bits(support[a]^int(cut,16))))==6 + for a,b,cut in result['exact']['best_terms']),'positive attaining representatives') + need(result['exact']['maximum_diagonals']==99 and result['monotone']['maximum_diagonals']==99,'sharp diagonal cap') + result['controls']=controls + return result +if __name__=='__main__': + ap=argparse.ArgumentParser();ap.add_argument('--write',action='store_true');args=ap.parse_args() + result=json.loads(json.dumps(run()));path=HERE/'CERTIFICATE.json' + if args.write:path.write_text(json.dumps(result,indent=2)+'\n') + else:need(result==json.loads(path.read_text()),'complete certificate mismatch') + print('PASS_RANK6_REPRESENTATIVES parents=7616 slices=967232 patterns=10 max_diagonals=99 unavoidable_missing=13 controls=3') diff --git a/research/p112-rank6-cover-representatives/verify.py b/research/p112-rank6-cover-representatives/verify.py new file mode 100644 index 0000000000..bc6fad08b9 --- /dev/null +++ b/research/p112-rank6-cover-representatives/verify.py @@ -0,0 +1,5 @@ +from scan import run,need,HERE +import json +if __name__ == "__main__": + need(json.loads(json.dumps(run()))==json.loads((HERE/"CERTIFICATE.json").read_text()),"complete certificate") + print("PASS_RANK6_REPRESENTATIVES") From 7e38878c38f629ed02663f30352d6308a4af66a6 Mon Sep 17 00:00:00 2001 From: woklerx Date: Tue, 13 Oct 2026 17:49:25 -0700 Subject: [PATCH 2/2] Credit concurrent union bound and lead with sharp joint optimum --- research/p112-rank6-cover-representatives/PR-BODY.md | 2 +- research/p112-rank6-cover-representatives/README.md | 8 ++++---- research/p112-rank6-cover-representatives/TASK.json | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/research/p112-rank6-cover-representatives/PR-BODY.md b/research/p112-rank6-cover-representatives/PR-BODY.md index 115e8084cb..d6b1c7e94c 100644 --- a/research/p112-rank6-cover-representatives/PR-BODY.md +++ b/research/p112-rank6-cover-representatives/PR-BODY.md @@ -1,4 +1,4 @@ -PR1347 leaves 21 diagonals uncovered in its ten-term rank-six frame cover and warns that one representative per frame pattern may hide repairs. This successor scans all 967232 maximal slices across 7616 parents and proves that every representative choice preserving each original term frame-hit set covers at most **99 of 112 diagonals**. Arbitrary joint cuts of cost at most six reduce to this census by the supplied rank-factor argument. A 99-diagonal attaining tuple and three controls are included. +Selecting one support representative for each of PR1347's ten rank-six frame patterns covers at most **99 of 112 diagonals**, and an explicit tuple attains 99. Concurrent [PR1402](https://github.com/CrocSwap/integer-mult-bounds/pull/1402), inspected at `e5917254b781e9f327436ac682baab1c93941aed`, gives the same complete representative census and the union bound of 102. This contribution strengthens that union bound by three unavoidable simultaneous misses through an exact 903-state multiple-choice calculation; no priority is claimed for the overlapping census or union obstruction. Arbitrary joint cuts of cost at most six reduce to the census by the supplied rank-factor argument. Three rejection controls and the attaining tuple are included. This is a scoped support obstruction; changing frame patterns, other parent costs, coefficients and physical synthesis remain open. No new kappa or supplier. Source PR1347 is pinned at 64fd5f9e91961dedc16118fcc7ad71ee82efe28f, retaining contributor lineage. Prepared for woklerx with substantial OpenAI Codex assistance; Apache-2.0. diff --git a/research/p112-rank6-cover-representatives/README.md b/research/p112-rank6-cover-representatives/README.md index 3bbd58cb4b..8d9ce1efd8 100644 --- a/research/p112-rank6-cover-representatives/README.md +++ b/research/p112-rank6-cover-representatives/README.md @@ -1,10 +1,10 @@ -# The rank-six frame cover cannot be repaired by changing support representatives +# Sharp joint-choice bound: the ten rank-six patterns cover at most 99 diagonals PR1347 supplies ten rank-six atoms with copy bill 60 meeting each P112 orthogonal frame at least eight times, but its chosen supports leave 21 diagonals uncovered. It explicitly warns that retaining one support representative per frame-hit pattern may lose useful diagonal coverage. This package resolves that question for its **ten published term patterns**: allowing any cost-seven C/N root-star parent, arbitrary joint support trims of cost at most six, and extra frame hits, **at most 99 of 112 diagonals can be covered**. At least 13 remain impossible. -Every original pattern has four tagged maximal representatives, two distinct diagonal supports, and no representative with a strict superset of its frame hits. The union of all alternatives still misses ten fixed diagonals; the complete multiple-choice calculation strengthens that to 13 simultaneously. An explicit support choice attaining 99 is in CERTIFICATE.json. This is a support obstruction, not a coefficient decoder or supplier. +The additional result is the **joint-choice optimum of 99**, not priority for the representative census or its union bound. Concurrent [PR1402](https://github.com/CrocSwap/integer-mult-bounds/pull/1402), inspected at head `e5917254b781e9f327436ac682baab1c93941aed`, independently gives the same four tagged maximal representatives per original pattern, two distinct diagonal supports, and their 102-diagonal union. Our complete multiple-choice calculation shows that selecting one representative for each of the ten terms necessarily loses at least three more diagonals: 13 are missing simultaneously, although only ten are absent from the union of every alternative. An explicit support choice attaining 99 is in CERTIFICATE.json. This is a support obstruction, not a coefficient decoder or supplier. -The independently written scan reconstructs all 1260 frames, all 57600 tagged parent pairs, 7616 cost-seven parents and 967232 maximal one-axis rank-six slices. All 903 distinct final union states of the ten binary choices are tested. The domain changes PR1347's representative choice, not its general frame-capacity theorem. Ten terms with different frame patterns, mixed ranks, other parents or punctures remain outside this result. +The independently written scan reconstructs all 1260 frames, all 57600 tagged parent pairs, 7616 cost-seven parents and 967232 maximal one-axis rank-six slices. No retained representative has a strict superset of an original pattern's frame hits. All 903 distinct final union states of the ten binary choices are tested. The domain changes PR1347's representative choice, not its general frame-capacity theorem. Ten terms with different frame patterns, mixed ranks, other parents or punctures remain outside this result. ## Proof @@ -33,4 +33,4 @@ Can ten rank-six terms cover every diagonal and every frame demand when frame hi ## Sources and credit -The cover and root order are copied byte-for-byte from Cinna Davis (@1337isnot1337), PR1347 at 64fd5f9e91961dedc16118fcc7ad71ee82efe28f; DEPENDENCY.json records paths, Git blobs and SHA256. Apache-2.0. Its source lineage retains Navinor PR1226, David Arias PR1236, Hanson Sun PR1242, Cinna Davis PR1323, DreamingOfClouds PR717 and themilkman216 PR968. New scan and proof prepared for woklerx with substantial OpenAI Codex assistance; no independent human review claimed. +The cover and root order are copied byte-for-byte from Cinna Davis (@1337isnot1337), PR1347 at 64fd5f9e91961dedc16118fcc7ad71ee82efe28f; DEPENDENCY.json records paths, Git blobs and SHA256. Apache-2.0. Its source lineage retains Navinor PR1226, David Arias PR1236, Hanson Sun PR1242, Cinna Davis PR1323, DreamingOfClouds PR717 and themilkman216 PR968. PR1402's concurrent complete representative census and union obstruction are credited above; it was identified during the final overlap refresh after this independent computation. No PR1402 executable or certificate is imported. This package adds the sharp one-choice-per-term optimum and the written domination proof for arbitrary joint restrictions of rank at most six. New scan and proof prepared for woklerx with substantial OpenAI Codex assistance; no independent human review claimed. diff --git a/research/p112-rank6-cover-representatives/TASK.json b/research/p112-rank6-cover-representatives/TASK.json index 18c2ca7f8b..fbe627296c 100644 --- a/research/p112-rank6-cover-representatives/TASK.json +++ b/research/p112-rank6-cover-representatives/TASK.json @@ -41,7 +41,7 @@ }, "scope_status": "refined", "actual_scope": "Sharp diagonal cap99 for arbitrary cost<=6 descendants of cost7 C/N parents preserving each term frame-hit set.", - "scope_change_reason": "Audit the support-representative gap explicitly left by PR1347 on its ten published frame-hit patterns.", + "scope_change_reason": "Audit the support-representative gap left by PR1347. Final overlap refresh found concurrent PR1402's union cap102; retain the additional sharp joint-choice cap99 and credit the overlapping representative census.", "bottleneck_link": "Rejects a bill60 candidate before coefficient synthesis and physical realization.", "budget_minutes": 60, "stop_rule": "Complete967232slice census and exact choice coverage.",