From 7f334e4c749fd83d03feb6c1de4e4cda9534c9dc Mon Sep 17 00:00:00 2001 From: mightyOil <82899331+mightyOil@users.noreply.github.com> Date: Tue, 13 Oct 2026 10:58:21 +0200 Subject: [PATCH] Research: classify the first E8 rank-five puncture boundary --- research/e8-rank5-boundary/CERTIFICATE.json | 1650 +++++++++++++++++ research/e8-rank5-boundary/CLAIM.json | 72 + research/e8-rank5-boundary/NOTICE.md | 25 + research/e8-rank5-boundary/README.md | 229 +++ research/e8-rank5-boundary/SOURCES.json | 21 + research/e8-rank5-boundary/VALIDATION.md | 47 + .../e8-rank5-boundary/independent_check.py | 265 +++ .../e8-rank5-boundary/sources/pr631/README.md | 190 ++ .../e8-rank5-boundary/sources/pr631/verify.py | 279 +++ research/e8-rank5-boundary/test_package.py | 62 + research/e8-rank5-boundary/verify.py | 302 +++ 11 files changed, 3142 insertions(+) create mode 100644 research/e8-rank5-boundary/CERTIFICATE.json create mode 100644 research/e8-rank5-boundary/CLAIM.json create mode 100644 research/e8-rank5-boundary/NOTICE.md create mode 100644 research/e8-rank5-boundary/README.md create mode 100644 research/e8-rank5-boundary/SOURCES.json create mode 100644 research/e8-rank5-boundary/VALIDATION.md create mode 100644 research/e8-rank5-boundary/independent_check.py create mode 100644 research/e8-rank5-boundary/sources/pr631/README.md create mode 100644 research/e8-rank5-boundary/sources/pr631/verify.py create mode 100644 research/e8-rank5-boundary/test_package.py create mode 100644 research/e8-rank5-boundary/verify.py diff --git a/research/e8-rank5-boundary/CERTIFICATE.json b/research/e8-rank5-boundary/CERTIFICATE.json new file mode 100644 index 0000000000..25c58b0f18 --- /dev/null +++ b/research/e8-rank5-boundary/CERTIFICATE.json @@ -0,0 +1,1650 @@ +{ + "all_flat_reader_pairs": 130305, + "basis_witnesses": [ + { + "basis_reader_ranks": [ + 5, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8 + ], + "basis_reader_root_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 + ], + [ + 8, + 9, + 14, + 15, + 16, + 17, + 18, + 19, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 32, + 33, + 34, + 35, + 36, + 37, + 40, + 41, + 42, + 43, + 46, + 47, + 48, + 49, + 54, + 55, + 56, + 57, + 60, + 61, + 64, + 65, + 68, + 69, + 72, + 73, + 76, + 77, + 80, + 81, + 84, + 85, + 88, + 89, + 92, + 93, + 96, + 97, + 100, + 101, + 104, + 105, + 108, + 109, + 112, + 113, + 116, + 117 + ], + [ + 2, + 3, + 4, + 5, + 6, + 7, + 10, + 11, + 12, + 13, + 20, + 21, + 26, + 27, + 28, + 29, + 32, + 33, + 34, + 35, + 36, + 37, + 40, + 41, + 42, + 43, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 62, + 63, + 66, + 67, + 70, + 71, + 74, + 75, + 78, + 79, + 82, + 83, + 86, + 87, + 88, + 89, + 92, + 93, + 96, + 97, + 100, + 101, + 104, + 105, + 108, + 109, + 112, + 113, + 116, + 117 + ], + [ + 0, + 1, + 4, + 5, + 6, + 7, + 10, + 11, + 12, + 13, + 16, + 17, + 18, + 19, + 22, + 23, + 24, + 25, + 30, + 31, + 36, + 37, + 40, + 41, + 42, + 43, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 62, + 63, + 66, + 67, + 70, + 71, + 72, + 73, + 76, + 77, + 80, + 81, + 84, + 85, + 90, + 91, + 94, + 95, + 98, + 99, + 102, + 103, + 104, + 105, + 108, + 109, + 112, + 113, + 116, + 117 + ], + [ + 0, + 1, + 2, + 3, + 6, + 7, + 10, + 11, + 12, + 13, + 14, + 15, + 18, + 19, + 22, + 23, + 24, + 25, + 28, + 29, + 32, + 33, + 34, + 35, + 38, + 39, + 46, + 47, + 48, + 49, + 54, + 55, + 58, + 59, + 62, + 63, + 64, + 65, + 68, + 69, + 74, + 75, + 78, + 79, + 80, + 81, + 84, + 85, + 90, + 91, + 94, + 95, + 96, + 97, + 100, + 101, + 106, + 107, + 110, + 111, + 112, + 113, + 116, + 117 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 22, + 23, + 24, + 25, + 26, + 27, + 32, + 33, + 34, + 35, + 40, + 41, + 42, + 43, + 44, + 45, + 54, + 55, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109, + 114, + 115, + 116, + 117 + ], + [ + 10, + 11, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 34, + 35, + 36, + 37, + 38, + 39, + 42, + 43, + 44, + 45, + 48, + 49, + 52, + 53, + 56, + 58, + 60, + 62, + 64, + 66, + 68, + 70, + 72, + 74, + 76, + 78, + 80, + 82, + 84, + 86, + 88, + 90, + 92, + 94, + 96, + 98, + 100, + 102, + 104, + 106, + 108, + 110, + 112, + 114, + 116, + 118 + ], + [ + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 36, + 37, + 38, + 39, + 40, + 41, + 44, + 45, + 46, + 47, + 50, + 51, + 56, + 59, + 61, + 62, + 65, + 66, + 68, + 71, + 73, + 74, + 76, + 79, + 80, + 83, + 85, + 86, + 89, + 90, + 92, + 95, + 96, + 99, + 101, + 102, + 104, + 107, + 109, + 110, + 113, + 114, + 116, + 119 + ], + [ + 0, + 2, + 4, + 6, + 8, + 10, + 13, + 15, + 17, + 19, + 21, + 23, + 24, + 27, + 29, + 31, + 33, + 34, + 37, + 39, + 41, + 42, + 45, + 47, + 48, + 51, + 52, + 54, + 56, + 63, + 67, + 69, + 70, + 71, + 75, + 77, + 78, + 79, + 81, + 82, + 83, + 84, + 85, + 86, + 91, + 93, + 94, + 95, + 97, + 98, + 99, + 100, + 101, + 102, + 105, + 106, + 107, + 108, + 109, + 110, + 112, + 113, + 114, + 116 + ] + ], + "deleted_root_indices": [ + 8, + 9, + 10, + 11, + 12, + 13, + 20, + 21, + 22, + 23, + 24, + 25, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55 + ] + }, + { + "basis_reader_ranks": [ + 5, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8 + ], + "basis_reader_root_indices": [ + [ + 0, + 1, + 2, + 3, + 4, + 5, + 14, + 15, + 16, + 17, + 26, + 27, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + [ + 0, + 2, + 5, + 6, + 8, + 11, + 12, + 14, + 17, + 18, + 20, + 23, + 24, + 27, + 28, + 30, + 33, + 34, + 37, + 39, + 40, + 43, + 44, + 47, + 48, + 51, + 52, + 55, + 56, + 58, + 59, + 60, + 61, + 63, + 66, + 68, + 70, + 71, + 72, + 73, + 75, + 77, + 80, + 82, + 83, + 84, + 85, + 87, + 88, + 89, + 91, + 93, + 96, + 98, + 99, + 100, + 101, + 103, + 105, + 110, + 112, + 113, + 115, + 117 + ], + [ + 0, + 3, + 4, + 6, + 8, + 11, + 12, + 15, + 16, + 18, + 20, + 23, + 24, + 27, + 29, + 31, + 32, + 35, + 36, + 38, + 41, + 42, + 44, + 47, + 48, + 51, + 52, + 55, + 56, + 58, + 59, + 60, + 61, + 63, + 64, + 65, + 67, + 69, + 74, + 76, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 87, + 88, + 89, + 91, + 93, + 97, + 102, + 104, + 106, + 107, + 108, + 109, + 111, + 112, + 113, + 115, + 117 + ], + [ + 1, + 2, + 4, + 6, + 8, + 11, + 12, + 15, + 17, + 19, + 21, + 22, + 25, + 26, + 28, + 30, + 33, + 34, + 36, + 38, + 41, + 42, + 44, + 47, + 48, + 51, + 52, + 55, + 56, + 58, + 59, + 60, + 61, + 63, + 64, + 65, + 67, + 69, + 72, + 73, + 75, + 77, + 81, + 86, + 90, + 92, + 94, + 95, + 96, + 98, + 99, + 100, + 101, + 103, + 104, + 106, + 107, + 108, + 109, + 111, + 112, + 113, + 115, + 117 + ], + [ + 1, + 3, + 5, + 7, + 9, + 10, + 13, + 14, + 16, + 18, + 20, + 23, + 24, + 26, + 28, + 30, + 33, + 34, + 36, + 38, + 41, + 42, + 44, + 47, + 48, + 51, + 52, + 55, + 57, + 62, + 66, + 68, + 70, + 71, + 74, + 76, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 87, + 90, + 92, + 94, + 95, + 96, + 98, + 99, + 100, + 101, + 103, + 104, + 106, + 107, + 108, + 109, + 111, + 112, + 113, + 115, + 117 + ], + [ + 6, + 7, + 8, + 9, + 18, + 19, + 20, + 21, + 28, + 29, + 30, + 31, + 36, + 37, + 38, + 39, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 58, + 59, + 60, + 61, + 66, + 67, + 68, + 69, + 74, + 75, + 76, + 77, + 82, + 83, + 84, + 85, + 90, + 91, + 92, + 93, + 98, + 99, + 100, + 101, + 106, + 107, + 108, + 109, + 114, + 115, + 116, + 117 + ], + [ + 0, + 2, + 5, + 6, + 9, + 10, + 12, + 14, + 17, + 18, + 21, + 22, + 24, + 27, + 28, + 31, + 32, + 34, + 37, + 38, + 41, + 43, + 45, + 46, + 48, + 51, + 53, + 54, + 56, + 57, + 59, + 60, + 62, + 63, + 65, + 68, + 69, + 71, + 72, + 74, + 75, + 78, + 80, + 81, + 83, + 84, + 86, + 87, + 88, + 90, + 91, + 94, + 96, + 97, + 99, + 100, + 102, + 103, + 106, + 109, + 112, + 114, + 115, + 118 + ], + [ + 0, + 2, + 5, + 6, + 9, + 11, + 13, + 14, + 17, + 18, + 21, + 23, + 25, + 27, + 28, + 31, + 33, + 35, + 37, + 38, + 40, + 42, + 45, + 47, + 49, + 50, + 52, + 54, + 56, + 57, + 58, + 61, + 62, + 63, + 64, + 68, + 69, + 70, + 73, + 74, + 75, + 79, + 80, + 81, + 82, + 85, + 86, + 87, + 89, + 90, + 91, + 95, + 96, + 97, + 98, + 101, + 102, + 103, + 107, + 108, + 113, + 114, + 115, + 119 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 8, + 9, + 10, + 11, + 12, + 13, + 18, + 19, + 28, + 29, + 36, + 37, + 44, + 45, + 46, + 47, + 48, + 49, + 56, + 57, + 58, + 59, + 64, + 65, + 66, + 67, + 72, + 73, + 74, + 75, + 80, + 81, + 82, + 83, + 88, + 89, + 90, + 91, + 96, + 97, + 98, + 99, + 104, + 105, + 106, + 107, + 112, + 113, + 114, + 115 + ] + ], + "deleted_root_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 + ] + } + ], + "comparison_ratio": "21/37", + "conjugacy_generators": [ + 5, + 4, + 3, + 1, + 2, + 0, + 3, + 2, + 4, + 3, + 1, + 5, + 4, + 3, + 2, + 0 + ], + "equality_orbit_size": 7560, + "equality_ratio": "31/42", + "generic_ratio_lower_bound": "9/14", + "independent_summary": { + "binary_dimension": 9, + "equality_pairs": [ + { + "deleted_root_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_root_indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 14, + 15, + 16, + 17, + 26, + 27, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111 + ], + "simple_indices": [ + 0, + 1, + 2, + 3, + 4 + ] + }, + { + "deleted_root_indices": [ + 8, + 9, + 10, + 11, + 12, + 13, + 20, + 21, + 22, + 23, + 24, + 25, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55 + ], + "reader_root_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 + ], + "simple_indices": [ + 1, + 2, + 3, + 4, + 5 + ] + } + ], + "flat_count": 56, + "minimum_deletions": 36, + "pairs_tested": 28616, + "punctures": [ + { + "cheap_rank_by_threshold": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 8 + ], + "deleted_root_indices": [ + 8, + 9, + 10, + 11, + 12, + 13, + 20, + 21, + 22, + 23, + 24, + 25, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55 + ], + "reader_rank_histogram": { + "5": 1, + "7": 42, + "8": 468 + }, + "star_cost": 62 + }, + { + "cheap_rank_by_threshold": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 8 + ], + "deleted_root_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_rank_histogram": { + "5": 1, + "7": 42, + "8": 468 + }, + "star_cost": 62 + } + ], + "reader_weight_histogram": { + "120": 1, + "56": 255, + "64": 255 + } + }, + "negative_controls": [ + "root", + "decoder", + "flat", + "distinct-cost-61-nonspanning-readers", + "wrong-characteristic" + ], + "orbit_sha256": "78aa98385aaa91de045d10876b460eb19f4d105e1a1fd68ad156524f4f6253bb", + "predecessor_sources": { + "sources/pr631/README.md": "281f706bf29d1f91dd64ba096f9d66d622f49e9d82d0ff306fb9374f77ba7333", + "sources/pr631/verify.py": "9add2f1d71466f00963652b818e168fe2e2a4fa6e62cafa9811389fdba7000c2" + }, + "rank_loss_thresholds": [ + 56, + 55, + 53, + 50, + 44, + 36, + 26, + 1 + ], + "schema": "e8-rank5-boundary-v1", + "single_port_restoration_controls": 72 +} diff --git a/research/e8-rank5-boundary/CLAIM.json b/research/e8-rank5-boundary/CLAIM.json new file mode 100644 index 0000000000..bb3e7693c0 --- /dev/null +++ b/research/e8-rank5-boundary/CLAIM.json @@ -0,0 +1,72 @@ +{ + "assignment_seed": 46, + "randomness": "Python secrets.randbelow(100), OS randomness, drawn once at 2026-10-13T08:35:58Z", + "track": "structural decoder research", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "claimed_at": "2026-10-13T08:41:34.289802+00:00", + "expected_finish": "2026-10-13T09:35:00Z", + "coordination": "GitHub GraphQL pinnedIssues empty; only open issue #650 requests Discussions. No reservation issue created. Claim recorded locally.", + "candidates": [ + { + "object": "Hurwitz adaptive nonlinear message supports", + "decision": "deferred; fixed-support #785 already complete and physical adaptive metadata pricing is unresolved" + }, + { + "object": "E8 first rank-five puncture boundary: exactly 36 deleted root lines", + "decision": "selected; #631 explicitly leaves 36 as its first open rank-threshold boundary. Enumerate all equality cases modulo Weyl conjugacy and optimize each star basis exactly." + }, + { + "object": "P112 extra-total decoder lift", + "decision": "rejected as overlapping #845; multiple lifts too broad for this sprint" + } + ], + "diversification": "46 modulo 3 = 1 selects the second candidate; restrict to the first previously unexcluded rank-five boundary, not a frontier-word retuning.", + "hypothesis": "At exactly 36 punctures, no star label decoder beats 63/111 copy cost per live port; cheap-reader compatibility may close the coarse rank-floor gap.", + "method": "Generate E8 roots and binary reader code; enumerate standard rank-five parabolic flats and all 511 nonzero reader words with exactly 36 deletions; quotient duplicate punctures, compute exact rational reader ranks and minimum-weight F2 bases. Inherited Weyl/parabolic reduction upgrades this equality census to all 36-puncture sets possessing a rank-five reader. Other sets have rank floor six.", + "deliverable": "Scoped negative-result note with written reduction, exact deterministic receipt, source pins, independent verification and mutation controls; no supplier or kappa claim.", + "stopping_rule": "Complete all 56 standard rank-five flats times 511 readers and all resulting equality punctures; no general deep-puncture annealing.", + "overlap_snapshot": { + "open_prs": 660, + "max_pr": 857, + "inspected": [ + 620, + 631, + 669, + 703, + 717, + 738, + 765, + 767, + 785, + 814, + 845, + 848, + 855 + ] + }, + "status": "completed", + "final_overlap_check": { + "checked_at": "2026-10-13T08:56:20.809094+00:00", + "open_prs": 667, + "max_pr": 874, + "main_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "pr631_head": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "pinned_coordination_issues": 0, + "finding": "No overlap with the exact 36-puncture equality classification. New #868 is Gaussian all-clique dual scope; #874 audits X4 ideal gain additivity." + }, + "result_update": { + "at": "2026-10-13T08:58:21.815166+00:00", + "classification": "scoped negative result; no new kappa", + "finding": "Every 36-puncture E8 star label decoder has cost at least 54 on 84 live ports. Exactly 7,560 punctures admitting a rank-five reader form one Weyl orbit and have exact star cost 62. Thus no 36-puncture set improves 63/111, extending PR631 through 36.", + "completed_coverage": { + "standard_rank_five_pairs": 28616, + "all_threshold_pairs": 130305, + "standard_equality_representatives": 2, + "complete_equality_orbit": 7560, + "reader_ranks_per_representative": 511, + "single_port_restorations": 72 + }, + "result_link": "https://github.com/mightyOil/integer-mult-bounds/tree/research/e8-rank5-boundary-seed46/research/e8-rank5-boundary", + "verification": "Both exact implementations pass on CPython 3.14.7 and 3.11.15, including isolated optimized mode; package mutations, predecessor controls and selected-record check pass. See VALIDATION.md." + } +} diff --git a/research/e8-rank5-boundary/NOTICE.md b/research/e8-rank5-boundary/NOTICE.md new file mode 100644 index 0000000000..47de55278c --- /dev/null +++ b/research/e8-rank5-boundary/NOTICE.md @@ -0,0 +1,25 @@ +# Attribution and license + +This package is contributed under the repository's Apache-2.0 license. +New work: Philipp (@mightyOil), 2026, with substantial OpenAI Codex assistance +in mathematical reasoning, code, validation and documentation. Independent +computational checks were implemented by a separate AI-assisted worker; this +is not a claim of independent human or proof-assistant review. + +The two files under `sources/pr631/` are unchanged sources by **Chi Zhao**, with +substantial OpenAI Codex assistance, from CrocSwap/integer-mult-bounds PR631, +commit `fb893b5ee1317c2da3b297e6fe78eca0857d1a76`. Their source notices are +retained. They are Apache-2.0 per their own notice and the repository license. + +Their sharp threshold theorem, parabolic/Weyl reduction, and earlier +35-puncture ratio theorem remain Chi Zhao's contribution. Their original +contextual use of "current" is historical and does not refer to the new +package's base or current selected frontier. + +The star label-decoder model and minimum-weight basis formulation come from +Joel Pulikkan / GamingPuzzled's PR620. DreamingOfClouds' PR595/PR602 and +eumemic's PR543 supply earlier format and supplier context, retaining their +own predecessor credit. See README.md and SOURCES.json for exact scope and pins. + +No changes are made to `upstream/`, the predecessor files, original supplier +sources, certificates/selected-result.json or repository-wide review ledgers. diff --git a/research/e8-rank5-boundary/README.md b/research/e8-rank5-boundary/README.md new file mode 100644 index 0000000000..29a0261475 --- /dev/null +++ b/research/e8-rank5-boundary/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-rank5-boundary/SOURCES.json b/research/e8-rank5-boundary/SOURCES.json new file mode 100644 index 0000000000..e979ea2e2a --- /dev/null +++ b/research/e8-rank5-boundary/SOURCES.json @@ -0,0 +1,21 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "predecessor_pr": 631, + "predecessor_head": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "files": { + "sources/pr631/README.md": { + "sha256": "281f706bf29d1f91dd64ba096f9d66d622f49e9d82d0ff306fb9374f77ba7333", + "original_path": "research/e8-continuation-20261013/punctures/README.md" + }, + "sources/pr631/verify.py": { + "sha256": "9add2f1d71466f00963652b818e168fe2e2a4fa6e62cafa9811389fdba7000c2", + "original_path": "research/e8-continuation-20261013/punctures/verify.py" + } + }, + "context_files": { + "certificates/selected-result.json": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/bitp.py": "a692723e1844cb4d3a6c4a346e31b1d707133a1e086176fda6a3fec32d108637", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/REPORT.md": "16c53bf8afd9f91eca02b2af9c9f5f09385823fc705dd1a48153508cfdff28b6" + } +} diff --git a/research/e8-rank5-boundary/VALIDATION.md b/research/e8-rank5-boundary/VALIDATION.md new file mode 100644 index 0000000000..85de37147a --- /dev/null +++ b/research/e8-rank5-boundary/VALIDATION.md @@ -0,0 +1,47 @@ +# Validation record + +Local checks on 2026-10-13, macOS 27.0.1, arm64, CPython **3.14.7** and +**3.11.15**. These are observed local results, not hosted-CI results. + +| Check | Observed result | +|---|---| +| `python3 -B research/e8-rank5-boundary/verify.py` | PASS; complete certificate matches | +| `python3 -I -O -B research/e8-rank5-boundary/verify.py` | PASS with all checks active | +| Independent checker with `--check research/e8-rank5-boundary/CERTIFICATE.json`, ordinary and isolated optimized | PASS; entire independent summary agrees | +| Both scripts, isolated optimized CPython 3.11.15 | PASS | +| `python3 -B research/e8-rank5-boundary/test_package.py` | PASS; relocated isolated replay, byte-identical receipt, cost/orbit mutations rejected, source mutation rejected before changing existing output | +| `python3 -B research/e8-rank5-boundary/sources/pr631/verify.py --negative-controls` | PASS; original thresholds and at-most-35 controls reproduced | +| `make selected-record-check` | PASS; selected κ remains `1661634653669567/10^18` | + +The first packaging-test run exposed a mismatch in the test's expected error +substring (`independent summary` versus `independent_summary`); the verifier +correctly rejected the corrupted cost. The expectation was corrected and the +complete packaging test then passed. No mathematical output changed. + +The separate mathematical review checked the equality reduction, the distinction +between standard representatives and Weyl orbits, the all-36 exclusion, and the +cost lower-bound wording. An additional scratch calculation used Fraction +elimination on coordinate Gram matrices and verified both rank histograms, +the threshold-span identity and all 72 restorations. These checks were +AI-assisted, not independent human peer review. The reusable independent +checker is included in the package. + +The primary verifier checks 130,305 standard-flat/reader pairs across dimensions +zero through seven, including all 28,616 rank-five pairs. It then checks both +511-reader rank tables, an explicit conjugating word and the complete +7,560-mask orbit under eight generators. The independent checker separately +reconstructs the rank-five census and both rank tables, not the full orbit. + +Before submission the open-PR inventory was refreshed to **667 open PRs through +#874**. The new Gaussian all-clique note #868 concerns a different geometry +and proof method; #874 concerns X4 gain additivity. Neither overlaps this +root-only rank-five equality classification. The pinned PR631 head remained +`fb893b5ee1317c2da3b297e6fe78eca0857d1a76`, and fetched `main` remained the +original base `f567884aeb8851b6e794af1184119a3bfbe1e631`. There was still no +pinned coordination issue. + +The full `make verify`, selected supplier cold reconstruction, Lean builds and +hosted CI were **not run** for this isolated research package. No existing +generator, supplier, selected certificate, `upstream/` file or global workflow +changes. The finite computations and written coverage argument do not prove +the full conditional integer-multiplication theorem. diff --git a/research/e8-rank5-boundary/independent_check.py b/research/e8-rank5-boundary/independent_check.py new file mode 100644 index 0000000000..5f82397459 --- /dev/null +++ b/research/e8-rank5-boundary/independent_check.py @@ -0,0 +1,265 @@ +#!/usr/bin/env python3 +"""Independent exact arithmetic check of the first E8 rank-five boundary. + +Standard library only, Python >= 3.10. No project or predecessor imports. +Rational ranks use normalized Fraction RREF; binary ranks use low-column RREF. +The minimum basis cost is computed by the cumulative-rank identity, not greedy. +The finite census uses the parabolic/Weyl reduction explained in README.md. + +Prepared by Philipp (@mightyOil), with substantial OpenAI Codex assistance. +SPDX-License-Identifier: Apache-2.0 +""" + +import argparse +from collections import Counter +from fractions import Fraction +from itertools import combinations, product +import json +from pathlib import Path + + +def require(condition, message): + """Keep every check active under python -O.""" + if not condition: + raise ValueError(message) + + +def rational_rref(rows): + """Incremental, normalized RREF over Q, retaining all pivot eliminations.""" + basis = {} + width = None + for source in rows: + row = [Fraction(value) for value in source] + if width is None: + width = len(row) + require(len(row) == width, "ragged rational matrix") + for pivot in sorted(basis): + coefficient = row[pivot] + if coefficient: + row = [x - coefficient * y for x, y in zip(row, basis[pivot])] + pivot = next((i for i, value in enumerate(row) if value), None) + if pivot is None: + continue + divisor = row[pivot] + row = [value / divisor for value in row] + for old_pivot, old_row in list(basis.items()): + coefficient = old_row[pivot] + if coefficient: + basis[old_pivot] = [x - coefficient * y + for x, y in zip(old_row, row)] + basis[pivot] = row + if len(basis) == width: + break + return [(pivot, basis[pivot]) for pivot in sorted(basis)] + + +def rational_rank(rows): + return len(rational_rref(rows)) + + +def lies_in_span(vector, rref): + residual = [Fraction(value) for value in vector] + for pivot, row in rref: + coefficient = residual[pivot] + residual = [x - coefficient * y for x, y in zip(residual, row)] + return not any(residual) + + +def binary_rref(rows): + """Eliminate the lowest nonzero bit and clear it from all retained rows.""" + basis = {} + for source in rows: + require(isinstance(source, int) and source >= 0, "invalid binary row") + row = source + for pivot in sorted(basis): + if row & (1 << pivot): + row ^= basis[pivot] + if not row: + continue + pivot = (row & -row).bit_length() - 1 + for old_pivot in list(basis): + if basis[old_pivot] & (1 << pivot): + basis[old_pivot] ^= row + basis[pivot] = row + return [basis[pivot] for pivot in sorted(basis)] + + +def indices(mask, size=120): + return [i for i in range(size) if mask & (1 << i)] + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right)) + + +def validate_roots(roots): + require(len(roots) == 120 and len(set(roots)) == 120, "invalid root count") + require(all(len(row) == 8 and dot(row, row) == 8 for row in roots), + "invalid root geometry") + require(all(next(x for x in row if x) > 0 for row in roots), + "noncanonical root line representative") + require(all(dot(left, right) % 4 == 0 for left in roots for right in roots), + "nonintegral quarter Gram matrix") + + +def geometry(): + roots = [] + for left, right in combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[left], row[right] = 2, 2 * sign + roots.append(tuple(row)) + for tail in product((-1, 1), repeat=7): + if sum(value < 0 for value in tail) % 2 == 0: + roots.append((1,) + tail) + validate_roots(roots) + + simple = [(1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0)] + for coordinate in range(6): + row = [0] * 8 + row[coordinate], row[coordinate + 1] = -2, 2 + simple.append(tuple(row)) + augmented = [list(row) + [int(i == j) for j in range(8)] + for i, row in enumerate(simple)] + inverse_rows = rational_rref(augmented) + require([pivot for pivot, _ in inverse_rows] == list(range(8)), + "simple system is singular") + inverse = [row[8:] for _, row in inverse_rows] + for root in roots: + coordinates = [sum(root[k] * inverse[k][j] for k in range(8)) + for j in range(8)] + require(all(value.denominator == 1 for value in coordinates), + "nonintegral simple coordinates") + require(all(value >= 0 for value in coordinates) + or all(value <= 0 for value in coordinates), + "mixed-sign simple coordinates") + return roots, simple + + +def reader_code(roots): + rows = [sum(((1 + dot(left, right) // 4) % 2) << j + for j, right in enumerate(roots)) for left in roots] + basis = binary_rref(rows) + require(len(basis) == 9, "reader code does not have dimension nine") + words = {0} + for row in basis: + words |= {word ^ row for word in words} + words.remove(0) + require(len(words) == 511, "incorrect nonzero reader count") + require(Counter(word.bit_count() for word in words) + == {56: 255, 64: 255, 120: 1}, "incorrect reader weight distribution") + return sorted(words) + + +def census(): + roots, simple = geometry() + words = reader_code(roots) + all_roots = (1 << len(roots)) - 1 + minimum = len(roots) + pairs = [] + flat_count = 0 + tested = 0 + for chosen in combinations(range(8), 5): + flat_count += 1 + flat_rref = rational_rref(simple[i] for i in chosen) + require(len(flat_rref) == 5, "incorrect parabolic dimension") + section = sum(1 << i for i, root in enumerate(roots) + if lies_in_span(root, flat_rref)) + for word in words: + tested += 1 + deleted = word & (all_roots ^ section) + count = deleted.bit_count() + minimum = min(minimum, count) + if count == 36: + require(rational_rank(roots[i] for i in indices(word & section)) == 5, + "equality reader does not retain rank five") + pairs.append({"simple_indices": list(chosen), + "reader_root_indices": indices(word), + "deleted_root_indices": indices(deleted)}) + require(flat_count == 56 and tested == 28616, "incomplete rank-five census") + require(minimum == 36 and len(pairs) == 2, "unexpected boundary equality census") + pairs.sort(key=lambda item: (item["simple_indices"], item["reader_root_indices"])) + + punctures = [] + for deletion_tuple in sorted({tuple(pair["deleted_root_indices"]) for pair in pairs}): + deleted = sum(1 << i for i in deletion_tuple) + live = all_roots ^ deleted + ranks = [(word, rational_rank(roots[i] for i in indices(word & live))) + for word in words] + histogram = Counter(rank for _, rank in ranks) + cheap_ranks = [len(binary_rref(word for word, rank in ranks if rank <= limit)) + for limit in range(8)] + # For a rank-nine matroid with weights in {0,...,8}, any minimum basis + # contains rank({p: weight(p)<=k}) elements of weight <=k. Sum its + # complementary counts over k=0,...,7 to obtain the total weight. + cost = sum(9 - rank for rank in cheap_ranks) + require(histogram == {5: 1, 7: 42, 8: 468}, "unexpected reader-rank histogram") + require(cheap_ranks == [0, 0, 0, 0, 0, 1, 1, 8], + "unexpected cumulative cheap-reader ranks") + require(cost == 62, "unexpected minimum star-basis cost") + punctures.append({"deleted_root_indices": list(deletion_tuple), + "reader_rank_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "cheap_rank_by_threshold": cheap_ranks, + "star_cost": cost}) + require(len(punctures) == 2, "unexpected number of distinct standard punctures") + return {"binary_dimension": len(binary_rref(words)), + "reader_weight_histogram": {str(k): v for k, v in sorted( + Counter(word.bit_count() for word in words).items())}, + "flat_count": flat_count, "pairs_tested": tested, + "minimum_deletions": minimum, "equality_pairs": pairs, + "punctures": punctures} + + +def expect_rejection(function, message): + try: + function() + except ValueError: + return + raise ValueError("negative control was accepted: " + message) + + +def controls(): + require(rational_rank([[1, 2], [2, 4]]) == 1, "dependent rational rank control") + require(rational_rank([[1, 1], [1, -1]]) == 2, "rational/binary distinction control") + require(rational_rank([[1, 1], [1, 1 + Fraction(1, 10**40)]]) == 2, + "small exact rational difference was lost") + require(len(binary_rref([1, 2, 3])) == 2, "dependent binary rank control") + require(len(binary_rref([3, 3])) == 1, "duplicate binary row control") + roots, _ = geometry() + corrupted = list(roots) + corrupted[0] = (3,) + corrupted[0][1:] + expect_rejection(lambda: validate_roots(corrupted), "corrupt root norm") + expect_rejection(lambda: validate_roots([roots[1]] + roots[1:]), "duplicate root") + expect_rejection(lambda: binary_rref([-1]), "negative binary row") + plane = rational_rref([[1, 0, 1], [0, 1, 1]]) + require(lies_in_span([1, 1, 2], plane), "span membership control") + require(not lies_in_span([1, 1, 3], plane), "extra independent vector accepted") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--check", type=Path, + help="compare certificate's independent_summary with recomputed census") + parser.add_argument("--json", action="store_true", help="print the complete independent summary") + args = parser.parse_args() + controls() + summary = census() + if args.check: + certificate = json.loads(args.check.read_text(encoding="utf-8")) + require(certificate.get("independent_summary") == summary, + "certificate independent_summary differs from independent recomputation") + print("Certificate independent_summary matches independent recomputation.") + if args.json: + print(json.dumps(summary, indent=2, sort_keys=True)) + else: + print("Independent Fraction-RREF check passed (all checks active under -O).") + print("Reader dimension: 9; weight histogram: {56: 255, 64: 255, 120: 1}.") + print("56 flats x 511 readers = 28616 pairs; minimum deletions: 36; equality pairs: 2.") + print("Both punctures: rank histogram {5: 1, 7: 42, 8: 468}; " + "cumulative ranks [0, 0, 0, 0, 0, 1, 1, 8]; minimum star cost 62.") + print("Exact arithmetic and rejection controls passed.") + + +if __name__ == "__main__": + main() diff --git a/research/e8-rank5-boundary/sources/pr631/README.md b/research/e8-rank5-boundary/sources/pr631/README.md new file mode 100644 index 0000000000..b17edb488f --- /dev/null +++ b/research/e8-rank5-boundary/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-rank5-boundary/sources/pr631/verify.py b/research/e8-rank5-boundary/sources/pr631/verify.py new file mode 100644 index 0000000000..c9fd83d4e0 --- /dev/null +++ b/research/e8-rank5-boundary/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-rank5-boundary/test_package.py b/research/e8-rank5-boundary/test_package.py new file mode 100644 index 0000000000..03eb1fac5f --- /dev/null +++ b/research/e8-rank5-boundary/test_package.py @@ -0,0 +1,62 @@ +#!/usr/bin/env python3 +"""Relocation, certificate tampering and source-binding controls (stdlib). + +Philipp (@mightyOil), with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def run(package, script, arguments=(), failure=None): + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(package / script), *arguments], + cwd=package.parent, text=True, capture_output=True) + if failure is None: + if result.returncode: + raise ValueError(result.stdout + result.stderr) + elif result.returncode == 0 or failure not in result.stderr: + raise ValueError("wrong mutation outcome: " + result.stdout + result.stderr) + + +def main(): + with tempfile.TemporaryDirectory(prefix="e8-boundary-package-") as temporary: + package = Path(temporary) / "relocated" + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + certificate = package / "CERTIFICATE.json" + original = certificate.read_bytes() + run(package, "verify.py") + run(package, "independent_check.py", ["--check", str(certificate)]) + regenerated = package / "regenerated.json" + run(package, "verify.py", ["--write", str(regenerated)]) + if regenerated.read_bytes() != original: + raise ValueError("relocated certificate is not byte-identical") + changed = json.loads(original) + changed["independent_summary"]["punctures"][0]["star_cost"] -= 1 + certificate.write_text(json.dumps(changed)) + run(package, "verify.py", failure="certificate mismatch") + run(package, "independent_check.py", ["--check", str(certificate)], + failure="independent_summary differs") + changed = json.loads(original) + changed["equality_orbit_size"] -= 1 + certificate.write_text(json.dumps(changed)) + run(package, "verify.py", failure="certificate mismatch") + certificate.write_bytes(original) + source = package / "sources" / "pr631" / "README.md" + source.write_bytes(source.read_bytes() + b"\nsource mutation\n") + protected = package / "protected-output.json" + protected.write_bytes(b"existing output must survive\n") + run(package, "verify.py", ["--write", str(protected)], failure="predecessor source hash") + if protected.read_bytes() != b"existing output must survive\n": + raise ValueError("failed validation overwrote output") + print("PASS_E8_BOUNDARY_PACKAGE: isolated relocation; byte-identical receipt; " + "cost and orbit mutations rejected; source mutation rejected before output write") + + +if __name__ == "__main__": + main() diff --git a/research/e8-rank5-boundary/verify.py b/research/e8-rank5-boundary/verify.py new file mode 100644 index 0000000000..b74e769fb1 --- /dev/null +++ b/research/e8-rank5-boundary/verify.py @@ -0,0 +1,302 @@ +#!/usr/bin/env python3 +"""Exact first rank-five E8 puncture boundary; Python 3.10+, stdlib only. + +Philipp (@mightyOil), with substantial OpenAI Codex assistance. Apache-2.0. +Self-contained; imports no predecessor implementation. See README.md for scope. +""" + +import argparse +from collections import Counter, deque +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +import json +from math import gcd +from pathlib import Path + +HERE = Path(__file__).resolve().parent +CONNECTION = [5, 4, 3, 1, 2, 0, 3, 2, 4, 3, 1, 5, 4, 3, 2, 0] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def indices(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +def binary_basis(rows): + pivots = {} + for row in rows: + while row: + p = row.bit_length() - 1 + if p in pivots: + row ^= pivots[p] + else: + pivots[p] = row + break + return list(pivots.values()) + + +def rational_rank(rows): + """Integer row operations, dividing content to keep entries small.""" + pivots = {} + for source in rows: + row = list(source) + for p, old in sorted(pivots.items()): + if row[p]: + a, b = row[p], old[p] + row = [b * x - a * y for x, y in zip(row, old)] + common = gcd(*row) + if common: + row = [x // common for x in row] + nonzero = next((i for i, x in enumerate(row) if x), None) + if nonzero is not None: + pivots[nonzero] = row + if len(pivots) == 8: + break + return len(pivots) + + +def inverse(matrix): + n = len(matrix) + a = [[Fraction(x) for x in row] + + [Fraction(i == j) for j in range(n)] for i, row in enumerate(matrix)] + for j in range(n): + pivot = next(i for i in range(j, n) if a[i][j]) + a[j], a[pivot] = a[pivot], a[j] + divisor = a[j][j] + a[j] = [x / divisor for x in a[j]] + for i in range(n): + if i != j: + factor = a[i][j] + a[i] = [x - factor * y for x, y in zip(a[i], a[j])] + return [row[n:] for row in a] + + +def geometry(fault=None): + roots = [] + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + r = [0] * 8 + r[i], r[j] = 2, 2 * sign + roots.append(tuple(r)) + roots.extend((1,) + signs for signs in product((-1, 1), repeat=7) + if sum(s < 0 for s 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): + r = [0] * 8 + r[i], r[i + 1] = -2, 2 + simple.append(tuple(r)) + if fault == "root": + roots[0] = (3,) + roots[0][1:] + require(len(set(roots)) == 120 and all(dot(r, r) == 8 for r in roots), + "root geometry") + require(all(dot(x, y) % 4 == 0 for x in roots for y in roots), "Gram integrality") + inv = inverse(simple) + supports = [] + for r in roots: + coefficients = [sum(r[i] * inv[i][j] for i in range(8)) for j in range(8)] + require(all(c.denominator == 1 for c in coefficients), "simple integrality") + require(all(c >= 0 for c in coefficients) or all(c <= 0 for c in coefficients), + "simple positivity") + supports.append(sum(1 << j for j, c in enumerate(coefficients) if c)) + rows = [sum(((1 + dot(x, y) // 4) % 2) << i for i, y in enumerate(roots)) + for x in roots] + if fault == "decoder": + rows[0] ^= 1 + basis = binary_basis(rows) + require(len(basis) == 9, "binary dimension") + code = [0] + for row in basis: + code += [x ^ row for x in code] + code.sort() + require(Counter(x.bit_count() for x in code[1:]) == {56: 255, 64: 255, 120: 1}, + "reader weights") + lookup = {r: i for i, r in enumerate(roots)} + lookup.update({tuple(-v for v in r): i for i, r in enumerate(roots)}) + permutations = [] + for a in simple: + perm = [lookup[tuple(x - dot(r, a) // 4 * y for x, y in zip(r, a))] + for r in roots] + require(sorted(perm) == list(range(120)), "reflection permutation") + require({transport(x, perm) for x in code} == set(code), "reader equivariance") + permutations.append(perm) + return roots, supports, code, permutations + + +def transport(mask, permutation): + return sum(1 << permutation[i] for i in indices(mask)) + + +def analyze_puncture(roots, code, puncture): + weights = {word: rational_rank(roots[i] for i in indices(word & ~puncture)) + for word in code[1:]} + live_rank = len(binary_basis(word & ~puncture for word in code[1:])) + require(live_rank == 9, "live binary dimension") + threshold_ranks = [len(binary_basis(word for word, w in weights.items() if w <= k)) + for k in range(8)] + chosen, basis_cost = [], 0 + for word in sorted(weights, key=lambda word: (weights[word], word)): + if len(binary_basis(chosen + [word])) > len(chosen): + chosen.append(word) + basis_cost += weights[word] + if len(chosen) == 9: + break + require(basis_cost == sum(9 - r for r in threshold_ranks), "basis cost identity") + return ({"deleted_root_indices": list(indices(puncture)), + "reader_rank_histogram": {str(k): v for k, v in sorted(Counter(weights.values()).items())}, + "cheap_rank_by_threshold": threshold_ranks, "star_cost": basis_cost}, + weights, chosen) + + +def price_basis(readers, weights): + require(len(readers) == 9 and len(binary_basis(readers)) == 9, + "decoder basis does not span nine dimensions") + return sum(weights[r] for r in readers) + + +def census(fault=None): + roots, supports, code, permutations = geometry(fault) + minima, equalities = [], [] + for dimension in range(8): + best = 120 + for subset in combinations(range(8), dimension): + simple_mask = sum(1 << i for i in subset) + flat = sum(1 << i for i, support in enumerate(supports) if not support & ~simple_mask) + if fault == "flat" and dimension == 5: + flat |= 1 << next(i for i in range(120) if not flat >> i & 1) + require(rational_rank(roots[i] for i in indices(flat)) == dimension, "flat dimension") + for word in code[1:]: + deleted = word & ~flat + count = deleted.bit_count() + best = min(best, count) + if dimension == 5 and count == 36: + require(rational_rank(roots[i] for i in indices(word & flat)) == 5, + "equality reader dimension") + equalities.append({"simple_indices": list(subset), + "reader_root_indices": list(indices(word)), + "deleted_root_indices": list(indices(deleted))}) + minima.append(best) + require(minima == [56, 55, 53, 50, 44, 36, 26, 1], "rank-loss thresholds") + require(len(equalities) == 2, "equality count") + punctures = sorted({sum(1 << i for i in e["deleted_root_indices"]) for e in equalities}) + records, witnesses, restored = [], [], 0 + for p in punctures: + record, weights, chosen = analyze_puncture(roots, code, p) + require(record["reader_rank_histogram"] == {"5": 1, "7": 42, "8": 468}, "reader rank histogram") + require(record["cheap_rank_by_threshold"] == [0, 0, 0, 0, 0, 1, 1, 8], "cheap span ranks") + require(record["star_cost"] == 62, "star cost") + require(price_basis(chosen, weights) == 62, "explicit basis invoice") + special = next(word for word, cost in weights.items() if cost == 5) + for i in indices(p): + require(rational_rank(roots[j] for j in indices((special & ~p) | (1 << i))) == 6, + "single-port restoration") + restored += 1 + records.append(record) + witnesses.append({"deleted_root_indices": list(indices(p)), + "basis_reader_root_indices": [list(indices(c)) for c in chosen], + "basis_reader_ranks": [weights[c] for c in chosen]}) + # The explicit path uses the order of the two standard-flat equality rows. + first, second = [sum(1 << i for i in e["deleted_root_indices"]) for e in equalities] + moved = first + for generator in CONNECTION: + moved = transport(moved, permutations[generator]) + require(moved == second, "conjugacy word") + seen, queue = {first}, deque([first]) + while queue: + p = queue.popleft() + for perm in permutations: + image = transport(p, perm) + if image not in seen: + seen.add(image) + queue.append(image) + require(len(seen) <= 7560, "orbit exceeds certificate") + require(len(seen) == 7560 and second in seen, "closed equality orbit") + require(all(p.bit_count() == 36 for p in seen), "orbit puncture sizes") + require(Fraction(54, 84) > Fraction(63, 111), "generic ratio exclusion") + require(Fraction(62, 84) > Fraction(63, 111), "equality ratio exclusion") + summary = {"binary_dimension": 9, + "reader_weight_histogram": {"56": 255, "64": 255, "120": 1}, + "flat_count": 56, "pairs_tested": 56 * 511, "minimum_deletions": 36, + "equality_pairs": sorted(equalities, key=lambda e: (e["simple_indices"], e["reader_root_indices"])), + "punctures": sorted(records, key=lambda e: e["deleted_root_indices"])} + return {"schema": "e8-rank5-boundary-v1", "independent_summary": summary, + "rank_loss_thresholds": minima, "all_flat_reader_pairs": 255 * 511, + "equality_orbit_size": len(seen), "conjugacy_generators": CONNECTION, + "orbit_sha256": sha256(b"".join(p.to_bytes(15, "big") for p in sorted(seen))).hexdigest(), + "basis_witnesses": witnesses, "single_port_restoration_controls": restored, + "generic_ratio_lower_bound": "9/14", "equality_ratio": "31/42", + "comparison_ratio": "21/37"} + + +def check_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for relative, pin in manifest["files"].items(): + require(sha256((HERE / relative).read_bytes()).hexdigest() == pin["sha256"], + "predecessor source hash: " + relative) + return {path: pin["sha256"] for path, pin in manifest["files"].items()} + + +def negative_controls(): + controls = [] + for fault, message in [("root", "root geometry"), ("decoder", "binary dimension"), + ("flat", "flat dimension")]: + try: + census(fault) + except ValueError as error: + require(message in str(error), "wrong rejection for " + fault) + controls.append(fault) + else: + raise ValueError("accepted corruption: " + fault) + # Nine DISTINCT cheap readers appear to cost 61, but span only eight + # binary dimensions. The ninth, rank-eight reader cannot be omitted. + roots, _, code, _ = geometry() + puncture = int("ffffcfc3f03f00", 16) + _, weights, chosen = analyze_puncture(roots, code, puncture) + cheap = [reader for reader in chosen if weights[reader] <= 7] + cheap.append(next(reader for reader in code[1:] + if weights[reader] == 7 and reader not in cheap)) + require(len(set(cheap)) == 9 and sum(weights[r] for r in cheap) == 61, + "cost-61 control setup") + try: + price_basis(cheap, weights) + except ValueError as error: + require("does not span nine" in str(error), "wrong cheap-basis rejection") + else: + raise ValueError("accepted cost-61 nondecoder") + controls.append("distinct-cost-61-nonspanning-readers") + # Rank must be rational: in characteristic two these doubled roots can vanish. + require(rational_rank([(2, 0), (0, 2)]) == 2 and + len(binary_basis([0, 0])) == 0, "wrong-characteristic control") + controls.append("wrong-characteristic") + return controls + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--check", type=Path, default=HERE / "CERTIFICATE.json") + parser.add_argument("--write", type=Path, help="write a fresh receipt instead of comparing one") + args = parser.parse_args() + result = census() + result["predecessor_sources"] = check_sources() + result["negative_controls"] = negative_controls() + if args.write is not None: + args.write.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + require(json.loads(args.check.read_text()) == result, "certificate mismatch") + print("PASS_E8_RANK5_BOUNDARY: 28616 rank-five pairs; 2 representatives; " + "7560 conjugate punctures; cost 62; 72 restorations; 5 negative controls; no new kappa") + + +if __name__ == "__main__": + main()