diff --git a/research/six-source-duo-add16-floor/FULL-COVERS.bin b/research/six-source-duo-add16-floor/FULL-COVERS.bin new file mode 100644 index 0000000000..a5031cba1c Binary files /dev/null and b/research/six-source-duo-add16-floor/FULL-COVERS.bin differ diff --git a/research/six-source-duo-add16-floor/README.md b/research/six-source-duo-add16-floor/README.md new file mode 100644 index 0000000000..a0ad8d5dd5 --- /dev/null +++ b/research/six-source-duo-add16-floor/README.md @@ -0,0 +1,244 @@ +# The six-source DUO batch optimum is 140 queries and 142 adds + +In the inherited six-source dirty-connector model, Aaron Wang/Navinor's +[PR2128](https://github.com/CrocSwap/integer-mult-bounds/pull/2128) construction +simultaneously minimizes the all-63-output batch's **queries (140)** and +**source/readout adds (142)**. Thus `(140,142)` is its only Pareto point for +these two charges. A paired-universal source word needs at least **14 calls +at every source-add budget**; the predecessor attains `(14,16)`. + +The unrestricted group-theoretic value is already reported by Volodymyr +Gavrylkiv, *Bases in Dihedral and Boolean Groups*, JIS 20 (2017), +[Table 3](https://cs.uwaterloo.ca/journals/JIS/VOL20/Gavrylkiv/gav4.pdf): +`r[(C2)^6]=14`. We credit that result. This contribution independently +rebuilds its finite lower bound, applies it to the connector's complete bill, +and supplies a separate exact 16-add word census. It does not introduce a +physical supplier or improve the selected kappa. + +## Model and inherited reduction + +Keep [Navinor's DUO model](../duo-toggle-connector/README.md), extending +Ross Richardson's [dirty connector](../universal-connector-boundary/README.md): +six read-only sources, arbitrary dirty targets, one arbitrary dirty connector +z, and complete F2-linear calls with fixed generic maps: + +``` +B_j: z += B_j x_j +DUO_{j,l}: z += B_j x_j + B_l x_l (j != l) +A_i: y_i += A_i z. +``` + +No extra connectors, source mutations, combined readouts or reads inside a +DUO are allowed. Restore z and all scratch. A source word has k calls and W +source-map applications: a singleton contributes one to W, a DUO two. The +inherited price is one overhead o per call and one marginal p per add. + +Write q_t for the source-parity prefix. Restoration forces q_k=q_0=0, +with every used source occurring a positive even number of times. Two +readouts give q_s XOR q_t. Paired universality is exactly +`D={q_s XOR q_t}=F2^6`. Necessity follows from independent scalar dirty +inputs; sufficiency holds for arbitrary A_i and B_j without commutativity. +This reduction and the attaining word are inherited, not new here. + +## Unrestricted 13-point exclusion + +For a restored k-call source word, the distinct prefixes form a set S of +size at most k: the last prefix repeats the first. Suppose a set of at most +13 points covers every difference. Enlarge it to exactly 13 distinct points, +translate one point to zero, and choose six independent translated points. +Such a basis exists because full difference coverage forces affine span 6. +An invertible linear map sends those six points to the coordinate basis. + +The normalized set therefore contains `0,1,2,4,8,16,32`; its other six +points are any six of the remaining 57. Every possible cover has a +representative in these **C(57,6)=36,288,252** combinations. Multiple +representatives of one affine orbit are allowed. This is an existence +reduction, not an orbit count. The transformation is used only in the +impossibility proof; it does not change or subsidize the physical alphabet. + +Two code-disjoint C++ implementations exhaust this complete domain: + +- `basis13_recursive.cpp` chooses points recursively and incrementally adds + literal pair differences. +- `basis13_bitset.cpp` enumerates six-bit selections in colexicographic order + using Gosper's rule, rebuilds each point set, and computes its differences + by XOR translations of a 64-bit incidence vector. All 4,096 singleton + translation identities are checked first. + +They agree on the entire coverage histogram, with maximum **63/64** and +4,200 attaining normalized sets. Neither has a full cover. Both check the +14-point positive fixture through their actual coverage computation and a +sharp 13-point near cover. Deadlines produce a rejected `TIMEOUT` receipt. +The native histogram is independently reconstructed, not accepted by hash. + +`basis.py` checks the receipts, literal attaining witnesses, invertible +normalization and 256 affine-image controls, and rejects a proper-subspace +fixture. These finite controls support the written normalization argument; +they are not a formal proof of all possible changes of basis. Since every +hypothetical cover is represented in the exhaustive domain, **k>=14** for +paired universality, independently of W. This lower bound even allows +arbitrary source-step masks, while retaining a single connector and the +same paired-readout rule. The known DUO word shows sharpness. + +## Complete batch lower bounds + +The batch contains one separate dirty output for every nonzero six-source +mask. Each output needs at least two readouts to cancel the unknown initial +connector. If its mask is absent from D, it needs at least four. Write M for +the number of missing nonzero masks. Then readouts `R>=126+2M` and total +queries `Q=k+R`. + +- If `k>=14`, then `Q>=140`. +- If `k=12` or `13`, the unrestricted exclusion gives `M>=1`, hence + `Q>=140` or `141` respectively. +- If `k<=11`, at most `C(k,2)` nonzero differences are present. Thus + `Q>=k+126+2(63-C(k,2))>=153` for `1<=k<=11`. + +Therefore **Q>=140 even when more than two readouts are permitted**. The +bound at k=12 is only an optimistic lower bound; no such attaining word is +claimed. The predecessor attains Q=140 at k=14 and R=126. + +Source restoration and dependence on all six inputs require positive even +W>=12. Expanding DUOs exposes more prefixes and preserves W. The retained +singleton census therefore gives the following add floors: + +| Source adds W | Required output readouts | Total adds W+R | +|---|---:|---:| +| 12 | at least 156 (15 missing masks) | at least 168 | +| 14 | at least 136 (5 missing masks) | at least 150 | +| 16 | at least 126 | at least 142 | +| even W>=18 | at least 126 | at least 144 | + +The old singleton maxima are 49/64 at W=12 and 59/64 at W=14, and are +fully replayed. Thus **W+R>=142**. Both minima are attained simultaneously +by PR2128's source word + +``` +2,16,8,16,1,4,48,4,3,4,32,8,4,16. +``` + +It has 14 calls, 16 adds, restoration and full coverage. Its complete bill +is `140o+142p`, optimal for every nonnegative o,p in this inherited tariff. +For strictly positive prices, a different query/add pair is more expensive. +This is a statement about a declared abstract interface, not practical +runtime, free physical composition, or a multiplication supplier invoice. + +## Independent restricted 16-add census + +The investigation first resolved the named `(k,W)=(13,16)` handoff. That +evidence is retained as an independent restricted cross-check, even though +the unrestricted basis result already excludes all k<=13 paired universals. + +A `(13,16)` word contains ten singletons and three DUOs. Expanding each +DUO gives a restored 16-step singleton word. Positive even source +multiplicities have exactly the profiles `(6,2,2,2,2,2)` or +`(4,4,2,2,2,2)`. The original prefixes hide precisely the three internal +midpoints: pairwise nonadjacent cyclic vertices, each merging distinct +labels. Conversely every such deletion makes a legal `(13,16)` word. +Repeated prefixes are allowed. Expanded internal boundaries are only proof +bookkeeping; the actual DUO offers no readout there. + +An expanded word must cover all differences if its visible subset does. +First-occurrence source relabeling leaves exactly + +``` +16! / (6! * (2!)^5 * 5!) = 7,567,560 +16! / ((4!)^2 * (2!)^4 * 2! * 4!) = 47,297,250 +total = 54,864,810. +``` + +`enumerate_rgs.cpp` uses restricted-growth words, parity feasibility and +incremental pair differences. `enumerate_partitions.cpp` independently +partitions positions into even blocks and uses bitset translations. They +agree byte-for-byte on **7,480 full-cover words**, all with the second +profile. [FULL-COVERS.bin](FULL-COVERS.bin) stores sorted little-endian +uint64 codes, sixteen 3-bit labels each, earliest in the least significant +bits: 59,840 bytes, SHA256 + +``` +251100fa9f200ddb24cefac8a6b8255cfa43d1f3bd7e4bc3f45120d4f3aa7262 +``` + +The literal Python audit partitions the table into 251 complete +rotation/reversal/relabeling orbits: sizes 8:1, 16:33, 32:217. These +symmetries preserve legal hidden midpoints and retained coverage. It checks +all 352 cyclic nonadjacent triples per representative, retaining the 86,900 +cases that merge distinct labels. It does not use the primary native +individual-removability prune. The maximum is 63/64. Non-full expanded +words cannot gain coverage by deletion. No timeout is used as an exclusion. + +The sharp near miss + +``` +2,1,4,1,2,9,20,8,32,8,16,8,33 +``` + +misses only mask 12. Four readouts at boundaries 0,1,2,6 repair it, at a +dominated batch bill of 141 queries and 144 adds. Splitting DUOs also +excludes `(12,16)`; the inherited 14-step bound excludes `(12,14)` and +`(13,14)`. The unrestricted result additionally closes `(12,18)`, +`(13,18)` and every higher-add paired-universal k<=13 cell. + +## Reproduce and limits + +Full replay needs Python 3.12 and a C++17 compiler (g++ or clang++). +Tested: Ubuntu 24.04, CPython 3.12.3, g++ 13.3.0. Set CXX to its executable +if c++ is unavailable. No compiler or dependency is downloaded. Default +replay builds in temporary storage and leaves the source package unchanged: + +```sh +python3 -I -O -B research/six-source-duo-add16-floor/verify.py +python3.12 scripts/research_package.py --package research/six-source-duo-add16-floor +``` + +Expected: `PASS_SIX_SOURCE_DUO_GLOBAL_OPTIMUM`. The complete receipt binds +four censuses, both histograms, the restricted word table, literal audits, +positive fixtures, mutations and exact batch floors. The first complete +four-census replay including compilation took 13.31 seconds and 120,300 KiB +peak RSS on one CPU. `--out NEW_PATH` creates a receipt exclusively. + +The optimized portable audit runs on Windows without a compiler: + +```sh +python3 -I -O -B research/six-source-duo-add16-floor/audit.py +``` + +It checks the saved **restricted** table, all orbits/deletions, the near +miss and full dirty-input positive replay. It does not re-establish either +native census's completeness or the unrestricted basis result. The full +native replay was not run on Windows. Positive replay covers all 70, 140 +and 210 independent columns at dimensions 1,2,3, with noncommuting maps at +dimensions 2 and 3. Dropped/moved readouts, a shrunk DUO and a dropped +source call reject. Both native basis enumerations also pass full-domain +UBSan runs. Missing source/compiler, drifted inputs, changed table/results, +deadline truncation and output overwrite are rejected. + +All implementations have the same author/assistant. Algorithmic agreement +is not independent human or formal-kernel review. No frame/owner admission, +physical compiler, chronological hosting, precision/tape proof, global +supplier moment, all-size theorem or outer exponent is supplied. + +## Open next questions + +The six-source abstract DUO query/add frontier is closed under the stated +rules. The relevant remaining question is physical admission: can one +pinned supplier implement a complete DUO call after all owner/frame, access, +restoration and precision costs? Start with one small arbitrary-input, +noncommuting fixture and a fully charged invoice. This package supplies no +such instance. Structured scope, source pins and handoff are in [TASK.json](TASK.json). + +## Credit + +Volodymyr Gavrylkiv / JIS 2017 Table 3: the known unrestricted 14-point +Boolean-group basis value. Ross Richardson / PR943 and PR934: interface +and prefix reduction. Navinor / PR1531: DUO model, five-source result and +prices. Aaron Wang/Navinor / PR2128 at +`697369a971eed02c0fbcd75ebefec9f59945f08e`: the attaining six-source word +and open-cell handoff. Douglas Colkitt / PR1185 and Hanson Sun / PR1215: +singleton result. PR2134/PR2146 retain credit for their distinct TRIO +censuses; their witnesses are not reproduced or attributed to this package. + +Prepared for Tairitsu-Aya with substantial OpenAI Codex assistance in +mathematics, code, source reading, verification and prose. Apache-2.0. +Frozen predecessors and the selected result are unchanged. This continues +a released handoff, not a new operation family or a fresh random draw. diff --git a/research/six-source-duo-add16-floor/RESULT.json b/research/six-source-duo-add16-floor/RESULT.json new file mode 100644 index 0000000000..82870eedca --- /dev/null +++ b/research/six-source-duo-add16-floor/RESULT.json @@ -0,0 +1,466 @@ +{ + "schema_version": 1, + "status": "PASS_SIX_SOURCE_DUO_GLOBAL_OPTIMUM", + "domain": "six read-only sources; singleton/DUO complete calls; one restored dirty connector; paired readouts", + "censuses": [ + { + "n": 5, + "unit_steps": 10, + "unit_words": 945, + "full_coverage_unit_words": 0, + "max_unit_coverage": 31, + "profile_max_four": 0, + "profile_max_six": 0, + "full_cover_table_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "n": 6, + "unit_steps": 12, + "unit_words": 10395, + "full_coverage_unit_words": 0, + "max_unit_coverage": 49, + "profile_max_four": 0, + "profile_max_six": 0, + "full_cover_table_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "n": 6, + "unit_steps": 14, + "unit_words": 945945, + "full_coverage_unit_words": 0, + "max_unit_coverage": 59, + "profile_max_four": 945945, + "profile_max_six": 0, + "full_cover_table_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + }, + { + "n": 6, + "unit_steps": 16, + "unit_words": 54864810, + "full_coverage_unit_words": 7480, + "max_unit_coverage": 64, + "profile_max_four": 47297250, + "profile_max_six": 7567560, + "full_cover_table_sha256": "251100fa9f200ddb24cefac8a6b8255cfa43d1f3bd7e4bc3f45120d4f3aa7262", + "primary_individually_removable_triples_checked": 10240, + "primary_retained_coverage_maximum": 63 + } + ], + "small_duo_positive_controls": { + "3": { + "calls": 5, + "adds": 6, + "coverage": 8 + }, + "4": { + "calls": 6, + "adds": 8, + "coverage": 16 + }, + "5": { + "calls": 10, + "adds": 12, + "coverage": 32 + } + }, + "deadline_control_rejected": true, + "audit": { + "full_unit_words": 7480, + "full_unit_codes_sha256": "251100fa9f200ddb24cefac8a6b8255cfa43d1f3bd7e4bc3f45120d4f3aa7262", + "full_cover_multiplicity_profiles": { + "2,2,2,2,4,4": 7480 + }, + "unit_orbits": 251, + "orbit_size_histogram": { + "8": 1, + "16": 33, + "32": 217 + }, + "cyclic_deletion_patterns": 352, + "tested_orbit_deletions": 86900, + "retained_coverage_histogram": { + "43": 151, + "44": 457, + "45": 640, + "46": 1689, + "47": 1372, + "48": 5235, + "49": 3059, + "50": 5729, + "51": 6779, + "52": 11081, + "53": 17290, + "54": 5585, + "55": 9414, + "56": 5472, + "57": 7656, + "58": 3481, + "60": 1313, + "63": 497 + }, + "max_coverage": 63, + "max_witness": { + "unit_labels": [ + 0, + 1, + 0, + 2, + 0, + 1, + 0, + 3, + 2, + 4, + 3, + 5, + 3, + 4, + 3, + 5 + ], + "hidden_prefixes": [ + 0, + 7, + 9 + ], + "steps": [ + 2, + 1, + 4, + 1, + 2, + 9, + 20, + 8, + 32, + 8, + 16, + 8, + 33 + ], + "calls": 13, + "adds": 16, + "prefixes": [ + 0, + 2, + 3, + 7, + 6, + 4, + 13, + 25, + 17, + 49, + 57, + 41, + 33 + ], + "coverage": 63, + "missing_masks": [ + 12 + ] + }, + "incumbent_steps": [ + 2, + 16, + 8, + 16, + 1, + 4, + 48, + 4, + 3, + 4, + 32, + 8, + 4, + 16 + ], + "incumbent": { + "calls": 14, + "adds": 16, + "prefixes": [ + 0, + 2, + 18, + 26, + 10, + 11, + 15, + 63, + 59, + 56, + 60, + 28, + 20, + 16 + ], + "coverage": 64, + "missing_masks": [] + }, + "positive_full_column_dimensions": [ + 1, + 2, + 3 + ], + "positive_full_input_columns": [ + 70, + 140, + 210 + ], + "behavioral_mutations_rejected": [ + "drop_readout", + "move_readout", + "shrink_duo", + "drop_source" + ], + "batch_at_minimum_add_budget": { + "root_queries": 140, + "adds": 142, + "source_calls": 14, + "source_adds": 16, + "readouts": 126 + } + }, + "unrestricted_basis": { + "domain": "all 13-element subsets of F2^6 up to existence of an affine-basis normalization", + "normalization": { + "fixed_points": [ + 0, + 1, + 2, + 4, + 8, + 16, + 32 + ], + "available_points": 57, + "chosen_points": 6, + "normalized_sets": 36288252 + }, + "coverage_histogram": { + "38": 3185, + "39": 9702, + "40": 84735, + "42": 287280, + "43": 625170, + "44": 987385, + "45": 49140, + "46": 1755075, + "47": 918540, + "48": 2374785, + "49": 4425372, + "50": 3338475, + "51": 5687605, + "52": 3222765, + "53": 5365605, + "54": 2373273, + "55": 2965200, + "56": 933240, + "57": 589820, + "58": 215250, + "60": 72450, + "63": 4200 + }, + "maximum_coverage": 63, + "maximum_witnesses": [ + [ + 0, + 1, + 2, + 3, + 4, + 5, + 8, + 16, + 30, + 32, + 46, + 54, + 57 + ], + [ + 0, + 1, + 2, + 4, + 8, + 16, + 22, + 27, + 29, + 32, + 39, + 40, + 41 + ] + ], + "attaining_14_points": [ + 0, + 2, + 18, + 26, + 10, + 11, + 15, + 63, + 59, + 56, + 60, + 28, + 20, + 16 + ], + "affine_image_controls": 256, + "proper_subspace_control_rejected": true, + "query_lower_bounds": [ + { + "source_calls": 1, + "missing_masks_at_least": 63, + "readouts_at_least": 252, + "queries_at_least": 253 + }, + { + "source_calls": 2, + "missing_masks_at_least": 62, + "readouts_at_least": 250, + "queries_at_least": 252 + }, + { + "source_calls": 3, + "missing_masks_at_least": 60, + "readouts_at_least": 246, + "queries_at_least": 249 + }, + { + "source_calls": 4, + "missing_masks_at_least": 57, + "readouts_at_least": 240, + "queries_at_least": 244 + }, + { + "source_calls": 5, + "missing_masks_at_least": 53, + "readouts_at_least": 232, + "queries_at_least": 237 + }, + { + "source_calls": 6, + "missing_masks_at_least": 48, + "readouts_at_least": 222, + "queries_at_least": 228 + }, + { + "source_calls": 7, + "missing_masks_at_least": 42, + "readouts_at_least": 210, + "queries_at_least": 217 + }, + { + "source_calls": 8, + "missing_masks_at_least": 35, + "readouts_at_least": 196, + "queries_at_least": 204 + }, + { + "source_calls": 9, + "missing_masks_at_least": 27, + "readouts_at_least": 180, + "queries_at_least": 189 + }, + { + "source_calls": 10, + "missing_masks_at_least": 18, + "readouts_at_least": 162, + "queries_at_least": 172 + }, + { + "source_calls": 11, + "missing_masks_at_least": 8, + "readouts_at_least": 142, + "queries_at_least": 153 + }, + { + "source_calls": 12, + "missing_masks_at_least": 1, + "readouts_at_least": 128, + "queries_at_least": 140 + }, + { + "source_calls": 13, + "missing_masks_at_least": 1, + "readouts_at_least": 128, + "queries_at_least": 141 + }, + { + "source_calls": 14, + "missing_masks_at_least": 0, + "readouts_at_least": 126, + "queries_at_least": 140 + } + ], + "add_lower_bounds": [ + { + "source_adds": 12, + "total_adds_at_least": 168 + }, + { + "source_adds": 14, + "total_adds_at_least": 150 + }, + { + "source_adds": 16, + "total_adds_at_least": 142 + }, + { + "source_adds": "even >=18", + "total_adds_at_least": 144 + } + ], + "minimum_paired_universal_source_calls_any_add_budget": 14, + "global_batch_optimum": { + "queries": 140, + "adds": 142 + }, + "literature": { + "author": "Volodymyr Gavrylkiv", + "title": "Bases in Dihedral and Boolean Groups", + "year": 2017, + "location": "Table 3", + "reported_value": "r[(C2)^6]=14", + "url": "https://cs.uwaterloo.ca/journals/JIS/VOL20/Gavrylkiv/gav4.pdf" + } + }, + "conclusions": { + "minimum_source_adds_for_universality": 16, + "minimum_source_calls_with_at_most_16_adds": 14, + "minimum_paired_universal_source_calls_any_add_budget": 14, + "excluded_cells": [ + [ + 12, + 14 + ], + [ + 12, + 16 + ], + [ + 13, + 14 + ], + [ + 13, + 16 + ] + ], + "minimum_all_63_row_batch_adds": 142, + "minimum_batch_queries_at_142_adds": 140, + "minimum_all_63_row_batch_queries": 140, + "unique_batch_pareto_point": [ + 140, + 142 + ], + "higher_add_pareto_cells_settled": true, + "physical_supplier_or_kappa_claim": false + } +} diff --git a/research/six-source-duo-add16-floor/SELECTION.json b/research/six-source-duo-add16-floor/SELECTION.json new file mode 100644 index 0000000000..70b1056bf0 --- /dev/null +++ b/research/six-source-duo-add16-floor/SELECTION.json @@ -0,0 +1,55 @@ +{ + "seed": "74bf109ebf4b0af1edf0adfb0ea5761c", + "track": "recursive-interfaces", + "suggestions": [ + { + "task_id": "connector-alphabet-change", + "scope_key": "ff4f5113ed2256ab19ed", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "method": "Construct and charge a legal extra operation on a minimal instance.", + "starting_points": [ + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "catalog_assessed_on": "2026-10-14", + "priority_revision": 4, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/six-source-duo-add16-floor/SOURCES.json b/research/six-source-duo-add16-floor/SOURCES.json new file mode 100644 index 0000000000..38b6604250 --- /dev/null +++ b/research/six-source-duo-add16-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/duo-toggle-connector/CERTIFICATE.json", + "usage": "input", + "git_blob": "accffc014ce13993ddce723abd4256dc0c884e5b", + "sha256": "a1ad3af8bbc872a8abcf8df543267eb82cfa0ede8d581a30b6c751307bb4f267" + }, + { + "path": "research/universal-connector-six-source/EXPECTED.json", + "usage": "input", + "git_blob": "160a96c50f77ba411af957b554da05a8470e70ca", + "sha256": "f1b1bec330640c81ac0da25ee8b3a0a49fe9ea5bb2eadaaa787c64bd62c9e73a" + } + ] +} diff --git a/research/six-source-duo-add16-floor/TASK.json b/research/six-source-duo-add16-floor/TASK.json new file mode 100644 index 0000000000..6a43eedcff --- /dev/null +++ b/research/six-source-duo-add16-floor/TASK.json @@ -0,0 +1,156 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently rebuild the known unrestricted 14-point F2^6 difference-basis minimum and apply it, with source-add census controls, to prove the global six-source DUO batch optimum (140 queries,142 adds). Retain the exact (13,16) word/deletion census as a separate restricted cross-check.", + "scope_change_reason": "The original card asks for a new operation family. This continues PR2128 within the existing DUO alphabet. After completing the 16-add handoff, a literature checkpoint identified Gavrylkiv 2017 Table 3 and prompted a bounded independent affine-basis-normalized census; neither the old basis value nor the predecessor witness is claimed as new.", + "bottleneck_link": "The declared abstract connector tariff is now closed: the predecessor simultaneously attains the minimum batch query count and add count, so larger source-add budgets cannot buy a better query/add point under these rules. Future progress needs physical implementation or a changed observation/connector contract; no selected exponent improvement follows.", + "budget_minutes": 70, + "stop_rule": "Each of two first waves was limited to 20 minutes and 1 GiB aggregate process RSS. The restricted search used three local CPU workers and exhausted in 3.097 seconds; the unrestricted basis follow-up used two and exhausted in 2.077 seconds, including its launcher. Incomplete receipts reject. The investigation stops after independent reconstruction, dirty-column replay, complete batch accounting and publication; no higher-add blind search.", + "outcome": "completed", + "evidence": "Two independent implementations enumerate all 36,288,252 affine-basis-normalized 13-point sets and agree on the entire coverage histogram: maximum 63/64, with 4,200 attaining normalized sets. This independently reproduces the lower bound reported in Gavrylkiv 2017 Table 3; the predecessor 14-point witness is a positive control. A separate pair enumerates all 54,864,810 normalized 16-add unit words and agrees on the complete 7,480-word table; a literal Python audit checks 86,900 legal midpoint triples over 251 complete orbits. Both native basis enumerations pass complete UBSan runs. Full replay checks 256 affine normalization controls, all 70/140/210 dirty input columns, four behavioral mutants, three deadline gates and exact query/add lower bounds. The only abstract Pareto point is (140,142); no physical supplier or kappa claim.", + "author": "Tairitsu-Aya", + "ai_assistance": "Substantial OpenAI Codex assistance with source reading, mathematics, implementation, verification and writing for Tairitsu-Aya. Both algorithms and the audit have the same author/assistant; no independent human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Can a selected physical supplier implement a complete DUO call under its real frame, access, scratch-restoration and precision obligations?", + "why_it_matters": "The abstract connector point affects the multiplication construction only after all implementation costs and admissibility obligations are charged.", + "first_step": "Choose one pinned supplier and implement a small noncommuting arbitrary-input DUO fixture with explicit owner/frame transitions and a full charged invoice.", + "blocked_by": "This package contains no admitted physical DUO instance, compiler or complete supplier bill." + } + ], + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/2128#issuecomment-6177901532", + "predecessors": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2128", + "head": "697369a971eed02c0fbcd75ebefec9f59945f08e", + "credit": "Aaron Wang/Navinor: attaining six-source (14,16) word, abstract bill and released open-cell handoff." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1531", + "credit": "Navinor: DUO operation model, prices and five-source result." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/943", + "credit": "Ross Richardson: dirty-connector interface and prefix-difference reduction, following PR934." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1185", + "credit": "Douglas Colkitt: six-source singleton construction and census." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1215", + "credit": "Hanson Sun: six-source singleton follow-up." + } + ], + "overlap_checkpoint": { + "searched_at": "2026-10-14T21:06:05.136655+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T21:02:41.382778+00:00", + "complete_pagination": true, + "records": 403 + }, + "discussions": { + "fetched_at": "2026-10-14T21:06:04.987759+00:00", + "complete_pagination": true, + "records": 826 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "submission_supplement": { + "checked_at": "2026-10-14T21:16:10Z", + "duo_discussion_threads": 9, + "discussion_search_complete": true, + "comment_coverage": "Last ten comments per thread; older hub histories truncated. Full prior snapshot at21:06 separately recorded.", + "pr_searches": [ + "DUO", + "Gavrylkiv" + ], + "matching_new_claim_found": false, + "nearest_predecessor_head": "697369a971eed02c0fbcd75ebefec9f59945f08e", + "limitations": "Search coverage is not a novelty guarantee; the underlying 14-point result is already published." + } + }, + "upstream_checkpoint": { + "checked_at": "2026-10-14T21:16:10Z", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "selected_changed": false, + "source_changed": false + }, + "literature_checkpoint": { + "source": "https://cs.uwaterloo.ca/journals/JIS/VOL20/Gavrylkiv/gav4.pdf", + "author": "Volodymyr Gavrylkiv", + "title": "Bases in Dihedral and Boolean Groups", + "year": 2017, + "location": "Table3, page8", + "reported_value": "r[(C2)^6]=14", + "scope": "Known unrestricted value independently reproduced here. The verifier has no network dependency or reliance on a downloaded table." + }, + "validation": { + "complete_four_census_first_replay": { + "python": "3.12.3", + "os": "Ubuntu24.04", + "compiler": "g++13.3.0", + "wall_seconds": 13.31, + "peak_rss_kib": 120300, + "cpu_affinity": [ + 1 + ] + }, + "windows": "Python3.12.9 optimized portable restricted audit and metadata only; full native replay unavailable.", + "sanitizers": "Both unrestricted native enumerators completely replay under -fsanitize=undefined -fno-sanitize-recover=all.", + "independent_human_or_formal_kernel_review": false, + "registered_full_replay": { + "python": "3.12.3", + "os": "Ubuntu24.04", + "compiler": "g++13.3.0", + "wall_seconds": 13.38, + "peak_rss_kib": 120360, + "cpu_affinity": [ + 1 + ] + }, + "isolated_export_checks": "Ten passed, including complete Git-free replay without source mutation, optimized portable audit, missing/drifted input, corrupted table, count-preserving audit receipt, false theorem receipt, absent compiler and exclusive output creation/rejection." + } +} diff --git a/research/six-source-duo-add16-floor/VERIFY.json b/research/six-source-duo-add16-floor/VERIFY.json new file mode 100644 index 0000000000..ea48e474cd --- /dev/null +++ b/research/six-source-duo-add16-floor/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/duo-toggle-connector/CERTIFICATE.json", + "research/universal-connector-six-source/EXPECTED.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Authenticate frozen live inputs; compile four C++17 enumerators with warnings as errors; independently reconstruct both unrestricted 36,288,252-set coverage histograms and the complete 54,864,810-word restricted domain/table; audit all 251 orbits and 86,900 midpoint triples; check 256 affine normalization controls, predecessor positives, all dirty input columns, behavioral mutations, exact query/add lower bounds and rejection of three timed-out censuses; compare complete RESULT." + } + ], + "native_environment": "C++17 compiler required; tested Ubuntu 24.04 with g++ 13.3.0. CXX may name g++/clang++. No native dependency is installed by this package. audit.py alone is portable but does not rebuild the complete census." +} diff --git a/research/six-source-duo-add16-floor/audit.py b/research/six-source-duo-add16-floor/audit.py new file mode 100644 index 0000000000..0c55473f44 --- /dev/null +++ b/research/six-source-duo-add16-floor/audit.py @@ -0,0 +1,247 @@ +#!/usr/bin/env python3 +"""Audit the full-cover table and every orbit's unpruned hidden-prefix choices. + +This portable check does not establish table completeness by itself. verify.py +rebuilds the table with two independent complete C++ enumerations. +Tairitsu-Aya, substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter, defaultdict +import hashlib +from itertools import combinations +import json +from pathlib import Path +import random +import struct + +HERE = Path(__file__).resolve().parent +COVERS_SHA256 = "251100fa9f200ddb24cefac8a6b8255cfa43d1f3bd7e4bc3f45120d4f3aa7262" +INCUMBENT = [2, 16, 8, 16, 1, 4, 48, 4, 3, 4, 32, 8, 4, 16] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def normalize(word): + names = {} + return tuple(names.setdefault(x, len(names)) for x in word) + + +def orbit(word): + result = set() + for row in (word, word[::-1]): + for shift in range(16): + result.add(normalize(row[shift:] + row[:shift])) + return result + + +def prefixes(word): + out = [0] + for label in word: + out.append(out[-1] ^ (1 << label)) + require(out[-1] == 0, "restored singleton expansion") + return out[:-1] + + +def differences(points): + return {a ^ b for a in points for b in points} + + +def word_stats(steps, n=6): + require(all(type(s) is int and 0 < s < (1 << n) and s.bit_count() in (1, 2) + for s in steps), "singleton/DUO alphabet") + points = [0] + for step in steps: + points.append(points[-1] ^ step) + require(points[-1] == 0, "connector restoration") + points.pop() + return {"calls": len(steps), "adds": sum(s.bit_count() for s in steps), + "prefixes": points, "coverage": len(differences(points)), + "missing_masks": sorted(set(range(1 << n)) - differences(points))} + + +def compress(word, hidden): + points = prefixes(word) + kept = [i for i in range(16) if i not in hidden] + steps = [points[a] ^ points[b] for a, b in zip(kept, kept[1:] + kept[:1])] + stats = word_stats(steps) + require(stats["calls"] == 13 and stats["adds"] == 16, "charged thirteen-call word") + return {"unit_labels": list(word), "hidden_prefixes": list(hidden), + "steps": steps, **stats} + + +def invertible_rows(size, rng): + rows = [1 << i for i in range(size)] + if size > 1: + for _ in range(12): + a, b = rng.sample(range(size), 2) + rows[a] ^= rows[b] + return rows + + +def apply_rows(matrix, values): + out = [] + for mask in matrix: + value = 0 + for column, entry in enumerate(values): + if mask & (1 << column): + value ^= entry + out.append(value) + return out + + +def matrix_product(left, right): + # Deliberately use literal scalar entries for the expected block matrix. + size = len(left) + return [sum((sum(((left[i] >> k) & 1) * ((right[k] >> j) & 1) + for k in range(size)) % 2) << j for j in range(size)) + for i in range(size)] + + +def full_column_replay(size, mutation=None): + """All 70*size arbitrary input columns, with noncommuting dense F2 maps.""" + rng = random.Random(20261014 + size) + sources = [[1 << (j * size + c) for c in range(size)] for j in range(6)] + initial_targets = [[1 << ((6 + j) * size + c) for c in range(size)] for j in range(63)] + initial_connector = [1 << (69 * size + c) for c in range(size)] + targets = [list(row) for row in initial_targets] + connector = list(initial_connector) + bs = [invertible_rows(size, rng) for _ in range(6)] + aa = [invertible_rows(size, rng) for _ in range(63)] + if size > 1: + bs[0] = [1 << i for i in range(size)] + bs[0][0] ^= 2 + aa[0] = [1 << i for i in range(size)] + aa[0][0], aa[0][1] = aa[0][1], aa[0][0] + require(matrix_product(aa[0], bs[0]) != matrix_product(bs[0], aa[0]), + "noncommuting positive-control maps") + points = word_stats(INCUMBENT)["prefixes"] + reads = defaultdict(list) + for mask in range(1, 64): + first, second = next((i, j) for i, j in combinations(range(14), 2) + if points[i] ^ points[j] == mask) + reads[first].append(mask) + reads[second].append(mask) + if mutation == "drop_readout": + first = min(t for t in reads if 1 in reads[t]) + reads[first].remove(1) + elif mutation == "move_readout": + first, second = sorted(t for t in reads if 1 in reads[t]) + reads[second].remove(1) + reads[first].append(1) + steps = list(INCUMBENT) + if mutation == "shrink_duo": + first = next(i for i, step in enumerate(steps) if step.bit_count() == 2) + steps[first] &= steps[first] - 1 + for boundary, step in enumerate(steps): + for mask in reads[boundary]: + delta = apply_rows(aa[mask - 1], connector) + targets[mask - 1] = [x ^ y for x, y in zip(targets[mask - 1], delta)] + if mutation == "drop_source" and boundary == 13: + continue + # A DUO exposes only its outer boundaries; there are no reads here. + for j in range(6): + if step & (1 << j): + delta = apply_rows(bs[j], sources[j]) + connector = [x ^ y for x, y in zip(connector, delta)] + expected = [list(row) for row in initial_targets] + for mask in range(1, 64): + for j in range(6): + if not mask & (1 << j): + continue + product = matrix_product(aa[mask - 1], bs[j]) + for row in range(size): + for column in range(size): + if product[row] & (1 << column): + expected[mask - 1][row] ^= 1 << (j * size + column) + return connector == initial_connector and targets == expected + + +def compute(data): + require(hashlib.sha256(data).hexdigest() == COVERS_SHA256, "full-cover table SHA256") + require(len(data) == 7480 * 8, "7480 full-cover records") + codes = [v for (v,) in struct.iter_unpack("> (3 * i)) & 7 for i in range(16)) for code in codes} + groups = defaultdict(set) + profile_histogram = Counter() + for word in words: + require(normalize(word) == word and max(word) == 5, "canonical six-source word") + profile = tuple(sorted(Counter(word).values())) + require(profile in ((2, 2, 2, 2, 2, 6), (2, 2, 2, 2, 4, 4)), "even multiplicity profile") + profile_histogram[",".join(map(str, profile))] += 1 + require(differences(prefixes(word)) == set(range(64)), "actual full-cover word") + family = orbit(word) + require(family <= words, "full-cover table closed under normalized dihedral action") + groups[min(family)].add(word) + for representative, family in groups.items(): + require(family == orbit(representative), "complete disjoint orbit partition") + patterns = [p for p in combinations(range(16), 3) + if all((a - b) % 16 not in (1, 15) for a, b in combinations(p, 2))] + require(len(patterns) == 352, "all cyclic three-edge matching patterns") + histogram = Counter() + best = None + for word in sorted(groups): + points = prefixes(word) + for hidden in patterns: + if any(word[(v - 1) % 16] == word[v] for v in hidden): + continue + retained = [points[i] for i in range(16) if i not in hidden] + size = len(differences(retained)) + histogram[size] += 1 + require(size < 64, "unexpected thirteen-call full cover") + if best is None or size > best["coverage"]: + best = compress(word, hidden) + require(best["coverage"] == 63, "sharp retained-coverage maximum") + repair = 0 + for index in (0, 1, 2, 6): + repair ^= best["prefixes"][index] + require(best["missing_masks"] == [12] and repair == 12, + "four-readout repair of the sharp near miss") + incumbent = word_stats(INCUMBENT) + require((incumbent["calls"], incumbent["adds"], incumbent["coverage"]) == (14, 16, 64), + "PR2128 incumbent positive control") + require(len(differences(prefixes(tuple(best["unit_labels"])))) == 64, + "exposing forbidden internal prefixes invalidates the exclusion") + for size in (1, 2, 3): + require(full_column_replay(size), "complete dirty-input positive replay") + mutations = ["drop_readout", "move_readout", "shrink_duo", "drop_source"] + for mutation in mutations: + require(not full_column_replay(2, mutation), "behavioral mutation not detected: " + mutation) + return { + "full_unit_words": len(words), "full_unit_codes_sha256": COVERS_SHA256, + "full_cover_multiplicity_profiles": dict(sorted(profile_histogram.items())), + "unit_orbits": len(groups), + "orbit_size_histogram": {str(k): v for k, v in sorted(Counter(map(len, groups.values())).items())}, + "cyclic_deletion_patterns": len(patterns), + "tested_orbit_deletions": sum(histogram.values()), + "retained_coverage_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "max_coverage": best["coverage"], "max_witness": best, + "incumbent_steps": INCUMBENT, "incumbent": incumbent, + "positive_full_column_dimensions": [1, 2, 3], + "positive_full_input_columns": [70, 140, 210], + "behavioral_mutations_rejected": mutations, + "batch_at_minimum_add_budget": {"root_queries": 140, "adds": 142, + "source_calls": 14, "source_adds": 16, "readouts": 126}, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="write audit receipt exclusively instead of comparing RESULT") + args = parser.parse_args() + result = compute((HERE / "FULL-COVERS.bin").read_bytes()) + if args.out: + with args.out.open("x", encoding="utf-8", newline="\n") as handle: + handle.write(json.dumps(result, indent=2) + "\n") + else: + expected = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + require(result == expected["audit"], "exact portable audit receipt") + print("PASS_DUO_ADD16_TABLE_AUDIT: 7480 covers, 251 orbits, 86900 deletions, maximum 63/64") + print("Table completeness is separately established by verify.py's two complete native censuses.") + + +if __name__ == "__main__": + main() diff --git a/research/six-source-duo-add16-floor/basis.py b/research/six-source-duo-add16-floor/basis.py new file mode 100644 index 0000000000..78096ae043 --- /dev/null +++ b/research/six-source-duo-add16-floor/basis.py @@ -0,0 +1,130 @@ +"""Literal checks of the affine normalization, native census and batch bounds. + +The unrestricted r[(C2)^6]=14 value is reported by Gavrylkiv (JIS 2017, +Table 3). The native enumerators independently rebuild its finite lower bound. +Tairitsu-Aya, substantial OpenAI Codex assistance. Apache-2.0. +""" +import math +import random + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def differences(points): + return {a ^ b for a in points for b in points} + + +def normalize(points): + """Translate one point to zero, then choose an ordered linear basis.""" + require(points and len(set(points)) == len(points), "distinct nonempty input set") + shifted = [p ^ points[0] for p in points] + coordinates = {0: 0} + basis = [] + for point in shifted: + if point not in coordinates: + index = len(basis) + basis.append(point) + coordinates.update({v ^ point: mask | (1 << index) for v, mask in list(coordinates.items())}) + require(len(basis) == 6 and len(coordinates) == 64, "full affine span is necessary") + result = sorted(coordinates[p] for p in shifted) + require({0, 1, 2, 4, 8, 16, 32} <= set(result), "normalized affine basis") + for value, mask in coordinates.items(): + reconstructed = 0 + for j, v in enumerate(basis): + if mask & (1 << j): + reconstructed ^= v + require(reconstructed == value, "normalization invertibility") + require(len(differences(result)) == len(differences(points)), "coverage invariant under affine normalization") + return result + + +def affine_controls(incumbent, near): + rng = random.Random(202610142108) + cases = 0 + for points in (incumbent, near): + for _ in range(128): + images = [1 << j for j in range(6)] + for _ in range(30): + i, j = rng.sample(range(6), 2) + images[i] ^= images[j] + offset = rng.randrange(64) + transformed = [] + for point in points: + value = offset + for j in range(6): + if point & (1 << j): + value ^= images[j] + transformed.append(value) + rng.shuffle(transformed) + normalized = normalize(transformed) + require(len(differences(normalized)) == len(differences(points)), "independent affine-image control") + cases += 1 + try: + normalize(list(range(13))) + except ValueError as error: + require("full affine span" in str(error), "proper-subspace control failed for wrong reason") + else: + raise ValueError("proper-subspace input was treated as full affine span") + return cases + + +def audit(first, second, incumbent, old_controls): + keys = ("status", "normalized_sets", "maximum_coverage", "histogram") + require(all(first[key] == second[key] for key in keys), "independent unrestricted censuses disagree") + require(first["status"] == "EXHAUSTED", "complete unrestricted basis census required") + require(first["normalized_sets"] == math.comb(57, 6) == 36288252, "all affine-basis-normalized 13-sets") + histogram = first["histogram"] + require(sum(histogram.values()) == first["normalized_sets"] and all(v > 0 for v in histogram.values()), + "complete coverage histogram") + require(max(map(int, histogram)) == first["maximum_coverage"] == 63, "unrestricted 13-point maximum") + witnesses = [] + for native in (first, second): + points = native["maximum_witness"] + require(len(points) == len(set(points)) == 13 and all(type(p) is int and 0 <= p < 64 for p in points), + "thirteen distinct binary points") + require({0, 1, 2, 4, 8, 16, 32} <= set(points), "native normalized domain") + require(len(differences(points)) == 63, "literal maximum-witness coverage") + witnesses.append(sorted(points)) + require(len(incumbent) == len(set(incumbent)) == 14 and len(differences(incumbent)) == 64, + "retained attaining fourteen-point basis") + transformed = affine_controls(incumbent, witnesses[0]) + # Source calls k<=11 have at most C(k,2) nonzero differences. The complete + # census gives at least one missing mask for k=12,13. Each missing output + # needs >=4 instead of >=2 readouts; larger k already costs >=14+126. + query_bounds = [] + for calls in range(1, 15): + missing = max(0, 63 - math.comb(calls, 2)) + if calls <= 13: + missing = max(missing, 1) + reads = 126 + 2 * missing + query_bounds.append({"source_calls": calls, "missing_masks_at_least": missing, + "readouts_at_least": reads, "queries_at_least": calls + reads}) + require(min(row["queries_at_least"] for row in query_bounds) == 140, "global batch query floor") + adds = [] + for width in (12, 14): + covered = old_controls[6, width]["max_coverage"] + adds.append({"source_adds": width, "total_adds_at_least": width + 126 + 2 * (64 - covered)}) + adds.extend([{"source_adds": 16, "total_adds_at_least": 142}, + {"source_adds": "even >=18", "total_adds_at_least": 144}]) + require(min(row["total_adds_at_least"] for row in adds) == 142, "global batch add floor") + return { + "domain": "all 13-element subsets of F2^6 up to existence of an affine-basis normalization", + "normalization": {"fixed_points": [0, 1, 2, 4, 8, 16, 32], "available_points": 57, + "chosen_points": 6, "normalized_sets": first["normalized_sets"]}, + "coverage_histogram": histogram, + "maximum_coverage": 63, + "maximum_witnesses": witnesses, + "attaining_14_points": incumbent, + "affine_image_controls": transformed, + "proper_subspace_control_rejected": True, + "query_lower_bounds": query_bounds, + "add_lower_bounds": adds, + "minimum_paired_universal_source_calls_any_add_budget": 14, + "global_batch_optimum": {"queries": 140, "adds": 142}, + "literature": {"author": "Volodymyr Gavrylkiv", "title": "Bases in Dihedral and Boolean Groups", + "year": 2017, "location": "Table 3", "reported_value": "r[(C2)^6]=14", + "url": "https://cs.uwaterloo.ca/journals/JIS/VOL20/Gavrylkiv/gav4.pdf"}, + } diff --git a/research/six-source-duo-add16-floor/basis13_bitset.cpp b/research/six-source-duo-add16-floor/basis13_bitset.cpp new file mode 100644 index 0000000000..5d54587dcf --- /dev/null +++ b/research/six-source-duo-add16-floor/basis13_bitset.cpp @@ -0,0 +1,73 @@ +// Independent colexicographic bit-combination census and XOR-set translations. +// Tairitsu-Aya, substantial OpenAI Codex assistance. Apache-2.0. +#include +#include +#include +#include +#include +#include +#include + +uint64_t shifted(uint64_t bits,unsigned vector) { + constexpr std::array lower={0x5555555555555555ULL,0x3333333333333333ULL, + 0x0f0f0f0f0f0f0f0fULL,0x00ff00ff00ff00ffULL,0x0000ffff0000ffffULL,0x00000000ffffffffULL}; + for(unsigned i=0;i<6;++i) if(vector&(1u<>stride); + } + return bits; +} +uint64_t difference_set(uint64_t points) { + uint64_t answer=0,pending=points; + while(pending) {unsigned p=__builtin_ctzll(pending);pending&=pending-1;answer|=shifted(points,p);} + return answer; +} +void controls() { + uint64_t known=0; + for(int point: {0,2,18,26,10,11,15,63,59,56,60,28,20,16}) known|=uint64_t(1)<0)) throw std::runtime_error("invalid deadline"); + for(unsigned x=0;x<64;++x) for(unsigned y=0;y<64;++y) + if(shifted(uint64_t(1)< available; + for(int p=0;p<64;++p) if(!(base&(uint64_t(1)< histogram{}; + uint64_t count=0,best_set=0,selection=63; + int maximum=0; + const auto start=std::chrono::steady_clock::now(); + auto elapsed=[&]() { return std::chrono::duration(std::chrono::steady_clock::now()-start).count(); }; + bool expired=false; + while(selection<(uint64_t(1)<<57)) { + if((count&65535)==0 && elapsed()>=seconds) {expired=true;break;} + uint64_t points=base,left=selection; + while(left) {unsigned at=__builtin_ctzll(left);left&=left-1;points|=uint64_t(1)<maximum) {maximum=size;best_set=points;} + // Gosper's next combination: all 57-bit words with exactly six ones. + uint64_t low=selection&-selection,raised=selection+low; + selection=raised|(((selection^raised)>>2)/low); + } + std::cout<<"{\"status\":\""<<(expired?"TIMEOUT":"EXHAUSTED")<<"\",\"normalized_sets\":"< +#include +#include +#include +#include +#include +#include +#include + +using Clock=std::chrono::steady_clock; +uint64_t extend(uint64_t coverage,int point,const int* previous,int count) { + for(int i=0;i known{0,2,18,26,10,11,15,63,59,56,60,28,20,16}; + uint64_t coverage=1; + for(int i=0;i<14;++i) coverage=extend(coverage,known[i],known.data(),i); + if(coverage!=~uint64_t(0)) throw std::runtime_error("fourteen-point positive control"); + const std::array near{0,1,2,4,8,16,32,3,5,30,46,54,57}; + coverage=1; + for(int i=0;i<13;++i) coverage=extend(coverage,near[i],near.data(),i); + if(__builtin_popcountll(coverage)!=63) throw std::runtime_error("thirteen-point near-cover control"); +} +struct Census { + std::array points{0,1,2,4,8,16,32}; + std::vector options; + std::array histogram{}; + std::array witness{}; + uint64_t count=0,nodes=0; + int best=0; + bool expired=false; + double seconds; + Clock::time_point start=Clock::now(); + explicit Census(double deadline):seconds(deadline) { + if(!(seconds>0)) throw std::runtime_error("invalid deadline"); + for(int p=0;p<64;++p) + if(std::find(points.begin(),points.begin()+7,p)==points.begin()+7) options.push_back(p); + if(options.size()!=57) throw std::runtime_error("wrong remaining domain"); + } + double elapsed() const { return std::chrono::duration(Clock::now()-start).count(); } + void walk(int index,int first,uint64_t coverage) { + if(expired) return; + if((++nodes&65535)==0 && elapsed()>=seconds) {expired=true;return;} + if(index==13) { + ++count; int size=__builtin_popcountll(coverage);++histogram[size]; + if(size>best) {best=size;witness=points;} + return; + } + int needed=13-index; + for(int j=first;j+needed<=int(options.size());++j) { + points[index]=options[j];uint64_t next=extend(coverage,points[index],points.data(),index); + walk(index+1,j+1,next); + if(expired) return; + } + } + void run() { + uint64_t initial=1; + for(int i=0;i<7;++i) for(int j=0;j +#include +#include +#include +#include +#include +#include +#include +#include + +uint64_t translate(uint64_t v,unsigned x) { + if(x&1) v=((v&0x5555555555555555ULL)<<1)|((v&0xAAAAAAAAAAAAAAAAULL)>>1); + if(x&2) v=((v&0x3333333333333333ULL)<<2)|((v&0xCCCCCCCCCCCCCCCCULL)>>2); + if(x&4) v=((v&0x0F0F0F0F0F0F0F0FULL)<<4)|((v&0xF0F0F0F0F0F0F0F0ULL)>>4); + if(x&8) v=((v&0x00FF00FF00FF00FFULL)<<8)|((v&0xFF00FF00FF00FF00ULL)>>8); + if(x&16) v=((v&0x0000FFFF0000FFFFULL)<<16)|((v&0xFFFF0000FFFF0000ULL)>>16); + if(x&32) v=(v<<32)|(v>>32); + return v; +} + +struct Census { + int n,length; + std::array word{}; + uint64_t words=0,full_words=0,profile_four=0,profile_six=0; + int best=0, profile=0; + std::vector complete; + std::chrono::steady_clock::time_point start=std::chrono::steady_clock::now(); + Census(int a,int b):n(a),length(b) {} + + void endpoint() { + ++words; + profile_four+=(profile==4);profile_six+=(profile==6); + uint64_t points=1;unsigned point=0; + for(int j=0;j(length-1)); + if(point) throw std::runtime_error("even-block word failed restoration"); + const uint64_t full=n==6?~uint64_t(0):(uint64_t(1)<<(1<=need) { + uint32_t bit=options & -options;options^=bit; + choose(options,need-1,block|bit,unassigned,label,twos,fours,sixes); + } + } + + void run() { + uint32_t all=(uint32_t(1)<>(8*j))&255)); + if(!out) throw std::runtime_error("audit output failed"); + double duration=std::chrono::duration(std::chrono::steady_clock::now()-start).count(); + std::cout<<"{\"status\":\"EXHAUSTED\",\"n\":"<6 || w>16 || w<2*n || w%2) throw std::runtime_error("invalid census domain"); + Census census(n,w);census.run();census.finish(argv[3]);return 0; + } catch(const std::exception& e) {std::cerr< +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using Clock = std::chrono::steady_clock; +struct Search { + int n, length, calls, remove, shard, shards, cut, maximum_count; + double seconds; + bool unit_only, timed_out = false, found = false; + Clock::time_point start = Clock::now(), last = start; + uint64_t nodes = 0, words = 0, full_words = 0, candidates = 0; + uint64_t profile_four = 0, profile_six = 0; + int best_unit = 0, best_screened = 0, max_eligible = 0; + std::array counts{}; + std::array labels{}, prefixes{}; + std::vector eligible, deleted, witness_steps, witness_prefixes, witness_unit, witness_deleted; + std::vector full_codes; + + Search(int nn, int ll, int kk, int ss, int ns, double tt, bool only) + : n(nn), length(ll), calls(kk), remove(ll-kk), shard(ss), shards(ns), + cut(std::min(6,ll)), maximum_count(ll-2*(nn-1)), seconds(tt), unit_only(only) { + if (n<1 || n>6 || length<2*n || length>16 || length%2 || calls<1 || + remove<0 || 2*remove>length || shard<0 || shard>=shards || seconds<=0) + throw std::runtime_error("invalid finite search domain"); + } + + double elapsed() const { return std::chrono::duration(Clock::now()-start).count(); } + uint64_t full() const { return n==6 ? ~uint64_t(0) : (uint64_t(1)<<(1<& values) { + std::cout << ",\""<2) throw std::runtime_error("invalid reconstructed call"); + weight+=w; parity^=step; + } + if (int(witness_steps.size())!=calls || weight!=length || parity) + throw std::runtime_error("reconstructed word does not match its bill"); + witness_unit.assign(labels.begin(),labels.begin()+length); + witness_deleted=deleted; + found=true; + } + + void choose_deletions(int offset, uint32_t hidden) { + if(found || timed_out) return; + if(int(deleted.size())==remove) { + ++candidates; + uint64_t coverage=1; + for(int i=0;i multiplicity{}; + for(int i=0;i=remove) choose_deletions(0,0); + } + + void dfs(int pos, int seen, int parity, uint64_t coverage) { + if(found || timed_out) return; + ++nodes; + if((nodes & 131071)==0) { + auto now=Clock::now(); + if(std::chrono::duration(now-start).count()>=seconds) {timed_out=true;return;} + if(std::chrono::duration(now-last).count()>=10) {report("RUNNING");last=now;} + } + if(pos==cut && shards>1) { + uint64_t code=1469598103934665603ULL; + for(int i=0;i=maximum_count) continue; + ++counts[lab]; + int required=0; + for(int i=0;i>(8*i))&255)); + if(!out) throw std::runtime_error("full-cover output failed"); + } +}; + +uint64_t coverage(const std::vector& points) { + uint64_t bits=1; + for(int a:points) for(int b:points) bits|=uint64_t(1)<<(a^b); + return bits; +} + +void selftest() { + std::vector old={2,16,8,16,1,4,48,4,3,4,32,8,4,16}; + std::vector unit,hidden,points={0}; int q=0; + for(int step:old) { + std::vector bits; + for(int j=0;j<6;++j) if(step&(1< retained; + for(int i=0;i<16;++i) if(std::find(hidden.begin(),hidden.end(),i)==hidden.end()) retained.push_back(points[i]); + if(unit.size()!=16 || hidden.size()!=2 || q || coverage(retained)!=~uint64_t(0)) + throw std::runtime_error("retained fourteen-call positive control"); + Search tiny(3,6,5,0,1,30,false);tiny.run(); + if(!tiny.found) throw std::runtime_error("three-source five-call positive control"); + Search count(6,12,12,0,1,30,true);count.run(); + if(count.timed_out || count.words!=10395 || count.best_unit!=49) + throw std::runtime_error("10395-word six-source singleton census control"); + std::cout<<"{\"status\":\"PASS_SELFTEST\",\"retained_fourteen_call_control\":true}"<