From 489c55e73cacda286cd6eb29b28f2327b5cb95c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Manuel=20E=2E=20Rey-=C3=81lvarez=20Zafiria?= Date: Mon, 31 Aug 2026 08:58:26 +0200 Subject: [PATCH] experimental: add a nonuniform T(509,35,8) certificate Add the explicit 762,054,269,114-face hierarchical cover, its fixed-asymptotic packing lemma, and two exact independent audits. --- .../atlas-nonuniform-turan-35-to-8/README.md | 45 + .../SHA256SUMS.txt | 9 + .../atlas-nonuniform-turan-35-to-8/cover.txt | 311 ++ .../independent_output.json | 71 + .../optimizer_output.json | 2540 +++++++++++++++++ .../primary_output.json | 93 + .../atlas_nonuniform_turan_35_to_8_cover.md | 153 + .../audit_atlas_nonuniform_turan_cover.py | 157 + .../optimize_atlas_nonuniform_turan_cover.py | 267 ++ .../verify_atlas_nonuniform_turan_cover.py | 210 ++ 10 files changed, 3856 insertions(+) create mode 100644 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/README.md create mode 100644 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/SHA256SUMS.txt create mode 100644 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt create mode 100644 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/independent_output.json create mode 100644 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/optimizer_output.json create mode 100644 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/primary_output.json create mode 100644 experimental/notes/atlas/atlas_nonuniform_turan_35_to_8_cover.md create mode 100644 experimental/scripts/audit_atlas_nonuniform_turan_cover.py create mode 100644 experimental/scripts/optimize_atlas_nonuniform_turan_cover.py create mode 100644 experimental/scripts/verify_atlas_nonuniform_turan_cover.py diff --git a/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/README.md b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/README.md new file mode 100644 index 000000000..01c32a92d --- /dev/null +++ b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/README.md @@ -0,0 +1,45 @@ +# Atlas nonuniform `T(509,35,8)` certificate + +**Author:** Manuel E. Rey-Álvarez Zafiria + +This directory records an explicit nonuniform hierarchical `T(509,35,8)` +system of cardinality `762,054,269,114`. + +`optimizer_output.json` contains the 305 selected six-color patterns and the +CP-SAT search metadata. The optimizer status is `FEASIBLE`; it is used only +as a source of an explicit witness, not as an optimality certificate. + +`cover.txt` is the compact frozen witness generated from that JSON file. +`primary_output.json` and `independent_output.json` record two exact audits. +Both auditors enumerate every relevant integer composition and recompute the +cardinality with integer binomial arithmetic. They use only the Python +standard library. + +From the repository root, reproduce the recorded cover and audits with: + +```text +python3 experimental/scripts/verify_atlas_nonuniform_turan_cover.py \ + experimental/data/certificates/atlas-nonuniform-turan-35-to-8/optimizer_output.json \ + /tmp/atlas_cover.txt \ + /tmp/atlas_primary_output.json + +python3 experimental/scripts/audit_atlas_nonuniform_turan_cover.py \ + /tmp/atlas_cover.txt \ + /tmp/atlas_independent_output.json + +cmp /tmp/atlas_cover.txt \ + experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt +cmp /tmp/atlas_primary_output.json \ + experimental/data/certificates/atlas-nonuniform-turan-35-to-8/primary_output.json +cmp /tmp/atlas_independent_output.json \ + experimental/data/certificates/atlas-nonuniform-turan-35-to-8/independent_output.json +``` + +The optional search implementation +`experimental/scripts/optimize_atlas_nonuniform_turan_cover.py` requires +OR-Tools. Re-running the search is unnecessary for checking the finite +theorem, and a time-limited parallel search need not reproduce the same +feasible witness. + +`SHA256SUMS.txt` authenticates the note, implementations, and recorded +certificate files. diff --git a/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/SHA256SUMS.txt b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/SHA256SUMS.txt new file mode 100644 index 000000000..bcf6fa449 --- /dev/null +++ b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/SHA256SUMS.txt @@ -0,0 +1,9 @@ +500ebb342a0071ff2a935b44feee785ea0e46fbc9d41d14ff92ffb22db6fd61c experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt +bffecc5a6121834418fb8236ffb8dd85c559218e27b152153e07fc0cfddf97a4 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/independent_output.json +721083a040bb6c7faab6c2c8bd0c635b4dadeebcc98f42e97f1b87569db6acfb experimental/data/certificates/atlas-nonuniform-turan-35-to-8/optimizer_output.json +33040f8f204f51b5dee13fe97b39f85d14d179f0ad265ba8cb15f8ee97021870 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/primary_output.json +32a86ce4189d65587862abcef02617363094930eaf6f905533a30be83dfb5868 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/README.md +3b2bd49ff90dd5beedf1120119bc4daab91175090b433be05af510e1c643a328 experimental/notes/atlas/atlas_nonuniform_turan_35_to_8_cover.md +9ba9428042712afcbf74842777330f9ecddac81fc37e68d318e58e26b2d395c1 experimental/scripts/audit_atlas_nonuniform_turan_cover.py +9f72e147439b121626eff0ad48bf0754adc0d31dc7ef2d17abaee24ea5576240 experimental/scripts/optimize_atlas_nonuniform_turan_cover.py +3f96b076f973b0cb852bfd83c5e9dd1185de08a84624f5334fb1e6696322db74 experimental/scripts/verify_atlas_nonuniform_turan_cover.py diff --git a/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt new file mode 100644 index 000000000..4a97d9568 --- /dev/null +++ b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt @@ -0,0 +1,311 @@ +ATLAS_NONUNIFORM_HIERARCHICAL_COVER_V1 +509 35 8 +3 +177 13 6 89 +0 0 0 0 0 8 +0 0 0 0 3 5 +0 0 0 0 4 4 +0 0 0 0 6 2 +0 0 0 0 8 0 +0 0 0 1 0 7 +0 0 0 1 7 0 +0 0 0 2 0 6 +0 0 0 3 0 5 +0 0 0 3 5 0 +0 0 0 4 0 4 +0 0 0 5 0 3 +0 0 0 6 2 0 +0 0 0 7 0 1 +0 0 0 8 0 0 +0 0 2 0 0 6 +0 0 2 2 0 4 +0 0 2 4 0 2 +0 0 3 1 1 3 +0 0 3 5 0 0 +0 0 4 0 0 4 +0 0 4 0 2 2 +0 0 4 0 4 0 +0 0 4 4 0 0 +0 0 5 2 0 1 +0 0 6 0 2 0 +0 0 8 0 0 0 +0 1 0 2 4 1 +0 2 0 0 3 3 +0 2 0 0 6 0 +0 2 0 3 0 3 +0 2 0 5 1 0 +0 2 3 0 3 0 +0 2 3 3 0 0 +0 2 6 0 0 0 +0 3 0 0 1 4 +0 3 0 0 5 0 +0 3 0 4 1 0 +0 3 0 5 0 0 +0 3 2 0 0 3 +0 3 2 0 3 0 +0 3 2 3 0 0 +0 3 3 0 0 2 +0 3 3 0 2 0 +0 4 0 0 2 2 +0 4 4 0 0 0 +0 5 0 0 0 3 +0 5 0 0 3 0 +0 5 0 3 0 0 +0 5 2 0 0 1 +0 6 0 2 0 0 +0 7 0 1 0 0 +0 8 0 0 0 0 +1 0 1 3 3 0 +1 0 2 0 5 0 +1 0 7 0 0 0 +1 2 0 0 0 5 +2 0 0 0 2 4 +2 0 0 0 4 2 +2 0 0 2 2 2 +2 0 0 4 2 0 +2 0 0 6 0 0 +2 0 4 2 0 0 +2 0 5 0 0 1 +2 3 0 0 3 0 +2 4 0 2 0 0 +2 6 0 0 0 0 +3 0 0 0 0 5 +3 0 0 0 5 0 +3 0 1 3 0 1 +3 0 2 0 3 0 +3 2 0 0 0 3 +3 2 3 0 0 0 +3 3 2 0 0 0 +3 5 0 0 0 0 +4 0 0 0 0 4 +4 0 0 0 2 2 +4 0 0 0 4 0 +4 0 0 2 0 2 +4 0 0 2 2 0 +4 0 0 4 0 0 +4 0 4 0 0 0 +4 4 0 0 0 0 +5 0 0 0 0 3 +5 0 3 0 0 0 +5 2 0 1 0 0 +6 0 1 0 1 0 +7 1 0 0 0 0 +8 0 0 0 0 0 +166 12 6 108 +0 0 0 0 0 8 +0 0 0 0 1 7 +0 0 0 0 4 4 +0 0 0 0 6 2 +0 0 0 0 8 0 +0 0 0 2 0 6 +0 0 0 2 4 2 +0 0 0 2 6 0 +0 0 0 3 0 5 +0 0 0 3 5 0 +0 0 0 4 2 2 +0 0 0 4 4 0 +0 0 0 5 0 3 +0 0 0 6 0 2 +0 0 0 6 2 0 +0 0 0 8 0 0 +0 0 1 0 2 5 +0 0 1 3 3 1 +0 0 2 0 0 6 +0 0 2 0 5 1 +0 0 2 2 0 4 +0 0 3 1 1 3 +0 0 3 3 1 1 +0 0 4 0 0 4 +0 0 4 0 2 2 +0 0 4 0 4 0 +0 0 4 4 0 0 +0 0 6 0 0 2 +0 0 6 0 2 0 +0 0 7 1 0 0 +0 0 8 0 0 0 +0 1 0 7 0 0 +0 1 1 3 0 3 +0 1 3 1 3 0 +0 2 0 0 0 6 +0 2 0 2 0 4 +0 2 1 0 5 0 +0 2 2 0 0 4 +0 2 2 0 2 2 +0 2 2 0 4 0 +0 2 2 4 0 0 +0 2 4 0 0 2 +0 2 4 0 2 0 +0 2 6 0 0 0 +0 3 0 1 1 3 +0 3 0 1 3 1 +0 3 1 3 1 0 +0 3 3 2 0 0 +0 3 5 0 0 0 +0 4 0 0 0 4 +0 4 0 0 2 2 +0 4 0 0 4 0 +0 4 0 4 0 0 +0 4 2 0 0 2 +0 4 2 0 2 0 +0 4 4 0 0 0 +0 5 3 0 0 0 +0 6 0 0 0 2 +0 6 0 0 2 0 +0 6 2 0 0 0 +0 7 0 1 0 0 +0 8 0 0 0 0 +1 0 0 0 7 0 +1 0 2 5 0 0 +1 0 5 2 0 0 +1 1 0 0 3 3 +1 2 0 5 0 0 +1 5 0 2 0 0 +2 0 0 0 2 4 +2 0 0 0 4 2 +2 0 0 0 6 0 +2 0 0 2 2 2 +2 0 0 2 4 0 +2 0 0 4 0 2 +2 0 0 4 2 0 +2 0 0 6 0 0 +2 0 1 0 0 5 +2 0 4 2 0 0 +2 0 5 0 0 1 +2 2 2 2 0 0 +2 3 3 0 0 0 +2 4 0 2 0 0 +2 5 1 0 0 0 +3 0 0 0 5 0 +3 0 1 3 0 1 +3 0 2 0 3 0 +3 1 0 1 0 3 +3 1 3 0 1 0 +3 2 0 0 3 0 +3 3 0 0 1 1 +4 0 0 0 0 4 +4 0 0 0 2 2 +4 0 0 0 4 0 +4 0 0 2 0 2 +4 0 0 2 2 0 +4 0 0 4 0 0 +4 0 4 0 0 0 +4 2 2 0 0 0 +4 4 0 0 0 0 +5 0 0 0 3 0 +5 0 0 3 0 0 +5 0 2 0 0 1 +5 2 1 0 0 0 +6 0 0 0 0 2 +6 0 0 0 2 0 +6 0 0 2 0 0 +7 0 0 1 0 0 +8 0 0 0 0 0 +166 12 6 108 +0 0 0 0 0 8 +0 0 0 0 1 7 +0 0 0 0 4 4 +0 0 0 0 6 2 +0 0 0 0 8 0 +0 0 0 2 0 6 +0 0 0 2 4 2 +0 0 0 2 6 0 +0 0 0 3 0 5 +0 0 0 3 5 0 +0 0 0 4 2 2 +0 0 0 4 4 0 +0 0 0 5 0 3 +0 0 0 6 0 2 +0 0 0 6 2 0 +0 0 0 8 0 0 +0 0 1 0 2 5 +0 0 1 3 3 1 +0 0 2 0 0 6 +0 0 2 0 5 1 +0 0 2 2 0 4 +0 0 3 1 1 3 +0 0 3 3 1 1 +0 0 4 0 0 4 +0 0 4 0 2 2 +0 0 4 0 4 0 +0 0 4 4 0 0 +0 0 6 0 0 2 +0 0 6 0 2 0 +0 0 7 1 0 0 +0 0 8 0 0 0 +0 1 0 7 0 0 +0 1 1 3 0 3 +0 1 3 1 3 0 +0 2 0 0 0 6 +0 2 0 2 0 4 +0 2 1 0 5 0 +0 2 2 0 0 4 +0 2 2 0 2 2 +0 2 2 0 4 0 +0 2 2 4 0 0 +0 2 4 0 0 2 +0 2 4 0 2 0 +0 2 6 0 0 0 +0 3 0 1 1 3 +0 3 0 1 3 1 +0 3 1 3 1 0 +0 3 3 2 0 0 +0 3 5 0 0 0 +0 4 0 0 0 4 +0 4 0 0 2 2 +0 4 0 0 4 0 +0 4 0 4 0 0 +0 4 2 0 0 2 +0 4 2 0 2 0 +0 4 4 0 0 0 +0 5 3 0 0 0 +0 6 0 0 0 2 +0 6 0 0 2 0 +0 6 2 0 0 0 +0 7 0 1 0 0 +0 8 0 0 0 0 +1 0 0 0 7 0 +1 0 2 5 0 0 +1 0 5 2 0 0 +1 1 0 0 3 3 +1 2 0 5 0 0 +1 5 0 2 0 0 +2 0 0 0 2 4 +2 0 0 0 4 2 +2 0 0 0 6 0 +2 0 0 2 2 2 +2 0 0 2 4 0 +2 0 0 4 0 2 +2 0 0 4 2 0 +2 0 0 6 0 0 +2 0 1 0 0 5 +2 0 4 2 0 0 +2 0 5 0 0 1 +2 2 2 2 0 0 +2 3 3 0 0 0 +2 4 0 2 0 0 +2 5 1 0 0 0 +3 0 0 0 5 0 +3 0 1 3 0 1 +3 0 2 0 3 0 +3 1 0 1 0 3 +3 1 3 0 1 0 +3 2 0 0 3 0 +3 3 0 0 1 1 +4 0 0 0 0 4 +4 0 0 0 2 2 +4 0 0 0 4 0 +4 0 0 2 0 2 +4 0 0 2 2 0 +4 0 0 4 0 0 +4 0 4 0 0 0 +4 2 2 0 0 0 +4 4 0 0 0 0 +5 0 0 0 3 0 +5 0 0 3 0 0 +5 0 2 0 0 1 +5 2 1 0 0 0 +6 0 0 0 0 2 +6 0 0 0 2 0 +6 0 0 2 0 0 +7 0 0 1 0 0 +8 0 0 0 0 0 diff --git a/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/independent_output.json b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/independent_output.json new file mode 100644 index 000000000..3c1ac8f2e --- /dev/null +++ b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/independent_output.json @@ -0,0 +1,71 @@ +{ + "block_reports": [ + { + "block_index": 0, + "block_size": 177, + "color_sizes": [ + 30, + 30, + 30, + 29, + 29, + 29 + ], + "colors": 6, + "local_distribution_count": 8568, + "local_witness_size": 13, + "maximum_cover_multiplicity": 8, + "minimum_cover_multiplicity": 1, + "pattern_count": 89, + "selected_eight_subsets": 254104519142 + }, + { + "block_index": 1, + "block_size": 166, + "color_sizes": [ + 28, + 28, + 28, + 28, + 27, + 27 + ], + "colors": 6, + "local_distribution_count": 6188, + "local_witness_size": 12, + "maximum_cover_multiplicity": 8, + "minimum_cover_multiplicity": 1, + "pattern_count": 108, + "selected_eight_subsets": 253974874986 + }, + { + "block_index": 2, + "block_size": 166, + "color_sizes": [ + 28, + 28, + 28, + 28, + 27, + 27 + ], + "colors": 6, + "local_distribution_count": 6188, + "local_witness_size": 12, + "maximum_cover_multiplicity": 8, + "minimum_cover_multiplicity": 1, + "pattern_count": 108, + "selected_eight_subsets": 253974874986 + } + ], + "cover_sha256": "500ebb342a0071ff2a935b44feee785ea0e46fbc9d41d14ff92ffb22db6fd61c", + "face_size": 8, + "global_block_distribution_count": 666, + "global_witness_size": 35, + "payload_sha256": "6c565e0081d6e861bbd502094bb5591402c9a41028718d3a86cbed7d6357a66b", + "proof_scope": "Exact coverage and cardinality only; no optimality claim.", + "row_count": 509, + "schema": "atlas-nonuniform-hierarchical-cover-independent-audit/v1", + "selected_eight_subsets": 762054269114, + "status": "PASS_INDEPENDENT_NONUNIFORM_HIERARCHICAL_35_TO_8_COVER" +} diff --git a/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/optimizer_output.json b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/optimizer_output.json new file mode 100644 index 000000000..05722db2b --- /dev/null +++ b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/optimizer_output.json @@ -0,0 +1,2540 @@ +{ + "best_objective_bound": 525564363395, + "block_records": [ + { + "block_index": 0, + "block_size": 177, + "color_sizes": [ + 30, + 30, + 30, + 29, + 29, + 29 + ], + "colors": 6, + "exact_selected_eight_subsets": 254104519142, + "face_pattern_count": 1287, + "hint_exact_selected_eight_subsets": 259712529862, + "hint_pattern_count": 88, + "local_witness_size": 13, + "maximum_witness_cover_multiplicity": 8, + "minimum_witness_cover_multiplicity": 1, + "selected_pattern_count": 89, + "selected_patterns": [ + [ + 0, + 0, + 0, + 0, + 0, + 8 + ], + [ + 0, + 0, + 0, + 0, + 3, + 5 + ], + [ + 0, + 0, + 0, + 0, + 4, + 4 + ], + [ + 0, + 0, + 0, + 0, + 6, + 2 + ], + [ + 0, + 0, + 0, + 0, + 8, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 7 + ], + [ + 0, + 0, + 0, + 1, + 7, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 6 + ], + [ + 0, + 0, + 0, + 3, + 0, + 5 + ], + [ + 0, + 0, + 0, + 3, + 5, + 0 + ], + [ + 0, + 0, + 0, + 4, + 0, + 4 + ], + [ + 0, + 0, + 0, + 5, + 0, + 3 + ], + [ + 0, + 0, + 0, + 6, + 2, + 0 + ], + [ + 0, + 0, + 0, + 7, + 0, + 1 + ], + [ + 0, + 0, + 0, + 8, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + 6 + ], + [ + 0, + 0, + 2, + 2, + 0, + 4 + ], + [ + 0, + 0, + 2, + 4, + 0, + 2 + ], + [ + 0, + 0, + 3, + 1, + 1, + 3 + ], + [ + 0, + 0, + 3, + 5, + 0, + 0 + ], + [ + 0, + 0, + 4, + 0, + 0, + 4 + ], + [ + 0, + 0, + 4, + 0, + 2, + 2 + ], + [ + 0, + 0, + 4, + 0, + 4, + 0 + ], + [ + 0, + 0, + 4, + 4, + 0, + 0 + ], + [ + 0, + 0, + 5, + 2, + 0, + 1 + ], + [ + 0, + 0, + 6, + 0, + 2, + 0 + ], + [ + 0, + 0, + 8, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 2, + 4, + 1 + ], + [ + 0, + 2, + 0, + 0, + 3, + 3 + ], + [ + 0, + 2, + 0, + 0, + 6, + 0 + ], + [ + 0, + 2, + 0, + 3, + 0, + 3 + ], + [ + 0, + 2, + 0, + 5, + 1, + 0 + ], + [ + 0, + 2, + 3, + 0, + 3, + 0 + ], + [ + 0, + 2, + 3, + 3, + 0, + 0 + ], + [ + 0, + 2, + 6, + 0, + 0, + 0 + ], + [ + 0, + 3, + 0, + 0, + 1, + 4 + ], + [ + 0, + 3, + 0, + 0, + 5, + 0 + ], + [ + 0, + 3, + 0, + 4, + 1, + 0 + ], + [ + 0, + 3, + 0, + 5, + 0, + 0 + ], + [ + 0, + 3, + 2, + 0, + 0, + 3 + ], + [ + 0, + 3, + 2, + 0, + 3, + 0 + ], + [ + 0, + 3, + 2, + 3, + 0, + 0 + ], + [ + 0, + 3, + 3, + 0, + 0, + 2 + ], + [ + 0, + 3, + 3, + 0, + 2, + 0 + ], + [ + 0, + 4, + 0, + 0, + 2, + 2 + ], + [ + 0, + 4, + 4, + 0, + 0, + 0 + ], + [ + 0, + 5, + 0, + 0, + 0, + 3 + ], + [ + 0, + 5, + 0, + 0, + 3, + 0 + ], + [ + 0, + 5, + 0, + 3, + 0, + 0 + ], + [ + 0, + 5, + 2, + 0, + 0, + 1 + ], + [ + 0, + 6, + 0, + 2, + 0, + 0 + ], + [ + 0, + 7, + 0, + 1, + 0, + 0 + ], + [ + 0, + 8, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 1, + 3, + 3, + 0 + ], + [ + 1, + 0, + 2, + 0, + 5, + 0 + ], + [ + 1, + 0, + 7, + 0, + 0, + 0 + ], + [ + 1, + 2, + 0, + 0, + 0, + 5 + ], + [ + 2, + 0, + 0, + 0, + 2, + 4 + ], + [ + 2, + 0, + 0, + 0, + 4, + 2 + ], + [ + 2, + 0, + 0, + 2, + 2, + 2 + ], + [ + 2, + 0, + 0, + 4, + 2, + 0 + ], + [ + 2, + 0, + 0, + 6, + 0, + 0 + ], + [ + 2, + 0, + 4, + 2, + 0, + 0 + ], + [ + 2, + 0, + 5, + 0, + 0, + 1 + ], + [ + 2, + 3, + 0, + 0, + 3, + 0 + ], + [ + 2, + 4, + 0, + 2, + 0, + 0 + ], + [ + 2, + 6, + 0, + 0, + 0, + 0 + ], + [ + 3, + 0, + 0, + 0, + 0, + 5 + ], + [ + 3, + 0, + 0, + 0, + 5, + 0 + ], + [ + 3, + 0, + 1, + 3, + 0, + 1 + ], + [ + 3, + 0, + 2, + 0, + 3, + 0 + ], + [ + 3, + 2, + 0, + 0, + 0, + 3 + ], + [ + 3, + 2, + 3, + 0, + 0, + 0 + ], + [ + 3, + 3, + 2, + 0, + 0, + 0 + ], + [ + 3, + 5, + 0, + 0, + 0, + 0 + ], + [ + 4, + 0, + 0, + 0, + 0, + 4 + ], + [ + 4, + 0, + 0, + 0, + 2, + 2 + ], + [ + 4, + 0, + 0, + 0, + 4, + 0 + ], + [ + 4, + 0, + 0, + 2, + 0, + 2 + ], + [ + 4, + 0, + 0, + 2, + 2, + 0 + ], + [ + 4, + 0, + 0, + 4, + 0, + 0 + ], + [ + 4, + 0, + 4, + 0, + 0, + 0 + ], + [ + 4, + 4, + 0, + 0, + 0, + 0 + ], + [ + 5, + 0, + 0, + 0, + 0, + 3 + ], + [ + 5, + 0, + 3, + 0, + 0, + 0 + ], + [ + 5, + 2, + 0, + 1, + 0, + 0 + ], + [ + 6, + 0, + 1, + 0, + 1, + 0 + ], + [ + 7, + 1, + 0, + 0, + 0, + 0 + ], + [ + 8, + 0, + 0, + 0, + 0, + 0 + ] + ], + "witness_pattern_count": 8568 + }, + { + "block_index": 1, + "block_size": 166, + "color_sizes": [ + 28, + 28, + 28, + 28, + 27, + 27 + ], + "colors": 6, + "exact_selected_eight_subsets": 253974874986, + "face_pattern_count": 1287, + "hint_exact_selected_eight_subsets": 253974874986, + "hint_pattern_count": 108, + "local_witness_size": 12, + "maximum_witness_cover_multiplicity": 8, + "minimum_witness_cover_multiplicity": 1, + "selected_pattern_count": 108, + "selected_patterns": [ + [ + 0, + 0, + 0, + 0, + 0, + 8 + ], + [ + 0, + 0, + 0, + 0, + 1, + 7 + ], + [ + 0, + 0, + 0, + 0, + 4, + 4 + ], + [ + 0, + 0, + 0, + 0, + 6, + 2 + ], + [ + 0, + 0, + 0, + 0, + 8, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 6 + ], + [ + 0, + 0, + 0, + 2, + 4, + 2 + ], + [ + 0, + 0, + 0, + 2, + 6, + 0 + ], + [ + 0, + 0, + 0, + 3, + 0, + 5 + ], + [ + 0, + 0, + 0, + 3, + 5, + 0 + ], + [ + 0, + 0, + 0, + 4, + 2, + 2 + ], + [ + 0, + 0, + 0, + 4, + 4, + 0 + ], + [ + 0, + 0, + 0, + 5, + 0, + 3 + ], + [ + 0, + 0, + 0, + 6, + 0, + 2 + ], + [ + 0, + 0, + 0, + 6, + 2, + 0 + ], + [ + 0, + 0, + 0, + 8, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 2, + 5 + ], + [ + 0, + 0, + 1, + 3, + 3, + 1 + ], + [ + 0, + 0, + 2, + 0, + 0, + 6 + ], + [ + 0, + 0, + 2, + 0, + 5, + 1 + ], + [ + 0, + 0, + 2, + 2, + 0, + 4 + ], + [ + 0, + 0, + 3, + 1, + 1, + 3 + ], + [ + 0, + 0, + 3, + 3, + 1, + 1 + ], + [ + 0, + 0, + 4, + 0, + 0, + 4 + ], + [ + 0, + 0, + 4, + 0, + 2, + 2 + ], + [ + 0, + 0, + 4, + 0, + 4, + 0 + ], + [ + 0, + 0, + 4, + 4, + 0, + 0 + ], + [ + 0, + 0, + 6, + 0, + 0, + 2 + ], + [ + 0, + 0, + 6, + 0, + 2, + 0 + ], + [ + 0, + 0, + 7, + 1, + 0, + 0 + ], + [ + 0, + 0, + 8, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 7, + 0, + 0 + ], + [ + 0, + 1, + 1, + 3, + 0, + 3 + ], + [ + 0, + 1, + 3, + 1, + 3, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 6 + ], + [ + 0, + 2, + 0, + 2, + 0, + 4 + ], + [ + 0, + 2, + 1, + 0, + 5, + 0 + ], + [ + 0, + 2, + 2, + 0, + 0, + 4 + ], + [ + 0, + 2, + 2, + 0, + 2, + 2 + ], + [ + 0, + 2, + 2, + 0, + 4, + 0 + ], + [ + 0, + 2, + 2, + 4, + 0, + 0 + ], + [ + 0, + 2, + 4, + 0, + 0, + 2 + ], + [ + 0, + 2, + 4, + 0, + 2, + 0 + ], + [ + 0, + 2, + 6, + 0, + 0, + 0 + ], + [ + 0, + 3, + 0, + 1, + 1, + 3 + ], + [ + 0, + 3, + 0, + 1, + 3, + 1 + ], + [ + 0, + 3, + 1, + 3, + 1, + 0 + ], + [ + 0, + 3, + 3, + 2, + 0, + 0 + ], + [ + 0, + 3, + 5, + 0, + 0, + 0 + ], + [ + 0, + 4, + 0, + 0, + 0, + 4 + ], + [ + 0, + 4, + 0, + 0, + 2, + 2 + ], + [ + 0, + 4, + 0, + 0, + 4, + 0 + ], + [ + 0, + 4, + 0, + 4, + 0, + 0 + ], + [ + 0, + 4, + 2, + 0, + 0, + 2 + ], + [ + 0, + 4, + 2, + 0, + 2, + 0 + ], + [ + 0, + 4, + 4, + 0, + 0, + 0 + ], + [ + 0, + 5, + 3, + 0, + 0, + 0 + ], + [ + 0, + 6, + 0, + 0, + 0, + 2 + ], + [ + 0, + 6, + 0, + 0, + 2, + 0 + ], + [ + 0, + 6, + 2, + 0, + 0, + 0 + ], + [ + 0, + 7, + 0, + 1, + 0, + 0 + ], + [ + 0, + 8, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 0, + 7, + 0 + ], + [ + 1, + 0, + 2, + 5, + 0, + 0 + ], + [ + 1, + 0, + 5, + 2, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + 3, + 3 + ], + [ + 1, + 2, + 0, + 5, + 0, + 0 + ], + [ + 1, + 5, + 0, + 2, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 2, + 4 + ], + [ + 2, + 0, + 0, + 0, + 4, + 2 + ], + [ + 2, + 0, + 0, + 0, + 6, + 0 + ], + [ + 2, + 0, + 0, + 2, + 2, + 2 + ], + [ + 2, + 0, + 0, + 2, + 4, + 0 + ], + [ + 2, + 0, + 0, + 4, + 0, + 2 + ], + [ + 2, + 0, + 0, + 4, + 2, + 0 + ], + [ + 2, + 0, + 0, + 6, + 0, + 0 + ], + [ + 2, + 0, + 1, + 0, + 0, + 5 + ], + [ + 2, + 0, + 4, + 2, + 0, + 0 + ], + [ + 2, + 0, + 5, + 0, + 0, + 1 + ], + [ + 2, + 2, + 2, + 2, + 0, + 0 + ], + [ + 2, + 3, + 3, + 0, + 0, + 0 + ], + [ + 2, + 4, + 0, + 2, + 0, + 0 + ], + [ + 2, + 5, + 1, + 0, + 0, + 0 + ], + [ + 3, + 0, + 0, + 0, + 5, + 0 + ], + [ + 3, + 0, + 1, + 3, + 0, + 1 + ], + [ + 3, + 0, + 2, + 0, + 3, + 0 + ], + [ + 3, + 1, + 0, + 1, + 0, + 3 + ], + [ + 3, + 1, + 3, + 0, + 1, + 0 + ], + [ + 3, + 2, + 0, + 0, + 3, + 0 + ], + [ + 3, + 3, + 0, + 0, + 1, + 1 + ], + [ + 4, + 0, + 0, + 0, + 0, + 4 + ], + [ + 4, + 0, + 0, + 0, + 2, + 2 + ], + [ + 4, + 0, + 0, + 0, + 4, + 0 + ], + [ + 4, + 0, + 0, + 2, + 0, + 2 + ], + [ + 4, + 0, + 0, + 2, + 2, + 0 + ], + [ + 4, + 0, + 0, + 4, + 0, + 0 + ], + [ + 4, + 0, + 4, + 0, + 0, + 0 + ], + [ + 4, + 2, + 2, + 0, + 0, + 0 + ], + [ + 4, + 4, + 0, + 0, + 0, + 0 + ], + [ + 5, + 0, + 0, + 0, + 3, + 0 + ], + [ + 5, + 0, + 0, + 3, + 0, + 0 + ], + [ + 5, + 0, + 2, + 0, + 0, + 1 + ], + [ + 5, + 2, + 1, + 0, + 0, + 0 + ], + [ + 6, + 0, + 0, + 0, + 0, + 2 + ], + [ + 6, + 0, + 0, + 0, + 2, + 0 + ], + [ + 6, + 0, + 0, + 2, + 0, + 0 + ], + [ + 7, + 0, + 0, + 1, + 0, + 0 + ], + [ + 8, + 0, + 0, + 0, + 0, + 0 + ] + ], + "witness_pattern_count": 6188 + }, + { + "block_index": 2, + "block_size": 166, + "color_sizes": [ + 28, + 28, + 28, + 28, + 27, + 27 + ], + "colors": 6, + "exact_selected_eight_subsets": 253974874986, + "face_pattern_count": 1287, + "hint_exact_selected_eight_subsets": 253974874986, + "hint_pattern_count": 108, + "local_witness_size": 12, + "maximum_witness_cover_multiplicity": 8, + "minimum_witness_cover_multiplicity": 1, + "selected_pattern_count": 108, + "selected_patterns": [ + [ + 0, + 0, + 0, + 0, + 0, + 8 + ], + [ + 0, + 0, + 0, + 0, + 1, + 7 + ], + [ + 0, + 0, + 0, + 0, + 4, + 4 + ], + [ + 0, + 0, + 0, + 0, + 6, + 2 + ], + [ + 0, + 0, + 0, + 0, + 8, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 6 + ], + [ + 0, + 0, + 0, + 2, + 4, + 2 + ], + [ + 0, + 0, + 0, + 2, + 6, + 0 + ], + [ + 0, + 0, + 0, + 3, + 0, + 5 + ], + [ + 0, + 0, + 0, + 3, + 5, + 0 + ], + [ + 0, + 0, + 0, + 4, + 2, + 2 + ], + [ + 0, + 0, + 0, + 4, + 4, + 0 + ], + [ + 0, + 0, + 0, + 5, + 0, + 3 + ], + [ + 0, + 0, + 0, + 6, + 0, + 2 + ], + [ + 0, + 0, + 0, + 6, + 2, + 0 + ], + [ + 0, + 0, + 0, + 8, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 2, + 5 + ], + [ + 0, + 0, + 1, + 3, + 3, + 1 + ], + [ + 0, + 0, + 2, + 0, + 0, + 6 + ], + [ + 0, + 0, + 2, + 0, + 5, + 1 + ], + [ + 0, + 0, + 2, + 2, + 0, + 4 + ], + [ + 0, + 0, + 3, + 1, + 1, + 3 + ], + [ + 0, + 0, + 3, + 3, + 1, + 1 + ], + [ + 0, + 0, + 4, + 0, + 0, + 4 + ], + [ + 0, + 0, + 4, + 0, + 2, + 2 + ], + [ + 0, + 0, + 4, + 0, + 4, + 0 + ], + [ + 0, + 0, + 4, + 4, + 0, + 0 + ], + [ + 0, + 0, + 6, + 0, + 0, + 2 + ], + [ + 0, + 0, + 6, + 0, + 2, + 0 + ], + [ + 0, + 0, + 7, + 1, + 0, + 0 + ], + [ + 0, + 0, + 8, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 7, + 0, + 0 + ], + [ + 0, + 1, + 1, + 3, + 0, + 3 + ], + [ + 0, + 1, + 3, + 1, + 3, + 0 + ], + [ + 0, + 2, + 0, + 0, + 0, + 6 + ], + [ + 0, + 2, + 0, + 2, + 0, + 4 + ], + [ + 0, + 2, + 1, + 0, + 5, + 0 + ], + [ + 0, + 2, + 2, + 0, + 0, + 4 + ], + [ + 0, + 2, + 2, + 0, + 2, + 2 + ], + [ + 0, + 2, + 2, + 0, + 4, + 0 + ], + [ + 0, + 2, + 2, + 4, + 0, + 0 + ], + [ + 0, + 2, + 4, + 0, + 0, + 2 + ], + [ + 0, + 2, + 4, + 0, + 2, + 0 + ], + [ + 0, + 2, + 6, + 0, + 0, + 0 + ], + [ + 0, + 3, + 0, + 1, + 1, + 3 + ], + [ + 0, + 3, + 0, + 1, + 3, + 1 + ], + [ + 0, + 3, + 1, + 3, + 1, + 0 + ], + [ + 0, + 3, + 3, + 2, + 0, + 0 + ], + [ + 0, + 3, + 5, + 0, + 0, + 0 + ], + [ + 0, + 4, + 0, + 0, + 0, + 4 + ], + [ + 0, + 4, + 0, + 0, + 2, + 2 + ], + [ + 0, + 4, + 0, + 0, + 4, + 0 + ], + [ + 0, + 4, + 0, + 4, + 0, + 0 + ], + [ + 0, + 4, + 2, + 0, + 0, + 2 + ], + [ + 0, + 4, + 2, + 0, + 2, + 0 + ], + [ + 0, + 4, + 4, + 0, + 0, + 0 + ], + [ + 0, + 5, + 3, + 0, + 0, + 0 + ], + [ + 0, + 6, + 0, + 0, + 0, + 2 + ], + [ + 0, + 6, + 0, + 0, + 2, + 0 + ], + [ + 0, + 6, + 2, + 0, + 0, + 0 + ], + [ + 0, + 7, + 0, + 1, + 0, + 0 + ], + [ + 0, + 8, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 0, + 7, + 0 + ], + [ + 1, + 0, + 2, + 5, + 0, + 0 + ], + [ + 1, + 0, + 5, + 2, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + 3, + 3 + ], + [ + 1, + 2, + 0, + 5, + 0, + 0 + ], + [ + 1, + 5, + 0, + 2, + 0, + 0 + ], + [ + 2, + 0, + 0, + 0, + 2, + 4 + ], + [ + 2, + 0, + 0, + 0, + 4, + 2 + ], + [ + 2, + 0, + 0, + 0, + 6, + 0 + ], + [ + 2, + 0, + 0, + 2, + 2, + 2 + ], + [ + 2, + 0, + 0, + 2, + 4, + 0 + ], + [ + 2, + 0, + 0, + 4, + 0, + 2 + ], + [ + 2, + 0, + 0, + 4, + 2, + 0 + ], + [ + 2, + 0, + 0, + 6, + 0, + 0 + ], + [ + 2, + 0, + 1, + 0, + 0, + 5 + ], + [ + 2, + 0, + 4, + 2, + 0, + 0 + ], + [ + 2, + 0, + 5, + 0, + 0, + 1 + ], + [ + 2, + 2, + 2, + 2, + 0, + 0 + ], + [ + 2, + 3, + 3, + 0, + 0, + 0 + ], + [ + 2, + 4, + 0, + 2, + 0, + 0 + ], + [ + 2, + 5, + 1, + 0, + 0, + 0 + ], + [ + 3, + 0, + 0, + 0, + 5, + 0 + ], + [ + 3, + 0, + 1, + 3, + 0, + 1 + ], + [ + 3, + 0, + 2, + 0, + 3, + 0 + ], + [ + 3, + 1, + 0, + 1, + 0, + 3 + ], + [ + 3, + 1, + 3, + 0, + 1, + 0 + ], + [ + 3, + 2, + 0, + 0, + 3, + 0 + ], + [ + 3, + 3, + 0, + 0, + 1, + 1 + ], + [ + 4, + 0, + 0, + 0, + 0, + 4 + ], + [ + 4, + 0, + 0, + 0, + 2, + 2 + ], + [ + 4, + 0, + 0, + 0, + 4, + 0 + ], + [ + 4, + 0, + 0, + 2, + 0, + 2 + ], + [ + 4, + 0, + 0, + 2, + 2, + 0 + ], + [ + 4, + 0, + 0, + 4, + 0, + 0 + ], + [ + 4, + 0, + 4, + 0, + 0, + 0 + ], + [ + 4, + 2, + 2, + 0, + 0, + 0 + ], + [ + 4, + 4, + 0, + 0, + 0, + 0 + ], + [ + 5, + 0, + 0, + 0, + 3, + 0 + ], + [ + 5, + 0, + 0, + 3, + 0, + 0 + ], + [ + 5, + 0, + 2, + 0, + 0, + 1 + ], + [ + 5, + 2, + 1, + 0, + 0, + 0 + ], + [ + 6, + 0, + 0, + 0, + 0, + 2 + ], + [ + 6, + 0, + 0, + 0, + 2, + 0 + ], + [ + 6, + 0, + 0, + 2, + 0, + 0 + ], + [ + 7, + 0, + 0, + 1, + 0, + 0 + ], + [ + 8, + 0, + 0, + 0, + 0, + 0 + ] + ], + "witness_pattern_count": 6188 + } + ], + "block_sizes": [ + 177, + 166, + 166 + ], + "branches": 0, + "conflicts": 0, + "exact_selected_eight_subsets": 762054269114, + "face_size": 8, + "global_witness_size": 35, + "local_witness_sizes": [ + 13, + 12, + 12 + ], + "payload_sha256": "85137596d011b269a5c1e5ded05929e99d4c79315c4e3e25b10f76e8a755c008", + "pigeonhole_budget": 34, + "random_seed": 314159, + "relative_bound_gap": 0.31033210534199124, + "row_count": 509, + "schema": "atlas-nonuniform-hierarchical-cover-cp-sat/v1", + "status": "FEASIBLE", + "wall_time_seconds": 600.238731 +} diff --git a/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/primary_output.json b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/primary_output.json new file mode 100644 index 000000000..99aa1e4a0 --- /dev/null +++ b/experimental/data/certificates/atlas-nonuniform-turan-35-to-8/primary_output.json @@ -0,0 +1,93 @@ +{ + "block_audits": [ + { + "block_index": 0, + "block_size": 177, + "color_sizes": [ + 30, + 30, + 30, + 29, + 29, + 29 + ], + "colors": 6, + "local_distribution_count": 8568, + "local_witness_size": 13, + "maximum_cover_multiplicity": 8, + "minimum_cover_multiplicity": 1, + "pattern_count": 89, + "selected_eight_subsets": 254104519142 + }, + { + "block_index": 1, + "block_size": 166, + "color_sizes": [ + 28, + 28, + 28, + 28, + 27, + 27 + ], + "colors": 6, + "local_distribution_count": 6188, + "local_witness_size": 12, + "maximum_cover_multiplicity": 8, + "minimum_cover_multiplicity": 1, + "pattern_count": 108, + "selected_eight_subsets": 253974874986 + }, + { + "block_index": 2, + "block_size": 166, + "color_sizes": [ + 28, + 28, + 28, + 28, + 27, + 27 + ], + "colors": 6, + "local_distribution_count": 6188, + "local_witness_size": 12, + "maximum_cover_multiplicity": 8, + "minimum_cover_multiplicity": 1, + "pattern_count": 108, + "selected_eight_subsets": 253974874986 + } + ], + "block_sizes": [ + 177, + 166, + 166 + ], + "cover_sha256": "500ebb342a0071ff2a935b44feee785ea0e46fbc9d41d14ff92ffb22db6fd61c", + "face_size": 8, + "global_block_distribution_count": 666, + "global_witness_size": 35, + "local_witness_sizes": [ + 13, + 12, + 12 + ], + "optimizer_claims_optimality": false, + "optimizer_payload_sha256": "85137596d011b269a5c1e5ded05929e99d4c79315c4e3e25b10f76e8a755c008", + "optimizer_status": "FEASIBLE", + "payload_sha256": "b4c72a1784c5a741cbe34c76971af134a3c04663fdc17481f600c35c851deb04", + "pigeonhole_budget": 34, + "previous_parity_selected_eight_subsets": 2725371892323, + "previous_uniform_six_color_selected_eight_subsets": 911798442756, + "proof_summary": [ + "Every 35-composition across the macroblocks reaches at least one recorded local threshold.", + "Every color composition at that local threshold dominates a frozen weight-eight pattern for the same block.", + "Therefore every 35-subset of the 509 rows contains a frozen selected eight-face." + ], + "reduction_factor_against_parity": 3.5763488281374567, + "reduction_factor_against_uniform_six_color": 1.1965006689301794, + "row_count": 509, + "schema": "atlas-nonuniform-hierarchical-cover-freeze-audit/v1", + "selected_eight_subsets": 762054269114, + "status": "PASS_EXACT_NONUNIFORM_HIERARCHICAL_35_TO_8_COVER" +} diff --git a/experimental/notes/atlas/atlas_nonuniform_turan_35_to_8_cover.md b/experimental/notes/atlas/atlas_nonuniform_turan_35_to_8_cover.md new file mode 100644 index 000000000..61597e6b8 --- /dev/null +++ b/experimental/notes/atlas/atlas_nonuniform_turan_35_to_8_cover.md @@ -0,0 +1,153 @@ +# A nonuniform hierarchical `T(509,35,8)` system for RS-MCA + +**Author:** Manuel E. Rey-Álvarez Zafiria + +**Status:** exact finite theorem with two independent certificate checks. + +## Definitions + +Write `[n]={0,...,n-1}`. A `T(n,s,r)` system is a family +`C subseteq binom([n],r)` such that every `s`-subset of `[n]` contains a +member of `C`. + +If a block is split into six color classes and `F` is an eight-subset of the +block, its color pattern is the weak six-composition + +```text +(|F intersect color 0|,...,|F intersect color 5|) +``` + +of eight. + +## Fixed-asymptotic packing lemma + +Let `K` be a field and `t>=2`. For `i=1,2`, let `A_i` be monic of degree +`t`, and let `B_i` have degree at most `t-1`. Write + +```text +A_i = X^t + a_i X^(t-1) + lower terms. +``` + +Assume that, for fixed `q,alpha in K`, + +```text +[X^(t-1)] B_i = q, +[X^(t-2)] B_i = alpha + q a_i. +``` + +If `B_1/A_1` and `B_2/A_2` are distinct rational functions, then they agree +at at most `2t-3` elements of `K` that are not poles of either function. + +Indeed, agreement at `x` implies + +```text +(A_1 B_2 - A_2 B_1)(x)=0. +``` + +The coefficients of degrees `2t-1` and `2t-2` in this cross numerator are + +```text +q-q=0 +``` + +and + +```text +(alpha+q a_2)+q a_1-(alpha+q a_1)-q a_2=0. +``` + +The cross numerator is nonzero because the rational functions are distinct, +and its degree is therefore at most `2t-3`. The root bound proves the claim. +In particular, at `t=5`, agreement on eight finite nonpole points determines +the rational function. If both representations are reduced and their +denominators are monic of degree five, it determines the pair `(A,B)`. + +## Nonuniform cover theorem + +There is an explicit `T(509,35,8)` system `C` with + +```text +|C| = 762,054,269,114. +``` + +Partition `[509]` into consecutive blocks `B_0,B_1,B_2` of sizes + +```text +177, 166, 166. +``` + +In each block, color its local indices cyclically modulo six. The resulting +color-class sizes are + +```text +B_0: (30,30,30,29,29,29), +B_1: (28,28,28,28,27,27), +B_2: (28,28,28,28,27,27). +``` + +The certificate freezes `89`, `108`, and `108` weight-eight color patterns +for the three blocks. The family `C` consists of all eight-subsets that lie +in one block and have a frozen pattern for that block. + +### Coverage proof + +Set the local witness thresholds to `(13,12,12)`. If a 35-subset met all +three blocks below their thresholds, it would have size at most + +```text +(13-1)+(12-1)+(12-1)=34, +``` + +a contradiction. It therefore contains at least `h_j` points in some block +`B_j`, where `h=(13,12,12)`. + +Choose `h_j` of those points and record their color composition `u`. The +certificate checks every weak six-composition of `h_j`: each such `u` +coordinatewise dominates at least one frozen weight-eight pattern `p` for +the same block. Selecting `p_l` points of color `l` gives a member of `C` +inside the original 35-subset. + +The primary verifier exhausts all 666 weak three-compositions of 35 and all +weak six-compositions of the relevant local threshold. The independent +auditor parses only the frozen pattern file and reconstructs the same checks +with a separate composition generator. + +### Exact cardinality + +For a pattern `p=(p_0,...,p_5)` in a block with color-class sizes +`c=(c_0,...,c_5)`, the number of represented eight-subsets is + +```text +product_l binom(c_l,p_l). +``` + +Distinct patterns and distinct blocks represent disjoint subsets. Exact +integer summation gives + +```text +|C intersect binom(B_0,8)| = 254,104,519,142, +|C intersect binom(B_1,8)| = 253,974,874,986, +|C intersect binom(B_2,8)| = 253,974,874,986, +|C| = 762,054,269,114. +``` + +This is approximately 16.4229468510 percent smaller than the explicit +uniform six-color cover of size `911,798,442,756`. It is smaller by factors +`3.5763488281` and `7.1526944775` than the parity and complete four-block +baselines of sizes `2,725,371,892,323` and `5,450,741,362,275`. + +## RS-MCA consequence and scope + +Suppose the active `t=5` rational sections satisfy the two fixed-asymptotic +coefficient identities above. Every section with at least 35 agreement rows +then has an agreement support containing a selected eight-face. On a +nonsingular selected face, the packing lemma permits at most one reduced +section. Thus `C` gives a false-negative-free candidate-generation reduction, +provided singular faces and denominator poles are retained for separate +analysis. + +The theorem proved here is the exact cover, its cardinality, and the packing +reduction. The recorded CP-SAT result is `FEASIBLE`, not `OPTIMAL`; no +minimality claim is made. This note does not report an exhaustive scan of all +selected faces, a global `d=474` exclusion, a Paper-D row, or a leaderboard +improvement. diff --git a/experimental/scripts/audit_atlas_nonuniform_turan_cover.py b/experimental/scripts/audit_atlas_nonuniform_turan_cover.py new file mode 100644 index 000000000..781e912a4 --- /dev/null +++ b/experimental/scripts/audit_atlas_nonuniform_turan_cover.py @@ -0,0 +1,157 @@ +#!/usr/bin/env python3 +"""Independent parser and exhaustive audit for the frozen Atlas cover.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +from math import comb, prod +from pathlib import Path + + +EXPECTED_CARDINALITY = 762_054_269_114 + + +def weak_compositions(total: int, length: int): + separators = length - 1 + slots = total + separators + if separators == 0: + yield (total,) + return + from itertools import combinations + + for cuts in combinations(range(slots), separators): + boundaries = (-1,) + cuts + (slots,) + yield tuple(boundaries[index + 1] - boundaries[index] - 1 for index in range(length)) + + +def parse_cover(path: Path): + raw = path.read_bytes() + tokens = raw.decode("ascii").split() + cursor = 0 + + def take() -> str: + nonlocal cursor + if cursor == len(tokens): + raise AssertionError("truncated cover") + value = tokens[cursor] + cursor += 1 + return value + + if take() != "ATLAS_NONUNIFORM_HIERARCHICAL_COVER_V1": + raise AssertionError("cover magic") + rows, witness_size, face_size = (int(take()) for _ in range(3)) + block_count = int(take()) + blocks = [] + for block_index in range(block_count): + size, threshold, colors, pattern_count = (int(take()) for _ in range(4)) + patterns = tuple( + tuple(int(take()) for _ in range(colors)) for _ in range(pattern_count) + ) + blocks.append((block_index, size, threshold, colors, patterns)) + if cursor != len(tokens): + raise AssertionError("trailing cover tokens") + return raw, rows, witness_size, face_size, tuple(blocks) + + +def audit(cover_path: Path, output_path: Path) -> dict: + raw, rows, witness_size, face_size, blocks = parse_cover(cover_path) + if (rows, witness_size, face_size) != (509, 35, 8): + raise AssertionError("fixture parameters") + if not blocks or sum(block[1] for block in blocks) != rows: + raise AssertionError("block partition") + + global_cases = 0 + for occupancy in weak_compositions(witness_size, len(blocks)): + global_cases += 1 + if not any(value >= block[2] for value, block in zip(occupancy, blocks)): + raise AssertionError(f"global miss {occupancy}") + + block_reports = [] + selected_total = 0 + for block_index, size, threshold, colors, patterns in blocks: + if not 2 <= colors <= 8 or threshold < face_size: + raise AssertionError("block dimensions") + if not patterns or len(patterns) != len(set(patterns)): + raise AssertionError("empty or duplicate pattern family") + if any( + len(pattern) != colors or any(value < 0 for value in pattern) + or sum(pattern) != face_size + for pattern in patterns + ): + raise AssertionError("invalid pattern") + + local_cases = 0 + min_cover = None + max_cover = 0 + for occupancy in weak_compositions(threshold, colors): + local_cases += 1 + covering = sum( + all(pattern[color] <= occupancy[color] for color in range(colors)) + for pattern in patterns + ) + if covering == 0: + raise AssertionError(f"local miss in block {block_index}: {occupancy}") + min_cover = covering if min_cover is None else min(min_cover, covering) + max_cover = max(max_cover, covering) + + color_sizes = tuple(size // colors + (color < size % colors) for color in range(colors)) + selected = sum( + prod(comb(color_sizes[color], pattern[color]) for color in range(colors)) + for pattern in patterns + ) + selected_total += selected + block_reports.append( + { + "block_index": block_index, + "block_size": size, + "local_witness_size": threshold, + "colors": colors, + "color_sizes": list(color_sizes), + "pattern_count": len(patterns), + "local_distribution_count": local_cases, + "minimum_cover_multiplicity": min_cover, + "maximum_cover_multiplicity": max_cover, + "selected_eight_subsets": selected, + } + ) + + if selected_total != EXPECTED_CARDINALITY: + raise AssertionError("unexpected certified cardinality") + + report = { + "schema": "atlas-nonuniform-hierarchical-cover-independent-audit/v1", + "status": "PASS_INDEPENDENT_NONUNIFORM_HIERARCHICAL_35_TO_8_COVER", + "row_count": rows, + "global_witness_size": witness_size, + "face_size": face_size, + "global_block_distribution_count": global_cases, + "block_reports": block_reports, + "selected_eight_subsets": selected_total, + "cover_sha256": hashlib.sha256(raw).hexdigest(), + "proof_scope": "Exact coverage and cardinality only; no optimality claim.", + } + canonical = (json.dumps(report, sort_keys=True, separators=(",", ":")) + "\n").encode( + "ascii" + ) + report["payload_sha256"] = hashlib.sha256(canonical).hexdigest() + output_path.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="ascii") + return report + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("cover", type=Path) + parser.add_argument("output", type=Path) + args = parser.parse_args() + report = audit(args.cover, args.output) + print( + "PASS independent nonuniform cover selected={}".format( + report["selected_eight_subsets"] + ) + ) + + +if __name__ == "__main__": + main() diff --git a/experimental/scripts/optimize_atlas_nonuniform_turan_cover.py b/experimental/scripts/optimize_atlas_nonuniform_turan_cover.py new file mode 100644 index 000000000..7fc5855f1 --- /dev/null +++ b/experimental/scripts/optimize_atlas_nonuniform_turan_cover.py @@ -0,0 +1,267 @@ +#!/usr/bin/env python3 +"""Optimize an exact nonuniform hierarchical T(509,35,8) cover.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import math +from pathlib import Path + +from ortools.sat.python import cp_model + + +ROW_COUNT = 509 +WITNESS_SIZE = 35 +FACE_SIZE = 8 + + +def compositions(total: int, parts: int): + if parts == 1: + yield (total,) + return + for first in range(total + 1): + for tail in compositions(total - first, parts - 1): + yield (first,) + tail + + +def balanced_sizes(total: int, parts: int) -> tuple[int, ...]: + return tuple((total + parts - 1 - index) // parts for index in range(parts)) + + +def parse_csv(value: str) -> tuple[int, ...]: + result = tuple(int(item) for item in value.split(",") if item) + if not result: + raise ValueError("empty integer list") + return result + + +def pattern_weight(pattern: tuple[int, ...], color_sizes: tuple[int, ...]) -> int: + return math.prod( + math.comb(size, multiplicity) + for size, multiplicity in zip(color_sizes, pattern) + ) + + +def lift_patterns( + patterns: tuple[tuple[int, ...], ...], target_colors: int +) -> tuple[tuple[int, ...], ...]: + """Refine the final color until every pattern has target_colors entries.""" + lifted = set(patterns) + if not lifted: + return () + source_colors = len(next(iter(lifted))) + if any(len(pattern) != source_colors for pattern in lifted): + raise ValueError("hint patterns have inconsistent color counts") + while source_colors > target_colors: + lifted = { + pattern[:-2] + (pattern[-2] + pattern[-1],) + for pattern in lifted + } + source_colors -= 1 + while source_colors < target_colors: + lifted = { + pattern[:-1] + (left, pattern[-1] - left) + for pattern in lifted + for left in range(pattern[-1] + 1) + } + source_colors += 1 + return tuple(sorted(lifted)) + + +def load_hint( + path: Path | None, + block_sizes: tuple[int, ...], + thresholds: tuple[int, ...], + colors: tuple[int, ...], +) -> tuple[tuple[tuple[int, ...], ...], ...]: + if path is None: + return tuple(() for _ in block_sizes) + payload = json.loads(path.read_text(encoding="ascii")) + if "block_records" in payload: + records = payload["block_records"] + if len(records) != len(block_sizes): + raise ValueError("hint block count mismatch") + result = [] + for record, size, threshold, color_count in zip( + records, block_sizes, thresholds, colors + ): + del size, threshold + result.append( + lift_patterns( + tuple( + tuple(map(int, pattern)) + for pattern in record["selected_patterns"] + ), + color_count, + ) + ) + return tuple(result) + + patterns = tuple(tuple(map(int, pattern)) for pattern in payload["selected_patterns"]) + return tuple(lift_patterns(patterns, color_count) for color_count in colors) + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("output", type=Path) + parser.add_argument("--block-sizes", default="170,170,169") + parser.add_argument("--local-witnesses", default="12,12,12") + parser.add_argument("--colors", default="6,6,6") + parser.add_argument("--hint", type=Path) + parser.add_argument("--time-limit", type=float, default=600.0) + parser.add_argument("--workers", type=int, default=8) + parser.add_argument("--random-seed", type=int, default=1) + args = parser.parse_args() + + block_sizes = parse_csv(args.block_sizes) + thresholds = parse_csv(args.local_witnesses) + colors = parse_csv(args.colors) + if not (len(block_sizes) == len(thresholds) == len(colors)): + raise ValueError("block, threshold and color lists must have equal lengths") + if sum(block_sizes) != ROW_COUNT: + raise ValueError(f"block sizes must sum to {ROW_COUNT}") + if sum(threshold - 1 for threshold in thresholds) >= WITNESS_SIZE: + raise ValueError("pigeonhole condition sum(h_j-1) < 35 is required") + if any(threshold < FACE_SIZE for threshold in thresholds): + raise ValueError("every local witness threshold must be at least eight") + if any(not 2 <= color_count <= 8 for color_count in colors): + raise ValueError("color counts must lie in 2..8") + + hints = load_hint(args.hint, block_sizes, thresholds, colors) + model = cp_model.CpModel() + block_data = [] + objective_terms = [] + + for block_index, (size, threshold, color_count, hint) in enumerate( + zip(block_sizes, thresholds, colors, hints) + ): + color_sizes = balanced_sizes(size, color_count) + faces = tuple(compositions(FACE_SIZE, color_count)) + witnesses = tuple(compositions(threshold, color_count)) + weights = tuple(pattern_weight(face, color_sizes) for face in faces) + face_index = {face: index for index, face in enumerate(faces)} + if any(face not in face_index for face in hint): + raise ValueError(f"hint for block {block_index} has an inadmissible pattern") + + selected = [ + model.new_bool_var(f"x_{block_index}_{face_index}") + for face_index in range(len(faces)) + ] + cover_lists = [] + for witness in witnesses: + covered_by = [ + index + for index, face in enumerate(faces) + if all(left <= right for left, right in zip(face, witness)) + ] + if not covered_by: + raise RuntimeError( + f"uncoverable block {block_index} witness pattern: {witness}" + ) + model.add(sum(selected[index] for index in covered_by) >= 1) + cover_lists.append(covered_by) + + hinted = set(hint) + for face, variable in zip(faces, selected): + model.add_hint(variable, int(face in hinted)) + objective_terms.extend( + weight * variable for weight, variable in zip(weights, selected) + ) + block_data.append( + (color_sizes, faces, witnesses, weights, selected, cover_lists, hint) + ) + + model.minimize(sum(objective_terms)) + solver = cp_model.CpSolver() + solver.parameters.max_time_in_seconds = args.time_limit + solver.parameters.num_search_workers = args.workers + solver.parameters.random_seed = args.random_seed + solver.parameters.log_search_progress = False + status = solver.solve(model) + if status not in (cp_model.OPTIMAL, cp_model.FEASIBLE): + raise RuntimeError(f"CP-SAT returned {solver.status_name(status)}") + + block_records = [] + exact_total = 0 + for block_index, ( + size, + threshold, + color_count, + data, + ) in enumerate(zip(block_sizes, thresholds, colors, block_data)): + color_sizes, faces, witnesses, weights, selected, cover_lists, hint = data + chosen_indices = tuple( + index for index, variable in enumerate(selected) if solver.boolean_value(variable) + ) + chosen = tuple(faces[index] for index in chosen_indices) + chosen_set = set(chosen_indices) + multiplicities = tuple( + sum(index in chosen_set for index in cover_list) + for cover_list in cover_lists + ) + if min(multiplicities) < 1: + raise RuntimeError(f"block {block_index} does not cover every witness") + exact_size = sum(weights[index] for index in chosen_indices) + exact_total += exact_size + block_records.append( + { + "block_index": block_index, + "block_size": size, + "local_witness_size": threshold, + "colors": color_count, + "color_sizes": list(color_sizes), + "face_pattern_count": len(faces), + "witness_pattern_count": len(witnesses), + "selected_pattern_count": len(chosen), + "selected_patterns": [list(face) for face in chosen], + "exact_selected_eight_subsets": exact_size, + "minimum_witness_cover_multiplicity": min(multiplicities), + "maximum_witness_cover_multiplicity": max(multiplicities), + "hint_pattern_count": len(hint), + "hint_exact_selected_eight_subsets": sum( + pattern_weight(face, color_sizes) for face in hint + ), + } + ) + + rounded_objective = round(solver.objective_value) + if exact_total != rounded_objective: + raise RuntimeError("exact objective and CP-SAT objective disagree") + report = { + "schema": "atlas-nonuniform-hierarchical-cover-cp-sat/v1", + "status": solver.status_name(status), + "row_count": ROW_COUNT, + "global_witness_size": WITNESS_SIZE, + "face_size": FACE_SIZE, + "block_sizes": list(block_sizes), + "local_witness_sizes": list(thresholds), + "pigeonhole_budget": sum(threshold - 1 for threshold in thresholds), + "block_records": block_records, + "exact_selected_eight_subsets": exact_total, + "best_objective_bound": int(math.ceil(solver.best_objective_bound)), + "relative_bound_gap": (exact_total - solver.best_objective_bound) / exact_total, + "wall_time_seconds": solver.wall_time, + "branches": solver.num_branches, + "conflicts": solver.num_conflicts, + "random_seed": args.random_seed, + } + canonical = json.dumps(report, sort_keys=True, separators=(",", ":")).encode("ascii") + report["payload_sha256"] = hashlib.sha256(canonical).hexdigest() + args.output.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="ascii") + print( + "{} Atlas nonuniform blocks={} selected={} bound={} gap={:.9f} seconds={:.3f}".format( + report["status"], + len(block_sizes), + exact_total, + report["best_objective_bound"], + report["relative_bound_gap"], + report["wall_time_seconds"], + ), + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/experimental/scripts/verify_atlas_nonuniform_turan_cover.py b/experimental/scripts/verify_atlas_nonuniform_turan_cover.py new file mode 100644 index 000000000..d9a3ac4ab --- /dev/null +++ b/experimental/scripts/verify_atlas_nonuniform_turan_cover.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Freeze and exactly audit a nonuniform hierarchical T(509,35,8) cover.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import math +from pathlib import Path + + +EXPECTED_CARDINALITY = 762_054_269_114 + + +def compositions(total: int, parts: int): + if parts == 1: + yield (total,) + return + for first in range(total + 1): + for tail in compositions(total - first, parts - 1): + yield (first,) + tail + + +def balanced_sizes(total: int, parts: int) -> tuple[int, ...]: + return tuple((total + parts - 1 - index) // parts for index in range(parts)) + + +def selected_count( + pattern: tuple[int, ...], color_sizes: tuple[int, ...] +) -> int: + return math.prod( + math.comb(size, multiplicity) + for size, multiplicity in zip(color_sizes, pattern) + ) + + +def freeze(payload: dict) -> bytes: + lines = [ + "ATLAS_NONUNIFORM_HIERARCHICAL_COVER_V1", + "{} {} {}".format( + payload["row_count"], + payload["global_witness_size"], + payload["face_size"], + ), + str(len(payload["block_records"])), + ] + for record in payload["block_records"]: + patterns = record["selected_patterns"] + lines.append( + "{} {} {} {}".format( + record["block_size"], + record["local_witness_size"], + record["colors"], + len(patterns), + ) + ) + lines.extend(" ".join(map(str, pattern)) for pattern in patterns) + return ("\n".join(lines) + "\n").encode("ascii") + + +def audit(optimizer_path: Path, cover_path: Path, output_path: Path) -> dict: + optimizer_bytes = optimizer_path.read_bytes() + payload = json.loads(optimizer_bytes) + if payload.get("schema") != "atlas-nonuniform-hierarchical-cover-cp-sat/v1": + raise AssertionError("optimizer schema") + payload_body = dict(payload) + reported_payload_sha256 = payload_body.pop("payload_sha256", None) + canonical_payload = json.dumps( + payload_body, sort_keys=True, separators=(",", ":") + ).encode("ascii") + if hashlib.sha256(canonical_payload).hexdigest() != reported_payload_sha256: + raise AssertionError("optimizer payload hash") + rows = int(payload["row_count"]) + witness_size = int(payload["global_witness_size"]) + face_size = int(payload["face_size"]) + if (rows, witness_size, face_size) != (509, 35, 8): + raise AssertionError("global parameters") + + records = payload["block_records"] + blocks = tuple(int(record["block_size"]) for record in records) + thresholds = tuple(int(record["local_witness_size"]) for record in records) + if tuple(map(int, payload["block_sizes"])) != blocks or sum(blocks) != rows: + raise AssertionError("block partition") + if tuple(map(int, payload["local_witness_sizes"])) != thresholds: + raise AssertionError("local thresholds") + pigeonhole_budget = sum(threshold - 1 for threshold in thresholds) + if pigeonhole_budget >= witness_size: + raise AssertionError("pigeonhole budget") + if int(payload["pigeonhole_budget"]) != pigeonhole_budget: + raise AssertionError("reported pigeonhole budget") + + global_distributions = tuple(compositions(witness_size, len(blocks))) + uncovered_global = tuple( + distribution + for distribution in global_distributions + if all(value < threshold for value, threshold in zip(distribution, thresholds)) + ) + if uncovered_global: + raise AssertionError("uncovered global block distribution") + + block_audits = [] + exact_total = 0 + for block_index, record in enumerate(records): + if int(record["block_index"]) != block_index: + raise AssertionError("block index") + size = blocks[block_index] + threshold = thresholds[block_index] + colors = int(record["colors"]) + if threshold < face_size or not 2 <= colors <= 8: + raise AssertionError("local dimensions") + color_sizes = balanced_sizes(size, colors) + if tuple(map(int, record["color_sizes"])) != color_sizes: + raise AssertionError("color sizes") + patterns = tuple(tuple(map(int, pattern)) for pattern in record["selected_patterns"]) + if len(patterns) != len(set(patterns)): + raise AssertionError("duplicate local pattern") + if any( + len(pattern) != colors or min(pattern) < 0 or sum(pattern) != face_size + for pattern in patterns + ): + raise AssertionError("malformed local pattern") + + local_distributions = tuple(compositions(threshold, colors)) + multiplicities = tuple( + sum( + all(left <= right for left, right in zip(pattern, distribution)) + for pattern in patterns + ) + for distribution in local_distributions + ) + if not multiplicities or min(multiplicities) < 1: + raise AssertionError("uncovered local distribution") + exact_block = sum(selected_count(pattern, color_sizes) for pattern in patterns) + if int(record["exact_selected_eight_subsets"]) != exact_block: + raise AssertionError("block cardinality") + if int(record["selected_pattern_count"]) != len(patterns): + raise AssertionError("block pattern count") + exact_total += exact_block + block_audits.append( + { + "block_index": block_index, + "block_size": size, + "local_witness_size": threshold, + "colors": colors, + "color_sizes": list(color_sizes), + "pattern_count": len(patterns), + "local_distribution_count": len(local_distributions), + "minimum_cover_multiplicity": min(multiplicities), + "maximum_cover_multiplicity": max(multiplicities), + "selected_eight_subsets": exact_block, + } + ) + if int(payload["exact_selected_eight_subsets"]) != exact_total: + raise AssertionError("global cardinality") + if exact_total != EXPECTED_CARDINALITY: + raise AssertionError("unexpected certified cardinality") + + cover_bytes = freeze(payload) + cover_path.write_bytes(cover_bytes) + report = { + "schema": "atlas-nonuniform-hierarchical-cover-freeze-audit/v1", + "status": "PASS_EXACT_NONUNIFORM_HIERARCHICAL_35_TO_8_COVER", + "row_count": rows, + "global_witness_size": witness_size, + "face_size": face_size, + "block_sizes": list(blocks), + "local_witness_sizes": list(thresholds), + "pigeonhole_budget": pigeonhole_budget, + "global_block_distribution_count": len(global_distributions), + "block_audits": block_audits, + "selected_eight_subsets": exact_total, + "previous_uniform_six_color_selected_eight_subsets": 911_798_442_756, + "reduction_factor_against_uniform_six_color": 911_798_442_756 / exact_total, + "previous_parity_selected_eight_subsets": 2_725_371_892_323, + "reduction_factor_against_parity": 2_725_371_892_323 / exact_total, + "optimizer_status": payload["status"], + "optimizer_claims_optimality": payload["status"] == "OPTIMAL", + "optimizer_payload_sha256": reported_payload_sha256, + "cover_sha256": hashlib.sha256(cover_bytes).hexdigest(), + "proof_summary": [ + "Every 35-composition across the macroblocks reaches at least one recorded local threshold.", + "Every color composition at that local threshold dominates a frozen weight-eight pattern for the same block.", + "Therefore every 35-subset of the 509 rows contains a frozen selected eight-face.", + ], + } + canonical = (json.dumps(report, sort_keys=True, separators=(",", ":")) + "\n").encode( + "ascii" + ) + report["payload_sha256"] = hashlib.sha256(canonical).hexdigest() + output_path.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="ascii") + return report + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("optimizer", type=Path) + parser.add_argument("cover", type=Path) + parser.add_argument("output", type=Path) + args = parser.parse_args() + report = audit(args.optimizer, args.cover, args.output) + print( + "PASS Atlas nonuniform cover blocks={} selected={}".format( + report["block_sizes"], report["selected_eight_subsets"] + ) + ) + + +if __name__ == "__main__": + main()