diff --git a/research/e8-joint-reader-bound/CERTIFICATE.json b/research/e8-joint-reader-bound/CERTIFICATE.json new file mode 100644 index 0000000000..89ebb9c1a7 --- /dev/null +++ b/research/e8-joint-reader-bound/CERTIFICATE.json @@ -0,0 +1,3115 @@ +{ + "assignment_seed": 46, + "base_commit": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", + "bounds": [ + { + "combined_lower_bound": 72, + "minimizing_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "punctures": 0, + "ratio_lower_bound": "3/5", + "relaxed_pair_cost": 72 + }, + { + "combined_lower_bound": 71, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 1, + "ratio_lower_bound": "71/119", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 70, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 2, + "ratio_lower_bound": "35/59", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 69, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 3, + "ratio_lower_bound": "23/39", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 68, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 4, + "ratio_lower_bound": "17/29", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 67, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 5, + "ratio_lower_bound": "67/115", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 66, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 6, + "ratio_lower_bound": "11/19", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 65, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 7, + "ratio_lower_bound": "65/113", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 64, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 8, + "ratio_lower_bound": "4/7", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 9, + "ratio_lower_bound": "21/37", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 10, + "ratio_lower_bound": "63/110", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 11, + "ratio_lower_bound": "63/109", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 12, + "ratio_lower_bound": "7/12", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 13, + "ratio_lower_bound": "63/107", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 14, + "ratio_lower_bound": "63/106", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 15, + "ratio_lower_bound": "3/5", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 16, + "ratio_lower_bound": "63/104", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 17, + "ratio_lower_bound": "63/103", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 18, + "ratio_lower_bound": "21/34", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 19, + "ratio_lower_bound": "63/101", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 20, + "ratio_lower_bound": "63/100", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 21, + "ratio_lower_bound": "7/11", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 22, + "ratio_lower_bound": "9/14", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 23, + "ratio_lower_bound": "63/97", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 24, + "ratio_lower_bound": "21/32", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 63, + "minimizing_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "punctures": 25, + "ratio_lower_bound": "63/95", + "relaxed_pair_cost": 63 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 26, + "ratio_lower_bound": "27/47", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 27, + "ratio_lower_bound": "18/31", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 28, + "ratio_lower_bound": "27/46", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 29, + "ratio_lower_bound": "54/91", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 30, + "ratio_lower_bound": "3/5", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 31, + "ratio_lower_bound": "54/89", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 32, + "ratio_lower_bound": "27/44", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 33, + "ratio_lower_bound": "18/29", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 34, + "ratio_lower_bound": "27/43", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 54, + "minimizing_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 35, + "ratio_lower_bound": "54/85", + "relaxed_pair_cost": 54 + }, + { + "combined_lower_bound": 53, + "minimizing_ranks": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 36, + "ratio_lower_bound": "53/84", + "relaxed_pair_cost": 53 + }, + { + "combined_lower_bound": 53, + "minimizing_ranks": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 37, + "ratio_lower_bound": "53/83", + "relaxed_pair_cost": 53 + }, + { + "combined_lower_bound": 53, + "minimizing_ranks": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 38, + "ratio_lower_bound": "53/82", + "relaxed_pair_cost": 53 + }, + { + "combined_lower_bound": 53, + "minimizing_ranks": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 39, + "ratio_lower_bound": "53/81", + "relaxed_pair_cost": 53 + }, + { + "combined_lower_bound": 53, + "minimizing_ranks": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 40, + "ratio_lower_bound": "53/80", + "relaxed_pair_cost": 53 + }, + { + "combined_lower_bound": 53, + "minimizing_ranks": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 41, + "ratio_lower_bound": "53/79", + "relaxed_pair_cost": 53 + }, + { + "combined_lower_bound": 53, + "minimizing_ranks": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 42, + "ratio_lower_bound": "53/78", + "relaxed_pair_cost": 53 + }, + { + "combined_lower_bound": 53, + "minimizing_ranks": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "punctures": 43, + "ratio_lower_bound": "53/77", + "relaxed_pair_cost": 53 + }, + { + "combined_lower_bound": 45, + "minimizing_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 44, + "ratio_lower_bound": "45/76", + "relaxed_pair_cost": 45 + }, + { + "combined_lower_bound": 45, + "minimizing_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 45, + "ratio_lower_bound": "3/5", + "relaxed_pair_cost": 45 + }, + { + "combined_lower_bound": 45, + "minimizing_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 46, + "ratio_lower_bound": "45/74", + "relaxed_pair_cost": 45 + }, + { + "combined_lower_bound": 45, + "minimizing_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 47, + "ratio_lower_bound": "45/73", + "relaxed_pair_cost": 45 + }, + { + "combined_lower_bound": 45, + "minimizing_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 48, + "ratio_lower_bound": "5/8", + "relaxed_pair_cost": 45 + }, + { + "combined_lower_bound": 45, + "minimizing_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 49, + "ratio_lower_bound": "45/71", + "relaxed_pair_cost": 45 + }, + { + "combined_lower_bound": 45, + "minimizing_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 50, + "ratio_lower_bound": "9/14", + "relaxed_pair_cost": 45 + }, + { + "combined_lower_bound": 45, + "minimizing_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 51, + "ratio_lower_bound": "15/23", + "relaxed_pair_cost": 45 + }, + { + "combined_lower_bound": 44, + "minimizing_ranks": [ + 4, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 52, + "ratio_lower_bound": "11/17", + "relaxed_pair_cost": 44 + }, + { + "combined_lower_bound": 44, + "minimizing_ranks": [ + 4, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 53, + "ratio_lower_bound": "44/67", + "relaxed_pair_cost": 44 + }, + { + "combined_lower_bound": 44, + "minimizing_ranks": [ + 4, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 54, + "ratio_lower_bound": "2/3", + "relaxed_pair_cost": 44 + }, + { + "combined_lower_bound": 44, + "minimizing_ranks": [ + 4, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "punctures": 55, + "ratio_lower_bound": "44/65", + "relaxed_pair_cost": 44 + } + ], + "coverage": { + "Weyl_generators": 8, + "distinct_reader_pairs": 130305, + "nonzero_readers": 511, + "puncture_budgets": 56, + "random_search": false, + "standard_flats": 256 + }, + "flat_census": [ + { + "dimension": 0, + "minimum_deletions": 56, + "root_lines": 0, + "simple_subset": 0 + }, + { + "dimension": 1, + "minimum_deletions": 55, + "root_lines": 1, + "simple_subset": 1 + }, + { + "dimension": 1, + "minimum_deletions": 55, + "root_lines": 1, + "simple_subset": 2 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 3 + }, + { + "dimension": 1, + "minimum_deletions": 55, + "root_lines": 1, + "simple_subset": 4 + }, + { + "dimension": 2, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 5 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 6 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 7 + }, + { + "dimension": 1, + "minimum_deletions": 55, + "root_lines": 1, + "simple_subset": 8 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 9 + }, + { + "dimension": 2, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 10 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 11 + }, + { + "dimension": 2, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 12 + }, + { + "dimension": 3, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 13 + }, + { + "dimension": 3, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 14 + }, + { + "dimension": 4, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 15 + }, + { + "dimension": 1, + "minimum_deletions": 55, + "root_lines": 1, + "simple_subset": 16 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 17 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 18 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 19 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 20 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 21 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 22 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 23 + }, + { + "dimension": 2, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 24 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 25 + }, + { + "dimension": 3, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 26 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 27 + }, + { + "dimension": 3, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 28 + }, + { + "dimension": 4, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 29 + }, + { + "dimension": 4, + "minimum_deletions": 44, + "root_lines": 12, + "simple_subset": 30 + }, + { + "dimension": 5, + "minimum_deletions": 36, + "root_lines": 20, + "simple_subset": 31 + }, + { + "dimension": 1, + "minimum_deletions": 55, + "root_lines": 1, + "simple_subset": 32 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 33 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 34 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 35 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 36 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 37 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 38 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 39 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 40 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 41 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 42 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 43 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 44 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 45 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 46 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 47 + }, + { + "dimension": 2, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 48 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 49 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 50 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 51 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 52 + }, + { + "dimension": 4, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 53 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 54 + }, + { + "dimension": 5, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 55 + }, + { + "dimension": 3, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 56 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 57 + }, + { + "dimension": 4, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 58 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 59 + }, + { + "dimension": 4, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 60 + }, + { + "dimension": 5, + "minimum_deletions": 41, + "root_lines": 15, + "simple_subset": 61 + }, + { + "dimension": 5, + "minimum_deletions": 36, + "root_lines": 20, + "simple_subset": 62 + }, + { + "dimension": 6, + "minimum_deletions": 28, + "root_lines": 36, + "simple_subset": 63 + }, + { + "dimension": 1, + "minimum_deletions": 55, + "root_lines": 1, + "simple_subset": 64 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 65 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 66 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 67 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 68 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 69 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 70 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 71 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 72 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 73 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 74 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 75 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 76 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 77 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 78 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 79 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 80 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 81 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 82 + }, + { + "dimension": 4, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 83 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 84 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 85 + }, + { + "dimension": 4, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 86 + }, + { + "dimension": 5, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 87 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 88 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 89 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 90 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 91 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 92 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 93 + }, + { + "dimension": 5, + "minimum_deletions": 43, + "root_lines": 13, + "simple_subset": 94 + }, + { + "dimension": 6, + "minimum_deletions": 35, + "root_lines": 21, + "simple_subset": 95 + }, + { + "dimension": 2, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 96 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 97 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 98 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 99 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 100 + }, + { + "dimension": 4, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 101 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 102 + }, + { + "dimension": 5, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 103 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 104 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 105 + }, + { + "dimension": 4, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 106 + }, + { + "dimension": 5, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 107 + }, + { + "dimension": 4, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 108 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 109 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 110 + }, + { + "dimension": 6, + "minimum_deletions": 43, + "root_lines": 13, + "simple_subset": 111 + }, + { + "dimension": 3, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 112 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 113 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 114 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 115 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 116 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 117 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 118 + }, + { + "dimension": 6, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 119 + }, + { + "dimension": 4, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 120 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 121 + }, + { + "dimension": 5, + "minimum_deletions": 41, + "root_lines": 15, + "simple_subset": 122 + }, + { + "dimension": 6, + "minimum_deletions": 40, + "root_lines": 16, + "simple_subset": 123 + }, + { + "dimension": 5, + "minimum_deletions": 41, + "root_lines": 15, + "simple_subset": 124 + }, + { + "dimension": 6, + "minimum_deletions": 35, + "root_lines": 21, + "simple_subset": 125 + }, + { + "dimension": 6, + "minimum_deletions": 26, + "root_lines": 30, + "simple_subset": 126 + }, + { + "dimension": 7, + "minimum_deletions": 1, + "root_lines": 63, + "simple_subset": 127 + }, + { + "dimension": 1, + "minimum_deletions": 55, + "root_lines": 1, + "simple_subset": 128 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 129 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 130 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 131 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 132 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 133 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 134 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 135 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 136 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 137 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 138 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 139 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 140 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 141 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 142 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 143 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 144 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 145 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 146 + }, + { + "dimension": 4, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 147 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 148 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 149 + }, + { + "dimension": 4, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 150 + }, + { + "dimension": 5, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 151 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 152 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 153 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 154 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 155 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 156 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 157 + }, + { + "dimension": 5, + "minimum_deletions": 43, + "root_lines": 13, + "simple_subset": 158 + }, + { + "dimension": 6, + "minimum_deletions": 35, + "root_lines": 21, + "simple_subset": 159 + }, + { + "dimension": 2, + "minimum_deletions": 54, + "root_lines": 2, + "simple_subset": 160 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 161 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 162 + }, + { + "dimension": 4, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 163 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 164 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 165 + }, + { + "dimension": 4, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 166 + }, + { + "dimension": 5, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 167 + }, + { + "dimension": 3, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 168 + }, + { + "dimension": 4, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 169 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 170 + }, + { + "dimension": 5, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 171 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 172 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 173 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 174 + }, + { + "dimension": 6, + "minimum_deletions": 44, + "root_lines": 12, + "simple_subset": 175 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 176 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 177 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 178 + }, + { + "dimension": 5, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 179 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 180 + }, + { + "dimension": 5, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 181 + }, + { + "dimension": 5, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 182 + }, + { + "dimension": 6, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 183 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 184 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 185 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 186 + }, + { + "dimension": 6, + "minimum_deletions": 44, + "root_lines": 12, + "simple_subset": 187 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 188 + }, + { + "dimension": 6, + "minimum_deletions": 40, + "root_lines": 16, + "simple_subset": 189 + }, + { + "dimension": 6, + "minimum_deletions": 35, + "root_lines": 21, + "simple_subset": 190 + }, + { + "dimension": 7, + "minimum_deletions": 27, + "root_lines": 37, + "simple_subset": 191 + }, + { + "dimension": 2, + "minimum_deletions": 53, + "root_lines": 3, + "simple_subset": 192 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 193 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 194 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 195 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 196 + }, + { + "dimension": 4, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 197 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 198 + }, + { + "dimension": 5, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 199 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 200 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 201 + }, + { + "dimension": 4, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 202 + }, + { + "dimension": 5, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 203 + }, + { + "dimension": 4, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 204 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 205 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 206 + }, + { + "dimension": 6, + "minimum_deletions": 43, + "root_lines": 13, + "simple_subset": 207 + }, + { + "dimension": 3, + "minimum_deletions": 52, + "root_lines": 4, + "simple_subset": 208 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 209 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 210 + }, + { + "dimension": 5, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 211 + }, + { + "dimension": 4, + "minimum_deletions": 51, + "root_lines": 5, + "simple_subset": 212 + }, + { + "dimension": 5, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 213 + }, + { + "dimension": 5, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 214 + }, + { + "dimension": 6, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 215 + }, + { + "dimension": 4, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 216 + }, + { + "dimension": 5, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 217 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 218 + }, + { + "dimension": 6, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 219 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 220 + }, + { + "dimension": 6, + "minimum_deletions": 43, + "root_lines": 13, + "simple_subset": 221 + }, + { + "dimension": 6, + "minimum_deletions": 41, + "root_lines": 15, + "simple_subset": 222 + }, + { + "dimension": 7, + "minimum_deletions": 33, + "root_lines": 23, + "simple_subset": 223 + }, + { + "dimension": 3, + "minimum_deletions": 50, + "root_lines": 6, + "simple_subset": 224 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 225 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 226 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 227 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 228 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 229 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 230 + }, + { + "dimension": 6, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 231 + }, + { + "dimension": 4, + "minimum_deletions": 49, + "root_lines": 7, + "simple_subset": 232 + }, + { + "dimension": 5, + "minimum_deletions": 48, + "root_lines": 8, + "simple_subset": 233 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 234 + }, + { + "dimension": 6, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 235 + }, + { + "dimension": 5, + "minimum_deletions": 47, + "root_lines": 9, + "simple_subset": 236 + }, + { + "dimension": 6, + "minimum_deletions": 44, + "root_lines": 12, + "simple_subset": 237 + }, + { + "dimension": 6, + "minimum_deletions": 44, + "root_lines": 12, + "simple_subset": 238 + }, + { + "dimension": 7, + "minimum_deletions": 40, + "root_lines": 16, + "simple_subset": 239 + }, + { + "dimension": 4, + "minimum_deletions": 46, + "root_lines": 10, + "simple_subset": 240 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 241 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 242 + }, + { + "dimension": 6, + "minimum_deletions": 44, + "root_lines": 12, + "simple_subset": 243 + }, + { + "dimension": 5, + "minimum_deletions": 45, + "root_lines": 11, + "simple_subset": 244 + }, + { + "dimension": 6, + "minimum_deletions": 43, + "root_lines": 13, + "simple_subset": 245 + }, + { + "dimension": 6, + "minimum_deletions": 44, + "root_lines": 12, + "simple_subset": 246 + }, + { + "dimension": 7, + "minimum_deletions": 43, + "root_lines": 14, + "simple_subset": 247 + }, + { + "dimension": 5, + "minimum_deletions": 41, + "root_lines": 15, + "simple_subset": 248 + }, + { + "dimension": 6, + "minimum_deletions": 40, + "root_lines": 16, + "simple_subset": 249 + }, + { + "dimension": 6, + "minimum_deletions": 35, + "root_lines": 21, + "simple_subset": 250 + }, + { + "dimension": 7, + "minimum_deletions": 35, + "root_lines": 22, + "simple_subset": 251 + }, + { + "dimension": 6, + "minimum_deletions": 35, + "root_lines": 21, + "simple_subset": 252 + }, + { + "dimension": 7, + "minimum_deletions": 28, + "root_lines": 28, + "simple_subset": 253 + }, + { + "dimension": 7, + "minimum_deletions": 14, + "root_lines": 42, + "simple_subset": 254 + }, + { + "dimension": 8, + "minimum_deletions": 0, + "root_lines": 120, + "simple_subset": 255 + } + ], + "independent_summary": { + "flat_capacities": [ + 0, + 1, + 3, + 6, + 12, + 20, + 36, + 63, + 120 + ], + "pair_union_minimum": 84, + "rank_invoice_minima_36_through_55": [ + 53, + 53, + 53, + 53, + 53, + 53, + 53, + 53, + 45, + 45, + 45, + 45, + 45, + 45, + 45, + 45, + 44, + 44, + 44, + 44 + ], + "reader_weight_histogram": { + "0": 1, + "120": 1, + "56": 255, + "64": 255 + }, + "single_reader_thresholds": [ + 56, + 55, + 53, + 50, + 44, + 36, + 26, + 1, + 0 + ] + }, + "minimum_pair_witness": [ + "72057594037927935", + "121988639063545046044787333114733914" + ], + "negative_controls": [ + { + "punctures": 36, + "ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "rejected_by": "joint-reader union constraint" + }, + { + "punctures": 43, + "ranks": [ + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "rejected_by": "joint-reader union constraint" + }, + { + "punctures": 51, + "ranks": [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "rejected_by": "joint-reader union constraint" + }, + { + "punctures": 35, + "ranks": [ + 5, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "rejected_by": "single-reader threshold" + }, + { + "punctures": 55, + "ranks": [ + 5, + 5, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "rejected_by": "nine physical ranks required" + }, + { + "punctures": 56, + "ranks": [ + 0, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "rejected_by": "puncture domain" + } + ], + "pair_union_histogram": { + "120": 765, + "84": 16320, + "88": 48195, + "92": 48960, + "96": 16065 + }, + "rank_loss_boundary": { + "live_label_rank": 8, + "punctures": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55 + ] + }, + "schema": 1, + "scope": "real E8 root-only star reader cost; no new kappa", + "single_reader_thresholds": [ + 56, + 55, + 53, + 50, + 44, + 36, + 26, + 1, + 0 + ], + "source_sha256": { + "sources/PR875-README.md": "bf744bd936c2def7ad83f0dd99706c15eb1864c01effc55edbeb78a6e8818dca", + "sources/pr631/README.md": "281f706bf29d1f91dd64ba096f9d66d622f49e9d82d0ff306fb9374f77ba7333", + "sources/pr631/verify.py": "9add2f1d71466f00963652b818e168fe2e2a4fa6e62cafa9811389fdba7000c2" + }, + "theorem": "C_star(P)/(120-|P|) >= 63/111 for |P|<=55, with equality possible only at |P|=9", + "threshold_witnesses": [ + { + "deleted_indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55 + ], + "reader": "72057594037927935", + "simple_subset": 0 + }, + { + "deleted_indices": [ + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87 + ], + "reader": "309485009749287474753961980", + "simple_subset": 1 + }, + { + "deleted_indices": [ + 1, + 2, + 3, + 4, + 5, + 14, + 15, + 16, + 17, + 26, + 27, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "reader": "5192217938648415812649824060424255", + "simple_subset": 5 + }, + { + "deleted_indices": [ + 1, + 3, + 4, + 5, + 15, + 16, + 17, + 26, + 27, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "reader": "5192217938648415812649824060424255", + "simple_subset": 13 + }, + { + "deleted_indices": [ + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55 + ], + "reader": "72057594037927935", + "simple_subset": 30 + }, + { + "deleted_indices": [ + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 57, + 58, + 59, + 60, + 61, + 62, + 81, + 82, + 83, + 84, + 85, + 86, + 97, + 98, + 99, + 100, + 101, + 102, + 105, + 106, + 107, + 108, + 109, + 110 + ], + "reader": "5192217938648415812649824060424255", + "simple_subset": 31 + }, + { + "deleted_indices": [ + 10, + 11, + 12, + 13, + 22, + 23, + 24, + 25, + 32, + 33, + 34, + 35, + 40, + 41, + 42, + 43, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55 + ], + "reader": "72057594037927935", + "simple_subset": 126 + }, + { + "deleted_indices": [ + 55 + ], + "reader": "315508349681617601994831493171495935", + "simple_subset": 127 + }, + { + "deleted_indices": [], + "reader": "72057594037927935", + "simple_subset": 255 + } + ] +} diff --git a/research/e8-joint-reader-bound/CLAIM.json b/research/e8-joint-reader-bound/CLAIM.json new file mode 100644 index 0000000000..2ee2cefe19 --- /dev/null +++ b/research/e8-joint-reader-bound/CLAIM.json @@ -0,0 +1,48 @@ +{ + "track": "Structural decoder research", + "assignment_seed": 46, + "random_source": "Python secrets.randbelow(100), operating-system randomness; one draw", + "base_commit": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", + "started_utc": "2026-10-13T13:26:04.736633+00:00", + "claimed_utc": "2026-10-13T13:29:33.805011+00:00", + "expected_finish_utc": "2026-10-13T14:06:00+00:00", + "time_budget_minutes": 40, + "orientation_limit_minutes": 8, + "verification_reserved_minutes": 10, + "coordination": "No pinned issues returned by GitHub GraphQL; two open issues are unrelated. Claim recorded locally.", + "candidates": [ + { + "task": "E8 joint-reader support-union obstruction to simultaneously cheap star readers", + "decision": "Chosen: analytic compatibility bound, distinct from single-reader thresholds and the 36-puncture equality census." + }, + { + "task": "Adaptive nonlinear Gaussian decoder routing with priced metadata", + "decision": "Not chosen: substantial conceptual overlap with PR912 adaptive Hurwitz routing." + }, + { + "task": "Higher-target proper-star puncture classification", + "decision": "Not chosen: active broad work in PR669 and PR772." + } + ], + "object": "120 real E8 root lines, 9-dimensional binary star reader space; simultaneous rank-constrained reader supports", + "hypothesis": "The minimum support union of independent readers and root-flat capacity bounds strengthen the single-reader puncture exclusion.", + "method": "Exact root/code census plus a written pair-union inequality; small complete rank-invoice optimization, no random annealing.", + "expected_deliverable": "Self-contained scoped structural negative result, exact certificates, independent arithmetic check and negative controls; no kappa claim.", + "stopping_rule": "Complete pair inequality and all puncture budgets below reader-space rank loss (56); stop or report narrower valid bound if it fails.", + "predecessors": { + "631": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "875": "7f334e4c749fd83d03feb6c1de4e4cda9534c9dc" + }, + "overlap": "Inspected open PRs through 934 and relevant decoder PRs; PR875 is exact 36-deletion equality/orbit, PR631 single-reader bounds, PR669 proper stars, PR912 nonlinear routing. No matching pair-union claim seen.", + "result_update": { + "completed_utc": "2026-10-13T13:43:50.758470+00:00", + "status": "Submitted scoped structural negative result; no new kappa", + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/939", + "result": "Shared-deletion pair-union constraints extend the real E8 star copy-ratio exclusion to all puncture sets of size at most 55. Necessary relaxed cost bounds are 53 for 36..43, 45 for 44..51, and 44 for 52..55; no attainability claim.", + "coverage": "256 parabolic flats, 511 nonzero readers, 130305 distinct pairs, 56 budgets; independent 486200 sorted profile visits; five package tests and predecessor controls pass.", + "scope": "Root-only fixed binary labels and additive star copy rank; 56+ punctures and general pairing-rank/nonlinear decoders are outside scope.", + "upstream_at_submission": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "upstream_selected_kappa": "1661957774647029/1000000000000000000", + "handoff": "README.md gives the single-command replay; PROOF.md supplies exhaustive coverage arguments; VALIDATION.md records independent and inherited checks." + } +} diff --git a/research/e8-joint-reader-bound/NOTICE.md b/research/e8-joint-reader-bound/NOTICE.md new file mode 100644 index 0000000000..61282856a1 --- /dev/null +++ b/research/e8-joint-reader-bound/NOTICE.md @@ -0,0 +1,28 @@ +# Attribution and license + +Prepared for Ross Richardson (@RossRichardson), with substantial OpenAI +Codex assistance in mathematical development, implementation, independent +computation, proof review and documentation. The independent checker and +separate review were also AI-assisted; no independent human review is claimed. + +New files follow the repository's Apache-2.0 license in ../../LICENSE. +Retained sources under sources/ are unchanged, with their original author +and assistance notices. Their exact commits, paths and hashes appear in +SOURCES.json. + +- Chi Zhao / @vectorsss, PR631: the E8 reader model, Weyl/parabolic coverage, + exact single-reader thresholds, small-puncture identity and <=35 theorem. + His README and verifier are preserved verbatim. +- Philipp / @mightyOil, PR875: the 36-puncture rank-five equality census, + exact orbit and cost. Its README is retained for attribution and scope; + our joint-reader inequality does not depend on its implementation. +- Joel Pulikkan / GamingPuzzled, PR620: the star minimum-basis accounting + and earlier decoder/puncture research. +- DreamingOfClouds, PR595/PR602: corrected format-limit context. +- eumemic, PR543 and subsequent punctured suppliers: E8 bit construction + context, with the earlier community and OpenAI #109 lineage credited + by the repository's contributor and upstream notices. + +The new contribution is the shared-puncture reader-union constraint, +its exact root-capacity invoice relaxation and the resulting <=55 +star-ratio exclusion. No literature-wide priority is asserted. diff --git a/research/e8-joint-reader-bound/OVERLAP.json b/research/e8-joint-reader-bound/OVERLAP.json new file mode 100644 index 0000000000..3af67aea16 --- /dev/null +++ b/research/e8-joint-reader-bound/OVERLAP.json @@ -0,0 +1,99 @@ +{ + "initial_open_count": 724, + "submission_open_count": 706, + "highest_pr_number_seen": 934, + "checked_utc": "2026-10-13T13:39:43.255795+00:00", + "pinned_coordination_issue": null, + "related_prs": [ + { + "number": 631, + "title": "Prove E8 star-decoder puncture thresholds through 35 deleted lines", + "headRefOid": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "updatedAt": "2026-10-12T23:12:30Z" + }, + { + "number": 875, + "title": "Scoped negative result: classify the E8 rank-five boundary at 36 punctures", + "headRefOid": "7f334e4c749fd83d03feb6c1de4e4cda9534c9dc", + "updatedAt": "2026-10-13T09:00:22Z" + }, + { + "number": 620, + "title": "Research notes (no \u03ba claim): E8 decoder floors are tight; #615 levers exhausted; +1.1e-7 \u03ba owner-map headroom on #617", + "headRefOid": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "updatedAt": "2026-10-13T02:36:29Z" + }, + { + "number": 669, + "title": "Research: prove higher-target star-code hierarchies and decoder geometry", + "headRefOid": "7d526020fc368ce4157cd436995c2f4fcf683318", + "updatedAt": "2026-10-13T09:34:35Z" + }, + { + "number": 715, + "title": "Scoped negative result: minimal E8 mixed-port extension is saturated", + "headRefOid": "d8ed5c6cf2781d6efa0062a2636e1a2644f96c85", + "updatedAt": "2026-10-13T04:41:15Z" + }, + { + "number": 717, + "title": "Format limits part 2 (no \u03ba claim): erratum to #595, exact invoice prices, frontier-word censuses, decoder floors, spec requirements, centre and fragmentation walls", + "headRefOid": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "updatedAt": "2026-10-13T09:29:47Z" + }, + { + "number": 725, + "title": "Scoped negative result: sharp global-star punctures and 67 attaining patterns", + "headRefOid": "6eadc4eb4ebc355b13fa36a3138d97a583ea7f37", + "updatedAt": "2026-10-13T04:52:28Z" + }, + { + "number": 732, + "title": "Research note: sharp off-target proper-star puncture threshold", + "headRefOid": "80431a74c31e807581f5c2258c87abe2084caacd", + "updatedAt": "2026-10-13T04:59:10Z" + }, + { + "number": 747, + "title": "Research: classify 240-port optimal punctures and certify the all-target threshold", + "headRefOid": "aeaf0899179a14644b412e838ede14db967c765e", + "updatedAt": "2026-10-13T05:03:15Z" + }, + { + "number": 765, + "title": "Scoped negative result: tensor E8 basis mixing cannot lower 72^d copy rank", + "headRefOid": "d8eaa3db32f76111b39db9b930f347ef30118a28", + "updatedAt": "2026-10-13T05:18:29Z" + }, + { + "number": 772, + "title": "Research: uniform proper-star ranks and all-target puncture thresholds", + "headRefOid": "02b59e553649c333072b5dd4dfb97e43942efa14", + "updatedAt": "2026-10-13T05:26:08Z" + }, + { + "number": 912, + "title": "Research/seed42 decoder", + "headRefOid": "945b3da1f1dd87cebd456b3a0459601b15f7ea8b", + "updatedAt": "2026-10-13T12:00:26Z" + } + ], + "finding": "No matching shared-puncture pair-union extension was found in the complete open PR metadata. PR631 and PR875 pins are unchanged. PR669 studies proper-star observation codes; PR912 studies adaptive Hurwitz routing. PR875 retains the exact rank-five equality classification which this bound does not supply.", + "immediate_submission_refresh": { + "checked_utc": "2026-10-13T13:42:19.024786+00:00", + "highest_pr": 937, + "new_since_full_inventory": [ + { + "headRefOid": "b303fed6dfe2066dcd78c0d8ed74d2a3b153ba72", + "number": 937, + "title": "Finite complex construction: two center shears save 5,562 primitives per invocation (no new kappa)" + }, + { + "headRefOid": "0679fb6e1e4c91f573ae07ab1d0ea273b13c74e3", + "number": 936, + "title": "Finite bit construction: five-wire prefixes save 340 further ADDs beyond PR904 (no new kappa)" + } + ], + "finding": "New bit and complex circuit contributions do not overlap the root-only joint-reader theorem." + } +} diff --git a/research/e8-joint-reader-bound/PROOF.md b/research/e8-joint-reader-bound/PROOF.md new file mode 100644 index 0000000000..dd25fb2860 --- /dev/null +++ b/research/e8-joint-reader-bound/PROOF.md @@ -0,0 +1,277 @@ +# Joint-reader obstruction through 55 E8 punctures + +**Scoped structural negative result.** In the root-only E8 binary label +decoder with additive star copy-rank accounting, no deletion of at most 55 +of the 120 real root lines improves the copy-cost/live-port ratio `63/111`. +This extends the at-most-35 exclusion of Chi Zhao / PR631 and the +36-puncture equality analysis of Philipp (@mightyOil) / PR875. The new step +is a compatibility constraint on two distinct readers subjected to the +**same** deletions; it does not assume the existence of nine simultaneously +cheap readers. + +This is a written mathematical argument supported by exact finite root/code +arithmetic, not a proof-assistant formalization. In particular, the +finite checks are not an enumeration of all puncture subsets: the geometric +reduction and support-union argument below supply their coverage. + +## 1. Precise model and inherited facts + +Let `L_0,...,L_119` represent the 120 unoriented E8 root lines in doubled +standard coordinates, each of squared norm 8. Define the binary matrix + +``` +B_st = (1 + L_s · L_t / 4) mod 2, +C = rowspace_F2(B). +``` + +The entries before reduction modulo two are integers. The inherited exact +code census is + +``` +dim_F2 C = 9, +{ wt(c) : 0 != c in C } = { 56, 64, 120 }, +weight multiplicities = { 56: 255, 64: 255, 120: 1 }. +``` + +For a deleted set `P` of root indices, put `p=|P|` and `v=120-p`. For a +nonzero reader `c in C`, its physical star rank is + +``` +s_P(c) = rank_Q { L_t : c_t=1 and t not in P }. +``` + +The cost under discussion is + +``` +C_star(P) = min { sum_{i=1}^9 s_P(c_i) : (c_1,...,c_9) is a basis of C }. +``` + +This is the star decoder model used by Joel Pulikkan / GamingPuzzled's +PR620 and inherited in PR631. It assumes unrestricted independent input +bits and additive costs for star totals. Additional totals whose +functionals span `C` contain a basis, so their nonnegative costs cannot +improve this minimum. This reduction does not identify star rank with +general source/reader pairing rank. + +For `p<=55`, restriction from `C` to the live ports is injective: a +nonzero codeword that vanished there would have its entire support in `P`, +contradicting the minimum weight 56. Consequently all nine reader +dimensions remain necessary, and independence before and after restriction +agrees. An invertible change of binary label coordinates preserves these +conditions. + +The proof inherits the sharp single-reader deletion thresholds from PR631: + +| Rank bound d | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | +|---|---:|---:|---:|---:|---:|---:|---:|---:|---:| +| Minimum required deletions delta_d | 56 | 55 | 53 | 50 | 44 | 36 | 26 | 1 | 0 | + +Thus `s_P(c)<=d` requires `p>=delta_d`. The last entry is the trivial +full-space extension of the predecessor's table. Also inherited is its +small-puncture identity, valid for `p<=13`: + +``` +C_star(P) = 72 - rank_F2 { u_t : t in P }. +``` + +Here `u_t` are the binary labels of the deleted root ports, in any fixed +nine-dimensional label coordinates. We need only its consequence +`C_star(P)>=72-p` for `p<=8`. These inherited facts, their finite census, +and their coverage arguments are preserved in +[the pinned PR631 source](sources/pr631/README.md); they are not new claims +of this contribution. + +## 2. Root-line capacities of physical spans + +For `d=0,...,8`, let `M_d` be the maximum number of the 120 root lines +contained in a root-spanned rational subspace of dimension at most `d`. +The exact capacity table is + +| Dimension bound d | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | +|---|---:|---:|---:|---:|---:|---:|---:|---:|---:| +| M_d | 0 | 1 | 3 | 6 | 12 | 20 | 36 | 63 | 120 | + +The standard parabolic types attaining the nontrivial entries are +`A1,A2,A3,D4,D5,E6,E7`; full E8 gives the last entry. Counts are of +**lines**, so are half the corresponding numbers of signed roots. + +For completeness, the all-subspace reduction is the same one used in +PR631. If `F` is a proper root-spanned subspace, choose a generic real +vector `n in F^perp` that is perpendicular to no root outside `F`. Such +a choice exists because there are finitely many roots outside `F`, each +excluding a proper hyperplane of `F^perp`. Move `n` into the closed +fundamental Weyl chamber. In a simple root system, every positive root has +nonnegative simple-root coefficients. Its inner product with this chamber +vector therefore vanishes exactly when its support uses only simple roots +orthogonal to the vector. The roots in the transported `F` are precisely +those in this standard parabolic span. Because `F` was root-spanned, +the dimension of that span is `dim F`. + +It follows that the finite census of all 256 subsets of the eight simple +roots, including the empty and full subsets, computes these capacities for +every root-spanned subspace. For an at-most-d bound, a smaller standard +subset can be extended to size d, so taking the maximum at exact size d +also suffices. The full-dimensional case is immediate. In particular, any +surviving reader of rational rank `d` contains at most `M_d` root lines. +This step concerns physical geometry alone and does not require a common +Weyl transformation for two different reader spans. + +## 3. The new joint-reader inequality + +Let `c,d` be two distinct nonzero words of `C`, and write `R_c,R_d` for +their supports before deletion. The word `c+d` is also nonzero. By the +minimum weight and the binary support identity, + +``` +|R_c union R_d| + = (wt(c) + wt(d) + wt(c+d)) / 2 + >= (56 + 56 + 56) / 2 + = 84. +``` + +If their surviving rational ranks are `a=s_P(c)` and `b=s_P(d)`, their +surviving sets have cardinalities at most `M_a` and `M_b`. A single set of +`p` deleted ports removes at most `p` members of their union, including +ports shared by both readers only once. Therefore + +``` +84 - p + <= |(R_c union R_d) minus P| + <= |R_c minus P| + |R_d minus P| + <= M_a + M_b. (1) +``` + +No disjointness is assumed. Replacing the union by the sum in the second +inequality only weakens the bound and cannot invalidate it. Distinctness +is essential: the argument would fail for `c=d`, because then `c+d=0`. +Members of a binary basis are nonzero and distinct, so (1) applies to any +two of them. + +## 4. A lower bound for every basis invoice + +Sort the nine reader ranks of any basis into nondecreasing order. Denote +its first two ranks by `a<=b`. Its cost is at least `a+8b`, because the +remaining seven ranks are also at least `b`. Every such basis therefore +supplies integers satisfying + +``` +0 <= a <= b <= 8, +delta_a <= p, delta_b <= p, +M_a + M_b >= 84-p, +cost_of_this_basis >= a+8b. +``` + +Minimizing over all bases gives the universal bound + +``` +L(p) = min { a+8b : 0<=a<=b<=8, + delta_a<=p, delta_b<=p, + M_a+M_b>=84-p }, +C_star(P) >= L(p). (2) +``` + +This is a relaxation: the feasible integer pairs need not occur for any +puncture set, and the other seven readers are not asserted to attain rank +`b`. Exhausting these at most 45 integer pairs for each `p` gives: + +| Deleted ports p | L(p) | One minimizing relaxed pair (a,b) | +|---|---:|---| +| 0 | 72 | (8,8) | +| 1 through 25 | 63 | (7,7) | +| 26 through 35 | 54 | (6,6) | +| 36 through 43 | 53 | (5,6) | +| 44 through 51 | 45 | (5,5) | +| 52 through 55 | 44 | (4,5) | + +The compatibility effect is already visible at `p=36`: two rank-five +readers would jointly occupy at most `20+20=40` live ports, although their +support union must retain at least `84-36=48`. More generally, two readers +of rank at most five require at least 44 deletions. This uses shared +deletions and is distinct from the single-reader threshold of 36. + +## 5. Ratio comparison and theorem + +For `0<=p<=8`, use the inherited bound `72-p`, which is stronger than the +pair relaxation where needed. Cross multiplication gives + +``` +111(72-p) - 63(120-p) = 432-48p > 0. +``` + +For each later interval, its cost bound is constant and `120-p` +decreases, so the smallest guaranteed ratio occurs at the interval's +left endpoint. The exact comparisons are: + +| p interval | Lower cost | Largest live-port count in interval | 111 times lower cost minus 63 times largest live count | +|---|---:|---:|---:| +| 9 through 25 | 63 | 111 | 0 | +| 26 through 35 | 54 | 94 | 72 | +| 36 through 43 | 53 | 84 | 591 | +| 44 through 51 | 45 | 76 | 207 | +| 52 through 55 | 44 | 68 | 600 | + +All are nonnegative. Thus for every puncture set with `|P|<=55`, + +``` +C_star(P) / (120-|P|) >= 63/111 = 21/37. +``` + +PR631 supplies an attaining nine-puncture example with independent deleted +labels and cost 63 on 111 live ports. Accordingly `63/111` is the optimum +ratio over the whole stated domain, although the minimum star cost at most +individual puncture counts is not determined here. In particular the +relaxed lower costs 53, 45 and 44 are **not** claimed to be attainable. +PR875's exact equality-class invoice at 36 punctures gives stronger +information for that class; our cost 53 there is only a sufficient universal +bound. + +## 6. Boundary, cost interpretation, and unresolved scope + +At 56 deletions a minimum-weight codeword can disappear: choosing its +support as `P` gives a nontrivial kernel of restriction. Nine independent +live reader dimensions are no longer automatic. This proof stops at 55; +it neither asserts nor excludes an improved ratio after dimension loss. + +The lower bound is on one necessary copy-cost component. Assigning zero +optimistic expense to helpers, source access, frame changes, restoration +and recursive children cannot overcome this component's ratio obstruction +within the fixed model. This is not a complete supplier invoice, and it +does not rule out improvements to other invoice terms at an unchanged or +worse copy ratio. + +The result does not cover general pairing-rank decoders, non-label or +nonlinear readers, extra/non-root ports, correlated inputs, changed stage +geometry, or improvements in another supplier or assembly constraint. +It supplies no new circuit, supplier word, unconditional multiplication +bound, or value of kappa. The selected construction's inherited all-size, +compiler, hosting, analytic, precision and tape obligations remain outside +this note. + +## 7. Provenance and attribution + +The task base is `91a2094f2e022930069e8cfdc810a3ea1b81cd09`, recorded in +[CLAIM.json](CLAIM.json), with structural-decoder assignment seed 46. The +predecessor source pins are: + +- Chi Zhao / [PR631](https://github.com/CrocSwap/integer-mult-bounds/pull/631), + head `fb893b5ee1317c2da3b297e6fe78eca0857d1a76`: root/code model, + parabolic-flat reduction, sharp single-reader thresholds, small-puncture + identity and the at-most-35 ratio theorem. +- Philipp (@mightyOil) / [PR875](https://github.com/CrocSwap/integer-mult-bounds/pull/875), + head `7f334e4c749fd83d03feb6c1de4e4cda9534c9dc`: first rank-five + equality-class analysis and at-most-36 exclusion; its retained + [README](sources/PR875-README.md) provides context, not a dependency of + inequalities (1) and (2). +- Joel Pulikkan / GamingPuzzled / PR620: the star model, minimum-basis + accounting and earlier puncture investigations. DreamingOfClouds / + PR595 and PR602 supply format-limit context; eumemic / PR543 and the + prior E8 supplier lineage supply construction context. + +The new contribution is the common-deletion support-union inequality, +its combination with root-flat capacity and single-reader constraints, +and the resulting exclusion through 55 deletions. No claim of novelty +outside this repository is made. This proof was developed, challenged +and written with **substantial OpenAI Codex assistance**, including an +AI-assisted separate review of the argument; no independent human review +is claimed. The retained predecessor files keep their original attribution +and Apache-2.0 license; this contribution follows the repository license. diff --git a/research/e8-joint-reader-bound/README.md b/research/e8-joint-reader-bound/README.md new file mode 100644 index 0000000000..a6d4ae2cbf --- /dev/null +++ b/research/e8-joint-reader-bound/README.md @@ -0,0 +1,101 @@ +# E8 star decoders: a joint-reader obstruction through 55 punctures + +**Scoped negative result; no new kappa.** Deleting at most 55 of the 120 real +E8 root lines cannot improve the star copy-cost/live-port ratio `63/111`. +The new argument rules out simultaneously cheap readers by charging their +shared deletion set once. It extends Chi Zhao's [PR631](https://github.com/CrocSwap/integer-mult-bounds/pull/631) +exclusion through 35 deletions and Philipp's [PR875](https://github.com/CrocSwap/integer-mult-bounds/pull/875) +36-deletion equality classification. + +Two distinct nonzero binary readers have a support union of at least 84 +root lines. A surviving rational rank-five reader contains at most 20 +lines, so two such readers need at least 44 shared deletions. This is a +compatibility bound, rather than another puncture search. Applying the +same inequality to all physical ranks gives: + +| Deleted lines | Universal lower bound on star cost | Worst endpoint ratio | +|---|---:|---:| +| 36–43 | 53 | `53/84 > 63/111` | +| 44–51 | 45 | `45/76 > 63/111` | +| 52–55 | 44 | `44/68 > 63/111` | + +These are lower bounds, **not claimed attainable costs**. Combining them +with the predecessor's smaller-puncture result gives the theorem through +55. The known nine-puncture construction still attains `63/111`. At 56 +deletions the reader space can lose a dimension, and this note stops. + +## Reproduce + +From the repository root, Python 3.10+ and the standard library suffice: + +```sh +python3 -I -B research/e8-joint-reader-bound/verify.py +``` + +Expected: + +```text +PASS_E8_JOINT_READER: 256 flats; 511 readers; 130305 pairs; punctures 0..55; 6 rejection controls; no new kappa +``` + +The default run writes nothing and compares the entire rebuilt +[CERTIFICATE.json](CERTIFICATE.json). `--write /tmp/e8-joint.json` emits +a deterministic rebuilt receipt. Both new checkers preserve checks with +`-O`; the unmodified predecessor intentionally refuses optimized execution. + +```sh +python3 -I -O -B research/e8-joint-reader-bound/independent_check.py +python3 -I -B research/e8-joint-reader-bound/test_package.py +``` + +The independent checker constructs all 240 signed roots before quotienting +by sign, uses Fraction RREF and direct span membership, and exhausts all +24,310 sorted nine-rank invoices at each of the 20 new puncture budgets. +It imports neither the primary verifier nor the predecessor implementation. +It checks the certificate's documented `independent_summary` only; source +pins, per-flat rows, threshold witnesses, the small-puncture inheritance, +and the rank-loss boundary have separate primary/predecessor coverage. + +The package tests replay both implementations from a path containing spaces, +require byte-identical regeneration, reject a changed bound or capacity, +reject modified source bytes before overwriting an output, and replay the +retained predecessor with its geometry/parity/flat controls. See +[VALIDATION.md](VALIDATION.md) for actual results and limitations. + +## Proof, scope, and handoff + +[PROOF.md](PROOF.md) defines the model, states the inherited results, +proves the shared-deletion inequality, and explains why all standard +parabolic flats cover arbitrary root-spanned reader spaces. The finite +census supports that written coverage argument; it is not an enumeration +of all puncture subsets or a formal proof of multiplication. + +The result concerns root-only E8 ports, fixed binary label readers, +independent input bits and additive star copy-rank costs. It does not +exclude general pairing-rank or nonlinear decoders, non-root ports, +changed geometry, helper savings, or 56+ punctures. No supplier, paid +recursive recurrence, improved assembly or new kappa is claimed. The +all-size/compiler, hosting, precision/tape and analytic obligations of +the selected construction remain inherited. + +This contribution adds only this directory. The exact base is +`91a2094f2e022930069e8cfdc810a3ea1b81cd09`; its selected conditional +kappa is `1661634653669567/10^18`, from PR799 with PR589 on PR555. +Existing generators, `upstream/`, and selected-frontier files are unchanged. +[SOURCES.json](SOURCES.json) pins retained predecessor bytes by commit, +SHA256 and Git blob, and records the inspected base context. +During final verification upstream advanced to `47481c89fd30a43f8f882eb4b391e89c29273fd0`, +which selects PR890 at conditional kappa `1661957774647029/10^18`. +This structural result is independent of that frontier change. + +[CLAIM.json](CLAIM.json) records the OS-random seed **46**, three candidate +tasks, local claim, bounded domain and overlap review. No pinned sprint +coordination issue existed. There was no randomized search or timeout; +all stated finite domains were completed. PR875's stronger classification +at exactly 36 deletions remains useful and is not superseded by our +coarser cost bound there. + +Prepared by **Ross Richardson (@RossRichardson)** with **substantial OpenAI +Codex assistance** in proof development, implementation, independent +checking and writing. See [NOTICE.md](NOTICE.md) for predecessor credit. +Apache-2.0; no independent human review is claimed. diff --git a/research/e8-joint-reader-bound/SOURCES.json b/research/e8-joint-reader-bound/SOURCES.json new file mode 100644 index 0000000000..ff91151c79 --- /dev/null +++ b/research/e8-joint-reader-bound/SOURCES.json @@ -0,0 +1,39 @@ +{ + "base_commit": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", + "retained_sources": [ + { + "pr": 631, + "commit": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "repository_path": "research/e8-continuation-20261013/punctures/README.md", + "local_path": "sources/pr631/README.md", + "git_blob": "b17edb488fed59f169798db35d2e9af86f0e4df4", + "sha256": "281f706bf29d1f91dd64ba096f9d66d622f49e9d82d0ff306fb9374f77ba7333" + }, + { + "pr": 631, + "commit": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "repository_path": "research/e8-continuation-20261013/punctures/verify.py", + "local_path": "sources/pr631/verify.py", + "git_blob": "c9fd83d4e0ff42c7dcc8d08907b8984e729b5794", + "sha256": "9add2f1d71466f00963652b818e168fe2e2a4fa6e62cafa9811389fdba7000c2" + }, + { + "pr": 875, + "commit": "7f334e4c749fd83d03feb6c1de4e4cda9534c9dc", + "repository_path": "research/e8-rank5-boundary/README.md", + "local_path": "sources/PR875-README.md", + "git_blob": "29a0261475652598f94f3493d317ea57e11f3f96", + "sha256": "bf744bd936c2def7ad83f0dd99706c15eb1864c01effc55edbeb78a6e8818dca" + } + ], + "base_context_sha256": { + "CONTRIBUTING.md": "1cae543effcabab91dab7f78423ee9283e60fb504f10848483d153331cd72bc4", + "certificates/selected-result.json": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699", + "docs/research/current-status.md": "415f85180f698329bea968798f2bc2519f56374cccc3e07c8e9051bd65192730", + "docs/research/pr-ledger.md": "d8169a360cd6e5842b47008362c7cce0ffcdd62733a8e8210ef6a8ff32bb65c9", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036" + }, + "license": "Apache-2.0", + "note": "Base context hashes describe the inspected base, not a lock on future selected results. Retained source bytes checked against GitHub Git blob IDs." +} diff --git a/research/e8-joint-reader-bound/VALIDATION.md b/research/e8-joint-reader-bound/VALIDATION.md new file mode 100644 index 0000000000..a3bffa62d9 --- /dev/null +++ b/research/e8-joint-reader-bound/VALIDATION.md @@ -0,0 +1,80 @@ +# Validation and review handoff + +Validated on 14 October 2026 (Australia/Melbourne), on macOS with CPython +3.14.6 and CPython 3.12.12. All arithmetic is exact and uses the standard +library. The two new implementations and proof received separate +AI-assisted review; no independent human or proof-assistant review is claimed. + +## Completed checks + +```sh +python3 -I -B research/e8-joint-reader-bound/verify.py +python3 -I -O -B research/e8-joint-reader-bound/independent_check.py +python3 -I -B research/e8-joint-reader-bound/test_package.py +python3.12 -I -B research/e8-joint-reader-bound/verify.py +python3.12 -I -O -B research/e8-joint-reader-bound/independent_check.py +make selected-record-check +git diff --check +``` + +- Primary: PASS; all 256 standard flats, 511 nonzero reader words, all + 130,305 distinct reader pairs, eight Weyl generators, nine exact + single-reader threshold witnesses, and 56 puncture budgets. +- Independent: PASS; alternate root ordering, normalized Fraction RREF, + direct root-span membership, weight/XOR pair-union calculation, and + 486,200 complete sorted-rank profile visits. Four independent rejection + controls pass. Comparison is limited to `independent_summary`. +- Package tests: **5/5 PASS**, including both new scripts in isolated + optimized mode after relocation to a path with spaces, byte-identical + regeneration, corrupted-cost rejection, corrupted-capacity rejection + by both engines, and corrupted-source rejection before output overwrite. +- The fifth package test replays pinned PR631 with its negative controls. + Its sharp thresholds, nine-puncture attaining example and <=35 theorem + checks pass. Its intentional optimized-mode refusal also passes. +- The primary's six rejection controls distinguish individual-reader + failure from shared-deletion incompatibility; valid relaxed profiles + at budgets 44 and 52 are accepted, without claiming realizability. +- A 56-puncture positive boundary control makes the live code rank eight, + justifying the stopping boundary rather than extrapolating the theorem. +- All three retained source files match GitHub Git blob IDs as well as + local SHA256 digests. No predecessor implementation is imported by + either new checker. +- A staged Git-tree export passes both new checkers under `-I -O -B` + and regenerates a byte-identical certificate. This checks the exact + staged package without relying on other checkout files. +- Selected-record integrity passes on the exact task base, with its + PR799 conditional kappa `1661634653669567/10^18`. + +## Provenance and current upstream context + +Original base: `91a2094f2e022930069e8cfdc810a3ea1b81cd09`. +The PR631 dependency is pinned to +`fb893b5ee1317c2da3b297e6fe78eca0857d1a76`; PR875 attribution/context is +pinned to `7f334e4c749fd83d03feb6c1de4e4cda9534c9dc`. + +During final verification upstream advanced to +`47481c89fd30a43f8f882eb4b391e89c29273fd0`, selecting PR890 at conditional +kappa `1661957774647029/10^18`. Its selected record, current status, review +and T21 construction proof were inspected. That new frontier is not a +dependency of this root-only structural result. The base provenance is +retained accurately rather than relabeling it as the newer commit. +There was no existing upstream directory at our package path. + +The final complete metadata inventory contained 706 open PRs through #934 +(the earlier inventory had 724; eighteen were integrated). Both direct +predecessor heads remained unchanged. No pinned coordination issue existed +at either check. Relevant heads and the scope comparison are in +[OVERLAP.json](OVERLAP.json). The claim and one result update are local. + +## Limits + +The finite checks do not enumerate all deletion sets or formally prove +the parabolic-flat argument. The written coverage proof is essential. +The primary certificate uses the inherited small-puncture result for +budgets 0–8; its source and replay are explicitly included above. + +No existing generator, supplier, selected certificate or upstream source +is changed. The expensive repository-wide `make verify` and selected +supplier cold replay were not rerun for this isolated research package. +No hosted CI pass, new kappa, paid supplier or complete multiplication +theorem is claimed. diff --git a/research/e8-joint-reader-bound/independent_check.py b/research/e8-joint-reader-bound/independent_check.py new file mode 100644 index 0000000000..b7da7bf739 --- /dev/null +++ b/research/e8-joint-reader-bound/independent_check.py @@ -0,0 +1,283 @@ +#!/usr/bin/env python3 +"""Independent finite checks for the E8 joint-reader lower bound. + +Uses Fraction RREF and direct root-span membership, not simple-root support +masks. Imports no primary verifier or predecessor implementation. The default +run compares only CERTIFICATE.json's independent_summary: capacities, reader +thresholds, weight histogram, pair-union minimum and the twenty invoice minima. +It does not verify other certificate fields or formally prove the parabolic +reduction. --write-summary instead writes its own detailed finite-check report. +Python 3.10+, standard library. Checks remain enabled with python -O. + +Prepared with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +from collections import Counter +from fractions import Fraction +from itertools import combinations, combinations_with_replacement, product +import json +from pathlib import Path + + +class VerificationError(Exception): + pass + + +def require(condition, message): + if not condition: + raise VerificationError(message) + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right)) + + +def canonical(vector): + first = next(x for x in vector if x) + return tuple(vector) if first > 0 else tuple(-x for x in vector) + + +def make_roots(): + # Construct all 240 signed roots, then quotient by sign. This order differs + # from the predecessor; certificate comparisons contain no root indices. + signed = set() + for i, j in combinations(range(8), 2): + for si, sj in product((-2, 2), repeat=2): + root = [0] * 8 + root[i], root[j] = si, sj + signed.add(tuple(root)) + signed.update(signs for signs in product((-1, 1), repeat=8) + if sum(x < 0 for x in signs) % 2 == 0) + require(len(signed) == 240, "signed root count") + require(all(dot(root, root) == 8 for root in signed), "root norms") + roots = sorted({canonical(root) for root in signed}) + require(len(roots) == 120, "root-line count") + simple = [(1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0)] + for i in range(6): + row = [0] * 8 + row[i], row[i + 1] = -2, 2 + simple.append(tuple(row)) + require(all(root in signed for root in simple), "simple roots") + return roots, simple + + +def rref(rows): + """Normalized rational Gauss-Jordan elimination, scanning columns.""" + matrix = [[Fraction(x) for x in row] for row in rows] + if not matrix: + return [], [] + pivots = [] + next_row = 0 + for column in range(len(matrix[0])): + selected = next((i for i in range(next_row, len(matrix)) + if matrix[i][column]), None) + if selected is None: + continue + matrix[next_row], matrix[selected] = matrix[selected], matrix[next_row] + divisor = matrix[next_row][column] + matrix[next_row] = [x / divisor for x in matrix[next_row]] + for i in range(len(matrix)): + if i != next_row and matrix[i][column]: + factor = matrix[i][column] + matrix[i] = [x - factor * y + for x, y in zip(matrix[i], matrix[next_row])] + pivots.append(column) + next_row += 1 + if next_row == len(matrix): + break + return matrix[:next_row], pivots + + +def in_span(vector, reduced, pivots): + remainder = [Fraction(x) for x in vector] + for row, pivot in zip(reduced, pivots): + factor = remainder[pivot] + remainder = [x - factor * y for x, y in zip(remainder, row)] + return not any(remainder) + + +def check_flat_dimension(roots, flat, dimension): + actual = len(rref([root for i, root in enumerate(roots) + if flat >> i & 1])[1]) + require(actual == dimension, "root-section dimension") + + +def make_code(roots): + rows = [] + for left in roots: + bits = 0 + for i, right in enumerate(roots): + inner = dot(left, right) + require(inner % 4 == 0, "decoder integrality") + bits |= ((1 + inner // 4) % 2) << i + rows.append(bits) + # Low-pivot binary elimination, independently of physical Fraction ranks. + pivots = {} + for original in rows: + row = original + while row: + low = row & -row + if low in pivots: + row ^= pivots[low] + else: + pivots[low] = row + break + require(len(pivots) == 9, "binary reader dimension") + words = {0} + for row in pivots.values(): + words.update([word ^ row for word in words]) + require(len(words) == 512 and set(rows) <= words, "reader-space closure") + return sorted(words - {0}) + + +def pair_union(c, d, code): + require(c != 0 and d != 0 and c != d, "pair requires distinct nonzero readers") + require(c ^ d in code, "pair XOR must be a codeword") + numerator = c.bit_count() + d.bit_count() + (c ^ d).bit_count() + require(numerator % 2 == 0, "pair union identity parity") + return numerator // 2 + + +def validate_invoice(punctures, ranks, cost, capacities, thresholds): + require(len(ranks) == 9 and list(ranks) == sorted(ranks), "nine sorted ranks") + require(all(0 <= d <= 8 for d in ranks), "rank domain") + require(all(thresholds[d] <= punctures for d in ranks), "single-reader threshold") + require(capacities[ranks[0]] + capacities[ranks[1]] >= 84 - punctures, + "shared-puncture pair constraint") + require(sum(ranks) == cost, "invoice sum") + + +def reject(call, message): + try: + call() + except VerificationError as error: + require(str(error) == message, "negative control failed at wrong obligation") + else: + raise VerificationError("negative control was accepted: " + message) + + +def reconstruct(): + roots, simple = make_roots() + require(len(rref(simple)[1]) == 8, "simple-system rank") + code = make_code(roots) + weights = dict(sorted(Counter(word.bit_count() for word in code).items())) + require(weights == {56: 255, 64: 255, 120: 1}, "nonzero weight distribution") + word_set = set(code) + union_min = min(pair_union(c, d, word_set) for c, d in combinations(code, 2)) + require(union_min == 84, "minimum pair support union") + + capacities = [] + thresholds = [] + flat_counts = [] + threshold_witness_ranks = [] + for dimension in range(9): + largest_flat = 0 + smallest_deletion = 121 + best_survivors = None + count = 0 + for indices in combinations(range(8), dimension): + reduced, pivots = rref([simple[i] for i in indices]) + require(len(pivots) == dimension, "standard-flat dimension") + flat = sum(1 << i for i, root in enumerate(roots) + if in_span(root, reduced, pivots)) + check_flat_dimension(roots, flat, dimension) + largest_flat = max(largest_flat, flat.bit_count()) + deletions, reader = min(((word & ~flat).bit_count(), word) for word in code) + if deletions < smallest_deletion: + smallest_deletion = deletions + best_survivors = reader & flat + count += 1 + capacities.append(largest_flat) + thresholds.append(smallest_deletion) + flat_counts.append(count) + witness_rank = len(rref([root for i, root in enumerate(roots) + if best_survivors >> i & 1])[1]) + require(witness_rank == dimension, "sharp threshold witness rank") + threshold_witness_ranks.append(witness_rank) + require(capacities == [0, 1, 3, 6, 12, 20, 36, 63, 120], "flat capacities") + require(thresholds == [56, 55, 53, 50, 44, 36, 26, 1, 0], "reader thresholds") + + # Exhaust all 24,310 sorted nine-rank profiles instead of reducing the + # optimization to the cheapest pair a+8*b. These are relaxation invoices, + # not purportedly realizable geometries or puncture sets. + profiles = list(combinations_with_replacement(range(9), 9)) + require(len(profiles) == 24310, "profile enumeration cardinality") + bounds = [] + for punctures in range(36, 56): + feasible = [] + for ranks in profiles: + if any(thresholds[d] > punctures for d in ranks): + continue + if any(capacities[a] + capacities[b] < 84 - punctures + for a, b in combinations(ranks, 2)): + continue + feasible.append(ranks) + minimum = min(map(sum, feasible)) + expected = 53 if punctures < 44 else 45 if punctures < 52 else 44 + require(minimum == expected, "rank-invoice optimum") + witness = min(ranks for ranks in feasible if sum(ranks) == minimum) + validate_invoice(punctures, witness, minimum, capacities, thresholds) + require(Fraction(minimum, 120 - punctures) > Fraction(63, 111), + "copy-ratio exclusion") + bounds.append({"punctures": punctures, "minimum_relaxed_cost": minimum, + "minimizing_rank_profile": list(witness), + "feasible_sorted_profiles": len(feasible)}) + + # The first control is the tempting but incompatible nine rank-five invoice + # at p=36: it passes all individual thresholds and fails only jointly. + reject(lambda: validate_invoice(36, [5] * 9, 45, capacities, thresholds), + "shared-puncture pair constraint") + reject(lambda: validate_invoice(36, [5] + [6] * 8, 52, capacities, thresholds), + "invoice sum") + reject(lambda: pair_union(code[0], code[0], word_set), + "pair requires distinct nonzero readers") + # Adding an independent root to a rank-one section must fail the same + # dimension check used in the census, rather than merely testing an error. + require(len(rref(roots[:2])[1]) == 2, "independent root control fixture") + reject(lambda: check_flat_dimension(roots, 3, 1), "root-section dimension") + # Physical rational rank and label binary rank are separate obligations. + require(len(rref([[1, 1], [1, -1]])[1]) == 2, + "wrong-characteristic physical-rank control") + + return {"root_lines": len(roots), "binary_reader_dimension": 9, + "nonzero_reader_weight_histogram": {str(k): v for k, v in weights.items()}, + "distinct_reader_pairs_checked": len(code) * (len(code) - 1) // 2, + "minimum_pair_support_union": union_min, + "standard_flat_counts_by_dimension": flat_counts, + "maximum_root_lines_by_dimension": capacities, + "minimum_deletions_by_reader_rank": thresholds, + "threshold_witness_ranks": threshold_witness_ranks, + "sorted_profiles_per_puncture_count": len(profiles), + "rank_invoice_bounds": bounds, "negative_controls": 4} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--check", type=Path, + default=Path(__file__).with_name("CERTIFICATE.json")) + parser.add_argument("--write-summary", type=Path, + help="write regenerated summary instead of reading a certificate") + args = parser.parse_args() + summary = reconstruct() + if args.write_summary: + args.write_summary.write_text(json.dumps(summary, indent=2, sort_keys=True) + "\n") + else: + certificate = json.loads(args.check.read_text()) + projection = { + "flat_capacities": summary["maximum_root_lines_by_dimension"], + "single_reader_thresholds": summary["minimum_deletions_by_reader_rank"], + "reader_weight_histogram": {"0": 1, **summary["nonzero_reader_weight_histogram"]}, + "pair_union_minimum": summary["minimum_pair_support_union"], + "rank_invoice_minima_36_through_55": [row["minimum_relaxed_cost"] + for row in summary["rank_invoice_bounds"]], + } + require(certificate.get("independent_summary") == projection, + "certificate independent_summary mismatch") + print("PASS_E8_JOINT_INDEPENDENT: 256 rational root flats; 130305 reader pairs; " + "486200 sorted rank profiles; 4 negative controls; no new kappa") + + +if __name__ == "__main__": + main() diff --git a/research/e8-joint-reader-bound/sources/PR875-README.md b/research/e8-joint-reader-bound/sources/PR875-README.md new file mode 100644 index 0000000000..29a0261475 --- /dev/null +++ b/research/e8-joint-reader-bound/sources/PR875-README.md @@ -0,0 +1,229 @@ +# The first E8 rank-five puncture boundary + +**Scoped negative result; no new supplier or κ.** At exactly 36 deleted +E8 root lines, no bit-side star label decoder improves the copy-rank/live-port +ratio `63/111`. Together with Chi Zhao's [PR631](https://github.com/CrocSwap/integer-mult-bounds/pull/631), +this extends its exclusion from at most 35 to **at most 36 punctures**. + +The new evidence explains why the first opening in that predecessor's coarse +rank bound does not help. Exactly **7,560** 36-puncture sets admit a reader of +rational rank five. They form **one Weyl orbit**. Every such set has the same +reader-rank histogram and exact minimum star cost: + +| Reader rank | 5 | 6 | 7 | 8 | +|---|---:|---:|---:|---:| +| Number of nonzero readers | 1 | 0 | 42 | 468 | +| Binary dimension spanned by readers up to this rank | 1 | 1 | 8 | 9 | + +An optimal nine-total basis therefore has weights `5,7,7,7,7,7,7,7,8`, costing +**62** on 84 live ports. Having one rank-five reader does not provide nine +independent cheap readers. All other 36-puncture sets have cost at least 54. +Both ratios exceed `63/111`: + +``` +62/84 = 31/42 > 21/37 = 63/111, +54/84 = 9/14 > 21/37. +``` + +This is an exhaustive equality-class calculation with a written coverage +argument, not a failed random search. The minimum cost across *all* +36-puncture sets is not determined; 54 is only the lower bound used for the +nonexceptional cases. + +## Reproduce + +From the repository root, Python 3.10+ and its standard library suffice: + +```sh +python3 -B research/e8-rank5-boundary/verify.py +``` + +Expected final line: + +``` +PASS_E8_RANK5_BOUNDARY: 28616 rank-five pairs; 2 representatives; 7560 conjugate punctures; cost 62; 72 restorations; 5 negative controls; no new kappa +``` + +The default command checks the entire committed `CERTIFICATE.json`, including +the predecessor source hashes. It writes nothing. `--write /tmp/e8-rank5.json` +regenerates the deterministic certificate after all checks pass. + +A separate implementation uses normalized Fraction RREF, low-pivot binary +elimination, direct span-membership tests instead of simple-coordinate masks, +and the cumulative-rank cost formula instead of the greedy basis algorithm: + +```sh +python3 -I -O -B research/e8-rank5-boundary/independent_check.py \ + --check research/e8-rank5-boundary/CERTIFICATE.json +``` + +It imports neither the primary verifier nor predecessor code. It checks all +28,616 rank-five pairs and both complete 511-reader rank tables. Its scope is +the `independent_summary` portion of the certificate; the orbit traversal and +other-dimensional threshold census are checked by the primary verifier. +Both new implementations retain all checks under optimized Python. + +The predecessor is retained byte-for-byte and can also be replayed: + +```sh +python3 -B research/e8-rank5-boundary/sources/pr631/verify.py --negative-controls +``` + +That older script intentionally refuses `-O`. See [VALIDATION.md](VALIDATION.md) +for the actual local validation record and its limits. + +## Model and coverage proof + +Use the standard 120 real E8 root **lines**, with representatives `L_t` in +doubled coordinates, squared norm eight. The binary decoder matrix is +`B_st = (1 + L_s · L_t / 4) mod 2`. Its row space `C` has dimension nine. +Its nonzero words have weights 56 (255 words), 64 (255 words), and 120 (one). +For a puncture set `P`, the star weight of a reader `c` is + +``` +s_P(c) = rank_Q {L_t : c_t = 1 and t not in P}. +``` + +We use exactly the star model in Joel Pulikkan / GamingPuzzled's PR620 +`s2-decoder/bitp.py`, inherited by PR631: minimize the sum of these weights +over a basis of the nine-dimensional reader space. A collection of additional +star totals must span that space and contains a basis; nonnegative weights +cannot make that collection cheaper than the minimum basis. This does not +cover general source/reader pairing-rank factorizations. + +**1. The code still has nine dimensions after 36 deletions.** A nonzero word +can vanish on all live ports only if its entire support was deleted. Its +minimum weight is 56, greater than 36. Restriction to the live ports is +injective, so independence before and after puncturing agrees. Invertible +changes of label coordinates also preserve it. + +**2. Any rank-five case is an equality case.** PR631's sharp deletion +thresholds for reader ranks at most `0,...,7` are +`[56,55,53,50,44,36,26,1]`. The primary verifier regenerates all of them over +255 standard flats and 511 readers. Since 44 deletions are needed for rank +four, a reader of rank at most five at our boundary has rank exactly five. +Let `F` be the span of its surviving roots. All reader roots outside `F` +were deleted. At least 36 deletions are needed to achieve this, and `|P|=36`, +so necessarily + +``` +P = support(c) \ F. +``` + +There are no leftover arbitrary deletions in this case. This equality is +the new search restriction; we are not reopening PR620's annealing search. + +**3. Standard flats cover every equality case.** We inherit PR631's +parabolic-flat reduction, repeated here for clarity. Choose a generic normal +in `F` perpendicular space, perpendicular to exactly the roots in `F`. +Move it to the closed fundamental Weyl chamber. Every positive root has +nonnegative simple-root coordinates, so the perpendicular roots are precisely +the roots supported on those simple roots perpendicular to the normal. Their +span is a standard rank-five parabolic flat. Thus it suffices to inspect +all `binom(8,5)=56` standard flats and all 511 reader words. The main verifier +checks integral, common-sign simple coordinates and preservation of the full +reader code by each of the eight simple reflections. Physical ranks are +preserved because these reflections are orthogonal. This supplies the +invariance needed to transport the cost calculation back to any original +puncture set. + +**4. The complete equality census has two standard representatives.** The +two `(simple subset, reader)` pairs are recorded in the certificate, with all +reader and deleted root indices. The simple subsets are `[0,1,2,3,4]` and +`[1,2,3,4,5]` in the explicitly generated simple system. These are *two +standard-flat representatives*, not two distinct Weyl orbits. The following +word in the eight simple reflections carries the first puncture set to the +second (apply from left to right): + +``` +5,4,3,1,2,0,3,2,4,3,1,5,4,3,2,0 +``` + +Breadth-first closure of the first set under all eight reflections has exactly +7,560 distinct masks. Every newly encountered image is enqueued and all eight +outgoing images are inspected before completion. Combined with the covering +argument and the explicit connection, this proves the asserted single orbit +and its exact size. Root numbering belongs to this standard-coordinate +package, not the Hamming-coordinate numbering of a shipped supplier. + +**5. Exact minimum cost.** For both representatives, compute all 511 rational +reader ranks. The histogram is shown above. Let `r_k` be the binary rank of +the span of all readers of weight at most `k`. For integer weights in `[0,8]`, +the minimum basis cost is `sum_{k=0}^7 (9-r_k)`: a greedy basis contains a +maximum independent set from each nested weight threshold. Here +`(r_0,...,r_7)=(0,0,0,0,0,1,1,8)`, yielding 62. The certificate also gives +an explicit attaining basis, whose weights are recomputed from roots. + +**6. The other cases.** If a 36-puncture set has no rank-five reader, Step 2 +also excludes lower ranks. Every basis reader has rank at least six, hence +the star cost is at least `9*6=54`. This completes the stated ratio exclusion. +Combining it with PR631's earlier theorem gives the at-most-36 corollary. + +## Controls and scope + +Every default primary replay includes: + +- Corrupted root geometry, binary decoder and flat-membership rejection. +- A tempting set of **nine distinct** cheap readers with invoice 61, rejected + because its binary span has dimension eight. +- A wrong-characteristic control: rational physical rank is not binary rank. +- All 72 single-port restorations across the two representatives. Each raises + the unique rank-five reader to rank six, confirming the deletion boundary. + +The final item is a positive boundary control, not 72 malformed-file rejections. +The independent implementation supplies separate rational, binary and geometry +controls. Receipt and source mutations are tested during packaging. + +The result concerns root-only E8 ports, unrestricted independent input bits, +the fixed label decoder, and additive **star** copy-rank accounting. It does +not rule out general pairing-rank decoders, extra/non-root ports, helper +savings, correlated inputs, changed stage geometry, or other mechanisms. +Puncture counts 37 and above are outside the new theorem. There is no new +global puncture optimum, formal proof-assistant theorem or full multiplication +theorem here. + +The hypothesis tested was a reduction of this copy-rank ratio at its first +unexcluded boundary. That necessary arithmetic opportunity fails even if +additional helper, source-access, frame, restoration and recursive-child +expenses are optimistically assigned zero. This says nothing about improving +another part of a full supplier invoice at an unchanged or worse copy ratio. +No new supplier or outer assembly is proposed or priced. The selected +construction's all-size/compiler, hosting, precision/tape and analytic +assumptions remain separate and unresolved by this note. + +## Provenance, prior work and assignment + +Base commit: `f567884aeb8851b6e794af1184119a3bfbe1e631`. At that base the +selected conditional saving is `1661634653669567/10^18` (PR799 with PR589 on +PR555), as recorded in `certificates/selected-result.json`. Its actual +construction, maintainer review and the PR ledger were inspected. This package +does not modify the selected record or any existing repository file. + +Assignment seed **46** was drawn once from operating-system randomness. +[CLAIM.json](CLAIM.json) records the three candidates, scope, stopping rule +and overlap checks. No pinned sprint coordination issue existed; the claim +and its result update are local. Completed coverage is 28,616 boundary pairs, +130,305 total threshold pairs, both equality representatives, both 511-reader +rank tables and the complete 7,560-mask equality orbit. There is no random +search or unreported timeout in these domains. + +The predecessor is pinned to PR631 head +`fb893b5ee1317c2da3b297e6fe78eca0857d1a76`; its original README and verifier +are retained under `sources/pr631/` without changes. [SOURCES.json](SOURCES.json) +records their hashes and exact paths, plus base-context hashes. Context hashes +describe the inspected base and are not a claim that future selected records +must stay unchanged. New scripts import no predecessor implementation. + +Credit **Chi Zhao / PR631** for the all-flat reduction, sharp single-reader +thresholds and earlier at-most-35 theorem; **Joel Pulikkan / GamingPuzzled / +PR620** for the model, optimum-basis method and puncture investigations; +**DreamingOfClouds / PR595 and PR602** for format-limit context; and **eumemic / +PR543** and the prior E8 supplier lineage for the original construction +context. These inherited results are not claimed as new. The new contribution +is the equality classification, its exact orbit and invoice, and the +36-puncture exclusion with independent arithmetic evidence. + +Prepared by **Philipp (@mightyOil)** with **substantial OpenAI Codex assistance** +in proof development, implementation, independent computational checking and +writing. The separate checks were also AI-assisted; no independent human +review is claimed. Apache-2.0; see [NOTICE.md](NOTICE.md). diff --git a/research/e8-joint-reader-bound/sources/pr631/README.md b/research/e8-joint-reader-bound/sources/pr631/README.md new file mode 100644 index 0000000000..b17edb488f --- /dev/null +++ b/research/e8-joint-reader-bound/sources/pr631/README.md @@ -0,0 +1,190 @@ +# Exact E8 puncture thresholds and a star-decoder exclusion + +**Result:** among all punctures of at most 35 of the 120 real E8 root lines, +no bit-side label decoder with star copy accounting improves the copy-cost / live-port +ratio **63/111**. Nine linearly independent punctured labels attain that ratio. +This is an exhaustive geometric bound, not a randomized search. + +A second result makes the previously sampled mixed-port obstruction exact: +a rational normal not proportional to an E8 root needs **at least 14 punctures** +to be compatible with any nonzero decoder label. The bound is sharp, including +for odd labels. Its D7 equality example has star copy cost 64 on 106 surviving +root ports, so that puncture itself is worse than 63/111. + +**No new supplier word, supplier exponent, or κ is claimed.** The current bit +supplier is already above the complex bottleneck. A smaller helper network can +still improve a word even if its copy ratio does not improve. + +## Reproduce + +From the repository root, using Python 3.9 or later and no external packages: + +```sh +python3 research/e8-continuation-20261013/punctures/verify.py --negative-controls +python3 research/e8-continuation-20261013/punctures/verify.py --write /tmp/e8-puncture-results.json +cmp research/e8-continuation-20261013/punctures/results.json /tmp/e8-puncture-results.json +``` + +The verifier uses exact integers and rational arithmetic. On the development +machine it runs in under one second. The JSON contains every standard parabolic +flat tested and explicit punctures witnessing all eight sharp rank thresholds. +Optimized Python (`-O` or `PYTHONOPTIMIZE`) is explicitly refused before any file +write. The optional negative controls inject corrupt root geometry, label parity +and a flat containing an extra independent root, and check rejection at the +corresponding structural invariants. They also check that `-O` writes no receipt. +Root indices use this package's doubled standard coordinates, **not** the +Hamming-coordinate numbering in #620 or the shipped word. + +## Definitions and exhaustive reduction + +Let L be one representative of each of the 120 E8 root lines, in doubled standard +coordinates with squared norm 8. Put G_st = L_s·L_t / 4 and B = (J+G) mod 2. +The binary matrix B has rank nine. For a label functional p, its reader set R(p) +is the support of the corresponding nonzero word in rowspace(B). There are 511 +such words. Their weights are 56 (255 words), 64 (255), and 120 (one). +For a puncture set P define + + s_P(p) = dim_Q span{L_t : t in R(p) minus P}. + +In the star label-decoder model used by #620's `bitp.py`, the optimum copy cost +is the minimum total weight of a basis of the nine-dimensional binary label +space, with weight s_P. Matroid greedy computes it exactly. Allowing extra +nonnegative-cost star totals cannot improve the minimum-basis cost: their source +functionals must span and therefore contain a basis. + +It suffices to test the 255 proper subsets I of a fixed simple system of E8. +Here is the coverage argument, which is part of the proof rather than a claim +that the program enumerates every flat individually. For a root-spanned proper +subspace F, choose a generic normal vector in F-perp, so exactly the roots in F +are perpendicular to it. Move this normal to the closed fundamental Weyl chamber. +Every positive root has nonnegative simple-root coordinates. A root is +perpendicular to the normal precisely when its support lies in the set I of +simple roots perpendicular to it. Thus the roots of F become exactly the roots +in the span of I. This is the usual parabolic-flat argument; see, for example, +the opening of Section 4 of [Baumeister et al., *On the Hurwitz action in finite Coxeter groups*](https://arxiv.org/html/1512.04764v1#S4). + +The verifier checks integrality and common-sign positivity of all simple-root +coordinates. It also checks that each of the eight simple reflections preserves +the 512 reader words and their self-pairing parity. Because these reflections +generate the Weyl group, taking minima over all reader words on these standard +flats covers every conjugate flat without enumerating the Weyl group. + +## Sharp rank-loss thresholds + +For d=0,...,7 let delta_d be the smallest number of roots that can be deleted +from any nonzero reader R(p) so its surviving Q-span has dimension at most d. +For each standard d-dimensional flat H, the required deletion count is +|R(p) minus H|. Minimize this over its 511 reader words and over all standard +flats of dimension d. Every lower-dimensional flat extends to one of dimension +d, so this also covers "at most d". The program checks that each minimizing +witness actually retains rank d. + +| d | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | +|---|---:|---:|---:|---:|---:|---:|---:|---:| +| delta_d | 56 | 55 | 53 | 50 | 44 | 36 | 26 | 1 | + +In particular, **25 punctures cannot produce any reader of rank six**, and +**35 punctures cannot produce any reader of rank five**. + +## Star-ratio theorem + +A sharper statement holds for |P| <= 13: + + C_star(P) = 72 - rank_F2{u_t : t in P}. + +To see this, the seven non-root-normal maximal parabolic hyperplanes need at +least 14 deletions for any reader to fit. For the remaining E7 hyperplane, +exactly one reader fits after fewer than 14 deletions: the reader of its normal +root, and the root itself must be deleted. Therefore the only cheap functionals +are the labels of punctured roots. They have weight seven; all others have +weight eight. No reader has smaller rank, since delta_6=26. The minimum-weight +basis takes a maximum independent subset of the cheap functionals, proving the +formula. The live binary labels still span dimension nine: a rank loss would +require deleting an entire nonzero reader, hence at least 56 ports. + +Now write p=|P|, v=120-p. The preceding facts imply: + +| punctures p | lower bound for star copy cost C | consequence | +|---|---:|---| +| 0,...,8 | 72-p | (72-p)/(120-p) > 63/111 | +| 9,...,25 | 63 | C/v >= 63/111, equality possible at p=9 | +| 26,...,35 | 54 | C/v >= 54/94 = 27/47 > 63/111 | + +The second and third rows use that any spanning set contains nine independent +functionals, each of rank at least seven or six, respectively. The verifier +supplies a nine-puncture control with independent labels and exact star cost 63. +This proves the asserted optimum over **all** punctures of size at most 35. + +For the fixed bit-side stage window h=8, the format ceiling in #595/#602 is +monotone in C/v, so this excludes improving that ceiling by such punctures within +the same star model. It does not compare full supplier words: helper counts, +frame changes, idle windows, hosting and outer assembly still have to be priced. + +## Sharp non-root-port obstruction + +The maximal parabolic hyperplanes have the following exact reader-deletion minima. +The odd-label minimum agrees with the unrestricted minimum in every row. + +| root subsystem | root lines in hyperplane | minimum deletions | +|---|---:|---:| +| E7 | 63 | 1 | +| D7 | 42 | 14 | +| E6+A1 | 37 | 27 | +| A7 | 28 | 28 | +| D5+A2 | 23 | 33 | +| A6+A1 | 22 | 35 | +| A4+A3 | 16 | 40 | +| A4+A2+A1 | 14 | 43 | + +For any non-root normal n, move n into the fundamental chamber. Its vanishing +simple roots form a proper subset I. If exactly the E7 node is missing, n is a +root normal, contrary to the premise. Otherwise I is contained in at least one +of the other seven maximal subsets. Its root section is contained in that +non-root hyperplane. Consequently every nonzero reader has at least 14 roots +outside n-perp. + +A compatible new bit-side port (physical vector n, nonzero binary label z) +requires every surviving root with z·u_t=1 to lie in n-perp. Hence all the roots +in R(z) outside n-perp must be punctured. This proves the universal lower bound +14, rather than only a bound on sampled or root-spanned normals. + +Equality occurs at the D7 normal e8. The unique minimizing reader deletes the +14 integer root lines involving coordinate eight. Its label has odd norm, so +it satisfies the added port's label self-pairing requirement. After puncturing +these lines, the reader-rank histogram is {7:15, 8:496}; their cheap functionals +have binary span dimension eight. The exact star optimum is therefore 64, not +63 or 62. This is a control for the root-only puncture, not a fully costed +mixed-port supplier construction. + +## Scope and next direction + +This closes a sizeable star-puncture search range. It does **not** lower-bound +Theorem C's general pairing-rank cost: two seven-dimensional reader/source +spans can have a pairing block of rank six. It also does not handle a new +non-label decoder, multiple added ports, or a helper-saving tradeoff at worse +copy ratio. + +A non-star construction is therefore a more relevant next test than further +star annealing among <=35 punctures. Alternatively, 36 is the first puncture +count at which the coarse rank thresholds here stop ruling out improvement; +that is a necessary opening, not evidence that nine cheap independent +functionals or an economical full word exist. + +## Provenance and assistance + +This work follows the questions and conventions in GamingPuzzled's #620, +`research/e8-decoder-floors-and-cold14-notes/s2-decoder/{bitp.py,sa_bit.py,hyper.py,addports.py}`; +DreamingOfClouds' #595/#602, `research/format-limits-corrected/`; and eumemic's +#543, `research/e8-bit-r420/`. The reader-rank census, exhaustive reduction and +<=35-puncture consequence are supplied here; no novelty outside this repository +is asserted. The mathematical coverage argument is stated explicitly and all +finite arithmetic is independently regenerated from roots by this package. +Base source pin: `17ce0c79b7b51c2634b439ea5a2b754f09909693`, with immutable references: + +- [#620 decoder and puncture notes](https://github.com/CrocSwap/integer-mult-bounds/tree/17ce0c79b7b51c2634b439ea5a2b754f09909693/research/e8-decoder-floors-and-cold14-notes/s2-decoder) +- [#595/#602 corrected format limits](https://github.com/CrocSwap/integer-mult-bounds/tree/17ce0c79b7b51c2634b439ea5a2b754f09909693/research/format-limits-corrected) +- [#543 bit supplier](https://github.com/CrocSwap/integer-mult-bounds/tree/17ce0c79b7b51c2634b439ea5a2b754f09909693/research/e8-bit-r420) + +Prepared by **Chi Zhao**, with **substantial OpenAI Codex assistance**. +Licensed under **Apache-2.0**, consistent with the repository. +No archived source was modified. diff --git a/research/e8-joint-reader-bound/sources/pr631/verify.py b/research/e8-joint-reader-bound/sources/pr631/verify.py new file mode 100644 index 0000000000..c9fd83d4e0 --- /dev/null +++ b/research/e8-joint-reader-bound/sources/pr631/verify.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +"""Exact E8 reader-flat census. Standard library only; Python >= 3.9. + +Chi Zhao, with substantial OpenAI Codex assistance. Apache-2.0. +See README.md for proof scope, +prior work, and the mathematical argument making the finite census exhaustive. +""" +if not __debug__: + raise SystemExit("Refusing optimized Python: exact validation requires assertions enabled.") + +import argparse +from collections import Counter +from fractions import Fraction +from itertools import combinations, product +import json +from math import gcd, lcm +from pathlib import Path +import subprocess +import sys +import tempfile + + +def pop(x): + return bin(x).count("1") + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def basis2(rows): + pivots = {} + for x in rows: + while x: + p = x.bit_length() - 1 + if p in pivots: + x ^= pivots[p] + else: + pivots[p] = x + break + return list(pivots.values()) + + +def rankq(rows): + """Fraction-free exact Gaussian elimination over Q.""" + pivots = {} + for original in rows: + row = list(original) + for p, b in sorted(pivots.items()): + if row[p]: + a, c = row[p], b[p] + row = [c * x - a * y for x, y in zip(row, b)] + g = gcd(*row) + if g: + row = [x // g for x in row] + p = next((j for j, x in enumerate(row) if x), None) + if p is not None: + pivots[p] = row + return len(pivots) + + +def inverse(matrix): + n = len(matrix) + a = [[Fraction(x) for x in row] + + [Fraction(int(i == j)) for j in range(n)] + for i, row in enumerate(matrix)] + for j in range(n): + k = next(i for i in range(j, n) if a[i][j]) + a[j], a[k] = a[k], a[j] + pivot = a[j][j] + a[j] = [x / pivot for x in a[j]] + for i in range(n): + if i != j: + c = a[i][j] + a[i] = [x - c * y for x, y in zip(a[i], a[j])] + return [row[n:] for row in a] + + +def geometry(fault=None): + lines = [] + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + r = [0] * 8 + r[i], r[j] = 2, 2 * sign + lines.append(tuple(r)) + for signs in product((-1, 1), repeat=7): + r = (1,) + signs + if sum(x < 0 for x in r) % 2 == 0: + lines.append(r) + simple = [(1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0)] + for i in range(6): + r = [0] * 8 + r[i], r[i + 1] = -2, 2 + simple.append(tuple(r)) + if fault == "geometry": + lines[0] = tuple(x + (i == 0) for i, x in enumerate(lines[0])) + assert len(lines) == 120 and all(dot(r, r) == 8 for r in lines), "invalid root geometry" + ainv = inverse(simple) + supports = [] + for r in lines: + coordinates = [sum(r[k] * ainv[k][j] for k in range(8)) + for j in range(8)] + assert all(x.denominator == 1 for x in coordinates) + assert all(x >= 0 for x in coordinates) or all(x <= 0 for x in coordinates) + supports.append(sum(1 << j for j, x in enumerate(coordinates) if x)) + return lines, simple, ainv, supports + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", type=Path, help="write the deterministic JSON receipt") + parser.add_argument("--negative-controls", action="store_true", + help="also check rejection of three corruptions and Python -O") + parser.add_argument("--fault", choices=("geometry", "parity", "flat"), help=argparse.SUPPRESS) + args = parser.parse_args() + lines, simple, ainv, supports = geometry(args.fault) + b = [sum(((1 + dot(x, y) // 4) % 2) << j + for j, y in enumerate(lines)) for x in lines] + assert all(dot(x, y) % 4 == 0 for x in lines for y in lines) + assert len(basis2(b)) == 9 + # Track self-pairing parity as well as reader supports. In characteristic + # two, q(sum a_i u_i) = sum a_i q(u_i); all root labels have q=1. + pivots = {} + for row in b: + x, odd = row, 1 + while x: + p = x.bit_length() - 1 + if p in pivots: + x ^= pivots[p][0] + odd ^= pivots[p][1] + else: + pivots[p] = (x, odd) + break + if not x: + assert odd == 0 + code = [(0, 0)] + for row, odd in pivots.values(): + code += [(x ^ row, q ^ odd) for x, q in code] + code.sort() + if args.fault == "parity": + code = [(x, q ^ int(x == b[0])) for x, q in code] + assert len(set(x for x, _ in code)) == 512 + assert all((row, 1) in code for row in b), "invalid root-label parity" + nonzero = [(x, q) for x, q in code if x] + code_set = set(code) + # Check Weyl equivariance using all eight simple reflections, including + # parity. This avoids assuming an arbitrary labeling is preserved. + index = {r: i for i, r in enumerate(lines)} + index.update({tuple(-x for x in r): i for i, r in enumerate(lines)}) + for a in simple: + perm = [] + for r in lines: + t = dot(r, a) + assert t % 4 == 0 + perm.append(index[tuple(x - t // 4 * y for x, y in zip(r, a))]) + assert len(set(perm)) == 120 + for support, odd in code: + transported = sum(1 << perm[i] for i in range(120) if support >> i & 1) + assert (transported, odd) in code_set + census = [] + minima = [] + witnesses = [] + for d in range(8): + best = None + for chosen in combinations(range(8), d): + subset = sum(1 << j for j in chosen) + flat = sum(1 << i for i, support in enumerate(supports) + if support & ~subset == 0) + if args.fault == "flat" and d == 6: + flat |= 1 << next(i for i in range(120) if not (flat >> i & 1)) + assert rankq([r for i, r in enumerate(lines) if flat >> i & 1]) == d, "invalid flat rank" + distances = [(pop(reader & ~flat), reader, odd) for reader, odd in nonzero] + distance, reader, odd = min(distances) + record = {"dimension": d, "simple_indices": list(chosen), + "root_lines": pop(flat), "minimum_deletions": distance, + "odd_minimum_deletions": min(x[0] for x in distances if x[2]), + "minimizer_count": sum(x[0] == distance for x in distances)} + census.append(record) + if best is None or distance < best[0]: + best = (distance, reader, flat, chosen) + distance, reader, flat, chosen = best + deletion = reader & ~flat + surviving = [r for i, r in enumerate(lines) if (reader & flat) >> i & 1] + assert rankq(surviving) == d + minima.append(distance) + witnesses.append({"dimension": d, "simple_indices": list(chosen), + "reader_lines": [i for i in range(120) if reader >> i & 1], + "punctures": [i for i in range(120) if deletion >> i & 1]}) + assert minima == [56, 55, 53, 50, 44, 36, 26, 1] + hyperplanes = [r for r in census if r["dimension"] == 7] + # Unique exceptional root hyperplane; all other normal lines need >=14. + assert sorted(r["minimum_deletions"] for r in hyperplanes) == [1, 14, 27, 28, 33, 35, 40, 43] + for record in hyperplanes: + omitted = next(j for j in range(8) if j not in record["simple_indices"]) + normal = [ainv[i][omitted] for i in range(8)] + den = lcm(*(x.denominator for x in normal)) + normal = [int(x * den) for x in normal] + g = gcd(*normal) + normal = [x // g for x in normal] + if next(x for x in normal if x) < 0: + normal = [-x for x in normal] + record["normal"] = normal + is_root = any(rankq([normal, r]) == 1 for r in lines) + assert is_root == (record["minimum_deletions"] == 1) + if is_root: + flat = sum(1 << i for i, r in enumerate(lines) if dot(normal, r) == 0) + cheap = [R for R, _ in nonzero if pop(R & ~flat) < 14] + root = next(i for i, r in enumerate(lines) if rankq([normal, r]) == 1) + assert cheap == [b[root]] and pop(b[root] & ~flat) == 1 + + def star_cost(punctures): + weighted = [] + for reader, _ in nonzero: + live = reader & ~punctures + rank = rankq([r for i, r in enumerate(lines) if live >> i & 1]) + weighted.append((rank, reader)) + selected, cost = [], 0 + for weight, reader in sorted(weighted): + if len(basis2(selected + [reader])) > len(selected): + selected.append(reader) + cost += weight + if len(selected) == 9: + break + return cost, dict(sorted(Counter(x[0] for x in weighted).items())) + + independent = [] + for i in range(120): + if len(basis2([b[j] for j in independent + [i]])) > len(independent): + independent.append(i) + if len(independent) == 9: + break + control_cost, control_hist = star_cost(sum(1 << i for i in independent)) + assert control_cost == 63 + d7 = next(r for r in hyperplanes if r["minimum_deletions"] == 14) + h = sum(1 << i for i, r in enumerate(lines) if dot(d7["normal"], r) == 0) + d7_readers = [r for r, odd in nonzero if pop(r & ~h) == 14] + assert len(d7_readers) == 1 + punctures = d7_readers[0] & ~h + d7_cost, d7_hist = star_cost(punctures) + assert pop(punctures) == 14 and d7_cost == 64 + assert len(basis2([b[i] for i in range(120) if punctures >> i & 1])) == 8 + assert Fraction(54, 94) > Fraction(63, 111) + result = {"schema": 1, "arithmetic": "exact integer and rational; standard library", + "root_lines": 120, "label_rank": 9, + "reader_weight_histogram": dict(sorted(Counter(pop(x) for x, _ in code).items())), + "minimum_punctures_for_reader_rank_at_most_d": minima, + "census": census, "sharp_witnesses": witnesses, + "independent_nine_control": {"punctures": independent, "star_cost": control_cost, + "reader_rank_histogram": control_hist}, + "sharp_fourteen_control": {"punctures": [i for i in range(120) if punctures >> i & 1], + "star_cost": d7_cost, "reader_rank_histogram": d7_hist}, + "optimal_star_cost_per_port_up_to_35_punctures": "63/111", + "scope": "bit E8 label decoders, star copy cost only; no supplier or kappa claim"} + if args.write: + args.write.write_text(json.dumps(result, indent=2) + "\n") + print("PASS: 255 standard parabolic flats; 511 nonzero reader supports; 8 Weyl generators") + print("PASS: sharp rank thresholds", minima) + print("PASS: non-root normal threshold 14; sharp D7 puncture costs 64") + print("PASS: optimum star cost/port among <=35 punctures is 63/111 (proof in README)") + if args.negative_controls: + script = str(Path(__file__).resolve()) + for fault, expected in [("geometry", "invalid root geometry"), + ("parity", "invalid root-label parity"), + ("flat", "invalid flat rank")]: + run = subprocess.run([sys.executable, script, "--fault", fault], + capture_output=True, text=True) + assert run.returncode != 0 and expected in run.stderr, (fault, run.stderr) + with tempfile.TemporaryDirectory(prefix="e8-puncture-negative-") as tmp: + receipt = Path(tmp) / "must-not-exist.json" + run = subprocess.run([sys.executable, "-O", script, "--write", str(receipt)], + capture_output=True, text=True) + assert run.returncode != 0 and "Refusing optimized Python" in run.stderr + assert not receipt.exists() + print("PASS: rejected corrupt geometry, parity and flat; rejected -O before writing") + + +if __name__ == "__main__": + main() diff --git a/research/e8-joint-reader-bound/test_package.py b/research/e8-joint-reader-bound/test_package.py new file mode 100644 index 0000000000..a8b4906e17 --- /dev/null +++ b/research/e8-joint-reader-bound/test_package.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +"""Relocation and evidence-corruption controls for the isolated research package.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + + +class PackageChecks(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory(prefix="e8 joint reader ") + self.root = Path(self.temp.name) / "relocated package" + shutil.copytree(HERE, self.root, ignore=shutil.ignore_patterns("__pycache__")) + + def tearDown(self): + self.temp.cleanup() + + def run_script(self, script, *args, optimized=True): + flags = ["-I", "-B"] + (["-O"] if optimized else []) + return subprocess.run([sys.executable, *flags, str(self.root / script), *map(str, args)], + cwd=self.temp.name, capture_output=True, text=True, timeout=60) + + def require_pass(self, result, marker): + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn(marker, result.stdout) + + def require_failure(self, result, marker): + self.assertNotEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn(marker, result.stderr) + + def test_relocated_optimized_replay_and_identical_regeneration(self): + self.require_pass(self.run_script("verify.py"), "PASS_E8_JOINT_READER") + self.require_pass(self.run_script("independent_check.py"), "PASS_E8_JOINT_INDEPENDENT") + output = self.root / "regenerated.json" + self.require_pass(self.run_script("verify.py", "--write", output), "PASS_E8_JOINT_READER") + self.assertEqual(output.read_bytes(), (self.root / "CERTIFICATE.json").read_bytes()) + + def test_primary_rejects_changed_cost_bound(self): + path = self.root / "CERTIFICATE.json" + receipt = json.loads(path.read_text()) + receipt["bounds"][36]["combined_lower_bound"] -= 1 + path.write_text(json.dumps(receipt)) + self.require_failure(self.run_script("verify.py"), "certificate mismatch") + + def test_both_reject_changed_flat_capacity(self): + path = self.root / "CERTIFICATE.json" + receipt = json.loads(path.read_text()) + receipt["independent_summary"]["flat_capacities"][5] = 21 + path.write_text(json.dumps(receipt)) + self.require_failure(self.run_script("verify.py"), "certificate mismatch") + self.require_failure(self.run_script("independent_check.py"), "independent_summary mismatch") + + def test_source_corruption_rejected_before_output_write(self): + source = self.root / "sources/pr631/README.md" + source.write_bytes(source.read_bytes() + b"\ncorruption\n") + output = self.root / "must remain unchanged.json" + output.write_text("sentinel") + result = self.run_script("verify.py", "--write", output) + self.require_failure(result, "source SHA256 mismatch") + self.assertEqual(output.read_text(), "sentinel") + + def test_pinned_predecessor_and_its_negative_controls(self): + result = self.run_script("sources/pr631/verify.py", "--negative-controls", optimized=False) + self.require_pass(result, "PASS: optimum star cost/port among <=35 punctures") + self.assertIn("rejected corrupt geometry, parity and flat", result.stdout) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/e8-joint-reader-bound/verify.py b/research/e8-joint-reader-bound/verify.py new file mode 100644 index 0000000000..dccc79c6a8 --- /dev/null +++ b/research/e8-joint-reader-bound/verify.py @@ -0,0 +1,274 @@ +#!/usr/bin/env python3 +"""Exact E8 joint-reader obstruction. Python 3.10+, standard library. + +Ross Richardson, with substantial OpenAI Codex assistance. Apache-2.0. +Definitions and parabolic reduction follow Chi Zhao's PR631; see PROOF.md. +All checks remain active under python -O. No predecessor code is imported. +""" +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from math import gcd +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def binary_basis(rows): + pivots = {} + for row in rows: + while row: + bit = row.bit_length() - 1 + if bit in pivots: + row ^= pivots[bit] + else: + pivots[bit] = row + break + return list(pivots.values()) + + +def rational_rank(rows): + pivots = {} + for original in rows: + row = list(original) + for col, basis in sorted(pivots.items()): + if row[col]: + a, b = row[col], basis[col] + row = [b * x - a * y for x, y in zip(row, basis)] + common = gcd(*row) + if common: + row = [x // common for x in row] + col = next((i for i, x in enumerate(row) if x), None) + if col is not None: + pivots[col] = row + return len(pivots) + + +def inverse(matrix): + n = len(matrix) + aug = [[Fraction(x) for x in row] + [Fraction(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + for col in range(n): + pivot = next(i for i in range(col, n) if aug[i][col]) + aug[col], aug[pivot] = aug[pivot], aug[col] + scale = aug[col][col] + aug[col] = [x / scale for x in aug[col]] + for i in range(n): + if i != col: + scale = aug[i][col] + aug[i] = [x - scale * y for x, y in zip(aug[i], aug[col])] + return [row[n:] for row in aug] + + +def geometry(): + roots = [] + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + root = [0] * 8 + root[i], root[j] = 2, 2 * sign + roots.append(tuple(root)) + roots += [(1,) + signs for signs in product((-1, 1), repeat=7) + if sum(x < 0 for x in signs) % 2 == 0] + simple = [(1, -1, -1, -1, -1, -1, -1, 1), (2, 2, 0, 0, 0, 0, 0, 0)] + for i in range(6): + root = [0] * 8 + root[i], root[i + 1] = -2, 2 + simple.append(tuple(root)) + require(len(set(roots)) == 120 and all(dot(r, r) == 8 for r in roots), + "root geometry") + inv = inverse(simple) + supports = [] + for root in roots: + coords = [sum(root[k] * inv[k][j] for k in range(8)) for j in range(8)] + require(all(x.denominator == 1 for x in coords), "integral simple coordinates") + require(all(x >= 0 for x in coords) or all(x <= 0 for x in coords), + "common-sign simple coordinates") + supports.append(sum(1 << j for j, x in enumerate(coords) if x)) + return roots, simple, supports + + +def decoder(roots, simple): + require(all(dot(x, y) % 4 == 0 for x in roots for y in roots), "integral Gram") + rows = [sum(((1 + dot(x, y) // 4) % 2) << i for i, y in enumerate(roots)) + for x in roots] + basis = binary_basis(rows) + require(len(basis) == 9, "reader code dimension") + code = [0] + for word in basis: + code += [word ^ x for x in code] + code = sorted(code) + require(len(set(code)) == 512, "reader code size") + histogram = Counter(x.bit_count() for x in code) + require(histogram == {0: 1, 56: 255, 64: 255, 120: 1}, "reader code weights") + root_index = {r: i for i, r in enumerate(roots)} + root_index.update({tuple(-x for x in r): i for i, r in enumerate(roots)}) + code_set = set(code) + for simple_root in simple: + perm = [root_index[tuple(x - (dot(r, simple_root) // 4) * y + for x, y in zip(r, simple_root))] for r in roots] + require(len(set(perm)) == 120, "reflection permutation") + for word in code: + image = sum(1 << perm[i] for i in range(120) if word >> i & 1) + require(image in code_set, "Weyl reader-code invariance") + return rows, code + + +def flat_census(roots, supports, code): + maxima = [0] * 9 + thresholds = [120] * 9 + census = [] + witnesses = [None] * 9 + for subset in range(256): + dimension = subset.bit_count() + indices = [i for i, s in enumerate(supports) if not s & ~subset] + flat = sum(1 << i for i in indices) + require(rational_rank([roots[i] for i in indices]) == dimension, "flat dimension") + distance, reader = min(((w & ~flat).bit_count(), w) for w in code[1:]) + maxima[dimension] = max(maxima[dimension], len(indices)) + if distance < thresholds[dimension]: + thresholds[dimension] = distance + witnesses[dimension] = {"simple_subset": subset, "reader": str(reader), + "deleted_indices": [i for i in range(120) + if (reader & ~flat) >> i & 1]} + census.append({"simple_subset": subset, "dimension": dimension, + "root_lines": len(indices), "minimum_deletions": distance}) + require(maxima == [0, 1, 3, 6, 12, 20, 36, 63, 120], "flat capacities") + require(thresholds == [56, 55, 53, 50, 44, 36, 26, 1, 0], "reader thresholds") + for d, witness in enumerate(witnesses): + deleted = sum(1 << i for i in witness["deleted_indices"]) + reader = int(witness["reader"]) + require(rational_rank([r for i, r in enumerate(roots) + if (reader & ~deleted) >> i & 1]) == d, "sharp threshold witness") + return maxima, thresholds, census, witnesses + + +def pair_bound(p, capacities, thresholds): + require(0 <= p < 56, "puncture domain must retain all nine reader dimensions") + candidates = [(a + 8 * b, a, b) for a in range(9) for b in range(a, 9) + if thresholds[a] <= p and thresholds[b] <= p + and capacities[a] + capacities[b] >= 84 - p] + require(bool(candidates), "nonempty relaxation") + return min(candidates) + + +def check_invoice(p, ranks, capacities, thresholds): + require(0 <= p < 56, "puncture domain must retain all nine reader dimensions") + require(len(ranks) == 9 and all(type(d) is int and 0 <= d <= 8 for d in ranks), + "nine physical ranks required") + require(all(thresholds[d] <= p for d in ranks), "single-reader threshold") + require(all(capacities[a] + capacities[b] >= 84 - p for a, b in combinations(ranks, 2)), + "joint-reader union constraint") + + +def negative_controls(capacities, thresholds): + cases = [(36, [5] * 9, "joint-reader union constraint"), + (43, [5, 5] + [6] * 7, "joint-reader union constraint"), + (51, [4, 5] + [6] * 7, "joint-reader union constraint"), + (35, [5] + [8] * 8, "single-reader threshold"), + (55, [5] * 8, "nine physical ranks required"), + (56, [0] + [8] * 8, "puncture domain")] + names = [] + for p, ranks, expected in cases: + try: + check_invoice(p, ranks, capacities, thresholds) + except ValueError as exc: + require(expected in str(exc), "negative control wrong rejection") + names.append({"punctures": p, "ranks": ranks, "rejected_by": expected}) + else: + raise ValueError("negative control unexpectedly accepted") + # These satisfy necessary inequalities; they are NOT constructed decoders. + for p, ranks in [(44, [5] * 9), (52, [4] + [5] * 8)]: + check_invoice(p, ranks, capacities, thresholds) + return names + + +def source_pins(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for entry in manifest["retained_sources"]: + data = (HERE / entry["local_path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == entry["sha256"], "source SHA256 mismatch") + git_blob = hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + require(git_blob == entry["git_blob"], "source Git blob mismatch") + return {entry["local_path"]: entry["sha256"] for entry in manifest["retained_sources"]} + + +def build(): + pins = source_pins() + roots, simple, supports = geometry() + rows, code = decoder(roots, simple) + capacities, thresholds, census, witnesses = flat_census(roots, supports, code) + union_hist = Counter((a | b).bit_count() for a, b in combinations(code[1:], 2)) + require(min(union_hist) == 84, "two-reader minimum union") + require(sum(union_hist.values()) == 130305, "complete distinct-reader pair census") + pair_witness = next((a, b) for a, b in combinations(code[1:], 2) if (a | b).bit_count() == 84) + bounds = [] + for p in range(56): + cost, a, b = pair_bound(p, capacities, thresholds) + # PR631 supplies the sharper bound for p<=8, replayed by the pinned + # predecessor verifier and proved in its retained README. + combined = max(cost, 72 - p) if p <= 8 else cost + ratio = Fraction(combined, 120 - p) + require(ratio >= Fraction(63, 111), "star ratio exclusion") + require(ratio > Fraction(63, 111) or p == 9, "strictness away from nine punctures") + bounds.append({"punctures": p, "relaxed_pair_cost": cost, "minimizing_ranks": [a] + [b] * 8, + "combined_lower_bound": combined, "ratio_lower_bound": str(ratio)}) + controls = negative_controls(capacities, thresholds) + require(binary_basis([pair_witness[0], pair_witness[0]]) == [pair_witness[0]], + "dependent pair boundary") + require(pair_witness[0].bit_count() < 84, "distinct-pair hypothesis is necessary") + # Verify the rank-loss stopping boundary explicitly. + first_reader = next(w for w in code if w.bit_count() == 56) + deleted_roots = [i for i in range(120) if first_reader >> i & 1] + live_rows = [r & ~first_reader for r in rows] + require(len(binary_basis(live_rows)) == 8, "56-puncture rank-loss boundary") + independent_summary = { + "flat_capacities": capacities, + "single_reader_thresholds": thresholds, + "reader_weight_histogram": {str(k): v for k, v in sorted(Counter(w.bit_count() for w in code).items())}, + "pair_union_minimum": 84, + "rank_invoice_minima_36_through_55": [row["relaxed_pair_cost"] for row in bounds[36:]], + } + return {"schema": 1, "scope": "real E8 root-only star reader cost; no new kappa", + "base_commit": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", "assignment_seed": 46, + "source_sha256": pins, "independent_summary": independent_summary, + "single_reader_thresholds": thresholds, "flat_census": census, + "threshold_witnesses": witnesses, + "pair_union_histogram": {str(k): v for k, v in sorted(union_hist.items())}, + "minimum_pair_witness": [str(x) for x in pair_witness], + "bounds": bounds, "negative_controls": controls, + "rank_loss_boundary": {"punctures": deleted_roots, "live_label_rank": 8}, + "coverage": {"standard_flats": 256, "nonzero_readers": 511, + "distinct_reader_pairs": 130305, "puncture_budgets": 56, + "Weyl_generators": 8, "random_search": False}, + "theorem": "C_star(P)/(120-|P|) >= 63/111 for |P|<=55, with equality possible only at |P|=9"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write a regenerated certificate after all checks pass") + parser.add_argument("--check", type=Path, default=HERE / "CERTIFICATE.json") + args = parser.parse_args() + result = build() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.write: + args.write.write_text(encoded) + else: + require(json.loads(args.check.read_text()) == result, "certificate mismatch") + print("PASS_E8_JOINT_READER: 256 flats; 511 readers; 130305 pairs; " + "punctures 0..55; 6 rejection controls; no new kappa") + + +if __name__ == "__main__": + main()