diff --git a/research/connector-char4-floor-obstructions/CERTIFICATE.json b/research/connector-char4-floor-obstructions/CERTIFICATE.json new file mode 100644 index 0000000000..81252921ab --- /dev/null +++ b/research/connector-char4-floor-obstructions/CERTIFICATE.json @@ -0,0 +1,906 @@ +{ + "claim": "9<=N(4)<=17", + "cube_control_max_mask_upper": 512526, + "cube_control_rows": [ + { + "cube_intersection": 23, + "mask_upper": 407076, + "r": 0 + }, + { + "cube_intersection": 24, + "mask_upper": 424651, + "r": 1 + }, + { + "cube_intersection": 24, + "mask_upper": 424651, + "r": 2 + }, + { + "cube_intersection": 25, + "mask_upper": 442226, + "r": 3 + }, + { + "cube_intersection": 25, + "mask_upper": 442226, + "r": 4 + }, + { + "cube_intersection": 26, + "mask_upper": 459801, + "r": 5 + }, + { + "cube_intersection": 26, + "mask_upper": 459801, + "r": 6 + }, + { + "cube_intersection": 26, + "mask_upper": 459801, + "r": 7 + }, + { + "cube_intersection": 26, + "mask_upper": 459801, + "r": 8 + }, + { + "cube_intersection": 27, + "mask_upper": 477376, + "r": 9 + }, + { + "cube_intersection": 27, + "mask_upper": 477376, + "r": 10 + }, + { + "cube_intersection": 28, + "mask_upper": 494951, + "r": 11 + }, + { + "cube_intersection": 28, + "mask_upper": 494951, + "r": 12 + }, + { + "cube_intersection": 29, + "mask_upper": 512526, + "r": 13 + }, + { + "cube_intersection": 29, + "mask_upper": 512526, + "r": 14 + }, + { + "cube_intersection": 29, + "mask_upper": 512526, + "r": 15 + }, + { + "cube_intersection": 29, + "mask_upper": 489406, + "r": 16 + }, + { + "cube_intersection": 30, + "mask_upper": 456838, + "r": 17 + }, + { + "cube_intersection": 30, + "mask_upper": 425924, + "r": 18 + }, + { + "cube_intersection": 31, + "mask_upper": 396607, + "r": 19 + }, + { + "cube_intersection": 31, + "mask_upper": 368831, + "r": 20 + }, + { + "cube_intersection": 32, + "mask_upper": 342541, + "r": 21 + }, + { + "cube_intersection": 32, + "mask_upper": 317683, + "r": 22 + }, + { + "cube_intersection": 32, + "mask_upper": 294204, + "r": 23 + }, + { + "cube_intersection": 32, + "mask_upper": 272052, + "r": 24 + }, + { + "cube_intersection": 33, + "mask_upper": 251176, + "r": 25 + }, + { + "cube_intersection": 33, + "mask_upper": 231526, + "r": 26 + }, + { + "cube_intersection": 34, + "mask_upper": 213053, + "r": 27 + }, + { + "cube_intersection": 34, + "mask_upper": 195709, + "r": 28 + }, + { + "cube_intersection": 35, + "mask_upper": 179447, + "r": 29 + }, + { + "cube_intersection": 35, + "mask_upper": 164221, + "r": 30 + }, + { + "cube_intersection": 35, + "mask_upper": 149986, + "r": 31 + }, + { + "cube_intersection": 35, + "mask_upper": 136698, + "r": 32 + }, + { + "cube_intersection": 36, + "mask_upper": 124314, + "r": 33 + }, + { + "cube_intersection": 36, + "mask_upper": 112792, + "r": 34 + }, + { + "cube_intersection": 37, + "mask_upper": 102091, + "r": 35 + }, + { + "cube_intersection": 37, + "mask_upper": 92171, + "r": 36 + }, + { + "cube_intersection": 38, + "mask_upper": 82993, + "r": 37 + }, + { + "cube_intersection": 38, + "mask_upper": 74519, + "r": 38 + }, + { + "cube_intersection": 38, + "mask_upper": 66712, + "r": 39 + }, + { + "cube_intersection": 38, + "mask_upper": 59536, + "r": 40 + }, + { + "cube_intersection": 38, + "mask_upper": 52956, + "r": 41 + }, + { + "cube_intersection": 38, + "mask_upper": 46938, + "r": 42 + }, + { + "cube_intersection": 38, + "mask_upper": 41449, + "r": 43 + }, + { + "cube_intersection": 38, + "mask_upper": 36457, + "r": 44 + }, + { + "cube_intersection": 38, + "mask_upper": 31931, + "r": 45 + }, + { + "cube_intersection": 38, + "mask_upper": 27841, + "r": 46 + }, + { + "cube_intersection": 38, + "mask_upper": 24158, + "r": 47 + }, + { + "cube_intersection": 38, + "mask_upper": 20854, + "r": 48 + }, + { + "cube_intersection": 38, + "mask_upper": 17902, + "r": 49 + }, + { + "cube_intersection": 38, + "mask_upper": 15276, + "r": 50 + }, + { + "cube_intersection": 38, + "mask_upper": 12951, + "r": 51 + }, + { + "cube_intersection": 38, + "mask_upper": 10903, + "r": 52 + }, + { + "cube_intersection": 38, + "mask_upper": 9109, + "r": 53 + }, + { + "cube_intersection": 38, + "mask_upper": 7547, + "r": 54 + }, + { + "cube_intersection": 38, + "mask_upper": 6196, + "r": 55 + }, + { + "cube_intersection": 38, + "mask_upper": 5036, + "r": 56 + }, + { + "cube_intersection": 38, + "mask_upper": 4048, + "r": 57 + }, + { + "cube_intersection": 38, + "mask_upper": 3214, + "r": 58 + }, + { + "cube_intersection": 38, + "mask_upper": 2517, + "r": 59 + }, + { + "cube_intersection": 38, + "mask_upper": 1941, + "r": 60 + }, + { + "cube_intersection": 38, + "mask_upper": 1471, + "r": 61 + }, + { + "cube_intersection": 38, + "mask_upper": 1093, + "r": 62 + }, + { + "cube_intersection": 38, + "mask_upper": 794, + "r": 63 + }, + { + "cube_intersection": 38, + "mask_upper": 562, + "r": 64 + }, + { + "cube_intersection": 38, + "mask_upper": 386, + "r": 65 + }, + { + "cube_intersection": 38, + "mask_upper": 256, + "r": 66 + }, + { + "cube_intersection": 38, + "mask_upper": 163, + "r": 67 + }, + { + "cube_intersection": 38, + "mask_upper": 99, + "r": 68 + }, + { + "cube_intersection": 38, + "mask_upper": 57, + "r": 69 + }, + { + "cube_intersection": 38, + "mask_upper": 31, + "r": 70 + }, + { + "cube_intersection": 38, + "mask_upper": 16, + "r": 71 + }, + { + "cube_intersection": 38, + "mask_upper": 8, + "r": 72 + }, + { + "cube_intersection": 38, + "mask_upper": 4, + "r": 73 + }, + { + "cube_intersection": 38, + "mask_upper": 2, + "r": 74 + }, + { + "cube_intersection": 38, + "mask_upper": 1, + "r": 75 + } + ], + "cube_control_source_count": 19, + "cube_sharpness": { + "cube_intersection": 22, + "k": 18, + "parity_repetitions": 0, + "valid_boundaries": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 30, + 42, + 57 + ] + }, + "depth_two": { + "calibration": [ + { + "canonical_words": 1, + "k": 1, + "solutions": 1 + }, + { + "canonical_words": 35, + "k": 2, + "solutions": 33 + }, + { + "canonical_words": 5775, + "k": 3, + "solutions": 547 + } + ], + "k4": { + "accounted_words": 2627625, + "canonical_words": 2627625, + "covered_threshold": 16, + "k": 4, + "pruned_depth": [ + 0, + 0, + 0, + 0, + 0, + 1, + 13, + 82, + 485, + 2068, + 6333, + 11821, + 23161, + 23782, + 24564, + 1757, + 0 + ], + "pruned_nodes": 94067, + "solutions": 421, + "visited_nodes": 136922 + }, + "k5_at_least_29": { + "accounted_words": 2546168625, + "canonical_words": 2546168625, + "covered_threshold": 29, + "k": 5, + "pruned_depth": [ + 0, + 0, + 0, + 0, + 0, + 1, + 13, + 82, + 517, + 2839, + 14291, + 56986, + 171020, + 396539, + 839804, + 1403538, + 1831982, + 1789540, + 125200, + 264, + 0 + ], + "pruned_nodes": 6632616, + "solutions": 4, + "visited_nodes": 8715495 + }, + "k5_at_least_30": { + "accounted_words": 2546168625, + "canonical_words": 2546168625, + "covered_threshold": 30, + "k": 5, + "pruned_depth": [ + 0, + 0, + 0, + 0, + 0, + 1, + 13, + 82, + 520, + 2852, + 14341, + 56754, + 170191, + 393302, + 846138, + 1356807, + 1778790, + 1760056, + 72092, + 8, + 0 + ], + "pruned_nodes": 6451947, + "solutions": 0, + "visited_nodes": 8462068 + }, + "k5_full": { + "accounted_words": 2546168625, + "canonical_words": 2546168625, + "covered_threshold": 32, + "k": 5, + "pruned_depth": [ + 0, + 0, + 0, + 0, + 0, + 1, + 13, + 82, + 520, + 2855, + 14356, + 56722, + 170248, + 396084, + 838536, + 1319815, + 1763175, + 1733205, + 25083, + 0, + 0 + ], + "pruned_nodes": 6320695, + "solutions": 0, + "visited_nodes": 8277996 + }, + "maximizer_count": 4 + }, + "eighteen_exclusion": { + "arithmetic": { + "base_exceptions": [ + 2, + 4, + 5 + ], + "base_rows": [ + { + "V_upper": 52686, + "X_upper": 46200, + "Z_upper": 43174, + "cube_cap": 22, + "excluded": true, + "incidence_numerator": 1017702, + "mask_upper": 256982, + "r": 0 + }, + { + "V_upper": 52686, + "X_upper": 46340, + "Z_upper": 41849, + "cube_cap": 22, + "excluded": true, + "incidence_numerator": 1011572, + "mask_upper": 255379, + "r": 1 + }, + { + "V_upper": 52686, + "X_upper": 46480, + "Z_upper": 40568, + "cube_cap": 23, + "excluded": false, + "incidence_numerator": 1040362, + "mask_upper": 262506, + "r": 2 + }, + { + "V_upper": 52686, + "X_upper": 46620, + "Z_upper": 39330, + "cube_cap": 23, + "excluded": true, + "incidence_numerator": 1032138, + "mask_upper": 260381, + "r": 3 + }, + { + "V_upper": 52686, + "X_upper": 46760, + "Z_upper": 38089, + "cube_cap": 24, + "excluded": false, + "incidence_numerator": 1053308, + "mask_upper": 265606, + "r": 4 + }, + { + "V_upper": 52686, + "X_upper": 46900, + "Z_upper": 36817, + "cube_cap": 24, + "excluded": false, + "incidence_numerator": 1042128, + "mask_upper": 262744, + "r": 5 + }, + { + "V_upper": 52686, + "X_upper": 47040, + "Z_upper": 35585, + "cube_cap": 24, + "excluded": true, + "incidence_numerator": 1031348, + "mask_upper": 259983, + "r": 6 + }, + { + "V_upper": 52686, + "X_upper": 47180, + "Z_upper": 34392, + "cube_cap": 24, + "excluded": true, + "incidence_numerator": 1020958, + "mask_upper": 257320, + "r": 7 + }, + { + "V_upper": 52686, + "X_upper": 47320, + "Z_upper": 33237, + "cube_cap": 25, + "excluded": true, + "incidence_numerator": 1030102, + "mask_upper": 259542, + "r": 8 + }, + { + "V_upper": 52686, + "X_upper": 47460, + "Z_upper": 32119, + "cube_cap": 25, + "excluded": true, + "incidence_numerator": 1018086, + "mask_upper": 256475, + "r": 9 + }, + { + "V_upper": 52686, + "X_upper": 47600, + "Z_upper": 31037, + "cube_cap": 26, + "excluded": true, + "incidence_numerator": 1020976, + "mask_upper": 257136, + "r": 10 + }, + { + "V_upper": 52686, + "X_upper": 47740, + "Z_upper": 29990, + "cube_cap": 26, + "excluded": true, + "incidence_numerator": 1007578, + "mask_upper": 253725, + "r": 11 + }, + { + "V_upper": 52686, + "X_upper": 47880, + "Z_upper": 28977, + "cube_cap": 27, + "excluded": true, + "incidence_numerator": 1004730, + "mask_upper": 252953, + "r": 12 + }, + { + "V_upper": 52686, + "X_upper": 48020, + "Z_upper": 27997, + "cube_cap": 27, + "excluded": true, + "incidence_numerator": 990170, + "mask_upper": 249254, + "r": 13 + }, + { + "V_upper": 52686, + "X_upper": 48160, + "Z_upper": 27049, + "cube_cap": 27, + "excluded": true, + "incidence_numerator": 976122, + "mask_upper": 245684, + "r": 14 + }, + { + "V_upper": 52686, + "X_upper": 48300, + "Z_upper": 26132, + "cube_cap": 27, + "excluded": true, + "incidence_numerator": 962570, + "mask_upper": 242239, + "r": 15 + }, + { + "V_upper": 52686, + "X_upper": 48440, + "Z_upper": 25245, + "cube_cap": 28, + "excluded": true, + "incidence_numerator": 951548, + "mask_upper": 239428, + "r": 16 + }, + { + "V_upper": 52686, + "X_upper": 48580, + "Z_upper": 24387, + "cube_cap": 28, + "excluded": true, + "incidence_numerator": 937084, + "mask_upper": 235757, + "r": 17 + }, + { + "V_upper": 52686, + "X_upper": 48720, + "Z_upper": 23557, + "cube_cap": 29, + "excluded": true, + "incidence_numerator": 921518, + "mask_upper": 231811, + "r": 18 + }, + { + "V_upper": 52686, + "X_upper": 48860, + "Z_upper": 22754, + "cube_cap": 29, + "excluded": true, + "incidence_numerator": 906298, + "mask_upper": 227953, + "r": 19 + }, + { + "V_upper": 52686, + "X_upper": 49000, + "Z_upper": 21977, + "cube_cap": 30, + "excluded": true, + "incidence_numerator": 886552, + "mask_upper": 222965, + "r": 20 + } + ], + "r_at_least_21_upper": 251176, + "residual_rows": [ + { + "X_edges_lower": 188, + "X_upper": 43216, + "X_vertices": 70, + "attained_H_upper": 252714, + "axis_deletions": 2, + "cube_cap": 23, + "not_attained_H_upper": 255394, + "r": 2 + }, + { + "X_edges_lower": 166, + "X_upper": 40420, + "X_vertices": 68, + "attained_H_upper": 248171, + "axis_deletions": 4, + "cube_cap": 24, + "not_attained_H_upper": 259733, + "r": 4 + }, + { + "X_edges_lower": 164, + "X_upper": 40552, + "X_vertices": 68, + "attained_H_upper": 245287, + "axis_deletions": 4, + "cube_cap": 24, + "not_attained_H_upper": 257507, + "r": 5 + } + ], + "source_count": 18, + "target_masks_including_zero": 262144 + }, + "controls": { + "axis_replacements": { + "axis_pairs": 400, + "good_triple_moves": 953664, + "words": 100 + }, + "short_components": [ + { + "min_local_repeats": 3, + "multiplicities": [ + 3, + 3 + ], + "words": 20 + }, + { + "min_local_repeats": 1, + "multiplicities": [ + 3, + 1 + ], + "words": 4 + } + ] + } + }, + "inventory_normal_form": { + "type_count_vectors_k10": 19448, + "types": [ + [ + 0, + 0, + 1, + 3 + ], + [ + 0, + 1, + 3, + 0 + ], + [ + 0, + 2, + 1, + 1 + ], + [ + 1, + 0, + 2, + 1 + ], + [ + 1, + 1, + 0, + 2 + ], + [ + 1, + 3, + 0, + 0 + ], + [ + 2, + 1, + 1, + 0 + ], + [ + 3, + 0, + 0, + 1 + ] + ], + "weak_compositions": 35 + }, + "random_words": 4000, + "small_translations": 2218720, + "small_words": 34720, + "structural_controls": { + "incidence_axis_words": 60, + "large_translations": 400000, + "large_words": 4000, + "result": "PASS", + "small_translations": 2218720, + "small_words": 34720 + } +} diff --git a/research/connector-char4-floor-obstructions/CUBE-SHARPNESS.json b/research/connector-char4-floor-obstructions/CUBE-SHARPNESS.json new file mode 100644 index 0000000000..6e98ee1a53 --- /dev/null +++ b/research/connector-char4-floor-obstructions/CUBE-SHARPNESS.json @@ -0,0 +1,152 @@ +{ + "bad_arc_groups": [ + [ + 0, + 1, + 2, + 3 + ], + [ + 4, + 5, + 6, + 7 + ], + [ + 8, + 9, + 10, + 11, + 12 + ], + [ + 13, + 14, + 15, + 16, + 17 + ] + ], + "claim": "finite witness H(18,0)=22 is sharp; no floor-attainment claim", + "cube_intersection": 22, + "cube_translate": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "k": 18, + "parity_repetitions": 0, + "valid_boundaries": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 30, + 42, + 57 + ], + "word": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 1, + 2, + 3, + 1, + 3, + 0, + 3, + 2, + 0, + 1, + 0, + 2, + 5, + 6, + 7, + 5, + 7, + 4, + 7, + 6, + 4, + 5, + 4, + 6, + 11, + 9, + 12, + 8, + 12, + 10, + 11, + 9, + 12, + 10, + 8, + 10, + 9, + 8, + 11, + 16, + 14, + 17, + 13, + 17, + 15, + 16, + 14, + 17, + 15, + 13, + 15, + 14, + 13, + 16 + ] +} diff --git a/research/connector-char4-floor-obstructions/DEPTH2.md b/research/connector-char4-floor-obstructions/DEPTH2.md new file mode 100644 index 0000000000..9b9062be3f --- /dev/null +++ b/research/connector-char4-floor-obstructions/DEPTH2.md @@ -0,0 +1,123 @@ +# Characteristic-four blocks of depth two carry at most four sources + +Claim type: a finite exhaustive census supporting a scoped obstruction. This +blocks the direct construction of ten sources from two depth-two five-source +blocks. It does not exclude a ten-source depth-four walk. + +A characteristic-four block is a word in which each of k source labels occurs +exactly four times. Its raw prefix counts are Q_t in {0,1,2,3,4}^k. Depth at most +two means every nonzero binary mask m equals Q_a + Q_b modulo four for some +0 <= a <= b <= 4k. Boundary zero pads a one-read representation; the final +boundary can be identified with zero for evaluating residues. + +## Census and symmetry + +Relabelling sources preserves the property, so enumerate words with source +labels ordered by first occurrence. This is one representative for each source +permutation orbit. The number of canonical words is + + (4k)! / ((4!)^k k!). + +For k=5 this is 2,546,168,625. No rotation or reversal quotient is used. + +A search state is a word prefix of length d, its current raw count vector n, +the set of previous raw prefix vectors p, and the binary masks already served +by a pair of previous boundaries. Each child increments one coordinate n_j<4; +a previously unused label can be introduced only when every lower label has +already been introduced. + +## Safe future-cut relaxation + +For any unserved mask, a future representation has either two boundaries at +or after the current boundary or one previous and one future boundary. + +If both boundaries are future and n_j >= 3, their two raw counts on source j +are each >=3 and <=4. Sums 6,7,8 yield binary residue only at 8, with bit zero. +Consequently all masks represented by two future boundaries belong to the +subcube fixing bit zero on every coordinate with n_j>=3. This is an +*overapproximation*: further restrictions are intentionally ignored. + +For a fixed earlier boundary p, a future boundary has a raw count r_j with +n_j <= r_j <=4. Since p_j <= n_j, possible binary bits are exactly the table +below. The row p_j=3 has no possibilities. + +| Earlier raw count p_j | Possible bit zero | Possible bit one | +|---|---|---| +| 0 | always, via future count 0 or 4 | only if n_j<=1, via future count 1 | +| 1 | only if n_j<=3, via future count 3 | always, via future count 4 | +| 2 | only if n_j<=2, via future count 2 | only if n_j<=3, via future count 3 | +| 3 | impossible | impossible | +| 4 | always, via future count 4 | impossible | + +For example, when p_j=2 and n_j=3, only bit one remains possible; when n_j=4, +neither bit remains possible. The Cartesian product of these per-coordinate +sets is another overapproximation, since it ignores whether one future +boundary can realize all coordinate counts simultaneously in a fixed suffix. + +Take the union of the already served masks, the two-future-boundary subcube, +and these one-old/one-future subcubes for every old p. If it omits any mask, +no continuation of this prefix can reach depth two. Pruning that subtree is +sound. Prefixes containing a count 3 can be omitted from the old-boundary +list because their row in the table has no allowed bit. + +## Exact accounting + +Suppose h labels have appeared. A canonical prefix has + + (4k-d)! / ((k-h)! product_j (4-n_j)!) + +canonical completions. The division by (k-h)! permutes only the unseen labels; +each full word on those labels has one first-occurrence ordering. At each +pruned subtree, add this quotient to the accounted count. For a coverage threshold T, if at least T masks have +already been served, every continuation remains a solution, so the same +quotient counts solutions. Prune when the future-possible union has fewer +than T masks. This is the same safe relaxation with a cardinality target. Otherwise visit its children. Matching the accounted total to +the closed-form family size is an additional census control. + +## Sharp maximum and complete catalog + +The replay counts masks including zero. Threshold 30 has no solution, and +threshold 29 has exactly four canonical solutions. Thus the maximum number +of nonzero masks is 28, and MAXIMIZERS.json is complete up to source +relabelling. The verifier directly checks all four distinct canonical words, +all missing-mask sets and their four permutation rounds. No rotation or +reversal symmetry is assumed. + +The threshold-30 census visits 8,462,068 nodes and prunes 6,451,947 subtrees. +The threshold-29 census visits 8,715,495 nodes and prunes 6,632,616 subtrees. +Both account for all 2,546,168,625 canonical words. The full-coverage mode is +retained as a control, and the k=4 census gives 421 solutions among +2,627,625 canonical words. The unpruned calibration rows +(k, canonical words, full-cover solutions) are (1, 1, 1), (2, 35, 33) and +(3, 5775, 547). Every threshold is compared with the unpruned histogram at +these small sizes, giving 14 threshold comparisons. + +## Optional independent native replay + +The registered standard-library verifier needs no compiler. The separately +written raw-coordinate engine is retained for independent opt-in replay. +The second CLI argument enables pruning and the third is the mask threshold, +including zero. From the repository root: + +```sh +cc -O3 -Wall -Wextra -Werror -pedantic -std=c11 research/connector-char4-floor-obstructions/independent_depth2.c -o /tmp/imb-depth2-independent +/tmp/imb-depth2-independent 5 1 30 +/tmp/imb-depth2-independent 5 1 29 +/tmp/imb-depth2-independent 4 0 16 +``` + +It recomputes the sharp counts and every depth-histogram entry independently. +The four-source command accounts for every canonical word with negative +feasibility pruning disabled and returns 421 solutions. Already-satisfied +prefixes may still aggregate their canonical completions. Native output is a cross-check; the general pruning proof and +canonical accounting remain part of the scoped finite claim. + +## Consequence + +Source deletion preserves depth at most two: erase the four events of an +unwanted source and project the readout boundaries. Therefore failure at +five sources excludes every larger depth-two block. Four sources are +attained by two concatenated two-source depth-one blocks from #4248, so the +maximum depth-two source count in characteristic four is exactly four. +This does not exclude a coupled ten-source depth-four walk. Depth-three +seven-source blocks remain open. diff --git a/research/connector-char4-floor-obstructions/MAXIMIZERS.json b/research/connector-char4-floor-obstructions/MAXIMIZERS.json new file mode 100644 index 0000000000..52c226ce79 --- /dev/null +++ b/research/connector-char4-floor-obstructions/MAXIMIZERS.json @@ -0,0 +1,128 @@ +{ + "canonical_maximizers": [ + { + "walk": [ + 0, + 1, + 2, + 3, + 4, + 0, + 2, + 4, + 1, + 3, + 1, + 3, + 4, + 0, + 2, + 3, + 4, + 2, + 1, + 0 + ], + "covered_nonzero": 28, + "missing": [ + 11, + 20, + 22 + ], + "permutation_rounds": true + }, + { + "walk": [ + 0, + 1, + 2, + 3, + 4, + 0, + 2, + 4, + 1, + 3, + 3, + 1, + 4, + 0, + 2, + 3, + 4, + 2, + 1, + 0 + ], + "covered_nonzero": 28, + "missing": [ + 11, + 20, + 22 + ], + "permutation_rounds": true + }, + { + "walk": [ + 0, + 1, + 2, + 3, + 4, + 1, + 2, + 4, + 0, + 3, + 0, + 3, + 4, + 1, + 2, + 3, + 4, + 2, + 0, + 1 + ], + "covered_nonzero": 28, + "missing": [ + 11, + 20, + 21 + ], + "permutation_rounds": true + }, + { + "walk": [ + 0, + 1, + 2, + 3, + 4, + 1, + 2, + 4, + 0, + 3, + 3, + 0, + 4, + 1, + 2, + 3, + 4, + 2, + 0, + 1 + ], + "covered_nonzero": 28, + "missing": [ + 11, + 20, + 21 + ], + "permutation_rounds": true + } + ] +} diff --git a/research/connector-char4-floor-obstructions/PROOF17.md b/research/connector-char4-floor-obstructions/PROOF17.md new file mode 100644 index 0000000000..37160d9663 --- /dev/null +++ b/research/connector-char4-floor-obstructions/PROOF17.md @@ -0,0 +1,330 @@ +# The characteristic-four floor fails at eighteen sources + +This is a scoped written proof in the unsigned dirty-connector floor model. +It excludes eighteen sources and, by #4248's deletion lemma, gives N(4) <= 17. +It uses finite controls and exact integer arithmetic, without claiming a +proof-kernel certificate. + +## 1. Prefixes and cube intersections + +A walk uses each of k sources exactly four times. Set L=4k. Its cyclic +prefixes are q_t in (Z/4)^k, t=0,...,L-1, and u_t=q_t modulo two. Define +A={u_t}, r=L-|A| and n=L-r. Cyclic rotation translates every prefix by the +same vector, preserving four-prefix sums modulo four and preserving r. + +For any translated binary cube, let V be its eligible boundary indices and +s=|V|. Write + + S0=min(k,floor(r/2)), + H(k,r)=k+S0+floor((k-S0)/4). + +Then s<=H(k,r). If V is empty this is immediate. Otherwise rotate to start +at an eligible boundary. Working in the translated coordinates, each source has one internal +edge 0->1 and one three-event bad arc 1->2->3->0. The bad arc stays in one +outside path, meaning a maximal path whose endpoints are eligible and whose +interior is outside the cube. + +For each outside path, let d count complete source bad arcs and h count +internal 0->1 edges executed while another coordinate is outside. Its length +is 3d+h, with d>=1. Across all outside paths, sum d=k. If R is the number of +paths and I=sum h, the eligible vertices satisfy s=k-I+R. + +Call a path small when h=0 and d<=3. It has 3d+1 parity vertices in a +subcube of dimension d, hence at least 3d+1-2^d>=2 local repeated vertices. +Charge each repeat to its later position, never to the path's first endpoint. +Charges from different paths are disjoint even at shared endpoints. + +There is no cyclic endpoint loss. The two endpoint parities of a small path +differ, because every one of its d sources occurs three times. If boundary L +is locally repeated, replace its charge by the first earlier parity-zero +vertex in that final path. This vertex is interior, globally repeated from +boundary zero, and locally first, so it was not already charged. Thus all +charges lie among the r repeated cyclic positions, and 2S<=r for S small paths. + +Paths with h>=1 contribute 1-h<=0 to R-I. Every other non-small path consumes +at least four bad arcs, while each small path consumes at least one. Hence + + R-I<=S+floor((k-S)/4)<=S0+floor((k-S0)/4), + +which proves the bound. The same endpoint repair also preserves the full +local-repeat lower bound for any individual h=0 path with d<=3. + +## 2. Free-coordinate slabs + +Allow f coordinates to be unrestricted, leaving k-f binary constraints. +The corresponding intersection bound is + + H_f=k+3f+S_f+floor((k-f-S_f)/4), + S_f=min(k-f,floor(r/2)). + +To see this, let G be the unrestricted-coordinate edges occurring in outside +paths; the other 4f-G such edges occur inside. The eligible vertex count is +k+3f+R-I-G. Every path with at least one internal or unrestricted edge has +contribution at most zero to R-I-G. The remaining small paths have the same +repeat charge, and the k-f constrained sources supply their bad arcs. +Consequently H_f<=H(k,r)+3f, using S_f<=S0 and k-f-S_f<=k-S0. + +## 3. Unions of cubes with the same parity + +Let a length-4k source cycle use every coordinate four times, with prefixes +q_t in (Z/4)^k. Let P be any p distinct binary vectors, p>=1. Then + + #{t: q_t+a is in union_(v in P) ({0,1}^k+2v)} + <= min(4k, 2k+2(p-1)). + +The translates have the same parity and are disjoint as subsets of (Z/4)^k. + +### Proof + +Write each coordinate of q_t+a as low bit plus twice high bit. A boundary is +eligible exactly when its high-bit pattern is in P. Each coordinate high bit +flips exactly twice in the whole source cycle, at its 1->2 and 3->0 events. + +Compress the cyclic sequence of eligible high-bit patterns by removing +consecutive repetitions, including across outside excursions with equal +endpoint patterns. Its number of transitions is zero for one visited region, and otherwise at most 2(p-1). Indeed, a +cyclic alternation A,B,A,B of distinct patterns would force a coordinate in +which A and B differ to flip at least four times, impossible. A cyclic word +on p letters with adjacent letters distinct and no such alternation has at +most 2(p-1) transitions. To prove this by induction, if some letter repeats, +take a shortest arc between consecutive occurrences of a repeated letter. +Every interior letter occurs once globally: another occurrence outside the +arc would alternate with its endpoints, and two inside would give a shorter +arc. Thus some letter occurs once. Remove it, costing at most two transitions, +and apply induction. If no letter repeats the bound is immediate for p>=2. + +Let F be the f coordinates on which the patterns in P are not all equal. +Call a source event a budgeted low edge when it flips only the low bit and +its own coordinate high bit occurs among P at that coordinate. There is one +such edge for each of the k-f fixed coordinates and two for each of the f +varying coordinates, for a total k+f. Each such edge has either both endpoints +eligible or both outside. Let I count those outside. + +An eligible vertex is entered by a budgeted low edge, a direct high-bit +transition between eligible regions, or an outside path. Classify outside +paths by whether their endpoint high patterns are equal or different. +Let R_same count the former and R_cross count the latter plus direct +high-bit transitions. Then, writing s for eligible vertices, + + s=k+f-I+R_same+R_cross. + +The compressed-region argument gives R_cross<=2(p-1). + +Consider a same-region outside path containing no budgeted low edge. At +least one high bit flips in the path, and since its endpoint patterns are +equal each coordinate flips either zero or twice. A varying coordinate +cannot flip twice: between its two high flips lies one of its budgeted low +edges, contradicting the assumption. Therefore some fixed coordinate flips +twice. Those two flips and the intervening wrong-high low edge are exactly +that source's three-event bad arc. Each fixed source has only one such arc, +which belongs to one outside path, so at most k-f same-region paths contain +no budgeted low edge. Paths with at least one budgeted low edge contribute +at most zero to R_same-I; budgeted low edges in cross paths only help. +Consequently R_same-I<=k-f. + +Substitution gives s<=k+f+(k-f)+2(p-1)=2k+2(p-1). + + +## 4. Three levels of triple classes + +In this section and below, put h=H(k,r). For equal-cardinality index sets, +colex order compares the largest index in their symmetric difference; +the set containing that index is larger. + +Let A={u_t} be the set of distinct parity prefixes. Ignore masks in +P={0} union {u_a+u_b:a!=b}; its size is at most 1+C(n,2), n=4k-r. +For every other mask, every four-readout representation has four different +parity-prefix values. Its four three-prefix parity sums are distinct and do +not belong to A. + +Consider all three-element boundary-index subsets whose parity sum is not +in A. Let V be the number of their distinct full sums modulo four. Join two +full sums when they differ by 2e_j for some j and both occur. Let X be the +number of connected components of this graph. Finally let Z be the number +of distinct parity sums of these full sums. Each parity class contains some +number t of X-components and v distinct full sums. + +An X-component with v_i full sums has all its carry differences supported on +at most v_i-1 coordinate axes, using a spanning tree. The slab bound gives +at most h+3(v_i-1) possible fourth boundaries across that component. Summing +over its t components gives 3v+(h-3)t. Separately, the same-parity +union-cube lemma above gives at most 2v+2k-2 fourth boundaries for the entire +parity class. + +Put d=2h-2k-2. When k+1<=h<=2k and t>=2, + + 3v+(h-3)t - (2v+2k-2) >= d(t-1), + +because v>=t and the remaining difference is (2k-h)(t-2)>=0. +For t=1 no subtraction is needed. Thus the total number of mask/parity-class +incidences is at most + + 3V+(2k-h-1)X+(2h-2k-2)Z. + +Each non-P mask has at least four different triple-parity-class incidences, +one from each distinct last-prefix parity in its representation. For fixed +triple parity and fixed last-prefix parity the binary target is determined, +so counting possible fourth indices upper-bounds incidences. Therefore + + masks <= 1+C(n,2) + + floor((3V+(2k-h-1)X+(2h-2k-2)Z)/4). + +The coefficients used below are nonnegative. Here h denotes H(k,r). + +## 5. Pair graphs bounding V, X and Z + +Use events 1,...,L-1, L=4k, so the closing source occurs three times and +others four times. For equal-source events a {a,b-1}, exact full-sum equality. +X: {a,b} -> {a-1,b-1}, changing the full sum by 2e_j. +Z: {b-1,b} -> {a-1,a}, parity equality, taking one earlier a per later b. + +Each replacement removes the largest index b. In a three-subset whose +parity is not in A it cannot create a repeated index, since that would make +the parity sum one prefix. Minimum-colex representatives for full values +avoid Y pairs; representatives for X-components avoid X and Y pairs; +representatives for parity classes avoid all three pair types after replacing +duplicate parity-prefix indices by their earliest representatives. + +For a graph with m forbidden pairs on N indices, and wedge count +W=sum_v C(deg(v),2), the number of independent triples is at most + + C(N,3)-m(N-2)+W. + +This is the first two inclusion-exclusion terms. Ignoring its negative +triangle correction is safe. + +The Y graph has exactly mY=6k-3 edges. The XY graph has at least +mX=12k-6-2r edges. The full XYZ graph, after discarding r duplicate parity +vertices, has at least mZ=15k-7-13r edges, clamped below at zero. + +For mX: earlier same-source event-endpoint pairs overlap only when two +successive occurrences are consecutive events. Each such adjacency costs +at most two XY pairs. Each adjacency ends at a repeated parity prefix, so +there are at most r. For mZ, the pre-deletion graph has at least15k-7-3r +edges by the following direct count, and its maximum degree is ten, as below. +For a source with q retained events, the later event of rank i>=2 has at most +2i-1 distinct earlier neighbors. Without adjacent equal-source events the +total is q^2-1. Summing q=4 for k-1 sources and q=3 for the closing source +gives 15k-7. A consecutive equal-source pair reduces this total by at most +three, and ends at a repeated parity prefix. There are at most r such pairs. +Deleting r vertices then loses at most 10r further edges. + +The maximum degrees for Y,XY,XYZ are respectively 6,9,10. Their wedge counts +are at most respectively 22k,70k,108k before vertex deletion, and at most +(D-1)m by maximum degree. To see the rank bounds, assign a boundary between +an event of occurrence rank i and the next event of occurrence rank j the +following degree upper bounds alpha_i+beta_j: + +| graph | alpha_(1..4) | beta_(1..4) | +|---|---|---| +| Y | 0,1,2,3 | 3,2,1,0 | +| XY | 3,4,5,6 | 3,2,1,0 | +| XYZ | 3,5,6,7 | 3,3,2,1 | + +The boundary zero may be assigned the omitted closing rank four; its actual +degree is smaller. The missing closing event only decreases the bounds. +Each rank occurs k times in each marginal. Rearranging alpha and beta in +the same order maximizes sum C(alpha+beta,2), giving +22k,70k,108k respectively. Deleting vertices cannot increase wedge count. + +Thus, for k=18,L=72 and n=72-r, + + V <= C(72,3)-105*70+min(5*105,22*18), + X <= C(72,3)-mX*70+min(8*mX,70*18), + Z <= C(n,3)-mZ*(n-2)+min(9*mZ,108*18), + +where mX=max(0,210-2r), mZ=max(0,263-13r). The right sides decrease with +the actual edge count on the ranges used, so substituting its lower bound +is safe. + +## 6. Initial eighteen-source cases + +At k=18,L=72, the exact arithmetic in axis_obstruction.py evaluates every +r=0,...,20. All rows exclude 2^18 masks except r=2,4,5, whose conservative +upper bounds including zero are 262506,265606,262744. A four-readout multiset reduces to an even subset of at most four of the +n distinct parity prefixes, giving at most 1+C(n,2)+C(n,4) parity masks. +For r>=21, n<=51 and + + 1+C(51,2)+C(51,4)=251176<262144=2^18. + +It remains to handle the three exceptional rows. Their theoretical cube caps +H are 23,24,24 respectively. + +## 7. Closing the exceptional cases + +Let q_0,...,q_(L-1) be the cyclic mod-four prefixes, L=72. Call index b +axis-deletable when some a=2 full values, the old slab +bound H+3(v_i-1) is at most4v_i+H-5. Thus a parity class with v full values and +t X-components has cap4v+(H-5)t. Combining with the same union cap2v+2k-2, +subtract (2H-2k-4)(t-1) when t>=2. The remaining difference is bounded below +by (2k-H+1)(t-2)>=0 because v>=t. Summing classes gives incidence numerator + + 4V+(2k-H-1)X+(2H-2k-4)Z. + +All coefficients are nonnegative here. No attained-H geometry is used in this +branch. The corrected counts are255394,259733,257507 for r2,4,5. + +If H is attained, let S count small h=0 outside paths, each with d<=3 bad arcs. +Rotate at an eligible boundary of that cube as in the component argument; +the walk still restores at L and the shifted cube is again a translated cube. +The component argument gives R-I <= S + floor((18-S)/4). At r2, S<=1 and +H=23 forces S=1 and at least4 other h=0 paths with d>=4. The small path +therefore has d<=2. A d2,h0 path has7 parity vertices in a two-dimensional +affine subcube, and hence at least3 local repeated vertices. These imply at +least3 global parity repeats. If its final endpoint is L, replace a charged L +by the first earlier parity-zero vertex in that path, just as in Section 1; +the endpoints have different parity, so this earlier occurrence is interior +and locally first. Thus d2 contradicts r2. The small path has d1, and is a +literal triple-equal-source run, giving q=2 axis deletions. + +At r4 or r5, S<=2 and H=24 force S=2 and at least4 other h=0 paths of d>=4. +The source budget18 is exhausted by minimum costs1+1+4+4+4+4, so both small +paths have d1. They give q=4 axis-deletable indices. We do not need to control +the fifth repeat at r5. + +The registered exact arithmetic in axis_obstruction.py gives the following upper +counts, all below262144. V and Z retain their conservative Section 5 bounds. + +| r | H | q | new X upper | H attained | H not attained | +|---|---|---|---|---|---| +| 2 | 23 | 2 | 43216 | 252714 | 255394 | +| 4 | 24 | 4 | 40420 | 248171 | 259733 | +| 5 | 24 | 4 | 40552 | 245287 | 257507 | + +Every eighteen-source floor walk is therefore excluded, and deletion gives +N(4)<=17. +The earlier certified lower bound remains9. diff --git a/research/connector-char4-floor-obstructions/README.md b/research/connector-char4-floor-obstructions/README.md new file mode 100644 index 0000000000..a96e19391a --- /dev/null +++ b/research/connector-char4-floor-obstructions/README.md @@ -0,0 +1,198 @@ +# Characteristic-four connector floor obstructions + +For the unsigned dirty connector of +[PR #4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231), let +N(c) be the largest source count k at which every source operator and every +nonzero binary-mask output operator can be called exactly c times while +restoring the arbitrarily dirty connector. The complete-call floor is +c(k + 2^k - 1). +[PR #4248](https://github.com/CrocSwap/integer-mult-bounds/pull/4248) +attains nine sources in characteristic four and supplies the deletion lemma. +[PR #4255](https://github.com/CrocSwap/integer-mult-bounds/pull/4255) +proves N(4) <= 20. + +This package establishes: + +- **9 <= N(4) <= 17.** A cube-union and triple-class argument excludes every + eighteen-source floor walk, closing all parity-repeat cases with exact + integer bounds below 262,144 masks including zero. +- **The maximum depth-two source count is four.** More sharply, a balanced + five-source block serves at most 28 of the 31 nonzero masks using two + prefix readouts. Exactly four words, up to source relabelling, attain 28. +- An all-ones readout normal form has eight possible source inventories + across four gaps. It gives 19,448 inventory-type count vectors at k = 10, + while leaving internal event orders to search. + +The upper bound is a scoped written proof with bounded controls. The +five-source maximum and catalog are exhaustive finite results. They do not +exclude ten sources in a general depth-four walk. There is no new κ, +selected-frontier change or complete multiplication theorem. + +## Interface and necessary conditions + +A characteristic-four floor walk has length 4k and uses each immutable source +exactly four times. Every nonzero binary mask m must be a sum of four +possibly repeated boundary prefix vectors modulo four. This is #4231/#4248's +prefix criterion. Zero is obtained by reading the zero boundary four times. + +Modulo two, a four-readout multiset reduces to an even subset of at most four +parity prefixes. Repeated parity-prefix values can be identified without +changing that set of parity sums. The full mod-four condition also constrains +how many prefixes can lie in a translate of the binary cube. + +## Upper bound: N(4) <= 17 + +[PROOF17.md](PROOF17.md) gives the complete argument. Its cube-intersection +lemma improves the cyclic repeat charge to 2S<=r, and extends to free-coordinate +slabs and unions of cubes with the same parity. It then counts three levels +of triple sums: exact modulo-four values, components connected by one-coordinate +carry changes, and parity classes. + +Colexicographic representatives and source-event pair graphs bound these +classes. The resulting count excludes all eighteen-source parity-repeat +cases except r=2,4,5. If the theoretical cube cap is attained in one of those +cases, the source budget forces one or two literal triple-source runs. Their +axis-deletable prefix indices sharpen the component count. If the cube cap +is not attained, a conservative four-per-axis bound closes the same cases. +The six final upper counts are all below 262,144. + +[axis_obstruction.py](axis_obstruction.py) replays all initial cases, the tail, +and both branches of each residual case. [n4_controls.py](n4_controls.py) +checks the strengthened cube, graph, class and incidence lemmas on bounded +families. The underlying written argument is uniform in the walk. + +## A normal form for future construction searches + +Take four readout boundaries for the all-ones mask and rotate the source walk +to begin at the first. Every prefix is translated by the same vector, so each +four-prefix sum changes by four times that vector, which vanishes modulo four. +The four cyclic gaps partition the source events. + +For each source, its gap inventory (a, b, c, d) has total four and satisfies +3a + 2b + c = 1 modulo four. Exactly eight of the 35 weak compositions satisfy +this equation: the cyclic rotations of (3, 0, 0, 1) and (0, 2, 1, 1). +Every source misses at least one gap. Repeated readouts give empty gaps and +remain allowed. + +Up to source relabelling, the inventory-type counts have C(k+7, 7) +possibilities, giving 19,448 at k = 10. This counts inventories, not event +orders. Each gap's prescribed multiset still needs an internal ordering. +When labels are fixed by inventory type, first-occurrence symmetry can be +imposed only within equal-type classes. No ten-source exclusion follows. + +## Sharp depth-two obstruction + +A block has depth at most two if every binary mask is a sum of at most two +of its prefix-count vectors modulo four. Boundary zero pads shorter reads. +Two concatenated two-source depth-one blocks from #4248 attain four sources. + +The complete first-occurrence-canonical census at five sources accounts for +all 20! / ((4!)^5 * 5!) = 2,546,168,625 words. None reaches 30 masks including +zero, and exactly four reach 29. [MAXIMIZERS.json](MAXIMIZERS.json) lists those +four words, their missing nonzero masks and their four-permutation structure. +Each is checked directly. The count of four plus four distinct valid canonical +witnesses proves catalog completeness up to source relabelling only. +Rotation and reversal are not quotiented out. + +[DEPTH2.md](DEPTH2.md) gives the safe future-cut relaxation, exact subtree +accounting and replay details. The threshold-30 census visits 8,462,068 nodes +and prunes 6,451,947 subtrees. The threshold-29 census visits 8,715,495 nodes +and prunes 6,632,616 subtrees. Both account for the complete canonical family. +Source deletion preserves depth at most two, so failure at five sources +excludes every larger depth-two block. This closes the concatenation route +using two five-source depth-two blocks, while allowing coupled depth-four +searches. + +## Reproduction + +From the repository root with CPython 3.12: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/connector-char4-floor-obstructions/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/connector-char4-floor-obstructions/independent_check.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-char4-floor-obstructions +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-char4-floor-obstructions --check-source-history +``` + +Expected main marker: +`PASS_CONNECTOR_CHAR4_FLOOR_OBSTRUCTIONS N4<=17 depth2_max=4 depth2_k5_coverage=28`. +Both principal registered checkers also run with optimized Python and explicit checks. +The main verifier recomputes [CERTIFICATE.json](CERTIFICATE.json), including +the eighteen-source triple-class cases and residual branches, the earlier +76-case cube arithmetic control, the inventory enumeration, full-coverage +controls, the sharp depth-two censuses and the maximizer catalog. Certificate +regeneration is available through `verify.py --write-certificate`. +Each checker prints a generated receipt bound to all package files. + +The main cube control checks all 70 labelled two-source words at all 16 +translations and all 34,650 labelled three-source words at all 64 translations, +for 2,218,720 translations. It also checks 4,000 deterministic larger words +at 100 translations each. The separately written component checker uses +literal coordinate states on 21,120 cases, directly checking the outside +components, disjoint repeated-parity charges and arithmetic table. It also +checks every maximizer independently. + +The depth-two Python replay checks its future-cut tables directly and compares +with an unpruned coordinate evaluator through three sources at every mask +threshold. A separately written iterative C engine agrees with every field +of both sharp five-source censuses and accounts for all 2,627,625 four-source +canonical words with negative feasibility pruning disabled, finding 421 +full-cover solutions. Already-satisfied prefixes may still aggregate their +canonical completions. Its opt-in +commands are in DEPTH2.md; it is not a registered CI obligation. +Predecessor constructions and exclusions are cited dependencies, not new +audit deliverables. Their exact heads and README hashes are recorded as +citations in [SOURCES.json](SOURCES.json). + +## Limitations + +N(4) remains open within 9 <= N(4) <= 17. There is no ten-source witness and +no exclusion of ten through seventeen sources. The single-cube bound alone +leaves too many possibilities at eighteen sources; the triple-class proof +uses collections of cube intersections to close that case. Moreover, the +72-event finite witness in [CUBE-SHARPNESS.json](CUBE-SHARPNESS.json) has +72 distinct parity prefixes and 22 prefixes in the unshifted binary cube. +Thus H(18,0)=22 is attained, so that uniform intersection cap cannot be +lowered at this corner. This is not a floor-attainment witness. The depth-two +census concerns only that block depth and characteristic four. + +The interface has immutable sources, unsigned calls and every nonzero binary +mask output. No physical caller, primitive tariff, admission, dispatch or +precision obligation is instantiated. Independent human and formal +proof-kernel review are unclaimed. + +The Python checkers allocate bounded integers and temporary collections. +In depth_two.py, walk_tables and inspect_state use preallocated tables and +an explicit 21-frame stack for k <= 5, with no recursion. CPython allocation +is a managed-runtime deviation from fixed-allocation operation. Fixed +dimensions, explicit iteration bounds, capacity checks and normal/optimized +replays bound and check the live state. A strict allocation-free consumer +would require the native fixed-array implementation instead of widening +this Python contract. The axis controls fix eighteen sources and one hundred +control words; the general incidence controls use at most nine sources and +at most C(36,3) triple values in their bounded component worklists. These +modules use the same managed-runtime deviation and explicit iteration bounds. +No unbounded input or concurrent mutation is accepted. + +## Open next questions + +Structured first steps and blockers are in [TASK.json](TASK.json). + +1. Find a ten-source floor walk in the eight-inventory normal form, or prove + ten sources fail. The four maximizing depth-two blocks give a complete + small seed catalog for coupled searches; concatenating two five-source + depth-two blocks cannot work. +2. Improve the triple-class and cube-union count at seventeen sources, or + find a further structural restriction on its possible walks. +3. Identify a concrete characteristic-four caller and price its complete + interface before using a larger abstract batch in a recursive supplier. + +## Credit + +This package was produced by Nick Petalas. The interface and floor are +#4231's. The nine-source lower bound and deletion lemma are #4248's; +the deletion argument extends #4232's characteristic-three version. +The parity-boundary counting approach builds on #4255. The connector +interface and prefix criterion originate in Ross Richardson's #943/#934 +lineage. Independent human and formal proof-kernel review are unclaimed. +Apache-2.0. diff --git a/research/connector-char4-floor-obstructions/SOURCES.json b/research/connector-char4-floor-obstructions/SOURCES.json new file mode 100644 index 0000000000..3ae468b942 --- /dev/null +++ b/research/connector-char4-floor-obstructions/SOURCES.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ], + "cited_predecessors": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4255", + "head": "0dba831b7e138c809f1900ecf51b4716ea99c505", + "readme": "research/connector-char4-floor-bounds/README.md", + "readme_sha256": "3b89e21a0c75ea5376d2c2ae2a55868911de902ec41cc6ece489212ca05e03fb", + "usage": "Cited written dependency; not vendored or read by executable replay." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4248", + "head": "e7df122403cfc2febfb6799abb821487d8d1ee49", + "readme": "research/connector-depth-blocks/README.md", + "readme_sha256": "0ce59767f249b24d65d7d14b466115858d82c0bbfaaa8eab46b7406f4e975331", + "usage": "Cited written dependency; not vendored or read by executable replay." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4231", + "head": "8a956cbc80dc55697fd3e214812ce567b5eca48f", + "readme": "research/unsigned-connector-characteristic/README.md", + "readme_sha256": "260ae8ca19cfd8add386666e823725065eb137bcaedf7577785d6eda4ee0200b", + "usage": "Cited written dependency; not vendored or read by executable replay." + } + ] +} diff --git a/research/connector-char4-floor-obstructions/TASK.json b/research/connector-char4-floor-obstructions/TASK.json new file mode 100644 index 0000000000..8c70ad7680 --- /dev/null +++ b/research/connector-char4-floor-obstructions/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/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.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Narrow the characteristic-four unsigned connector floor interval from 9 <= N(4) <= 20 to 9 <= N(4) <= 17 by a cube-union and triple-class proof with axis-deletion residual cases. Prove the sharp five-source depth-two coverage maximum 28 of 31 nonzero masks, classify all four maximizing words up to source relabelling, and provide an eight-inventory all-ones search normalization.", + "scope_change_reason": "The question targets exact N(4). The alphabet stays fixed and the source count changes, a scope-change trigger on the original card. This proof limits batch sizes for any characteristic-four floor consumer.", + "bottleneck_link": "Side result about the complete-call interface floor; no physical consumer or kappa change is supplied.", + "budget_minutes": 100, + "stop_rule": "At the research checkpoint, publish the strongest independently checked bound or construction. Do not claim a general ten-source exclusion from a restricted search.", + "outcome": "completed", + "evidence": "Written translated-cube/outside-component proof, all 76 parity-duplicate cases, exhaustive small translated-cube controls and separately written literal component checks. Complete canonical depth-two censuses at thresholds 30 and 29 account for 2,546,168,625 words, find zero and four solutions respectively, and agree with an independent C engine. Standard-library replay validates every maximizer and compares pruning with unpruned small cases. All 35 gap inventories are enumerated, leaving eight types and 19,448 type-count vectors at k=10. A 72-event eighteen-source witness attains the cube cap H(18,0)=22 with no parity-prefix duplicates; it is a finite sharpness witness, not a floor word. The stronger eighteen-source triple-class count excludes all repeat cases except r=2,4,5; axis deletions and conservative nonattainment bounds exclude all six residual branches, yielding N(4)<=17.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is N(4) exactly, within 9 <= N(4) <= 17?", + "why_it_matters": "It determines the largest batch paying exactly four calls per operator.", + "first_step": "Use the eight-inventory all-ones normal form to search event orders outside the known nine-source insertion family, or derive a stronger obstruction.", + "blocked_by": "Neither a ten-source witness nor a universal ten-source exclusion is known." + }, + { + "question": "Can the cube-union/triple-class method exclude seventeen sources?", + "why_it_matters": "The present universal obstruction stops at eighteen sources.", + "first_step": "Generalize the graph and incidence arithmetic to k=17 and identify the remaining structural deficits.", + "blocked_by": "The current estimates are not strong enough at seventeen sources; no exclusion is claimed." + }, + { + "question": "Does a concrete characteristic-four caller benefit from a floor batch?", + "why_it_matters": "Abstract query counts alone do not improve a recursive supplier.", + "first_step": "Identify an immutable-source caller and price all primitives, input admission and dispatch.", + "blocked_by": "No physical caller is instantiated." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19083546", + "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "overlap_scope": "Live open PR list, account PR list, last thirty handoff comments, active discussions, merged connector PR search and origin/main README grep; cached helper covers 376 open PRs and 3149 discussion records with complete pagination. Closed work and arbitrary code diffs remain incompletely covered." + } +} diff --git a/research/connector-char4-floor-obstructions/VERIFY.json b/research/connector-char4-floor-obstructions/VERIFY.json new file mode 100644 index 0000000000..1511613e52 --- /dev/null +++ b/research/connector-char4-floor-obstructions/VERIFY.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Translated-cube arithmetic and small/exploratory controls; full sharp depth-two censuses, catalog, inventory lemma and unpruned calibration; eighteen-source triple classes, all residual branches and axis replacements; strengthened cube/slab/union, graph/rank and incidence controls" + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Translated-cube arithmetic and small/exploratory controls; full sharp depth-two censuses, catalog, inventory lemma and unpruned calibration; optimized Python; eighteen-source triple classes, all residual branches and axis replacements; strengthened cube/slab/union, graph/rank and incidence controls" + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent literal outside-component charges, arithmetic and maximizer coverage; independently recomputed eighteen-source arithmetic" + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent literal outside-component charges, arithmetic and maximizer coverage; optimized Python; independently recomputed eighteen-source arithmetic" + } + ] +} diff --git a/research/connector-char4-floor-obstructions/axis_obstruction.py b/research/connector-char4-floor-obstructions/axis_obstruction.py new file mode 100644 index 0000000000..0d4d47a9d6 --- /dev/null +++ b/research/connector-char4-floor-obstructions/axis_obstruction.py @@ -0,0 +1,177 @@ +"""Integer arithmetic and finite controls for the eighteen-source obstruction. + +The written proof supplies the graph and cube bounds. This module evaluates +all parity-repeat cases and checks literal-run axis replacements independently +of the arithmetic. It uses no external solver or local package dependency. +""" +from itertools import combinations +import json +from math import comb + +K = 18 +LENGTH = 72 +TARGET = 1 << K + + +def independent_triples(vertices, edges, degree, wedge_cap): + if not (3 <= vertices <= LENGTH and 0 <= edges <= comb(vertices, 2)): + raise ValueError('invalid graph-count arguments') + if degree < 1 or wedge_cap < 0: + raise ValueError('invalid degree or wedge cap') + wedges = min((degree-1)*edges, wedge_cap) + return comb(vertices, 3)-edges*(vertices-2)+wedges + + +def cube_cap(repeats): + if not 0 <= repeats <= 20: + raise ValueError('repeat row outside the bounded table') + small = min(K, repeats//2) + return K+small+(K-small)//4 + + +def incidence_numerator(values, components, parities, cap, axis_cost): + if axis_cost not in (3, 4): + raise ValueError('unsupported component cost') + component_coefficient = 2*K-cap-axis_cost+2 + parity_coefficient = 2*cap-2*K-2 + if min(values, components, parities, component_coefficient, parity_coefficient) < 0: + raise ValueError('negative incidence parameter') + return axis_cost*values+component_coefficient*components+parity_coefficient*parities + + +def base_rows(): + values = independent_triples(LENGTH, 6*K-3, 6, 22*K) + rows = [] + for repeats in range(21): + n = LENGTH-repeats + cap = cube_cap(repeats) + x_edges = max(0, 12*K-6-2*repeats) + z_edges = max(0, 15*K-7-13*repeats) + components = independent_triples(LENGTH, x_edges, 9, 70*K) + parities = independent_triples(n, z_edges, 10, 108*K) + numerator = incidence_numerator(values, components, parities, cap, 3) + upper = 1+comb(n, 2)+numerator//4 + rows.append({'r': repeats, 'cube_cap': cap, 'V_upper': values, + 'X_upper': components, 'Z_upper': parities, + 'incidence_numerator': numerator, 'mask_upper': upper, + 'excluded': upper < TARGET}) + return rows + + +def residual_rows(rows): + by_repeat = {row['r']: row for row in rows} + result = [] + for repeats, deletions in ((2, 2), (4, 4), (5, 4)): + base = by_repeat[repeats] + n = LENGTH-repeats + cap = base['cube_cap'] + vertices = LENGTH-deletions + edges = 12*K-6-2*repeats-9*deletions + components = independent_triples(vertices, edges, 9, 70*K) + attained = incidence_numerator(base['V_upper'], components, base['Z_upper'], cap, 3) + absent = incidence_numerator(base['V_upper'], base['X_upper'], base['Z_upper'], cap-1, 4) + pair_count = 1+comb(n, 2) + result.append({'r': repeats, 'cube_cap': cap, 'axis_deletions': deletions, + 'X_vertices': vertices, 'X_edges_lower': edges, + 'X_upper': components, 'attained_H_upper': pair_count+attained//4, + 'not_attained_H_upper': pair_count+absent//4}) + return result + + +def evaluate(): + rows = base_rows() + residual = residual_rows(rows) + exceptions = [row['r'] for row in rows if not row['excluded']] + if exceptions != [2, 4, 5]: + raise RuntimeError('unexpected residual cases') + for row in residual: + if max(row['attained_H_upper'], row['not_attained_H_upper']) >= TARGET: + raise RuntimeError('residual case was not excluded') + tail = 1+comb(51, 2)+comb(51, 4) + if tail >= TARGET: + raise RuntimeError('parity tail was not excluded') + return {'source_count': K, 'target_masks_including_zero': TARGET, + 'base_rows': rows, 'base_exceptions': exceptions, + 'residual_rows': residual, 'r_at_least_21_upper': tail} + + +def inspect_axis_word(word, replacements): + if len(word) != LENGTH or any(word.count(j) != 4 for j in range(K)): + raise ValueError('invalid control word') + vectors, parities, current = [], [], [0]*K + for source in word: + vectors.append(tuple(current)) + parities.append(sum((x % 2) << j for j, x in enumerate(current))) + current[source] = (current[source]+1) % 4 + if any(current): + raise RuntimeError('control word did not restore') + for later, (earlier, source) in replacements.items(): + if not 0 <= earlier < later < LENGTH: + raise ValueError('invalid replacement indices') + difference = tuple((x-y) % 4 for x, y in zip(vectors[later], vectors[earlier])) + if difference != tuple(2 if j == source else 0 for j in range(K)): + raise RuntimeError('axis difference failed') + prefix_parities = set(parities) + checked = 0 + for triple in combinations(range(LENGTH), 3): + parity = parities[triple[0]] ^ parities[triple[1]] ^ parities[triple[2]] + if parity in prefix_parities: + continue + for later in triple: + if later not in replacements: + continue + earlier, _ = replacements[later] + if earlier in triple: + raise RuntimeError('good triple replacement collided') + changed = tuple(sorted(earlier if t == later else t for t in triple)) + if not changed[::-1] < triple[::-1]: + raise RuntimeError('colex did not decrease') + after = parities[changed[0]] ^ parities[changed[1]] ^ parities[changed[2]] + if after != parity: + raise RuntimeError('triple parity changed') + checked += 1 + return checked + + +def axis_controls(): + checked = 0 + state = 1020426 + for case in range(100): + word = [0, 1]+[j for j in range(2, K) for _ in range(4)] + for i in range(len(word)-1, 0, -1): + state = (6364136223846793005*state+1442695040888963407) & ((1 << 64)-1) + other = state % (i+1) + word[i], word[other] = word[other], word[i] + at = 5+(case % 50) + word[at:at] = [0]*3 + word += [1]*3 + replacements = {at+2: (at, 0), at+3: (at+1, 0), 70: (0, 1), 71: (69, 1)} + checked += inspect_axis_word(word, replacements) + return {'words': 100, 'axis_pairs': 400, 'good_triple_moves': checked} + + +def short_component_controls(): + result = [] + for length in (6, 4): + repeats = [] + for chosen in combinations(range(length), 3): + word = [0 if i in chosen else 1 for i in range(length)] + parity, seen, count = 0, {0}, 0 + for source in word: + parity ^= 1 << source + count += parity in seen + seen.add(parity) + repeats.append(count) + result.append({'multiplicities': [3, length-3], 'words': len(repeats), + 'min_local_repeats': min(repeats)}) + if [row['min_local_repeats'] for row in result] != [3, 1]: + raise RuntimeError('short-component repeat bound failed') + return result + + +def calibrate(): + return {'axis_replacements': axis_controls(), 'short_components': short_component_controls()} + + +if __name__ == '__main__': + print(json.dumps({'arithmetic': evaluate(), 'controls': calibrate()}, indent=2, sort_keys=True)) diff --git a/research/connector-char4-floor-obstructions/depth_two.py b/research/connector-char4-floor-obstructions/depth_two.py new file mode 100644 index 0000000000..0bb82bd833 --- /dev/null +++ b/research/connector-char4-floor-obstructions/depth_two.py @@ -0,0 +1,307 @@ +"""Replay the scoped characteristic-four depth-two block census. + +Each source occurs exactly four times. A depth-two block represents every +binary mask as the sum of two prefix vectors modulo four, with boundary zero +available for padding. Source labels are ordered by first occurrence. The safe +pruning lemma is documented in DEPTH2.md. + +Resource bounds: k is validated in 1..5, table storage has at most +2 * 5**5 * 4**5 unsigned 32-bit entries, and DFS frames have capacity 4*k+1. +Python necessarily allocates integers and iterator objects during traversal; +live state stays within these fixed input-derived bounds. A separately written native implementation is retained as an optional +independent cross-check. +""" +from array import array +import argparse +import itertools +import json +import math +from typing import NamedTuple + +MAX_K = 5 + + +class Tables(NamedTuple): + k: int + past_count: int + full: int + actual: array + future: array + both_future: tuple + valid_past: tuple + children: tuple + ways: tuple + depths: tuple + + +def subcubes(k): + """Index each Boolean subcube by its fixed-zero and fixed-one masks.""" + masks = 1 << k + cubes = [0] * (1 << (2*k)) + for zero in range(masks): + for one in range(masks): + if not zero & one: + cubes[zero | (one << k)] = sum( + 1 << mask for mask in range(masks) + if not mask & zero and mask & one == one) + return cubes + + +def allowed_future(past, current, cubes, k): + """Masks feasible coordinatewise for one old and one future boundary.""" + zero = one = 0 + for j, (p, n) in enumerate(zip(past, current)): + if p == 0: + if n >= 2: + zero |= 1 << j + elif p == 1: + if n == 4: + one |= 1 << j + elif p == 2: + if n == 4: + return 0 + if n == 3: + one |= 1 << j + elif p == 4: + zero |= 1 << j + else: + raise RuntimeError('past-count three must be omitted') + return cubes[zero | (one << k)] + + +def fill_pair_tables(currents, pasts, cubes, k): + """Precompute actual new readouts and safe one-future-cut relaxations.""" + width = len(pasts) + actual = array('I', [0]) * (len(currents)*width) + future = array('I', [0]) * (len(currents)*width) + if actual.itemsize != 4: + raise RuntimeError('this replay requires 32-bit unsigned integer storage') + for cid, current in enumerate(currents): + base = cid*width + for pid, past in enumerate(pasts): + if any(p > n for p, n in zip(past, current)): + continue + residues = tuple((p+n) % 4 for p, n in zip(past, current)) + if all(r <= 1 for r in residues): + actual[base+pid] = 1 << sum(r << j for j, r in enumerate(residues)) + future[base+pid] = allowed_future(past, current, cubes, k) + return actual, future + + +def build_tables(k): + """Initialize every fixed-capacity table before the census traversal.""" + if not 1 <= k <= MAX_K: + raise ValueError(f'k must lie in 1..{MAX_K}') + cubes = subcubes(k) + powers = tuple(5**j for j in range(k)) + pasts = tuple(itertools.product((0, 1, 2, 4), repeat=k)) + past_index = {past: pid for pid, past in enumerate(pasts)} + currents = [None] * (5**k) + for counts in itertools.product(range(5), repeat=k): + currents[sum(v*powers[j] for j, v in enumerate(counts))] = counts + actual, future = fill_pair_tables(currents, pasts, cubes, k) + both_future, valid_past, children, ways, depths = [], [], [], [], [] + for cid, counts in enumerate(currents): + depth = sum(counts) + introduced = sum(v != 0 for v in counts) + denominator = math.factorial(k-introduced) * math.prod( + math.factorial(4-v) for v in counts) + numerator = math.factorial(4*k-depth) + if numerator % denominator: + raise RuntimeError('nonintegral subtree completion count') + ways.append(numerator // denominator) + depths.append(depth) + children.append(tuple(cid+powers[j] for j, v in enumerate(counts) + if v < 4 and j <= introduced)) + both_future.append(cubes[sum((v >= 3) << j for j, v in enumerate(counts))]) + valid_past.append(past_index.get(counts, -1)) + return Tables(k, len(pasts), (1 << (1 << k))-1, actual, future, + tuple(both_future), tuple(valid_past), tuple(children), + tuple(ways), tuple(depths)) + + +def inspect_state(tables, cid, served, prefix_ids, count): + """Update served masks and the safe future-representation upper bound.""" + pid = tables.valid_past[cid] + if pid >= 0: + if count >= len(prefix_ids): + raise RuntimeError('past-prefix capacity exhausted') + prefix_ids[count] = pid + count += 1 + base = cid*tables.past_count + possible = tables.both_future[cid] + for index in range(count): + position = base+prefix_ids[index] + served |= tables.actual[position] + possible |= tables.future[position] + return served, possible | served, count + + +def walk_tables(tables, threshold): + """Traverse the canonical word tree with a bounded explicit DFS stack.""" + capacity = 4*tables.k+1 + prefix_ids = [0]*capacity + state_ids, served_masks = [0]*capacity, [1]*capacity + prefix_counts, next_children = [0]*capacity, [-1]*capacity + pruned_depth = [0]*capacity + nodes = pruned = accounted = solutions = 0 + depth = 0 + step_limit = 2*capacity*tables.ways[0]+1 + for _ in range(step_limit): + if depth < 0: + return nodes, pruned, accounted, solutions, pruned_depth + cid = state_ids[depth] + if next_children[depth] == -1: + nodes += 1 + served, possible, count = inspect_state( + tables, cid, served_masks[depth], prefix_ids, prefix_counts[depth]) + served_masks[depth], prefix_counts[depth] = served, count + if served.bit_count() >= threshold or possible.bit_count() < threshold: + accounted += tables.ways[cid] + if served.bit_count() >= threshold: + solutions += tables.ways[cid] + else: + pruned += 1 + pruned_depth[tables.depths[cid]] += 1 + depth -= 1 + continue + next_children[depth] = 0 + if not tables.children[cid]: + raise RuntimeError('unclassified terminal state') + child_index = next_children[depth] + children = tables.children[cid] + if child_index == len(children): + depth -= 1 + continue + next_children[depth] += 1 + child = children[child_index] + inherited_served, inherited_count = served_masks[depth], prefix_counts[depth] + depth += 1 + if depth >= capacity: + raise RuntimeError('DFS frame capacity exhausted') + state_ids[depth], served_masks[depth] = child, inherited_served + prefix_counts[depth], next_children[depth] = inherited_count, -1 + raise RuntimeError('canonical traversal iteration bound exhausted') + + +def census(k, threshold=None): + if not 1 <= k <= MAX_K: + raise ValueError(f'k must lie in 1..{MAX_K}') + if threshold is None: + threshold = 1 << k + if not 1 <= threshold <= 1 << k: + raise ValueError('threshold exceeds the mask count') + tables = build_tables(k) + nodes, pruned, accounted, solutions, pruned_depth = walk_tables(tables, threshold) + expected = math.factorial(4*k) // (math.factorial(4)**k * math.factorial(k)) + if accounted != expected: + raise RuntimeError(f'completion accounting failed: {accounted} != {expected}') + return {'k': k, 'covered_threshold': threshold, 'canonical_words': expected, 'visited_nodes': nodes, + 'pruned_nodes': pruned, 'accounted_words': accounted, + 'solutions': solutions, 'pruned_depth': pruned_depth} + + +def served_by_pairs(word, k): + """Direct integer-coordinate calibration, without future-cut pruning.""" + if not 1 <= k <= MAX_K: + raise ValueError(f'k must lie in 1..{MAX_K}') + if len(word) != 4*k or any(word.count(j) != 4 for j in range(k)): + raise ValueError('expected a balanced characteristic-four source word') + prefix = [(0,)*k] + for label in word: + current = list(prefix[-1]) + current[label] += 1 + prefix.append(tuple(current)) + served = 0 + for a, b in itertools.combinations_with_replacement(prefix, 2): + residues = tuple((x+y) % 4 for x, y in zip(a, b)) + if all(value <= 1 for value in residues): + served |= 1 << sum(value << j for j, value in enumerate(residues)) + return served + + +def canonical(word): + if len(word) > 4*MAX_K: + raise ValueError('canonical calibration word exceeds the size bound') + introduced = set() + for label in word: + if label not in introduced: + if label != len(introduced): + return False + introduced.add(label) + return True + + +def brute_histogram(k): + """Unpruned control on all k**(4*k) strings, restricted to k<=3.""" + if not 1 <= k <= 3: + raise ValueError('unpruned calibration is bounded at three sources') + histogram = [0] * ((1 << k)+1) + words = 0 + for word in itertools.product(range(k), repeat=4*k): + if any(word.count(j) != 4 for j in range(k)) or not canonical(word): + continue + words += 1 + histogram[served_by_pairs(word, k).bit_count()] += 1 + return words, histogram + + +def coordinate_controls(): + tables = build_tables(1) + for current in range(5): + expected = sum(1 << bit for bit in (0, 1) if any( + (a+b) % 4 == bit for a, b in itertools.combinations_with_replacement( + range(current, 5), 2))) + if tables.both_future[current] != expected: + raise RuntimeError('two-future-cut relaxation control failed') + for pid, past in enumerate((0, 1, 2, 4)): + if past > current: + continue + expected = sum(1 << bit for bit in (0, 1) if any( + (past+future) % 4 == bit for future in range(current, 5))) + if tables.future[current*4+pid] != expected: + raise RuntimeError('old/future-cut relaxation control failed') + positive = (0, 1, 0, 0, 0, 1, 1, 1, 2, 3, 2, 2, 2, 3, 3, 3) + if served_by_pairs(positive, 4) != (1 << 16)-1: + raise RuntimeError('known four-source depth-two block rejected') + try: + served_by_pairs(positive[:-1], 4) + except ValueError: + pass + else: + raise RuntimeError('dropped-call word accepted') + negative = tuple(j for j in range(5) for _ in range(4)) + if served_by_pairs(negative, 5).bit_count() != 16: + raise RuntimeError('sorted five-source depth-two control failed') + for invalid in (0, MAX_K+1): + try: + build_tables(invalid) + except ValueError: + continue + raise RuntimeError('invalid table dimension accepted') + + +def calibrate(): + coordinate_controls() + result = [] + for k in range(1, 4): + words, histogram = brute_histogram(k) + for threshold in range(1, (1 << k)+1): + pruned = census(k, threshold) + expected = sum(histogram[threshold:]) + if words != pruned['canonical_words'] or expected != pruned['solutions']: + raise RuntimeError(f'unpruned threshold control disagrees at k={k}') + result.append({'k': k, 'canonical_words': words, 'solutions': histogram[-1]}) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--k', type=int, choices=range(1, MAX_K+1), default=5) + parser.add_argument('--threshold', type=int, default=None) + args = parser.parse_args() + print(json.dumps({'census': census(args.k, args.threshold), 'calibration': calibrate()}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/connector-char4-floor-obstructions/independent_check.py b/research/connector-char4-floor-obstructions/independent_check.py new file mode 100644 index 0000000000..0be03b20a4 --- /dev/null +++ b/research/connector-char4-floor-obstructions/independent_check.py @@ -0,0 +1,244 @@ +"""Independent outside-component and cyclic charge checks from literal states.""" +from itertools import combinations, product +from random import Random +from math import comb +import json +import hashlib +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def cycle_states(walk, k, start): + state = list(start) + states = [tuple(state)] + for source in walk: + state[source] = (state[source] + 1) % 4 + states.append(tuple(state)) + if states[0] != states[-1]: + raise ArithmeticError('cycle not restored') + return states + + +def component_stats(states, walk, first, last): + bad = [0] * len(states[0]) + internal = 0 + for t in range(first, last): + source = walk[t] + if states[t][source] == 0: + internal += 1 + else: + bad[source] += 1 + if any(count not in (0, 3) for count in bad): + raise ArithmeticError('source bad arc split between components') + d = sum(count == 3 for count in bad) + if d < 1 or last - first != 3 * d + internal: + raise ArithmeticError('component length formula fails') + seen = set() + repeated = [] + for t in range(first, last + 1): + parity = tuple(value % 2 for value in states[t]) + if parity in seen: + repeated.append(t) + seen.add(parity) + if internal == 0 and d <= 3 and len(repeated) < 2: + raise ArithmeticError('small component has fewer than two repeats') + return d, internal, repeated + + +def inspect(walk, k, origin): + states = cycle_states(walk, k, origin) + inside = [all(value <= 1 for value in state) for state in states] + if not any(inside): + return 0 + pivot = inside.index(True) + rotated = walk[pivot:] + walk[:pivot] + states = cycle_states(rotated, k, states[pivot]) + inside = [all(value <= 1 for value in state) for state in states] + vertices = [t for t, ok in enumerate(inside) if ok] + components = [(a, b) for a, b in zip(vertices, vertices[1:]) if b - a > 1] + stats = [component_stats(states, rotated, a, b) for a, b in components] + s = len(vertices) - 1 + small = sum(h == 0 and d <= 3 for d, h, repeats in stats) + internal_outside = sum(h for d, h, repeats in stats) + if sum(d for d, h, repeats in stats) != k or s != k - internal_outside + len(stats): + raise ArithmeticError('global edge/component accounting fails') + global_seen, global_repeats = set(), set() + for t, state in enumerate(states[:-1]): + value = tuple(v % 2 for v in state) + if value in global_seen: + global_repeats.add(t) + global_seen.add(value) + r = len(global_repeats) + charges = set() + for d, h, repeats in stats: + if h == 0 and d <= 3: + for t in repeats: + if t in charges or (t < len(walk) and t not in global_repeats): + raise ArithmeticError('duplicate or invalid parity charge') + charges.add(t) + if len(walk) in charges: + start, end = components[-1] + target = tuple(v % 2 for v in states[end]) + choices = [t for t in range(start + 1, end) + if tuple(v % 2 for v in states[t]) == target] + if not choices or choices[0] in charges or choices[0] not in global_repeats: + raise ArithmeticError('cyclic endpoint charge repair fails') + charges.remove(end) + charges.add(choices[0]) + capital_s = min(k, r // 2) + bound = k + capital_s + (k - capital_s) // 4 + if 2 * small > len(charges) or len(charges) > r or s > bound: + raise ArithmeticError('component charge/intersection bound fails') + return 1 + + +def compare_certificate(result): + certificate = json.loads((HERE / "CERTIFICATE.json").read_text()) + actual = [(r["r"], r["H"], r["upper"]) for r in result["rows"]] + expected = [(r["r"], r["cube_intersection"], r["mask_upper"]) for r in certificate["cube_control_rows"]] + if actual != expected or result["max_k19_upper"] != certificate["cube_control_max_mask_upper"]: + raise ArithmeticError("independent cube table differs from certificate") + if result["component_cases"] != 21120 or result["nonempty_cases"] != 20976: + raise ArithmeticError("independent component family incomplete") + + +def check_catalog(): + rows = json.loads((HERE / "MAXIMIZERS.json").read_text())["canonical_maximizers"] + if len(rows) != 4: + raise ArithmeticError("unexpected catalog size") + words = set() + for row in rows: + word = row["walk"] + if len(word) != 20 or any(word.count(j) != 4 for j in range(5)): + raise ArithmeticError("invalid catalog word") + order = list(dict.fromkeys(word)) + if order != list(range(5)) or tuple(word) in words: + raise ArithmeticError("catalog is noncanonical or duplicated") + words.add(tuple(word)) + q = cycle_states(word, 5, [0]*5) + masks = set() + for a, b in combinations(range(21), 2): + value = tuple((x+y) % 4 for x, y in zip(q[a], q[b])) + if max(value) <= 1: + masks.add(sum(x << j for j, x in enumerate(value))) + for a in range(21): + value = tuple(2*x % 4 for x in q[a]) + if max(value) <= 1: + masks.add(sum(x << j for j, x in enumerate(value))) + if len(masks) != 29 or [m for m in range(1, 32) if m not in masks] != row["missing"]: + raise ArithmeticError("independent catalog coverage differs") + if not all(set(word[t:t+5]) == set(range(5)) for t in range(0, 20, 5)): + raise ArithmeticError("catalog word lacks four permutation rounds") + + +def receipt(): + digest = hashlib.sha256() + names = ('PROOF17.md', 'axis_obstruction.py', 'n4_controls.py', 'CERTIFICATE.json', 'CUBE-SHARPNESS.json', 'README.md', 'SOURCES.json', 'TASK.json', 'VERIFY.json', 'DEPTH2.md', 'MAXIMIZERS.json', 'depth_two.py', 'independent_depth2.c', 'independent_check.py', 'verify.py') + for name in names: + digest.update(name.encode() + b"\0" + hashlib.sha256((HERE / name).read_bytes()).digest()) + return digest.hexdigest() + + +def check_sharpness(): + data = json.loads((HERE / "CUBE-SHARPNESS.json").read_text()) + word = data["word"] + if len(word) != 72 or any(word.count(j) != 4 for j in range(18)): + raise ArithmeticError("sharpness word multiplicities") + states = cycle_states(word, 18, [0]*18)[:-1] + parity = {tuple(v % 2 for v in q) for q in states} + inside = [t for t, q in enumerate(states) if all(v <= 1 for v in q)] + if len(parity) != 72 or len(inside) != 22 or inside != data["valid_boundaries"]: + raise ArithmeticError("independent sharpness check failed") + + +def check_seventeen(data): + """Recompute all base cases and both residual branches without producer code.""" + total, target = 72, 1 << 18 + values = comb(total, 3) - 105 * 70 + min(5 * 105, 22 * 18) + rows = [] + for repeats in range(21): + retained = total - repeats + cap = 18 + repeats // 2 + (18 - repeats // 2) // 4 + xedges, zedges = 210 - 2 * repeats, 263 - 13 * repeats + xbound = comb(total, 3) - 70 * xedges + min(8 * xedges, 70 * 18) + zbound = comb(retained, 3) - (retained - 2) * zedges + min(9 * zedges, 108 * 18) + numerator = 3 * values + (35 - cap) * xbound + (2 * cap - 38) * zbound + bound = 1 + comb(retained, 2) + numerator // 4 + rows.append({'r': repeats, 'cube_cap': cap, 'V_upper': values, + 'X_upper': xbound, 'Z_upper': zbound, + 'incidence_numerator': numerator, 'mask_upper': bound, + 'excluded': bound < target}) + exceptions = [row['r'] for row in rows if not row['excluded']] + if exceptions != [2, 4, 5]: + raise ArithmeticError('independent base cases leave unexpected exceptions') + residual = [] + for repeats, deletions in ((2, 2), (4, 4), (5, 4)): + row = rows[repeats] + vertices, edges = total - deletions, 210 - 2 * repeats - 9 * deletions + xbound = comb(vertices, 3) - edges * (vertices - 2) + min(8 * edges, 70 * 18) + cap = row['cube_cap'] + attained = 3 * values + (35 - cap) * xbound + (2 * cap - 38) * row['Z_upper'] + absent = 4 * values + (35 - cap) * row['X_upper'] + (2 * cap - 40) * row['Z_upper'] + pair_bound = 1 + comb(total - repeats, 2) + yes, no = pair_bound + attained // 4, pair_bound + absent // 4 + if max(yes, no) >= target: + raise ArithmeticError('independent residual branch does not exclude eighteen') + residual.append({'r': repeats, 'cube_cap': cap, 'axis_deletions': deletions, + 'X_vertices': vertices, 'X_edges_lower': edges, 'X_upper': xbound, + 'attained_H_upper': yes, 'not_attained_H_upper': no}) + tail = 1 + comb(51, 2) + comb(51, 4) + if tail >= target: + raise ArithmeticError('independent parity tail does not exclude eighteen') + expected = {'source_count': 18, 'target_masks_including_zero': target, + 'base_rows': rows, 'base_exceptions': exceptions, 'residual_rows': residual, + 'r_at_least_21_upper': tail} + if data != expected: + raise ArithmeticError('seventeen certificate differs from independent arithmetic') + return {'base_rows': len(rows), 'residual_branches': 2 * len(residual), + 'tail_bound': tail, 'result': 'PASS'} + + +def main(): + checked = nonempty = 0 + for zero in combinations(range(8), 4): + walk = [0 if t in zero else 1 for t in range(8)] + for origin in product(range(4), repeat=2): + nonempty += inspect(walk, 2, origin) + checked += 1 + rng = Random(102052) + for k in (3, 4, 9, 19): + for _ in range(100): + walk = [j for j in range(k) for _ in range(4)] + rng.shuffle(walk) + q = cycle_states(walk, k, [0] * k) + for _ in range(50): + point = rng.choice(q[:-1]) + origin = tuple((rng.randrange(2) - value) % 4 for value in point) + nonempty += inspect(walk, k, origin) + checked += 1 + rows = [] + for r in range(76): + capital_s = min(19, (r + 1) // 2) + h = 19 + capital_s + (19 - capital_s) // 4 + cube = comb(76, 3) * h // 4 + comb(76, 2) + 1 + n = 76 - r + parity = 1 + comb(n, 2) + comb(n, 4) if n >= 4 else 1 + comb(n, 2) + rows.append({'r': r, 'H': h, 'cube_bound': cube, 'parity_bound': parity, + 'upper': min(cube, parity)}) + if max(row['upper'] for row in rows) >= 1 << 19: + raise ArithmeticError('nineteen-source exclusion fails') + result = {'component_cases': checked, 'nonempty_cases': nonempty, + 'max_k19_upper': max(row['upper'] for row in rows), 'rows': rows} + compare_certificate(result) + check_catalog() + check_sharpness() + data = json.loads((HERE / "CERTIFICATE.json").read_text()) + print("independent_seventeen", json.dumps(check_seventeen(data["eighteen_exclusion"]["arithmetic"]), sort_keys=True)) + print(json.dumps({key: value for key, value in result.items() if key != 'rows'}, sort_keys=True)) + print('receipt_sha256', receipt()) + print('PASS_INDEPENDENT_CHAR4_OBSTRUCTIONS N4<=17') + + +if __name__ == '__main__': + main() diff --git a/research/connector-char4-floor-obstructions/independent_depth2.c b/research/connector-char4-floor-obstructions/independent_depth2.c new file mode 100644 index 0000000000..5be13353fe --- /dev/null +++ b/research/connector-char4-floor-obstructions/independent_depth2.c @@ -0,0 +1,153 @@ +/* Independent bounded iterative census; raw coordinates and generic tables. */ +#include +#include +#include +#include +#include + +#define MAX_K 5 +#define MAX_N 20 +#define MAX_NODES UINT64_C(100000000) +struct frame { int counts[MAX_K], introduced, next, entered; uint32_t served; }; +static struct frame frames[MAX_N + 1]; +static int history[MAX_N + 1][MAX_K]; +static uint64_t factorial[MAX_N + 1]; +static uint32_t cube[1 << (2 * MAX_K)]; +static int past_options[5][5], future_options[5]; +static int k, length; +static uint32_t full; +static int target; + +static int bit_count(uint32_t value) { + int result = 0; + for (int bit = 0; bit < 32; bit++) result += (int)((value >> bit) & 1U); + return result; +} + +static void make_tables(void) { + for (int current = 0; current <= 4; current++) { + for (int prior = 0; prior <= 4; prior++) { + for (int future = current; future <= 4; future++) { + int residue = (prior + future) % 4; + if (residue <= 1) past_options[current][prior] |= 1 << residue; + } + } + for (int a = current; a <= 4; a++) for (int b = a; b <= 4; b++) { + int residue = (a + b) % 4; + if (residue <= 1) future_options[current] |= 1 << residue; + } + } + for (int code = 0; code < (1 << (2 * k)); code++) { + for (int mask = 0; mask < (1 << k); mask++) { + int possible = 1; + for (int j = 0; j < k; j++) { + int options = (code >> (2 * j)) & 3; + if (!(options & (1 << ((mask >> j) & 1)))) possible = 0; + } + if (possible) cube[code] |= UINT32_C(1) << mask; + } + } +} + +static uint64_t completions(const struct frame *f, int depth) { + uint64_t denominator = factorial[k - f->introduced]; + for (int j = 0; j < k; j++) denominator *= factorial[4 - f->counts[j]]; + if (factorial[length - depth] % denominator != 0) exit(3); + return factorial[length - depth] / denominator; +} + +static uint32_t update_served(uint32_t served, int depth) { + for (int t = 0; t <= depth; t++) { + int mask = 0, valid = 1; + for (int j = 0; j < k; j++) { + int residue = (history[t][j] + history[depth][j]) % 4; + if (residue > 1) { valid = 0; break; } + mask |= residue << j; + } + if (valid) served |= UINT32_C(1) << mask; + } + return served; +} + +static uint32_t possible_masks(uint32_t served, int depth) { + int code = 0; + for (int j = 0; j < k; j++) code |= future_options[history[depth][j]] << (2 * j); + uint32_t possible = served | cube[code]; + for (int t = 0; t <= depth && possible != full; t++) { + code = 0; + for (int j = 0; j < k; j++) + code |= past_options[history[depth][j]][history[t][j]] << (2 * j); + possible |= cube[code]; + } + return possible; +} + +static int census(int pruning) { + uint64_t nodes = 0, pruned = 0, accounted = 0, solutions = 0, leaves = 0; + uint64_t pruned_depth[MAX_N + 1] = {0}; + int depth = 0; + frames[0].served = 1; + for (uint64_t steps = 0; steps < MAX_NODES * 3 && depth >= 0; steps++) { + struct frame *f = &frames[depth]; + if (!f->entered) { + f->entered = 1; + if (++nodes > MAX_NODES) return 4; + f->served = update_served(f->served, depth); + uint32_t possible = pruning ? possible_masks(f->served, depth) : full; + if (bit_count(f->served) >= target || bit_count(possible) < target || depth == length) { + uint64_t ways = completions(f, depth); + accounted += ways; + if (bit_count(f->served) >= target) solutions += ways; + else if (bit_count(possible) < target) { pruned++; pruned_depth[depth]++; } + else leaves++; + depth--; + continue; + } + } + int j = f->next; + for (; j < k && j <= f->introduced; j++) if (f->counts[j] < 4) break; + f->next = j + 1; + if (j == k || j > f->introduced) { depth--; continue; } + struct frame child = *f; + child.counts[j]++; + child.introduced += j == f->introduced; + child.next = 0; + child.entered = 0; + depth++; + frames[depth] = child; + for (int v = 0; v < k; v++) history[depth][v] = child.counts[v]; + } + uint64_t denominator = factorial[k]; + for (int j = 0; j < k; j++) denominator *= factorial[4]; + uint64_t expected = factorial[length] / denominator; + if (printf("{\"k\":%d,\"target\":%d,\"pruning\":%d,\"nodes\":%" PRIu64 ",\"pruned\":%" PRIu64 + ",\"accounted\":%" PRIu64 ",\"expected\":%" PRIu64 ",\"solutions\":%" PRIu64 + ",\"leaves\":%" PRIu64 ",\"pruned_depth\":[", k, target, pruning, nodes, pruned, + accounted, expected, solutions, leaves) < 0) return 6; + for (int t = 0; t <= length; t++) + if (printf("%s%" PRIu64, t ? "," : "", pruned_depth[t]) < 0) return 6; + if (puts("]}") == EOF || fflush(stdout) == EOF) return 6; + return depth == -1 && accounted == expected ? 0 : 5; +} + +int main(int argc, char **argv) { + if (argc != 4) return 2; + char *tail = NULL; + errno = 0; + long requested = strtol(argv[1], &tail, 10); + if (errno || tail == argv[1] || *tail || requested < 1 || requested > MAX_K) return 2; + k = (int)requested; + errno = 0; + requested = strtol(argv[2], &tail, 10); + if (errno || tail == argv[2] || *tail || (requested != 0 && requested != 1)) return 2; + errno = 0; + long wanted = strtol(argv[3], &tail, 10); + if (errno || tail == argv[3] || *tail || wanted < 1 || wanted > (1 << k)) return 2; + target = (int)wanted; + length = 4 * k; + full = (uint32_t)((UINT64_C(1) << (1 << k)) - 1); + factorial[0] = 1; + for (int i = 1; i <= length; i++) factorial[i] = factorial[i - 1] * (uint64_t)i; + make_tables(); + return census((int)requested); +} diff --git a/research/connector-char4-floor-obstructions/n4_controls.py b/research/connector-char4-floor-obstructions/n4_controls.py new file mode 100644 index 0000000000..a361a5f137 --- /dev/null +++ b/research/connector-char4-floor-obstructions/n4_controls.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Bounded standard-library controls for the characteristic-four upper bound.""" + +from collections import defaultdict +from itertools import combinations, combinations_with_replacement, product +import json +from math import comb +from random import Random + +# Each coordinate occupies one nibble. A four-prefix sum has coordinate +# digit at most twelve, so addition cannot carry into another coordinate. +# Bit one of each nibble detects residues two or three modulo four. + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def packed_prefixes(word, k): + require(1 <= k <= 19, "control source range") + require(len(word) == 4 * k, "control word length") + require(all(word.count(j) == 4 for j in range(k)), "source multiplicities") + values = [] + counts = [0] * k + for symbol in word: + values.append(sum(count << (4 * j) for j, count in enumerate(counts))) + counts[symbol] = (counts[symbol] + 1) % 4 + require(all(count == 0 for count in counts), "restoration") + low_mask = sum(1 << (4 * j) for j in range(k)) + r = 4 * k - len({value & low_mask for value in values}) + return values, r + + +def cube_cap(k, r): + small = min(k, r // 2) + return k + small + (k - small) // 4 + + +def pair_graphs(word, k): + events = [[] for _ in range(k)] + y, xy, full = set(), set(), set() + for b, symbol in enumerate(word[:-1], 1): + previous = events[symbol] + if previous: + full.add((b - 1, b)) + for a in previous: + y.add((a - 1, b)) + xy.add((a - 1, b)) + xy.add((a, b)) + full.add((a - 1, b)) + full.add((a, b)) + previous.append(b) + return y, xy, full + + +def graph_degrees(graph, length): + degrees = [0] * length + for a, b in graph: + degrees[a] += 1 + degrees[b] += 1 + return max(degrees), sum(d * (d - 1) // 2 for d in degrees) + + +def inspect_graph_cube(word, k, offsets): + values, r = packed_prefixes(word, k) + families = pair_graphs(word, k) + for graph, degree, wedges in zip(families, (6, 9, 10), (22 * k, 70 * k, 108 * k)): + actual_degree, actual_wedges = graph_degrees(graph, 4 * k) + require(actual_degree <= degree, "maximum degree") + require(actual_wedges <= wedges, "rank wedge bound") + require(len(families[0]) == 6 * k - 3, "Y pair count") + require(len(families[1]) >= 12 * k - 6 - 2 * r, "XY pair count") + low = sum(1 << (4 * j) for j in range(k)) + retained, seen = set(), set() + for index, value in enumerate(values): + if value & low not in seen: + retained.add(index) + seen.add(value & low) + induced = {(a, b) for a, b in families[2] if a in retained and b in retained} + require(len(induced) >= 15 * k - 7 - 13 * r, "retained full pair count") + for offset in offsets: + actual = sum(not ((value + offset) & (2 * low)) for value in values) + require(actual <= cube_cap(k, r), "strengthened cyclic cube cap") + return len(offsets) + + +def small_graph_cube_controls(): + checked, words = 0, 0 + for k in (2, 3): + offsets = tuple(sum(x << (4 * j) for j, x in enumerate(v)) + for v in product(range(4), repeat=k)) + positions = tuple(range(4 * k)) + for zero in combinations(positions, 4): + rest = tuple(t for t in positions if t not in zero) + choices = (rest,) if k == 2 else combinations(rest, 4) + for one in choices: + word = [2] * (4 * k) + for t in zero: + word[t] = 0 + for t in one: + word[t] = 1 + checked += inspect_graph_cube(word, k, offsets) + words += 1 + return words, checked + + +def large_graph_cube_controls(): + rng = Random(1020230) + checked = 0 + for k in (4, 9, 18, 19): + for _ in range(1000): + word = [j for j in range(k) for _ in range(4)] + rng.shuffle(word) + offsets = tuple(sum(rng.randrange(4) << (4 * j) for j in range(k)) + for _ in range(100)) + checked += inspect_graph_cube(word, k, offsets) + return checked + + +def full_components(full_values, k): + labels = {} + count = 0 + for value in full_values: + if value in labels: + continue + queue = [value] + labels[value] = count + for _ in range(len(full_values)): + if not queue: + break + current = queue.pop() + for j in range(k): + neighbor = current ^ (2 << (4 * j)) + if neighbor in full_values and neighbor not in labels: + labels[neighbor] = count + queue.append(neighbor) + require(not queue, "component work bound") + count += 1 + return labels, count + + +def triple_classes(values, k): + low = sum(1 << (4 * j) for j in range(k)) + prefix_parity = {value & low for value in values} + groups = defaultdict(set) + triples = [] + for indices in combinations(range(len(values)), 3): + full = sum(values[t] for t in indices) & (3 * low) + parity = full & low + if parity not in prefix_parity: + groups[parity].add(full) + triples.append((indices, full)) + full_values = set().union(*groups.values()) if groups else set() + labels, count = full_components(full_values, k) + return groups, full_values, labels, count, triples + + +def axis_colex_controls(k, values, r, labels, count, triples): + axes = {2 << (4 * j) for j in range(k)} + deleted = {b for b in range(len(values)) + if any(values[a] ^ values[b] in axes for a in range(b))} + leaders = {} + for indices, full in triples: + encoded = sum(1 << t for t in indices) + label = labels[full] + if label not in leaders or encoded < leaders[label]: + leaders[label] = encoded + forbidden = sum(1 << t for t in deleted) + require(all(not leader & forbidden for leader in leaders.values()), "axis colex leader") + selected = set(sorted(deleted)[:4]) + q = len(selected) + n = len(values) - q + edge_lower = max(0, 12 * k - 6 - 2 * r - 9 * q) + bound = comb(n, 3) - edge_lower * (n - 2) + min(8 * edge_lower, 70 * k) + require(count <= bound, "axis-deletion component count") + + +def inspect_incidence(word, k): + values, r = packed_prefixes(word, k) + low = sum(1 << (4 * j) for j in range(k)) + groups, full_values, labels, xcomp, triples = triple_classes(values, k) + cap = cube_cap(k, r) + incidences = 0 + for parity, group in groups.items(): + components = len({labels[value] for value in group}) + eligible = {t for t, prefix in enumerate(values) + if any(not ((prefix + full) & (2 * low)) for full in group)} + require(len(eligible) <= 3 * len(group) + (cap - 3) * components, + "free-slab component count") + require(len(eligible) <= 2 * len(group) + 2 * k - 2, "union component count") + incidences += len({parity ^ (values[t] & low) for t in eligible}) + upper = (3 * len(full_values) + (2 * k - cap - 1) * xcomp + + (2 * cap - 2 * k - 2) * len(groups)) + require(incidences <= upper, "merged class incidence") + prefix_parity = {value & low for value in values} + pairs = {0} | {a ^ b for a, b in combinations(prefix_parity, 2)} + masks = set() + for readout in combinations_with_replacement(values, 4): + total = sum(readout) + if not total & (2 * low): + masks.add(total & low) + require(4 * len(masks - pairs) <= incidences, "four distinct parity classes") + axis_colex_controls(k, values, r, labels, xcomp, triples) + + +def incidence_controls(): + rng = Random(1020230) + checked = 0 + for k in (5, 6, 9): + for _ in range(20): + word = [j for j in range(k) for _ in range(4)] + rng.shuffle(word) + inspect_incidence(word, k) + checked += 1 + return checked + + +def run_controls(): + words, small = small_graph_cube_controls() + large = large_graph_cube_controls() + incidence = incidence_controls() + return {"small_words": words, "small_translations": small, + "large_words": 4000, "large_translations": large, + "incidence_axis_words": incidence, "result": "PASS"} + + +if __name__ == "__main__": + print(json.dumps(run_controls(), indent=2, sort_keys=True)) diff --git a/research/connector-char4-floor-obstructions/verify.py b/research/connector-char4-floor-obstructions/verify.py new file mode 100644 index 0000000000..403eb625af --- /dev/null +++ b/research/connector-char4-floor-obstructions/verify.py @@ -0,0 +1,203 @@ +#!/usr/bin/env python3 +"""Replay exact arithmetic and finite controls for characteristic-four floor obstructions.""" + +from itertools import combinations, product +from math import comb +from random import Random +import json +import hashlib +from pathlib import Path +import sys +from depth_two import census, calibrate, canonical, served_by_pairs +from axis_obstruction import evaluate as axis_evaluate, calibrate as axis_calibrate +from n4_controls import run_controls as structural_controls + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def limit(k, r): + small = min(k, (r + 1) // 2) + return k + small + (k - small) // 4 + + +def packed_prefixes(word, k): + require(len(word) == 4 * k, "length") + require(all(word.count(j) == 4 for j in range(k)), "multiplicities") + values = [0] + counts = [0] * k + for symbol in word[:-1]: + counts[symbol] = (counts[symbol] + 1) % 4 + values.append(sum(count << (4 * j) for j, count in enumerate(counts))) + parity_mask = sum(1 << (4 * j) for j in range(k)) + r = 4 * k - len({value & parity_mask for value in values}) + return values, r + + +def inspect_word(word, k, offsets): + values, r = packed_prefixes(word, k) + bad_mask = sum(2 << (4 * j) for j in range(k)) + upper = limit(k, r) + maximum = 0 + for offset in offsets: + actual = sum(not ((value + offset) & bad_mask) for value in values) + require(actual <= upper, f"intersection bound: {word}, {offset}, {r}, {actual}, {upper}") + maximum = max(maximum, actual) + return maximum + + +def exhaustive_small(): + words = 0 + translations = 0 + for k in (2, 3): + offsets = tuple(sum(x << (4 * j) for j, x in enumerate(v)) + for v in product(range(4), repeat=k)) + positions = tuple(range(4 * k)) + for zero in combinations(positions, 4): + rest = tuple(t for t in positions if t not in zero) + choices = (rest,) if k == 2 else combinations(rest, 4) + for one in choices: + word = [2] * (4 * k) + for t in zero: + word[t] = 0 + for t in one: + word[t] = 1 + inspect_word(word, k, offsets) + words += 1 + translations += len(offsets) + return words, translations + + +def random_large(): + rng = Random(102019) + checked = 0 + for k in (4, 9, 18, 19): + for _ in range(1000): + word = [j for j in range(k) for _ in range(4)] + rng.shuffle(word) + offsets = tuple(sum(rng.randrange(4) << (4 * j) for j in range(k)) + for _ in range(100)) + inspect_word(word, k, offsets) + checked += 1 + return checked + + +def arithmetic(): + rows = [] + for r in range(76): + n = 76 - r + cube = comb(76, 3) * limit(19, r) // 4 + comb(76, 2) + 1 + parity = 1 + comb(n, 2) + comb(n, 4) + upper = min(cube, parity) + require(upper < 1 << 19, "nineteen-source strict exclusion") + rows.append({"r": r, "cube_intersection": limit(19, r), "mask_upper": upper}) + return rows + + +def inventory_normal_form(): + compositions = [v for v in product(range(5), repeat=4) if sum(v) == 4] + types = sorted(v for v in compositions if (3*v[0] + 2*v[1] + v[2]) % 4 == 1) + rotations = set() + for template in ((3, 0, 0, 1), (0, 2, 1, 1)): + for shift in range(4): + rotations.add(template[shift:] + template[:shift]) + require(len(compositions) == 35, "inventory composition count") + require(set(types) == rotations and len(types) == 8, "inventory types") + require(all(0 in row for row in types), "every inventory must miss a gap") + return {"weak_compositions": len(compositions), "types": [list(v) for v in types], + "type_count_vectors_k10": comb(17, 7)} + + +def check_maximizers(): + rows = json.loads((HERE / "MAXIMIZERS.json").read_text())["canonical_maximizers"] + require(len(rows) == 4, "maximizer catalog size") + seen = set() + for row in rows: + word = row["walk"] + require(canonical(word), "maximizer is not first-occurrence canonical") + require(tuple(word) not in seen, "duplicate maximizer") + seen.add(tuple(word)) + reached = served_by_pairs(word, 5) + missing = [m for m in range(1, 32) if not (reached >> m) & 1] + require(reached.bit_count() == 29 and row["covered_nonzero"] == 28, + "maximizer coverage") + require(row["missing"] == missing, "maximizer missing masks") + rounds = all(sorted(word[t:t+5]) == list(range(5)) for t in range(0, 20, 5)) + require(rounds and row["permutation_rounds"], "maximizer round structure") + return len(rows) + + +def check_cube_sharpness(): + data = json.loads((HERE / "CUBE-SHARPNESS.json").read_text()) + require(data["k"] == 18 and data["cube_translate"] == [0]*18, "sharpness scope") + values, repeated = packed_prefixes(data["word"], 18) + high = sum(2 << (4*j) for j in range(18)) + inside = [t for t, value in enumerate(values) if not value & high] + require(repeated == data["parity_repetitions"] == 0, "sharpness parity repeats") + require(len(inside) == data["cube_intersection"] == limit(18, 0) == 22, + "sharpness intersection") + require(inside == data["valid_boundaries"], "sharpness boundary list") + groups = data["bad_arc_groups"] + require([len(g) for g in groups] == [4, 4, 5, 5], "sharpness groups") + require(sorted(j for g in groups for j in g) == list(range(18)), "group partition") + word = data["word"] + require(word[:18] == list(range(18)), "sharpness initial calls") + offset = 18 + for group in groups: + length = 3*len(group) + require(sorted(word[offset:offset+length]) == sorted(group*3), "bad arc inventory") + offset += length + return {"k": 18, "parity_repetitions": repeated, "cube_intersection": len(inside), + "valid_boundaries": inside} + + +def depth_two_results(): + data = {"k4": census(4), "k5_full": census(5), + "k5_at_least_30": census(5, 30), "k5_at_least_29": census(5, 29), + "calibration": calibrate(), "maximizer_count": check_maximizers()} + require(data["k5_at_least_30"]["solutions"] == 0, "depth-two maximum exceeds 29") + require(data["k5_at_least_29"]["solutions"] == data["maximizer_count"], + "maximizer catalog is incomplete") + return data + + +def receipt(): + digest = hashlib.sha256() + names = ('PROOF17.md', 'axis_obstruction.py', 'n4_controls.py', 'CERTIFICATE.json', 'CUBE-SHARPNESS.json', 'README.md', 'SOURCES.json', 'TASK.json', 'VERIFY.json', 'DEPTH2.md', 'MAXIMIZERS.json', 'depth_two.py', 'independent_depth2.c', 'independent_check.py', 'verify.py') + for name in names: + digest.update(name.encode() + b"\0" + hashlib.sha256((HERE / name).read_bytes()).digest()) + return digest.hexdigest() + + +def main(): + require(sys.argv[1:] in ([], ["--write-certificate"]), "unexpected arguments") + rows = arithmetic() + words, translations = exhaustive_small() + large_words = random_large() + result = {"claim": "9<=N(4)<=17", "cube_control_rows": rows, + "small_words": words, "small_translations": translations, + "random_words": large_words, + "cube_control_source_count": 19, + "cube_control_max_mask_upper": max(row["mask_upper"] for row in rows), + "eighteen_exclusion": {"arithmetic": axis_evaluate(), "controls": axis_calibrate()}, + "structural_controls": structural_controls(), + "inventory_normal_form": inventory_normal_form(), + "cube_sharpness": check_cube_sharpness(), + "depth_two": depth_two_results()} + if sys.argv[1:]: + (HERE / "CERTIFICATE.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + require(result == json.loads((HERE / "CERTIFICATE.json").read_text()), + "certificate differs from recomputation") + print(json.dumps({"claim": result["claim"], "k18_residual_branches": 6, + "depth2_max_nonzero": 28, "canonical_maximizers": 4}, sort_keys=True)) + print("receipt_sha256", receipt()) + print("PASS_CONNECTOR_CHAR4_FLOOR_OBSTRUCTIONS N4<=17 depth2_max=4 depth2_k5_coverage=28") + + +if __name__ == "__main__": + main()