diff --git a/research/seven-source-root-minimum/CENSUS.json b/research/seven-source-root-minimum/CENSUS.json new file mode 100644 index 0000000000..1f65730172 --- /dev/null +++ b/research/seven-source-root-minimum/CENSUS.json @@ -0,0 +1,348 @@ +{ + "cases": 87972885, + "difference_histogram": { + "29": 429, + "34": 2002, + "38": 4004, + "40": 2002, + "41": 1820, + "43": 8554, + "44": 106, + "45": 4368, + "47": 6734, + "49": 14560, + "50": 1428, + "51": 5460, + "52": 2982, + "53": 364, + "54": 11298, + "56": 17458, + "58": 4648, + "59": 7392, + "60": 1386, + "61": 2912, + "62": 8834, + "64": 9380, + "65": 770, + "67": 8316, + "69": 5208, + "71": 2720 + }, + "groups": { + "2+2+2+1": { + "missing_histogram": { + "33": 7, + "34": 161, + "35": 1260, + "36": 4578, + "37": 15666, + "38": 48041, + "39": 95802, + "40": 137074, + "41": 182203, + "42": 239274, + "43": 296100, + "44": 347977, + "45": 374003, + "46": 393127, + "47": 421967, + "48": 449785, + "49": 501298, + "50": 536480, + "51": 617876, + "52": 665980, + "53": 690669, + "54": 670621, + "55": 653737, + "56": 654318, + "57": 663138, + "58": 658189, + "59": 651595, + "60": 603911, + "61": 558831, + "62": 530173, + "63": 460887, + "64": 415611, + "65": 364707, + "66": 302953, + "67": 254632, + "68": 193753, + "69": 165781, + "70": 116025, + "71": 87010, + "72": 61782, + "73": 42189, + "74": 23198, + "75": 19390, + "76": 5978, + "77": 5208, + "78": 5152, + "81": 1078 + }, + "partitions": 105 + }, + "3+2+1+1": { + "missing_histogram": { + "28": 112, + "29": 392, + "30": 4032, + "31": 13188, + "32": 35364, + "33": 91560, + "34": 160790, + "35": 252798, + "36": 359422, + "37": 472164, + "38": 573328, + "39": 669634, + "40": 736001, + "41": 817509, + "42": 889581, + "43": 1015798, + "44": 1116031, + "45": 1188607, + "46": 1223117, + "47": 1251446, + "48": 1299970, + "49": 1378202, + "50": 1434993, + "51": 1384586, + "52": 1335964, + "53": 1325177, + "54": 1300943, + "55": 1231860, + "56": 1119090, + "57": 1035027, + "58": 915880, + "59": 796453, + "60": 667870, + "61": 589820, + "62": 452382, + "63": 383691, + "64": 273336, + "65": 227724, + "66": 126294, + "67": 111888, + "68": 42014, + "69": 45836, + "70": 14364, + "71": 10220, + "73": 3892 + }, + "partitions": 210 + }, + "3+2+2": { + "missing_histogram": { + "20": 70, + "21": 420, + "22": 945, + "23": 2450, + "24": 5453, + "25": 12285, + "26": 24955, + "27": 45346, + "28": 69300, + "29": 106162, + "30": 151200, + "31": 193228, + "32": 249459, + "33": 290752, + "34": 358638, + "35": 396578, + "36": 458269, + "37": 497140, + "38": 573559, + "39": 604163, + "40": 668073, + "41": 722183, + "42": 751548, + "43": 774193, + "44": 774543, + "45": 795452, + "46": 753438, + "47": 732851, + "48": 685279, + "49": 638001, + "50": 539994, + "51": 559944, + "52": 393568, + "53": 392287, + "54": 268709, + "55": 268765, + "56": 125951, + "57": 153650, + "58": 47166, + "59": 63364, + "60": 18578, + "61": 17416, + "63": 3850 + }, + "partitions": 105 + }, + "3+3+1": { + "missing_histogram": { + "13": 28, + "14": 210, + "15": 609, + "16": 2492, + "17": 7154, + "18": 17087, + "19": 30884, + "20": 56910, + "21": 90118, + "22": 134008, + "23": 168623, + "24": 227164, + "25": 251503, + "26": 316071, + "27": 342118, + "28": 414057, + "29": 458913, + "30": 495355, + "31": 481117, + "32": 528255, + "33": 479262, + "34": 541660, + "35": 519029, + "36": 500304, + "37": 464758, + "38": 408758, + "39": 327320, + "40": 368081, + "41": 398048, + "42": 417179, + "43": 362544, + "44": 288239, + "45": 189252, + "46": 108808, + "47": 42588, + "48": 15932, + "49": 5012 + }, + "partitions": 70 + }, + "4+1+1+1": { + "missing_histogram": { + "19": 7, + "21": 28, + "22": 224, + "23": 812, + "24": 3276, + "25": 6426, + "26": 16863, + "27": 27118, + "28": 45675, + "29": 65002, + "30": 86590, + "31": 100548, + "32": 123578, + "33": 137753, + "34": 167741, + "35": 167776, + "36": 199913, + "37": 192941, + "38": 210315, + "39": 215845, + "40": 215033, + "41": 222390, + "42": 246820, + "43": 235403, + "44": 243537, + "45": 253638, + "46": 225918, + "47": 221956, + "48": 199143, + "49": 170373, + "50": 148848, + "51": 147462, + "52": 108157, + "53": 100814, + "54": 68411, + "55": 50918, + "56": 32319, + "57": 38248, + "58": 12320, + "59": 17528, + "61": 2058 + }, + "partitions": 35 + }, + "4+2+1": { + "missing_histogram": { + "10": 7, + "11": 126, + "12": 672, + "13": 2226, + "14": 6832, + "15": 15750, + "16": 37814, + "17": 58345, + "18": 103985, + "19": 145257, + "20": 222607, + "21": 266441, + "22": 378364, + "23": 419349, + "24": 532532, + "25": 535318, + "26": 678552, + "27": 708379, + "28": 744842, + "29": 734286, + "30": 873614, + "31": 800107, + "32": 815094, + "33": 785519, + "34": 691040, + "35": 661052, + "36": 614551, + "37": 715918, + "38": 611471, + "39": 644896, + "40": 490574, + "41": 413721, + "42": 262500, + "43": 158144, + "44": 46144, + "45": 13146 + }, + "partitions": 105 + }, + "5+1+1": { + "missing_histogram": { + "4": 350, + "5": 504, + "6": 3024, + "7": 616, + "8": 12852, + "9": 6734, + "10": 17437, + "11": 31031, + "12": 59346, + "13": 57190, + "14": 79576, + "15": 104405, + "16": 152649, + "17": 121562, + "18": 182056, + "19": 152054, + "20": 173670, + "21": 132657, + "22": 208236, + "23": 184240, + "24": 182119, + "25": 195678, + "26": 166684, + "27": 180579, + "28": 166516, + "29": 153216, + "30": 97524, + "31": 15330 + }, + "partitions": 21 + } + }, + "partitions": 651, + "sources": 7, + "words": 135135 +} diff --git a/research/seven-source-root-minimum/README.md b/research/seven-source-root-minimum/README.md new file mode 100644 index 0000000000..2fac5ab937 --- /dev/null +++ b/research/seven-source-root-minimum/README.md @@ -0,0 +1,263 @@ +# Four dirty roots are necessary and sufficient at seven sources + +**Scoped root-count optimum; no new kappa.** In the generic F2 connector +interface below, all 127 nonzero seven-source masks require **at least four +arbitrary-dirty root rows** if every source map and every output map is called +exactly twice. This remains true with arbitrarily many invertible F2 root-frame +changes and per-occurrence physical ports. The four-root star construction +already supplied by [PR2182](https://github.com/CrocSwap/integer-mult-bounds/pull/2182) +attains the minimum. **The new contribution is the three-root exclusion and +therefore the exact seven-source root minimum, not the attaining construction.** + +The proof reduces every schedule in this infinite frame/length domain to a +finite necessary condition. Two separately written implementations exhaust +135,135 source words and 651 source-class partitions: 87,972,885 cases. Every +case fails that condition. The smallest deficit is four mandatory masks. +A literal attaining program, symbolic replay, rectangular-map checks, and +failure controls accompany the census. This is a written proof with exact +finite evidence, not a proof-assistant formalization. + +## Interface and quantifiers + +There are seven immutable sources x_j, 127 distinct output rows y_m, and k +root rows z_p, all initially arbitrary. All roots have the same vector width. +For independently chosen compatible F2-linear maps B_j and A_m, the target is + +``` +y_m += A_m(sum_{j: m_j=1} B_j(x_j)), 1 <= m <= 127. +``` + +A schedule uses complete fixed-map additive calls B_j into a root and A_m +from a root into its own output. It uses **exactly two calls to every B_j and +every A_m**. The schedule is data-independent and must implement the identity +for arbitrary maps and inputs. Sources and roots restore; outputs are not +observed or used as workspace. Child scratch is private, restores, and cannot +alias source, target or root rows. Linear maps need not be invertible, square, +symmetric or commuting. + +For the lower bound, grant every invertible scalar F2 mixing of the k root +rows at any time, at no cost, and allow any physical port on each child call. +This is a relaxation of paid root XORs. It does not grant resets, clean roots, +source mixing, target feedback, extra map calls, or matrix-valued transformations +inside a root row. The upper bound uses only explicitly charged XORs +`X(p,q): z_p += z_q` and restores the identity root frame. + +The theorem is about the minimum root count **at these minimum map incidences**. +It does not minimize total work across schedules that call maps more often. +Multi-root source incidence need not be even in general: the verifier includes +a restoring three-call source excursion to guard that distinction. + +## Reduction to source-axis classes + +Write h_j = B_j(x_j), and let R_t be the current invertible root frame. A +source call at physical port p injects normalized axis R_t^-1 e_p. Since +exactly two calls to each source must restore all independent h_j columns, +their normalized axes coincide; call this nonzero vector v_j. Let q_t be the +source-incidence parity after the first t source calls. The normalized root +state is + +``` +z_initial + sum_j v_j q_t[j] h_j. +``` + +A physical root with dirty covector r has source coefficients +`(r dot v_j) q_t[j]`. Two readouts of the same arbitrary A_m must have the +same dirty covector, or initial root dirt survives. Their target mask is thus + +``` +m = s_r AND (q_a XOR q_b), where s_r[j] = r dot v_j. +``` + +This is a necessary condition even if the selected covector is not available +at those boundaries. Granting all covectors at every boundary only enlarges +the realizable set. Put `D(w) = {q_a XOR q_b}` for the closed source word w. +Transfers between source calls do not add new q values. + +It suffices to exclude k=3: fewer rows embed in this model with unused dirty +rows. The all-ones output requires a covector r_* with r_* dot v_j = 1 for +every j. Thus the occupied axes lie in the four-point affine plane +`{v in F2^3: r_* dot v = 1}`. Partition the seven sources by identical axes. +There are at most four nonempty classes. + +**Mandatory-mask lemma.** With three or four occupied classes, a mask meeting +at least three classes can only use a covector responding to every occupied +axis. Consequently it must itself belong to D(w). + +For three occupied axes the assertion is immediate: responding to three means +responding to all three. For four axes, their sum is zero, so every covector +has even total response. A response containing three axes therefore contains +all four. Equivalently, three distinct points in this affine plane are linearly +independent: a dependence among them would contradict r_* dot v = 1. + +With one occupied class, all nonzero masks already require the all-source +response; choose any refinement into three nonempty classes and its mandatory +masks remain necessary. With two classes, split one into two nonempty classes. +Every mask meeting all three refined classes meets both original classes, so +it also requires the all-source response and lies in D(w). There are seven +sources, so these refinements exist. This covers the smaller-class cases +without importing a prior lower-bound census. + +## Complete finite domain and result + +Every source occurs twice, so relabeling by first occurrence reduces the source +order to a pairing of 14 positions: `(14)!/(2^7 7!) = 135135` words. After this +relabeling, retain **every** set partition of the seven labels into three or +four nonempty classes. There are S(7,3)=301 and S(7,4)=350, respectively. No +source-color symmetry is discarded without retaining its class assignment. + +For every word/partition pair, compute the mandatory set M of masks meeting +at least three classes and count `|M minus D(w)|`. The exact minima are: + +| Class sizes | Partitions | Minimum missing mandatory masks | +|---|---:|---:| +| 5+1+1 | 21 | 4 | +| 4+2+1 | 105 | 10 | +| 3+3+1 | 70 | 13 | +| 3+2+2 | 105 | 20 | +| 4+1+1+1 | 35 | 19 | +| 3+2+1+1 | 210 | 28 | +| 2+2+2+1 | 105 | 33 | + +Every minimum is positive. Hence no three-root schedule exists. This is an +exhaustive necessary-condition exclusion, not a failed heuristic search. Full +missing-count histograms and the source-difference histogram are in +[CENSUS.json](CENSUS.json). A further check is possible: merging two of four +classes yields three classes whose mandatory set is a subset of the original; +the four-class enumeration is redundant for exclusion but supplied explicitly. + +The C++ engine generates position matchings, forms prefix XOR differences, and +builds mandatory masks by testing per-mask class incidence. The Python engine +generates restricted-growth words, accumulates contiguous-interval parities, +and builds mandatory masks by products of within-class subsets. Their complete +histograms agree. Neither imports predecessor census code. The registered +Python replay recomputes all cases; it does not trust a native receipt. + +Specializing extra source maps to zero and discarding their identity calls +extends the lower bound to **at least four roots for every n >= 7** in the same +paired-call model. It does not assert that four suffice beyond seven. + +## Attainment and complete cost + +PR2182's construction uses k=n-3 roots. At n=7, reserve a center z0 and three +leaves z1,z2,z3. Run the closed center source cycle B0 B1 B0 B1, visiting all +8 center frames `z0 += sum u_i z_(i+1)` at each of its four prefix states. +Use alternating forward/reverse reflected Gray tours, returning the frame to +identity after four tours. Inject B4, B5, B6 into the three leaves. Run the +analogous center cycle B2 B3 B2 B3 and the same tours. Finally repeat the three +leaf injections to restore their arbitrary dirt. + +For mask `m = a | (b << 2) | (c << 4)`, read A_m at prefix a and frame c in +the first phase, and prefix b and frame c in the second. The dirty covectors +match, and their difference is the requested source sum. This proves the +attainment for arbitrary compatible maps. [WITNESS.json](WITNESS.json) lists +every physical operation; [program.py](program.py) emits this **credited +predecessor construction**, and the verifier independently interprets it. + +The program has 14 complete B calls, 254 complete A calls, and 56 root XORs: +32 of X(0,1), 16 of X(0,2), and 8 of X(0,3). With p_j=0 for j<4 and p_j=j-3 +otherwise, its full conditional node bill is + +``` +C_7(L) = H_4(L) + 2 sum_j T_Bj(L,p_j) + 2 sum_m T_Am(L,0) + + 32 T_X(L,0,1) + 16 T_X(L,0,2) + 8 T_X(L,0,3). +``` + +Here each T is a complete child/transfer price including that operation's +access, dispatch, scratch restoration and head return. H_4 includes root +admission, initial layout, reusable map preparation, schedule generation/storage +and any remaining controller costs; charges included in T are not counted +again. Four root rows must remain reserved throughout. Sequential child calls +may reuse private scratch only when its admission contract permits it; with +maximum private scratch S(L), roots plus private scratch need 4L+S(L) cells, +in addition to all source/output and preparation storage. On a direct scalar +backend, a root XOR costs L bit XORs, not a free frame change. No actual recursive +supplier/caller is bound here, and no favorable physical recurrence or new +multiplication exponent is inferred from this invoice. + +## Reproduce and checks + +Base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. The selected +conditional kappa remains `836330098538459/500000000000000000` (PR1094). +With Python 3.12 standard library, from the repository root: + +```sh +python3.12 -I -O -B research/seven-source-root-minimum/verify.py +``` + +Expected: + +``` +PASS_SEVEN_SOURCE_ROOT_MINIMUM words=135135 partitions=651 cases=87972885 roots=4 B=14 A=254 X=56 dense_columns=4362 mutations=329 affine_checks=245 +``` + +The independent native comparison (GCC or Clang with unsigned 128-bit support): + +```sh +c++ -O3 -std=c++17 -Wall -Wextra research/seven-source-root-minimum/census.cpp -o /tmp/seven-root-census +/tmp/seven-root-census > /tmp/seven-root-native.json +python3.12 -I -O -B research/seven-source-root-minimum/verify.py --native-result /tmp/seven-root-native.json +``` + +Registered replay: + +```sh +python3.12 scripts/research_package.py --package research/seven-source-root-minimum +``` + +Besides full census regeneration, verification checks all formal dirty/source +columns of the attaining program forward and backward, 4,362 concrete basis +columns across 18 rectangular/singular-map forward/inverse cases, all 324 +single-operation omissions, five port/direction/label/schema mutations, the +245 finite affine-plane cases, and a differently computed mandatory mask set. +Positive controls admit the known six-source/three-root program, a neutral +transfer pair, and odd source incidence in a restoring multi-root excursion. +Historical pins require Git only for the registered metadata check; direct +scientific replay is self-contained and performs no network access or writes. + +## Scope, overlap and credit + +The three candidates considered were the five-source arbitrary-price frontier +(already PR2063), paired heterogeneous output events (already PR2230), and the +seven-source root minimum explicitly left open by PR2182. The last was chosen +under the user's fresh OS assignment seed 54, recursive interfaces. The card's +scope is recorded as **changed**: this settles an interface-capacity question, +not a new supplier or success at the original alphabet-cost acceptance gate. + +PR2182, pinned at `dc252de1cc594829c3031abdb4de104713bc474a`, supplies the normalized-axis +method, the two-root n>=6 boundary, and the attaining star. It explicitly leaves +n>=7 root optimality open. Ross Richardson's PR934/PR943 supply the underlying +dirty-connector contract and prefix criterion, and Douglas Colkitt's PR1185 +supplies the earlier six-source/Gray lineage. Their common-factor/dirty-commutator +predecessors include PR889 and Chafik Boukhalfa's PR628. + +Cinna Davis's PR2229 and PR2236 use one root and weight-1/2/3 output masks at 14 +and 16 source calls. The full-mask, arbitrary-frame, three-root exclusion here +has a different quantified domain. Adam Gall's PR2063 establishes five-source +one-root tariffs; it is not resubmitted. Related PR2208 allows additional calls +and develops different all-word tariff bounds. Exact heads, source hashes and +fresh overlap coverage are recorded in [SOURCES.json](SOURCES.json) and +[TASK.json](TASK.json). The final refresh at 2026-10-15 03:20 UTC completely paginated 502 open PRs +and 989 discussion/comment/reply records, with no warnings. No matching result +was found; this is not a guarantee against unseen work. +The coordination record is [Discussion2275](https://github.com/CrocSwap/integer-mult-bounds/discussions/2275). + +Prepared by **Mason Hale**, with substantial **OpenAI Codex** assistance in +proof derivation, code, experiments, review and writing. Apache-2.0. No +independent human review or proof-assistant verification is claimed. No selected +frontier, upstream source, or frozen predecessor file is changed. Global +selected cold replay is not needed for this isolated package and was not run. + +## Open next questions + +1. Does four-root attainment extend to eight sources at two calls per map? + This would locate the next storage boundary. Start from the normalized + affine-plane model in F2^4 and the existing five-root star; a complete + reduction is needed before scaling the census. +2. What is the minimum paid transfer bill at seven sources with four roots? + The 56-X star is an upper bound only. Start by optimizing a fixed legal + readout/source schedule with exact dirty-frame states. Global optimality + needs a justified search-length bound and actual port tariffs. +3. Does a concrete recursive caller profit from the four-root interface? + Instantiate every T and H term above and compare with a one-root schedule + using extra child calls. The missing caller, stock, tape and precision + contracts remain the blockers; this root theorem alone supplies no gain. diff --git a/research/seven-source-root-minimum/SOURCES.json b/research/seven-source-root-minimum/SOURCES.json new file mode 100644 index 0000000000..9f38191774 --- /dev/null +++ b/research/seven-source-root-minimum/SOURCES.json @@ -0,0 +1,89 @@ +{ + "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/universal-connector-boundary/CERTIFICATE.json", + "usage": "provenance", + "git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0", + "sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + { + "path": "research/universal-connector-boundary/NOTICE.md", + "usage": "provenance", + "git_blob": "d9afdf81f656278dab69239f0fd94924f97df87b", + "sha256": "1172648a1883827399d5103a9916deaa4314e4ee2c28653c183890f6bd5a7a17" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + } + ], + "external_provenance": { + "pr": 2182, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2182", + "head": "dc252de1cc594829c3031abdb4de104713bc474a", + "author": "conorholds", + "role": "Normalized-axis reduction and credited four-root attaining star; no runtime imports or external replay dependencies. These pins were checked locally; generic metadata validation checks the base-commit files above.", + "files": [ + { + "path": "research/scalable-dirty-connectors/README.md", + "git_blob": "dc3f9202735a5d55e95e34e64746f4afb74bfba6", + "sha256": "3484f6454736045ea4a6ab6e67710cce9a238ada28d61d694aed4c4b017c78d5" + }, + { + "path": "research/scalable-dirty-connectors/connector.py", + "git_blob": "a927f6978d48d44ce1d3f4b59fadf81a5d6c1058", + "sha256": "217f28ae78e42a523100014da9ba3c84bddabe5cf7180b4026e9702ef367c955" + } + ] + }, + "related_work": [ + { + "pr": 2063, + "head": "4caa7660fa4a31c4cfeaf177fabc3b56549dd065", + "scope": "Five-source one-root tariff optimum; not claimed here." + }, + { + "pr": 2229, + "head": "b4eab83755969d406edba9f25b7890e4db4c4931", + "scope": "One-root seven-source sparse masks at 14 source calls." + }, + { + "pr": 2236, + "head": "be03870d764e7875ea9a9f6cc69933c9b1a2456a", + "scope": "One-root seven-source sparse masks at 16 source calls." + }, + { + "pr": 2208, + "head": "28480ef4fdb4caeab89765ea56595bf1f6f37688", + "scope": "All-word tariffs allowing more than two calls per map." + } + ] +} diff --git a/research/seven-source-root-minimum/TASK.json b/research/seven-source-root-minimum/TASK.json new file mode 100644 index 0000000000..07bcc5cfb2 --- /dev/null +++ b/research/seven-source-root-minimum/TASK.json @@ -0,0 +1,135 @@ +{ + "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": "Prove the exact minimum of four arbitrary-dirty F2 root rows for all seven-source masks at exactly two calls per source/output map, allowing arbitrary invertible scalar root frames and per-occurrence ports.", + "scope_change_reason": "The selected card asks for an added operation and favorable completed budget. This instead settles the explicit seven-source root-minimum question in PR2182; it is an interface-capacity side result with a fully priced inherited upper bound.", + "bottleneck_link": "Minimum-call sharing cannot reduce the seven-source star from four roots to three in this contract. This constrains the stock/cost tradeoff; no actual recursive caller, physical savings, supplier admission or kappa improvement is established.", + "budget_minutes": 60, + "stop_rule": "Stop after the complete seven-source paired-word/class census and independent replay; do not expand to eight sources or optimize transfers. Reserve the final quarter for verification, overlap refresh and handoff.", + "outcome": "completed", + "evidence": "CENSUS.json: 135135 words times 651 partitions, 87972885 cases, every case misses mandatory masks. Separate C++ and Python implementations agree. WITNESS.json: credited PR2182 star, 4 roots / 14 B / 254 A / 56 XORs; 4362 dense basis columns, 329 rejection controls, 245 affine checks.", + "author": "Mason Hale", + "ai_assistance": "Substantial OpenAI Codex assistance in scoping, proof derivation, implementation, experiments, self-review and writing. No independent human review or proof-assistant formalization.", + "open_questions": [ + { + "question": "Can four roots attain all eight-source masks at exactly two calls per map?", + "why_it_matters": "Locates the next stock boundary beyond the now-sharp seven-source result.", + "first_step": "Use the normalized F2^4 affine-plane model and the known five-root star; derive a complete reduction before enumerating.", + "blocked_by": "No attaining four-root program or sufficiently reduced exclusion domain." + }, + { + "question": "What is the minimum paid transfer cost at seven sources with four roots?", + "why_it_matters": "The 56-transfer upper bound may overstate the price of incidence-minimal sharing.", + "first_step": "Optimize a fixed source/readout witness with exact dirty-frame states and charge every physical XOR.", + "blocked_by": "No global finite transfer-length bound or concrete port tariffs." + }, + { + "question": "Does a concrete recursive caller profit from this interface?", + "why_it_matters": "Root capacity alone does not establish a physical or exponent gain.", + "first_step": "Instantiate all complete child/transfer prices and H_4 in the displayed invoice against a one-root baseline.", + "blocked_by": "Caller, stock, tape, preparation and precision contracts are not supplied." + } + ], + "assignment_seed": 54, + "assignment_seed_source": "secrets.randbelow(100), operating-system randomness, 2026-10-15", + "track": "recursive-interfaces", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2275", + "candidates": [ + { + "scope": "Five-source positive complete-map tariffs", + "decision": "Rejected: exact overlap with PR2063." + }, + { + "scope": "Heterogeneous paired-output dispatch events", + "decision": "Rejected: covered by PR2230." + }, + { + "scope": "Seven-source minimum dirty-root count at paired map incidence", + "decision": "Chosen: explicit open next question in PR2182, differing from one-root sparse-mask PR2229/2236." + } + ], + "overlap": { + "searched_at": "2026-10-15T03:20:18.421506+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T03:18:29.557953+00:00", + "complete_pagination": true, + "records": 502 + }, + "discussions": { + "fetched_at": "2026-10-15T03:20:18.334076+00:00", + "complete_pagination": true, + "records": 989 + } + }, + "local_records": 1538, + "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.", + "conclusion": "No matching three-root/seven-source universal paired-call result found. Own Discussion2275 is excluded. PR2182 leaves this question open; PR2229/2236 are one-root sparse-mask results; PR2241 uses clean output anchors and is distinct." + }, + "upstream_checkpoint": { + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "selected_kappa": "836330098538459/500000000000000000", + "checked_at_utc": "2026-10-15T03:18:29Z" + }, + "validation": { + "python": "3.12.14", + "platform": "macOS-26.5.1-arm64-arm-64bit", + "native_compiler": "Apple clang version 21.0.0 (clang-2100.1.1.101)", + "results": [ + "Fresh complete C++ and Python census histograms agree.", + "Optimized registered package replay and source-pin validation pass.", + "Four-root witness exactly equals pinned PR2182 star(7).", + "All 4362 dense columns, 329 mutations and 245 affine cases pass.", + "Read-only no-Git export passes. Corrupted CENSUS.json rejects.", + "Original universal-connector predecessor check passes." + ], + "not_run": [ + "Hosted CI (not yet published)", + "Selected global cold replay", + "Proof-assistant formalization", + "Independent human review", + "Physical caller/stock/tape/precision admission" + ] + } +} diff --git a/research/seven-source-root-minimum/VERIFY.json b/research/seven-source-root-minimum/VERIFY.json new file mode 100644 index 0000000000..f5fe0da7ad --- /dev/null +++ b/research/seven-source-root-minimum/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Fresh complete 87972885-case census, mandatory-mask/affine lemmas, literal four-root attainment, all 4362 dense basis columns, 329 semantic failure controls and six-source/neutral/odd-incidence positive controls. No cached native result is trusted." + } + ] +} diff --git a/research/seven-source-root-minimum/WITNESS.json b/research/seven-source-root-minimum/WITNESS.json new file mode 100644 index 0000000000..bfd5fe0b37 --- /dev/null +++ b/research/seven-source-root-minimum/WITNESS.json @@ -0,0 +1,1626 @@ +{ + "sources": 7, + "roots": 4, + "operations": [ + [ + "A", + 4, + 0 + ], + [ + "A", + 8, + 0 + ], + [ + "A", + 12, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 16, + 0 + ], + [ + "A", + 20, + 0 + ], + [ + "A", + 24, + 0 + ], + [ + "A", + 28, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 48, + 0 + ], + [ + "A", + 52, + 0 + ], + [ + "A", + 56, + 0 + ], + [ + "A", + 60, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 32, + 0 + ], + [ + "A", + 36, + 0 + ], + [ + "A", + 40, + 0 + ], + [ + "A", + 44, + 0 + ], + [ + "X", + 0, + 3 + ], + [ + "A", + 96, + 0 + ], + [ + "A", + 100, + 0 + ], + [ + "A", + 104, + 0 + ], + [ + "A", + 108, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 112, + 0 + ], + [ + "A", + 116, + 0 + ], + [ + "A", + 120, + 0 + ], + [ + "A", + 124, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 80, + 0 + ], + [ + "A", + 84, + 0 + ], + [ + "A", + 88, + 0 + ], + [ + "A", + 92, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 64, + 0 + ], + [ + "A", + 68, + 0 + ], + [ + "A", + 72, + 0 + ], + [ + "A", + 76, + 0 + ], + [ + "B", + 0, + 0 + ], + [ + "A", + 65, + 0 + ], + [ + "A", + 69, + 0 + ], + [ + "A", + 73, + 0 + ], + [ + "A", + 77, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 81, + 0 + ], + [ + "A", + 85, + 0 + ], + [ + "A", + 89, + 0 + ], + [ + "A", + 93, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 113, + 0 + ], + [ + "A", + 117, + 0 + ], + [ + "A", + 121, + 0 + ], + [ + "A", + 125, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 97, + 0 + ], + [ + "A", + 101, + 0 + ], + [ + "A", + 105, + 0 + ], + [ + "A", + 109, + 0 + ], + [ + "X", + 0, + 3 + ], + [ + "A", + 33, + 0 + ], + [ + "A", + 37, + 0 + ], + [ + "A", + 41, + 0 + ], + [ + "A", + 45, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 49, + 0 + ], + [ + "A", + 53, + 0 + ], + [ + "A", + 57, + 0 + ], + [ + "A", + 61, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 17, + 0 + ], + [ + "A", + 21, + 0 + ], + [ + "A", + 25, + 0 + ], + [ + "A", + 29, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 1, + 0 + ], + [ + "A", + 5, + 0 + ], + [ + "A", + 9, + 0 + ], + [ + "A", + 13, + 0 + ], + [ + "B", + 1, + 0 + ], + [ + "A", + 3, + 0 + ], + [ + "A", + 7, + 0 + ], + [ + "A", + 11, + 0 + ], + [ + "A", + 15, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 19, + 0 + ], + [ + "A", + 23, + 0 + ], + [ + "A", + 27, + 0 + ], + [ + "A", + 31, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 51, + 0 + ], + [ + "A", + 55, + 0 + ], + [ + "A", + 59, + 0 + ], + [ + "A", + 63, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 35, + 0 + ], + [ + "A", + 39, + 0 + ], + [ + "A", + 43, + 0 + ], + [ + "A", + 47, + 0 + ], + [ + "X", + 0, + 3 + ], + [ + "A", + 99, + 0 + ], + [ + "A", + 103, + 0 + ], + [ + "A", + 107, + 0 + ], + [ + "A", + 111, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 115, + 0 + ], + [ + "A", + 119, + 0 + ], + [ + "A", + 123, + 0 + ], + [ + "A", + 127, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 83, + 0 + ], + [ + "A", + 87, + 0 + ], + [ + "A", + 91, + 0 + ], + [ + "A", + 95, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 67, + 0 + ], + [ + "A", + 71, + 0 + ], + [ + "A", + 75, + 0 + ], + [ + "A", + 79, + 0 + ], + [ + "B", + 0, + 0 + ], + [ + "A", + 66, + 0 + ], + [ + "A", + 70, + 0 + ], + [ + "A", + 74, + 0 + ], + [ + "A", + 78, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 82, + 0 + ], + [ + "A", + 86, + 0 + ], + [ + "A", + 90, + 0 + ], + [ + "A", + 94, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 114, + 0 + ], + [ + "A", + 118, + 0 + ], + [ + "A", + 122, + 0 + ], + [ + "A", + 126, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 98, + 0 + ], + [ + "A", + 102, + 0 + ], + [ + "A", + 106, + 0 + ], + [ + "A", + 110, + 0 + ], + [ + "X", + 0, + 3 + ], + [ + "A", + 34, + 0 + ], + [ + "A", + 38, + 0 + ], + [ + "A", + 42, + 0 + ], + [ + "A", + 46, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 50, + 0 + ], + [ + "A", + 54, + 0 + ], + [ + "A", + 58, + 0 + ], + [ + "A", + 62, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 18, + 0 + ], + [ + "A", + 22, + 0 + ], + [ + "A", + 26, + 0 + ], + [ + "A", + 30, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 2, + 0 + ], + [ + "A", + 6, + 0 + ], + [ + "A", + 10, + 0 + ], + [ + "A", + 14, + 0 + ], + [ + "B", + 1, + 0 + ], + [ + "B", + 4, + 1 + ], + [ + "B", + 5, + 2 + ], + [ + "B", + 6, + 3 + ], + [ + "A", + 1, + 0 + ], + [ + "A", + 2, + 0 + ], + [ + "A", + 3, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 16, + 0 + ], + [ + "A", + 17, + 0 + ], + [ + "A", + 18, + 0 + ], + [ + "A", + 19, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 48, + 0 + ], + [ + "A", + 49, + 0 + ], + [ + "A", + 50, + 0 + ], + [ + "A", + 51, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 32, + 0 + ], + [ + "A", + 33, + 0 + ], + [ + "A", + 34, + 0 + ], + [ + "A", + 35, + 0 + ], + [ + "X", + 0, + 3 + ], + [ + "A", + 96, + 0 + ], + [ + "A", + 97, + 0 + ], + [ + "A", + 98, + 0 + ], + [ + "A", + 99, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 112, + 0 + ], + [ + "A", + 113, + 0 + ], + [ + "A", + 114, + 0 + ], + [ + "A", + 115, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 80, + 0 + ], + [ + "A", + 81, + 0 + ], + [ + "A", + 82, + 0 + ], + [ + "A", + 83, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 64, + 0 + ], + [ + "A", + 65, + 0 + ], + [ + "A", + 66, + 0 + ], + [ + "A", + 67, + 0 + ], + [ + "B", + 2, + 0 + ], + [ + "A", + 68, + 0 + ], + [ + "A", + 69, + 0 + ], + [ + "A", + 70, + 0 + ], + [ + "A", + 71, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 84, + 0 + ], + [ + "A", + 85, + 0 + ], + [ + "A", + 86, + 0 + ], + [ + "A", + 87, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 116, + 0 + ], + [ + "A", + 117, + 0 + ], + [ + "A", + 118, + 0 + ], + [ + "A", + 119, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 100, + 0 + ], + [ + "A", + 101, + 0 + ], + [ + "A", + 102, + 0 + ], + [ + "A", + 103, + 0 + ], + [ + "X", + 0, + 3 + ], + [ + "A", + 36, + 0 + ], + [ + "A", + 37, + 0 + ], + [ + "A", + 38, + 0 + ], + [ + "A", + 39, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 52, + 0 + ], + [ + "A", + 53, + 0 + ], + [ + "A", + 54, + 0 + ], + [ + "A", + 55, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 20, + 0 + ], + [ + "A", + 21, + 0 + ], + [ + "A", + 22, + 0 + ], + [ + "A", + 23, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 4, + 0 + ], + [ + "A", + 5, + 0 + ], + [ + "A", + 6, + 0 + ], + [ + "A", + 7, + 0 + ], + [ + "B", + 3, + 0 + ], + [ + "A", + 12, + 0 + ], + [ + "A", + 13, + 0 + ], + [ + "A", + 14, + 0 + ], + [ + "A", + 15, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 28, + 0 + ], + [ + "A", + 29, + 0 + ], + [ + "A", + 30, + 0 + ], + [ + "A", + 31, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 60, + 0 + ], + [ + "A", + 61, + 0 + ], + [ + "A", + 62, + 0 + ], + [ + "A", + 63, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 44, + 0 + ], + [ + "A", + 45, + 0 + ], + [ + "A", + 46, + 0 + ], + [ + "A", + 47, + 0 + ], + [ + "X", + 0, + 3 + ], + [ + "A", + 108, + 0 + ], + [ + "A", + 109, + 0 + ], + [ + "A", + 110, + 0 + ], + [ + "A", + 111, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 124, + 0 + ], + [ + "A", + 125, + 0 + ], + [ + "A", + 126, + 0 + ], + [ + "A", + 127, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 92, + 0 + ], + [ + "A", + 93, + 0 + ], + [ + "A", + 94, + 0 + ], + [ + "A", + 95, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 76, + 0 + ], + [ + "A", + 77, + 0 + ], + [ + "A", + 78, + 0 + ], + [ + "A", + 79, + 0 + ], + [ + "B", + 2, + 0 + ], + [ + "A", + 72, + 0 + ], + [ + "A", + 73, + 0 + ], + [ + "A", + 74, + 0 + ], + [ + "A", + 75, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 88, + 0 + ], + [ + "A", + 89, + 0 + ], + [ + "A", + 90, + 0 + ], + [ + "A", + 91, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 120, + 0 + ], + [ + "A", + 121, + 0 + ], + [ + "A", + 122, + 0 + ], + [ + "A", + 123, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 104, + 0 + ], + [ + "A", + 105, + 0 + ], + [ + "A", + 106, + 0 + ], + [ + "A", + 107, + 0 + ], + [ + "X", + 0, + 3 + ], + [ + "A", + 40, + 0 + ], + [ + "A", + 41, + 0 + ], + [ + "A", + 42, + 0 + ], + [ + "A", + 43, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 56, + 0 + ], + [ + "A", + 57, + 0 + ], + [ + "A", + 58, + 0 + ], + [ + "A", + 59, + 0 + ], + [ + "X", + 0, + 2 + ], + [ + "A", + 24, + 0 + ], + [ + "A", + 25, + 0 + ], + [ + "A", + 26, + 0 + ], + [ + "A", + 27, + 0 + ], + [ + "X", + 0, + 1 + ], + [ + "A", + 8, + 0 + ], + [ + "A", + 9, + 0 + ], + [ + "A", + 10, + 0 + ], + [ + "A", + 11, + 0 + ], + [ + "B", + 3, + 0 + ], + [ + "B", + 4, + 1 + ], + [ + "B", + 5, + 2 + ], + [ + "B", + 6, + 3 + ] + ] +} diff --git a/research/seven-source-root-minimum/census.cpp b/research/seven-source-root-minimum/census.cpp new file mode 100644 index 0000000000..6739d8e22d --- /dev/null +++ b/research/seven-source-root-minimum/census.cpp @@ -0,0 +1,110 @@ +// Exact matching/colour census, independent of census.py's word and set generators. +// Mason Hale, with OpenAI Codex assistance. Apache-2.0. +#include +#include +#include +#include +#include +#include +#include + +using Bits = __uint128_t; // GCC and Clang; all shifts are in [0,127]. +int popcount(Bits x) { + return __builtin_popcountll(static_cast(x)) + + __builtin_popcountll(static_cast(x >> 64)); +} +struct Group { + uint64_t partitions = 0; + std::map histogram; +}; +struct Partition { Bits required; std::string key; }; +std::vector partitions; +std::map groups; +std::array colour; +std::array word; +std::map differences; +uint64_t words = 0; + +void colours(int t, int used) { + if (t == 7) { + if (used < 3) return; + std::vector sizes(used, 0); + for (int c : colour) ++sizes[c]; + std::sort(sizes.rbegin(), sizes.rend()); + std::string key; + for (int s : sizes) key += (key.empty() ? "" : "+") + std::to_string(s); + Bits required = 0; + for (int mask = 1; mask < 128; ++mask) { + unsigned hit = 0; + for (int j = 0; j < 7; ++j) + if ((mask >> j) & 1) hit |= 1u << colour[j]; + if (__builtin_popcount(hit) >= 3) required |= Bits(1) << mask; + } + partitions.push_back({required, key}); + ++groups[key].partitions; + return; + } + for (int c = 0; c <= used && c < 4; ++c) { + colour[t] = c; + colours(t + 1, used + (c == used)); + } +} + +void inspect() { + ++words; + std::array prefixes{}; + for (int i = 0; i < 14; ++i) prefixes[i + 1] = prefixes[i] ^ (1 << word[i]); + Bits covered = 1; + for (int i = 0; i < 15; ++i) + for (int j = 0; j < i; ++j) covered |= Bits(1) << (prefixes[i] ^ prefixes[j]); + ++differences[popcount(covered)]; + for (const auto &p : partitions) + ++groups[p.key].histogram[popcount(p.required & ~covered)]; +} + +void match(int label) { + int first = 0; + while (first < 14 && word[first] >= 0) ++first; + if (first == 14) { inspect(); return; } + word[first] = label; + for (int second = first + 1; second < 14; ++second) { + if (word[second] >= 0) continue; + word[second] = label; + match(label + 1); + word[second] = -1; + } + word[first] = -1; +} + +void print_histogram(const std::map &h) { + std::cout << "{"; + bool first = true; + for (auto [key, count] : h) { + if (!first) std::cout << ","; + first = false; + std::cout << '"' << key << "\":" << count; + } + std::cout << "}"; +} + +int main() { + colours(0, 0); + word.fill(-1); + match(0); + std::cout << "{\"sources\":7,\"words\":" << words + << ",\"partitions\":" << partitions.size() + << ",\"cases\":" << words * partitions.size() + << ",\"difference_histogram\":"; + print_histogram(differences); + std::cout << ",\"groups\":{"; + bool first = true; + for (auto &[key, group] : groups) { + if (!first) std::cout << ","; + first = false; + std::cout << '"' << key << "\":{\"partitions\":" << group.partitions + << ",\"missing_histogram\":"; + print_histogram(group.histogram); + std::cout << "}"; + } + std::cout << "}}\n"; +} diff --git a/research/seven-source-root-minimum/census.py b/research/seven-source-root-minimum/census.py new file mode 100644 index 0000000000..ae80f172cb --- /dev/null +++ b/research/seven-source-root-minimum/census.py @@ -0,0 +1,110 @@ +"""Independent exact Python census. Mason Hale, with OpenAI Codex assistance. + +Apache-2.0. No predecessor implementation is imported. The reduction from +arbitrary frame schedules to this finite domain is proved in README.md. +""" +from collections import Counter +from itertools import product +import json + + +def source_words(n): + """Restricted-growth words: each introduced label occurs exactly twice.""" + word, counts = [], [] + + def visit(): + if len(word) == 2 * n: + yield tuple(word) + return + for label in range(len(counts) + (len(counts) < n)): + fresh = label == len(counts) + if fresh: + counts.append(0) + if counts[label] < 2: + counts[label] += 1 + word.append(label) + yield from visit() + word.pop() + counts[label] -= 1 + if fresh: + counts.pop() + + yield from visit() + + +def partitions(n): + """Set partitions into three or four nonempty blocks, as source bitmasks.""" + def insert(j, blocks): + if j == n: + if 3 <= len(blocks) <= 4: + yield tuple(blocks) + return + for i in range(len(blocks)): + extended = list(blocks) + extended[i] |= 1 << j + yield from insert(j + 1, extended) + if len(blocks) < 4: + yield from insert(j + 1, [*blocks, 1 << j]) + + yield from insert(0, []) + + +def mandatory(blocks): + """All masks meeting >=3 classes, by a product of within-class subsets.""" + choices = [] + for block in blocks: + subsets, sub = [0], block + while sub: + subsets.append(sub) + sub = (sub - 1) & block + choices.append(subsets) + result = 0 + for selection in product(*choices): + if sum(bool(x) for x in selection) >= 3: + result |= 1 << sum(selection) # blocks are disjoint + return result + + +def interval_differences(word): + """Parity of each contiguous substring; no prefix-difference generator.""" + result = 1 + for start in range(len(word)): + parity = 0 + for label in word[start:]: + parity ^= 1 << label + result |= 1 << parity + return result + + +def census(n=7): + prepared, groups = [], {} + for blocks in partitions(n): + key = "+".join(map(str, sorted((x.bit_count() for x in blocks), reverse=True))) + if key not in groups: + groups[key] = {"partitions": 0, "missing_histogram": Counter()} + groups[key]["partitions"] += 1 + prepared.append((mandatory(blocks), groups[key]["missing_histogram"])) + words = 0 + differences = Counter() + for word in source_words(n): + words += 1 + have = interval_differences(word) + differences[have.bit_count()] += 1 + for required, histogram in prepared: + histogram[(required & ~have).bit_count()] += 1 + return { + "sources": n, + "words": words, + "partitions": len(prepared), + "cases": words * len(prepared), + "difference_histogram": dict(sorted(differences.items())), + "groups": { + key: {"partitions": entry["partitions"], + "missing_histogram": dict(sorted(entry["missing_histogram"].items()))} + for key, entry in sorted(groups.items()) + }, + } + + +if __name__ == "__main__": + print(json.dumps(census(), indent=2, sort_keys=True)) diff --git a/research/seven-source-root-minimum/program.py b/research/seven-source-root-minimum/program.py new file mode 100644 index 0000000000..8fdcec5dae --- /dev/null +++ b/research/seven-source-root-minimum/program.py @@ -0,0 +1,30 @@ +"""Emit the credited PR2182 star upper bound; this is not a new construction. + +Mason Hale, with OpenAI Codex assistance. Apache-2.0. +""" + + +def star(n): + if not isinstance(n, int) or n < 4: + raise ValueError("need n >= 4") + roots = n - 3 + gray = [i ^ (i >> 1) for i in range(1 << (n - 4))] + operations, frame = [], 0 + for phase in range(2): + if phase: + operations += [["B", j, j - 3] for j in range(4, n)] + for t, point in enumerate((0, 1, 3, 2)): + itinerary = gray if t % 2 == 0 else gray[::-1] + for destination in itinerary: + for bit in range(n - 4): + if (frame ^ destination) >> bit & 1: + operations.append(["X", 0, bit + 1]) + frame ^= 1 << bit + for other in range(4): + low = (point | other << 2) if phase == 0 else (other | point << 2) + mask = low | destination << 4 + if mask: + operations.append(["A", mask, 0]) + operations.append(["B", 2 * phase + (t % 2), 0]) + operations += [["B", j, j - 3] for j in range(4, n)] + return {"sources": n, "roots": roots, "operations": operations} diff --git a/research/seven-source-root-minimum/verify.py b/research/seven-source-root-minimum/verify.py new file mode 100644 index 0000000000..14bd3fd89d --- /dev/null +++ b/research/seven-source-root-minimum/verify.py @@ -0,0 +1,196 @@ +"""Full finite replay and semantic controls, active under python -O. + +The census supports the written reduction, not a proof-assistant claim. +Mason Hale, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from itertools import combinations +import argparse +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from census import census, interval_differences, mandatory, partitions +from program import star + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def formal(program): + """Opaque h_j=B_j(x_j) and initial dirty-root symbols; separate A rows.""" + n, k = program["sources"], program["roots"] + roots = [1 << i for i in range(k)] + outputs = [0] * (1 << n) + for kind, label, port in program["operations"]: + require(type(port) is int and 0 <= port < k, "bad port") + if kind == "X": + require(type(label) is int and 0 <= label < k and label != port, "bad shear") + roots[label] ^= roots[port] + elif kind == "B": + require(type(label) is int and 0 <= label < n, "bad source") + roots[port] ^= 1 << (k + label) + elif kind == "A": + require(type(label) is int and 0 < label < 1 << n, "bad target") + outputs[label] ^= roots[port] + else: + raise ValueError("unknown operation") + require(roots == [1 << i for i in range(k)], "dirty roots do not restore") + require(outputs == [m << k for m in range(1 << n)], "wrong output or uncancelled dirt") + + +def apply_matrix(matrix, vector): + answer = [] + for mask in matrix: + value = 0 + for i, x in enumerate(vector): + if mask >> i & 1: + value ^= x + answer.append(value) + return answer + + +def dense(program, widths, seed, reverse=False): + """All input columns at once, concrete rectangular/singular binary maps.""" + n, k = program["sources"], program["roots"] + sx, sz, sy = widths + rng = random.Random(seed) + b = [[rng.randrange(1 << sx) for _ in range(sz)] for _ in range(n)] + a = [[rng.randrange(1 << sz) for _ in range(sy)] for _ in range((1 << n) - 1)] + b[0] = [0] * sz + a[0] = [0] * sy + offset = 0 + + def row(size): + nonlocal offset + result = [1 << i for i in range(offset, offset + size)] + offset += size + return result + + x = [row(sx) for _ in range(n)] + z = [row(sz) for _ in range(k)] + y = [row(sy) for _ in range((1 << n) - 1)] + before_z, before_y = [r[:] for r in z], [r[:] for r in y] + ops = program["operations"][::-1] if reverse else program["operations"] + for kind, label, port in ops: + if kind == "X": + z[label] = [u ^ v for u, v in zip(z[label], z[port])] + elif kind == "B": + z[port] = [u ^ v for u, v in zip(z[port], apply_matrix(b[label], x[label]))] + else: + y[label - 1] = [u ^ v for u, v in zip(y[label - 1], apply_matrix(a[label - 1], z[port]))] + expected = [] + for mask in range(1, 1 << n): + total = [0] * sz + for j in range(n): + if mask >> j & 1: + total = [u ^ v for u, v in zip(total, apply_matrix(b[j], x[j]))] + expected.append([u ^ v for u, v in zip(before_y[mask - 1], apply_matrix(a[mask - 1], total))]) + require(z == before_z and y == expected, "dense dirty-basis replay failed") + return offset + + +def controls(program): + rejected = 0 + + def reject(operations): + nonlocal rejected + try: + formal({**program, "operations": operations}) + except ValueError: + rejected += 1 + else: + raise ValueError("mutation escaped") + + ops = program["operations"] + for i in range(len(ops)): + reject(ops[:i] + ops[i + 1:]) + for kind in ("A", "B", "X"): + i = next(j for j, op in enumerate(ops) if op[0] == kind) + bad = [x[:] for x in ops] + if kind == "X": + bad[i][1], bad[i][2] = bad[i][2], bad[i][1] + else: + bad[i][2] = (bad[i][2] + 1) % program["roots"] + reject(bad) + i = next(i for i, op in enumerate(ops) if op[0] == "A") + bad = [x[:] for x in ops] + bad[i][1] = 2 if bad[i][1] == 1 else 1 + reject(bad) + reject([["X", 0, 0], *ops]) + formal({**program, "operations": [["X", 0, 1], ["X", 0, 1], *ops]}) + # Three B calls can restore in a multi-root excursion. The theorem must + # not import the one-root even-incidence rule. + z = [1, 2] + for kind, p in (("B", 0), ("B", 1), ("X", 0), ("B", 1), ("X", 0)): + z[p] ^= 4 if kind == "B" else z[1] + require(z == [1, 2], "odd-incidence positive control failed") + return rejected + + +def geometric_controls(): + checked = 0 + for full in range(1, 8): + plane = [v for v in range(1, 8) if (v & full).bit_count() % 2] + require(len(plane) == 4, "wrong affine plane") + for size in (3, 4): + for axes in combinations(plane, size): + for r in range(1, 8): + response = [(r & v).bit_count() % 2 for v in axes] + require(sum(response) < 3 or all(response), "rainbow lemma false") + checked += 1 + for blocks in partitions(7): + expected = sum(1 << m for m in range(128) if sum(bool(m & b) for b in blocks) >= 3) + require(mandatory(blocks) == expected, "mandatory mask engine mismatch") + # This necessary condition must admit the known six-source/three-root case. + word = (0, 1, 0, 1, 4, 5, 2, 3, 2, 3, 4, 5) + blocks = (15, 16, 32) + require(mandatory(blocks) & ~interval_differences(word) == 0, "six-source control excluded") + return checked + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--native-result", type=Path) + args = ap.parse_args() + result = census() + require(result["words"] == 135135 and result["partitions"] == 651, + "enumeration cardinality mismatch") + require(result["cases"] == 87972885, "case count mismatch") + for entry in result["groups"].values(): + require(0 not in entry["missing_histogram"], "three-root candidate survives") + require(sum(entry["missing_histogram"].values()) == 135135 * entry["partitions"], + "incomplete group coverage") + canonical = json.loads(json.dumps(result)) + require(canonical == json.loads((HERE / "CENSUS.json").read_text()), "census receipt mismatch") + if args.native_result: + require(canonical == json.loads(args.native_result.read_text()), "C++/Python census disagreement") + program = json.loads((HERE / "WITNESS.json").read_text()) + require(program == star(7), "literal witness differs from credited star construction") + formal(program) + formal({**program, "operations": program["operations"][::-1]}) + formal(star(6)) + counts = Counter(op[0] for op in program["operations"]) + require(counts == {"B": 14, "A": 254, "X": 56}, "invoice mismatch") + require(Counter(op[1] for op in program["operations"] if op[0] == "B") == dict.fromkeys(range(7), 2), + "source multiplicity mismatch") + require(Counter(op[1] for op in program["operations"] if op[0] == "A") == dict.fromkeys(range(1, 128), 2), + "output multiplicity mismatch") + require(Counter(op[2] for op in program["operations"] if op[0] == "X") == {1: 32, 2: 16, 3: 8}, + "directional transfer invoice mismatch") + columns = sum(dense(program, shape, seed, reverse) + for shape in ((2, 3, 2), (3, 2, 1), (3, 4, 2)) + for seed in (54, 55, 56) for reverse in (False, True)) + rejected = controls(program) + geometry = geometric_controls() + print(f"PASS_SEVEN_SOURCE_ROOT_MINIMUM words=135135 partitions=651 cases=87972885 " + f"roots=4 B=14 A=254 X=56 dense_columns={columns} mutations={rejected} affine_checks={geometry}") + + +if __name__ == "__main__": + main()