diff --git a/research/a8-p112-decoder-screen/CERTIFICATE.json b/research/a8-p112-decoder-screen/CERTIFICATE.json new file mode 100644 index 0000000000..2e668cca66 --- /dev/null +++ b/research/a8-p112-decoder-screen/CERTIFICATE.json @@ -0,0 +1,1968 @@ +{ + "active_witness_costs": [ + 1, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "all_pairs_checked_per_witness": 12544, + "anchors": [ + { + "anchor": 0, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 19822 + }, + { + "anchor": 1, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 19822 + }, + { + "anchor": 2, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 19697 + }, + { + "anchor": 3, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 19697 + }, + { + "anchor": 4, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 18790 + }, + { + "anchor": 5, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 18790 + }, + { + "anchor": 6, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 16155 + }, + { + "anchor": 7, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 16155 + }, + { + "anchor": 8, + "compatible_leaves": 39485, + "configurations": 2251, + "maximum_histogram": { + "9": 2251 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "planes": 4365 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 11552 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13356 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 8792 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 3710 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 1176 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 392 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 56 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 36 + } + ], + "planes": 43435, + "rejected_branches": 13907 + } + ], + "column_label_ranks": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "coordinate_permutation_punctures": 945, + "deficiency_upper_bound": 10, + "dropped_witness_costs": [ + 0, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "frame_indices": [ + 0, + 15, + 26, + 33, + 42, + 89, + 112, + 119 + ], + "frame_labels": [ + 508, + 499, + 463, + 319, + 259, + 268, + 304, + 448 + ], + "kind": "scoped proof with exhaustive finite lemmas", + "live_root_rank": 8, + "live_roots": 112, + "model": "fixed A8 simplex; one P112 frame puncture; all-pairs; separate term costs", + "schema_version": 1, + "semantic_controls": [ + "coefficient_perturbation", + "active_term_deleted", + "label_pairing_corrupted", + "nonorthogonal_puncture", + "unpunctured_dimension_lemma", + "omitted_mutual_compatibility_changes_bound", + "false_cost_seventy", + "nonreal_kernel_shift_positive" + ], + "sharp_copy_cost": 71, + "total_compatible_leaves": 462141, + "total_configurations": 19299, + "total_planes": 390915 +} diff --git a/research/a8-p112-decoder-screen/PROOF.md b/research/a8-p112-decoder-screen/PROOF.md new file mode 100644 index 0000000000..4f18ea6417 --- /dev/null +++ b/research/a8-p112-decoder-screen/PROOF.md @@ -0,0 +1,185 @@ +# Sharp copy cost 71 for the A8 simplex on a matching-frame P112 puncture + +This is a scoped mathematical proof whose finite lemmas are exhaustively +recomputed by two implementations. It is not a formal multiplication theorem. +The deficiency-space method is due to the P120 predecessor, mightyOil's +[PR1248](https://github.com/CrocSwap/integer-mult-bounds/pull/1248). The one-sided +overcomplete representation comes from joaqcoo's +[PR1224](https://github.com/CrocSwap/integer-mult-bounds/pull/1224). Here the +puncture changes the finite lemmas, and every lemma needed below is recomputed. + +## 1. Fixed family and puncture + +Work in the sum-zero subspace V of Q^9. Use the 120 oriented E8 root lines + +- e_a-e_b for 0 <= a < b <= 8, in lexicographic order (36 lines); +- 1_S-(1/3)1 for three-element subsets S of {0,...,8}, in lexicographic order + (84 lines). + +Puncture the orthogonal frame + + F = { e_(2j)-e_(2j+1), + e_(2j)+e_(2j+1)+e_8-(1/3)1 : j=0,1,2,3 }. + +Its zero-based indices are [0,15,26,33,42,89,112,119]. It is the first +orthogonal eight-frame in the declared root order; the verifier checks this +by complete lexicographic backtracking until the first solution. Let P be +the 112 live lines. They span V (rank eight, checked over Q). + +Fix the nine simplex normals b_k=e_k-(1/9)1, and T_ik=r_ik for live roots r_i. +The variable factor D has 112 rows and nine columns. Require + + D T^t = 2G, G_ij = r_i dot r_j, + +on **all** live pairs, with ordinary transpose. Coefficients can be arbitrary +complex numbers. Terms are charged separately by the F2 rank of the pairing +matrix (G_ij+1) mod 2 restricted to their nonzero row and column supports. +Zero terms are allowed, but the sharp witness below has all nine terms active. + +Since the live roots span V, the identity is equivalent to + + D_ik = 2r_ik + t_i, t_i arbitrary in C. + +Indeed D_i-2r_i is orthogonal to V and hence is a multiple of the all-ones +vector. This argument is valid over C with the bilinear ordinary transpose; +no positivity or conjugation is invoked. + +## 2. Exact reduction to binary deficiency spaces + +Use labels in F2^9: + + u_ab = 1+e_a+e_b, u_S = 1_S. + +For every pair of the 120 roots, u_i dot u_j=(G_ij+1) mod 2. This is checked +on all 14,400 entries. For each k, the live labels on the column support +{i:r_ik != 0} span all of F2^9. Thus the pairing rank of term k equals the +dimension of the label span on its row support {i:D_ik != 0}. + +Define + + K_k = {w : w dot u_i=0 whenever D_ik != 0}, delta_k=dim K_k. + +The total copy cost is exactly 81-sum_k delta_k. It is enough to prove that +the sum of the nine deficiencies is at most ten. + +If w in K_j and z in K_k both evaluate to one on u_i, then D_ij=D_ik=0. +Consequently r_ij=r_ik. Call this necessary relation compatibility of the two +functionals at columns j,k. It uses only zero patterns, so it applies to all +complex shifts, including generic shifts that create no zero entries. + +## 3. Finite covering of every possible deficiency tuple + +If every delta_k <= 1, the sum is at most nine already. Otherwise choose an +anchor j with delta_j >= 2 and a binary plane U contained in K_j. We check +every anchor and every plane; no symmetry assumption enters the primary check. + +Each binary plane has a unique representation by 0 64/112`, the family cannot improve the standard P112 copied-information +bill, even before extra physical costs. This is a copy-cost rejection of one +route, not a completed recurrence calculation or a bound for arbitrary decoders. + +## Exact scope and evidence + +The roots are `e_a-e_b` and `1_S-(1/3)1` in the sum-zero subspace of Q^9. The +fixed column normals are `b_k=e_k-(1/9)1`. On live roots, `T_ik=r_ik` and every +exact decoder is `D_ik=2r_ik+t_i`, with arbitrary `t_i` in C and ordinary +transpose. The puncture is + +```text +F = {e_(2j)-e_(2j+1), e_(2j)+e_(2j+1)+e_8-(1/3)1 : j=0,1,2,3} +``` + +It has indices `[0,15,26,33,42,89,112,119]` in the pair-then-triple lexicographic +root order. Terms are billed separately by binary pairing rank. Masked +identities and shared-copy pricing are excluded. + +All nine column-label spans still have rank nine, so the copy cost is +`81 - sum(delta_k)`. However, puncturing creates two-dimensional partner +deficiency spaces: the P120 dimension-one lemma is false here. Enumerating all +subspaces of these enlarged spaces and imposing their mutual compatibility +proves `sum(delta_k) <= 10`. + +- Primary replay: all nine anchors, 390,915 binary planes, 19,299 distinct + ordered partner-space tuples, and 462,141 compatible subspace choices. +- Separate replay: labels reconstructed from the Gram pairing matrix, + annihilator row reduction, direct Cartesian-product enumeration, and a + checked stabilizer transporting two anchor representatives to all nine. +- Both check all 12,544 entries of the active witness. The primary also checks + the zero-term witness; the separate checker prices actual pairing submatrices. +- Eight semantic controls include a coefficient error, a deleted term, corrupt + labels, a nonorthogonal puncture, the false inherited dimension-one lemma, + missing mutual compatibility, a false cost of 70, and a valid non-real shift. +- Six package tests exercise optimized relocated/read-only replay, the separate + checker without the primary file, and changed, incomplete, missing or + malformed receipts. + +The argument covering every complex shift is in [PROOF.md](PROOF.md). The +deterministic finite evidence is [CERTIFICATE.json](CERTIFICATE.json). The +second implementation is by the same AI assistant, not independent human review. + +## Reproduce + +From the repository root, Python 3.12 and the standard library: + +```sh +python3 -I -B research/a8-p112-decoder-screen/verify.py +python3 -I -B research/a8-p112-decoder-screen/independent.py +python3 scripts/research_package.py --package research/a8-p112-decoder-screen --check-only +python3 scripts/research_package.py --package research/a8-p112-decoder-screen +``` + +The last command runs both checkers and the six package tests. Expected markers: + +```text +PASS_A8_P112_DECODER_FLOOR planes=390915 configurations=19299 compatible_leaves=462141 cost=71 controls=8 +PASS_A8_P112_INDEPENDENT anchors=2 transported=9 planes=86870 compatible_leaves=92317 cost=71 +PASS_REGISTERED_RESEARCH_PACKAGE research/a8-p112-decoder-screen outcome=negative-result +``` + +`verify.py --write` explicitly regenerates the certificate. Normal replay is +read-only. Source pins and exact predecessor heads are in [SOURCES.json](SOURCES.json); +the pending predecessors are attribution/context, not imported code or assumed +finite lemmas. [TASK.json](TASK.json) records the chooser, scope and next questions. +See [VALIDATION.md](VALIDATION.md) for measured checks and limits. + +No supplier word, delivery/frame/restoration/hosting invoice, new moment, +selected cold replay, Lean proof, or complete multiplication theorem is supplied. +The selected frontier and all inherited all-size/compiler, common-label and +mutable-source, hosting, precision/tape, recovery, analytic-transfer and bit +H1-H5 obligations remain unchanged. Hosted CI and human review are unclaimed. + +## Coordination + +Base `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`; chooser nonce +`a57142e8e77d6c0af036ca35809daf69`, track `complex-mechanisms`, revision 2, +card `complex-masked-decoder`, scope key `2a6f2c726b78f9ae7d26`. This refines +the card's overcomplete-family branch to PR1248's explicit puncture question. + +Nearest predecessors are PR1248 (P120 optimum) and PR1224 (normal form and +bounded searches). PR1212/1213 and discussion #1275 concern eight-term masked +rigidity; PR1236 and discussion #1267 concern masked root-star/co-star supports. +These are distinct hypotheses. Two parallel sessions from the same account +study bit-side zero-frame feedback (discussion #1290) and selected bit hosting +(discussion #1289); this package does neither. The original claim is in +[discussion #1241](https://github.com/CrocSwap/integer-mult-bounds/discussions/1241#discussioncomment-18909913). +The final overlap check used a shared snapshot of 788 open PRs and 40 +discussion records with complete pagination, fetched at 21:54:03 and 21:54:12 +UTC on 2026-10-13. It may miss later changes. + +## Open next questions + +- **Other frame punctures relative to the fixed simplex.** Do they also have + minimum cost at least 64? Enumerate orthogonal frames and their S9 orbits, + then recompute column ranks and partner dimensions for a representative + outside the matching-frame orbit. This tests whether the remaining P112 + part of PR1248's question can improve copy cost. The present enumerator + deliberately rejects partner dimensions above two and may need extension. +- **Another specified nine-normal frame.** Can the A7+A1 or A2+E6 family in + PR1224 admit copy cost below 64 on a named P112 puncture? First establish its + exact ratio classes, column spans and a favorable complete cost budget. + The simplex's common kernel vector and compatibility census do not transfer + automatically; physical realization would remain an additional obligation. + +## Credit and disclosure + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Credit Philipp / **mightyOil**, PR1248, for the deficiency-space method, P120 +floor and explicit P112 follow-up; **joaqcoo**, PR1224, for the nine-term normal +form, A8 frame and ratio-class viewpoint; **DreamingOfClouds**, PR717/595/446, +for the decoder and pairing-rank cost model; **themilkman216**, PR968, and +**woklerx**, PR1077/1180, for surrounding floor results; and the classical +E8/A8 geometry. The selected supplier lineage retains its existing credit. +No predecessor file is changed. New work is Apache-2.0, the repository license. diff --git a/research/a8-p112-decoder-screen/SOURCES.json b/research/a8-p112-decoder-screen/SOURCES.json new file mode 100644 index 0000000000..5de83e4d2c --- /dev/null +++ b/research/a8-p112-decoder-screen/SOURCES.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/complex-decoder-field-extension-seed44/README.md", + "usage": "input", + "git_blob": "a6e6d2e04249191c1bce5c6e2977c11f9969b7a3", + "sha256": "788a99eef3f187c2cbff6d490933fcc8f8e7fd15d1b685c188023605916887d4" + }, + { + "path": "research/complex-frame-pair-decoders/README.md", + "usage": "input", + "git_blob": "be5bbbee8e30a4ee39fa513896e8fc7e0bb3721e", + "sha256": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e" + } + ], + "predecessor_references": [ + { + "pr": 1248, + "head": "f226f4329a996b0a1bea8794179a91b5d0ed80bf", + "author": "Philipp / mightyOil", + "role": "Method and question attribution; no imported code or unverified finite-lemma dependency. Not required for runtime replay.", + "files": [ + { + "path": "research/a8-simplex-decoder-floor/README.md", + "git_blob": "cc814ae890f18da884b70ae6e471f31a75bade5f", + "sha256": "4f279ea113cea46593609cdcd580099c24ec8aa02428aae0c5bae54baa0e4557" + }, + { + "path": "research/a8-simplex-decoder-floor/PROOF.md", + "git_blob": "4d1d3bcd8799c833dfbb63ed5319af5fe863fa1a", + "sha256": "7e3a5407fc535fd9cc7f25f06aab787b0216f09121e571938cccedb383aab3c4" + } + ] + }, + { + "pr": 1224, + "head": "00e6ed0810b8ebc7f6133e2c036d0f1c9a3a4162", + "author": "joaqcoo", + "role": "Method and question attribution; no imported code or unverified finite-lemma dependency. Not required for runtime replay.", + "files": [ + { + "path": "research/nine-term-decoder-normal-form-seed42/README.md", + "git_blob": "9cf8ecd3eda302b57ab14302c429b00c255f2dba", + "sha256": "d272081da47d6ea6a2404fddff211418dd6e7c236babf7eb4560737e818c1677" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/PROOF.md", + "git_blob": "e510fd180a286445fd6fc484057001bfc60f8c9c", + "sha256": "0503e07f1764708e9e72c01be88d3dad1b213e73eb3c23397a603032791fd23a" + } + ] + } + ] +} diff --git a/research/a8-p112-decoder-screen/TASK.json b/research/a8-p112-decoder-screen/TASK.json new file mode 100644 index 0000000000..46e568faa0 --- /dev/null +++ b/research/a8-p112-decoder-screen/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "refined", + "actual_scope": "Sharp separate-term copy-cost floor for the fixed A8 simplex nine-term all-pairs decoder on the matching-frame P112 puncture and its 945 coordinate-permutation images, over arbitrary complex row shifts.", + "scope_change_reason": "Take the card's overcomplete-family branch and PR1248's explicit P112 follow-up. Change the puncture from P120, recompute every finite lemma, and use only proved coordinate symmetry for the corollary.", + "bottleneck_link": "The complex supplier binds. A copy cost at most 63 would be a necessary first saving against standard P112 cost 64 under this billing model. The sharp floor 71 rejects this family before physical synthesis; no complete moment or supplier claim follows.", + "budget_minutes": 60, + "stop_rule": "Stop construction if an exact floor excludes cost at most 63; otherwise certify a candidate before any physical budget claim. About 60 minutes total, with final quarter for verification and handoff. No expanded optimizer search.", + "outcome": "negative-result", + "evidence": "PROOF.md and CERTIFICATE.json: all 390915 planes across nine anchors; 19299 partner-space tuples; 462141 compatible subspace choices; sum deficiency at most 10; sharp all-nine-active witness cost 71. Separate Gram-derived implementation and eight semantic controls; six package tests.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in research, both implementations, proof, testing and writing. Same-assistant separate implementation is not independent human review.", + "open_questions": [ + { + "question": "What is the fixed-simplex optimum for a P112 frame puncture outside the 945 matching-frame orbit?", + "why_it_matters": "The remaining frame orientations could have different copy costs and are not bounded here.", + "first_step": "Enumerate E8 orthogonal frames modulo explicit S9 coordinate permutations; recompute column ranks and partner dimensions for one unrepresented orbit.", + "blocked_by": "This proof covers one orbit only; larger partner spaces require a complete subspace enumerator beyond dimensions zero through two." + }, + { + "question": "Can another specified nine-normal family from PR1224 beat copy cost 64 on a named P112 puncture?", + "why_it_matters": "A different normal frame changes the zero-pattern constraints and may evade this scoped obstruction.", + "first_step": "Choose A7+A1 or A2+E6, derive its kernel and ratio classes, and screen exact label ranks plus a favorable complete cost budget.", + "blocked_by": "The common all-ones kernel and this compatibility census are specific to the A8 simplex; physical costs would remain additional obligations." + } + ], + "chooser": { + "nonce": "a57142e8e77d6c0af036ca35809daf69", + "track": "complex-mechanisms", + "scope_key": "2a6f2c726b78f9ae7d26", + "priority_revision": 2 + }, + "coordination": "Claim posted in discussion #1241 (comment 18909913) by the submitting account; the agent session itself made no GitHub writes." +} diff --git a/research/a8-p112-decoder-screen/VALIDATION.md b/research/a8-p112-decoder-screen/VALIDATION.md new file mode 100644 index 0000000000..28e50b51f0 --- /dev/null +++ b/research/a8-p112-decoder-screen/VALIDATION.md @@ -0,0 +1,70 @@ +# Local validation + +Executed on 2026-10-13 with CPython 3.12.3, Linux x86_64, standard library only. +The package uses one busy process at a time and no GPU. No packages were +installed. All source and evidence generation ran in one donated agent session. + +## Completed checks + +```sh +python3 -B research/complex-decoder-field-extension-seed44/verify.py +python3 -B scripts/research_baseline.py +python3 -I -B research/a8-p112-decoder-screen/verify.py --write +python3 -I -B research/a8-p112-decoder-screen/independent.py +python3 -I -B research/a8-p112-decoder-screen/test_package.py -k missing_receipt +python3 -B scripts/research_package.py --package research/a8-p112-decoder-screen --check-only +python3 -B scripts/research_package.py --package research/a8-p112-decoder-screen +python3 -B -m unittest discover -s tests -p 'test_research_*.py' +python3 -B scripts/verify_selected_result.py +``` + +Every command passed. The registered replay reran the primary checker, separate +checker and full six-test package file in **58.024 seconds**; its six tests took +39.221 seconds. The 20 repository research-workflow tests passed with no skips +(0.386 seconds reported by unittest). These are host-specific verifier timings, +not multiplication-runtime measurements. No broad historical replay was run. + +The primary check covers 390,915 planes across all nine anchors, 19,299 partner +space tuples and 462,141 compatible subspace choices. It re-derives the sharp +cost 71, both witnesses, the 945-frame orbit, and eight semantic controls. The +separate checker uses different label coordinates, annihilator algebra and +Cartesian products, checks 86,870 planes for two symmetry representatives, +and proves its transport to all nine anchors using explicit permutations. + +The eight semantic controls comprise six deliberate rejection cases, a check +that dropping mutual compatibility admits the false deficiency allowance 11, +and a positive non-real kernel-shift fixture. The six package tests check: + +- isolated optimized replay in a relocated read-only directory with unchanged + file hashes; +- the separate checker with the primary checker file absent; +- rejection of an altered cost claim, a missing anchor, a missing receipt, and + malformed JSON. + +The initial predecessor command is a source-bound positive control, not the +selected supplier's cold replay. The baseline and selected-record integrity +checks confirmed the recorded selected kappa and pins; no selected file was +edited. The new scripts use explicit exceptions, so their checks remain active +under `python -O`. + +## What was not checked + +No other P112 frame orbit, arbitrary nine-normal family, masked identity, +shared-copy implementation or physical supplier is certified. No delivery, +restoration, frame, hosting, precision/tape or complete moment invoice was +constructed. `make frontier1094-verify`, native/Lean builds, hosted CI, an +all-size compiler and the complete multiplication theorem were not run or +proved. The written covering argument has no independent human review. + +PR1248 and PR1224 were fetched anonymously and read at the exact heads in +SOURCES.json. Their code and certificates are not runtime dependencies; the +new package recomputes its own needed finite facts. The predecessor head/hash +references are attribution evidence and are not checked by the generic runner, +which checks the main-tree source inventory in `SOURCES.json.files`. + +The final overlap query used a shared offline snapshot: 788 open PRs +fetched 2026-10-13T21:54:03.402700+00:00 and 40 discussion records fetched +2026-10-13T21:54:12.002645+00:00, both marked complete pagination. It does not +cover later updates or every diff. The claim is in discussion #1241. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. diff --git a/research/a8-p112-decoder-screen/VERIFY.json b/research/a8-p112-decoder-screen/VERIFY.json new file mode 100644 index 0000000000..808084f7f4 --- /dev/null +++ b/research/a8-p112-decoder-screen/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All nine anchors, exhaustive deficiency bound, 945-frame symmetry orbit, both witnesses and eight semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate Gram-derived labels, annihilator algebra, Cartesian products, checked anchor stabilizer and direct pairing-rank witness." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 180, + "checks": "Six optimized relocation, read-only, separate-code and receipt-corruption package controls." + } + ] +} diff --git a/research/a8-p112-decoder-screen/independent.py b/research/a8-p112-decoder-screen/independent.py new file mode 100644 index 0000000000..02035af27f --- /dev/null +++ b/research/a8-p112-decoder-screen/independent.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Separate check: Gram-derived labels, annihilator algebra, Cartesian products. + +No primary or predecessor imports. The primary checks nine anchors; here an +explicit frame stabilizer reduces the coverage to two orbits, {0,...,7}, {8}. +Separate implementation by the same AI assistant is not independent peer review. +""" + +from collections import Counter +from fractions import Fraction +from functools import lru_cache +from itertools import combinations, product +import json +from pathlib import Path + + +def check(value, message): + if not value: + raise RuntimeError(message) + + +def rref(vectors, width=9): + rows = sorted(set(vectors) - {0}) + n = 0 + for column in range(width): + pivot = next((i for i in range(n, len(rows)) if (rows[i] >> column) & 1), None) + if pivot is None: + continue + rows[n], rows[pivot] = rows[pivot], rows[n] + for i in range(len(rows)): + if i != n and ((rows[i] >> column) & 1): + rows[i] ^= rows[n] + n += 1 + return tuple(rows[:n]) + + +@lru_cache(maxsize=100000) +def combine(a, b): + return rref(a + b) + + +@lru_cache(maxsize=100000) +def annihilator(equations): + pivots = [(x & -x).bit_length() - 1 for x in equations] + answer = [] + for f in range(9): + if f not in pivots: + answer.append((1 << f) | sum(((x >> f) & 1) << p + for x, p in zip(equations, pivots))) + check(all((v & e).bit_count() % 2 == 0 for v in answer for e in equations), + 'annihilator equations') + return tuple(answer) + + +def nonzero_span(basis): + space = {0} + for vector in basis: + space |= {x ^ vector for x in tuple(space)} + return tuple(sorted(space - {0})) + + +def geometry(): + roots = [] + for a in range(9): + for b in range(a + 1, 9): + row = [Fraction(0)] * 9 + row[a], row[b] = Fraction(1), Fraction(-1) + roots.append(tuple(row)) + for subset in combinations(range(9), 3): + roots.append(tuple(Fraction(int(k in subset)) - Fraction(1, 3) for k in range(9))) + gram = [[sum(x * y for x, y in zip(a, b)) for b in roots] for a in roots] + check(all(x.denominator == 1 for row in gram for x in row), 'integral Gram') + pairing = [[(int(x) + 1) % 2 for x in row] for row in gram] + columns, selected = [], [] + for j in range(120): + column = sum(pairing[i][j] << i for i in range(120)) + if len(rref(columns + [column], 120)) > len(columns): + columns.append(column) + selected.append(j) + check(len(columns) == 9, 'full pairing rank nine') + labels = [sum(pairing[i][j] << p for p, j in enumerate(selected)) for i in range(120)] + frame = (0, 15, 26, 33, 42, 89, 112, 119) + check(all(gram[i][j] == 0 for i, j in combinations(frame, 2)), 'frame orthogonality') + # Explicit generators preserve the puncture and are transitive on 0..7. + swaps = [[(0, 1)], [(0, 2), (1, 3)], [(0, 4), (1, 5)], [(0, 6), (1, 7)]] + lookup = {r: i for i, r in enumerate(roots)} + permutations = [] + for exchanges in swaps: + permutation = list(range(9)) + for a, b in exchanges: + permutation[a], permutation[b] = permutation[b], permutation[a] + images = [] + for root in roots: + image = tuple(root[permutation[k]] for k in range(9)) + if image not in lookup: + image = tuple(-x for x in image) + check(image in lookup, 'root-line permutation') + images.append(lookup[image]) + check({images[i] for i in frame} == set(frame), 'puncture stabilizer') + permutations.append(permutation) + orbit = {0} + while True: + new = orbit | {p[i] for p in permutations for i in orbit} + if new == orbit: + break + orbit = new + check(orbit == set(range(8)) and all(p[8] == 8 for p in permutations), 'anchor orbits') + indices = [i for i in range(120) if i not in frame] + live_roots = [roots[i] for i in indices] + live_labels = [labels[i] for i in indices] + for k in range(9): + check(len(rref(u for u, r in zip(live_labels, live_roots) if r[k])) == 9, + 'column rank in Gram-derived label coordinates') + # Direct ranks of the actual pairing submatrices, not the label shortcut. + d = [[2 * (x - r[2 if i == 0 else 0]) for x in r] for i, r in enumerate(live_roots)] + for i, row in enumerate(d): + for j, root in enumerate(live_roots): + check(sum(x * y for x, y in zip(row, root)) == 2 * gram[indices[i]][indices[j]], + 'rational all-pairs identity') + costs = [] + for k in range(9): + ys = [indices[j] for j, r in enumerate(live_roots) if r[k]] + matrix = [sum(pairing[indices[i]][j] << p for p, j in enumerate(ys)) + for i, row in enumerate(d) if row[k]] + costs.append(len(rref(matrix, len(ys)))) + check(costs == [1, 8, 8, 9, 9, 9, 9, 9, 9], 'direct pairing-rank witness price') + return live_roots, live_labels, selected, permutations + + +def audit_anchor(roots, labels, anchor): + others = [k for k in range(9) if k != anchor] + equations = {} + for k in others: + relevant = [(u, r) for u, r in zip(labels, roots) if r[k] != r[anchor]] + equations[k] = [rref(u for u, _ in relevant if (u & w).bit_count() % 2) + for w in range(512)] + configs = {} + dimension_hist = Counter() + # Enumerate planes using RREF bases, not the primary's sorted nonzero pairs. + plane_bases = set() + for a in range(1, 512): + for b in range(a + 1, 512): + plane_bases.add(rref((a, b))) + check(len(plane_bases) == 43435, 'all planes by canonical RREF') + for a, b in sorted(plane_bases): + spaces = tuple(nonzero_span(annihilator(combine(equations[k][a], equations[k][b]))) + for k in others) + dims = tuple(sorted((len(h) + 1).bit_length() - 1 for h in spaces)) + check(max(dims) <= 2, 'partner space dimensions') + dimension_hist[dims] += 1 + configs[spaces] = configs.get(spaces, 0) + 1 + options_cache = {} + for spaces in configs: + for k, h in zip(others, spaces): + key = (k, h) + if key in options_cache: + continue + subspaces = [()] + [(z,) for z in h] + if len(h) == 3: + subspaces.append(rref(h)) + result = [] + for basis in subspaces: + constraints = rref(x for z in basis for x in equations[k][z]) + zero_rows = frozenset(i for i, u in enumerate(labels) + if any((u & z).bit_count() % 2 for z in basis)) + result.append((len(basis), constraints, zero_rows)) + options_cache[key] = result + compatible_count = raw_count = 0 + maximum_hist = Counter() + for spaces in configs: + maximum = 0 + for choices in product(*(options_cache[k, h] for k, h in zip(others, spaces))): + raw_count += 1 + # Test rowwise consistency directly: all forced-zero coordinates at + # a row must have the same coefficient. No bitset compatibility table. + consistent = True + forced_value = {} + for k, (_, _, zero_rows) in zip(others, choices): + for row in zero_rows: + value = roots[row][k] + if row in forced_value and forced_value[row] != value: + consistent = False + break + forced_value[row] = value + if not consistent: + break + if not consistent: + continue + compatible_count += 1 + constraints = rref(x for _, equations_, _ in choices for x in equations_) + score = 9 - len(constraints) + sum(dim for dim, _, _ in choices) + check(score <= 10, 'deficiency upper bound') + maximum = max(maximum, score) + maximum_hist[maximum] += 1 + return {'anchor': anchor, 'planes': len(plane_bases), 'configurations': len(configs), + 'compatible_leaves': compatible_count, 'raw_products': raw_count, + 'maximum_histogram': {str(k): v for k, v in sorted(maximum_hist.items())}, + 'partner_dimension_histogram': [{'dimensions': list(k), 'planes': v} + for k, v in sorted(dimension_hist.items())]} + + +def main(): + roots, labels, selected, permutations = geometry() + receipt = json.loads((Path(__file__).resolve().parent / 'CERTIFICATE.json').read_text()) + results = [audit_anchor(roots, labels, a) for a in (0, 8)] + for result in results: + anchors = range(8) if result['anchor'] == 0 else (8,) + for a in anchors: + for key in ('planes', 'configurations', 'compatible_leaves', 'maximum_histogram', + 'partner_dimension_histogram'): + check(result[key] == receipt['anchors'][a][key], 'primary receipt mismatch: ' + key) + check(receipt['sharp_copy_cost'] == 71 and receipt['active_witness_costs'] == + [1, 8, 8, 9, 9, 9, 9, 9, 9], 'price receipt') + print('PASS_A8_P112_INDEPENDENT anchors=2 transported=9 planes=86870 ' + 'compatible_leaves=92317 cost=71') + + +if __name__ == '__main__': + main() diff --git a/research/a8-p112-decoder-screen/test_package.py b/research/a8-p112-decoder-screen/test_package.py new file mode 100644 index 0000000000..aef2d0d550 --- /dev/null +++ b/research/a8-p112-decoder-screen/test_package.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Relocation, optimized execution, and receipt rejection controls.""" + +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + + +class PackageControls(unittest.TestCase): + def setUp(self): + self.temporary = tempfile.TemporaryDirectory(prefix='a8-p112-') + self.root = Path(self.temporary.name) + self.package = self.root / 'package' + self.package.mkdir() + for name in ('verify.py', 'independent.py', 'CERTIFICATE.json'): + shutil.copyfile(HERE / name, self.package / name) + + def tearDown(self): + self.temporary.cleanup() + + def run_script(self, script='verify.py'): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(self.package / script)], + cwd=self.root, capture_output=True, text=True, timeout=120) + + def change_receipt(self, change): + path = self.package / 'CERTIFICATE.json' + value = json.loads(path.read_text()) + change(value) + path.write_text(json.dumps(value) + '\n') + + def test_primary_optimized_relocated_read_only(self): + paths = list(self.package.iterdir()) + before = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in paths} + for path in paths: + path.chmod(0o444) + self.package.chmod(0o555) + try: + result = self.run_script() + finally: + self.package.chmod(0o755) + for path in paths: + path.chmod(0o644) + self.assertEqual(result.returncode, 0, result.stderr[-1000:]) + self.assertIn('PASS_A8_P112_DECODER_FLOOR', result.stdout) + self.assertEqual(before, {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.package.iterdir()}) + + def test_separate_checker_without_primary(self): + (self.package / 'verify.py').unlink() + result = self.run_script('independent.py') + self.assertEqual(result.returncode, 0, result.stderr[-1000:]) + self.assertIn('PASS_A8_P112_INDEPENDENT', result.stdout) + + def test_changed_claim_rejected(self): + self.change_receipt(lambda value: value.update(sharp_copy_cost=70)) + result = self.run_script() + self.assertNotEqual(result.returncode, 0) + self.assertIn('certificate differs from exact replay', result.stderr) + + def test_missing_anchor_rejected(self): + self.change_receipt(lambda value: value['anchors'].pop(4)) + result = self.run_script() + self.assertNotEqual(result.returncode, 0) + self.assertIn('certificate differs from exact replay', result.stderr) + + def test_missing_receipt_rejected(self): + (self.package / 'CERTIFICATE.json').unlink() + result = self.run_script() + self.assertNotEqual(result.returncode, 0) + self.assertIn('FileNotFoundError', result.stderr) + + def test_truncated_receipt_rejected(self): + (self.package / 'CERTIFICATE.json').write_text('{"anchors": [') + result = self.run_script() + self.assertNotEqual(result.returncode, 0) + self.assertIn('JSONDecodeError', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/a8-p112-decoder-screen/verify.py b/research/a8-p112-decoder-screen/verify.py new file mode 100644 index 0000000000..188d3a8fda --- /dev/null +++ b/research/a8-p112-decoder-screen/verify.py @@ -0,0 +1,364 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact finite lemmas for one A8 simplex P112 decoder floor. + +The deficiency method follows mightyOil's PR1248. This implementation extends +it to the declared puncture, enumerating every subspace of every partner space. +No predecessor code, numerical solver, or unproved symmetry reduction is used. +""" + +import argparse +from collections import Counter +from fractions import Fraction +from itertools import combinations +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +FRAME = (0, 15, 26, 33, 42, 89, 112, 119) +FULL = (1 << 9) - 1 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def binary_basis(vectors): + pivots = {} + for value in vectors: + while value: + p = value.bit_length() - 1 + if p in pivots: + value ^= pivots[p] + else: + pivots[p] = value + break + return tuple(pivots[p] for p in sorted(pivots, reverse=True)) + + +def rank(vectors): + return len(binary_basis(vectors)) + + +def rational_rank(rows): + pivots = {} + for row in rows: + v = list(map(Fraction, row)) + for p in range(len(v)): + if not v[p]: + continue + if p in pivots: + multiple = v[p] + v = [x - multiple * y for x, y in zip(v, pivots[p])] + else: + multiple = v[p] + pivots[p] = [x / multiple for x in v] + break + return len(pivots) + + +def members(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def model(): + """Rows are (binary label, v=3r), in the declared canonical order.""" + rows = [] + for a, b in combinations(range(9), 2): + rows.append((FULL ^ (1 << a) ^ (1 << b), + tuple(3 * (int(k == a) - int(k == b)) for k in range(9)))) + for triple in combinations(range(9), 3): + label = sum(1 << k for k in triple) + rows.append((label, tuple(2 if k in triple else -1 for k in range(9)))) + return rows + + +def first_frame(rows): + adjacency = [{j for j in range(i + 1, len(rows)) + if dot(rows[i][1], rows[j][1]) == 0} for i in range(len(rows))] + + def visit(prefix, candidates): + if len(prefix) == 8: + return prefix + for i in sorted(candidates): + rest = candidates & adjacency[i] + if len(prefix) + 1 + len(rest) >= 8: + found = visit(prefix + (i,), rest) + if found is not None: + return found + return None + + return visit((), set(range(len(rows)))) + + +def matching_frame_orbit(rows): + """Coordinate-permutation images: choose one singleton and four pairs.""" + lookup = {v: i for i, (_, v) in enumerate(rows)} + + def matchings(items): + if not items: + yield () + return + a = items[0] + for b in items[1:]: + for rest in matchings(tuple(x for x in items[1:] if x != b)): + yield ((a, b),) + rest + + frames = set() + for singleton in range(9): + for pairs in matchings(tuple(k for k in range(9) if k != singleton)): + indices = [] + for a, b in pairs: + pair = tuple(3 * (int(k == a) - int(k == b)) for k in range(9)) + triple = tuple(2 if k in (a, b, singleton) else -1 for k in range(9)) + indices.extend((lookup[pair], lookup[triple])) + frame = tuple(sorted(indices)) + require(all(dot(rows[i][1], rows[j][1]) == 0 for i, j in combinations(frame, 2)), + 'matching-frame orbit orthogonality') + frames.add(frame) + require(len(frames) == 945 and FRAME in frames, 'matching-frame orbit count') + return len(frames) + + +def check_model(rows, frame=FRAME): + require(len(rows) == 120 and len({u for u, _ in rows}) == 120, + '120 distinct root labels required') + require(len(frame) == 8 and len(set(frame)) == 8 and + all(type(i) is int and 0 <= i < 120 for i in frame), 'frame shape') + for i, j in combinations(frame, 2): + require(dot(rows[i][1], rows[j][1]) == 0, 'puncture must be an orthogonal frame') + for u, v in rows: + require(sum(v) == 0 and dot(v, v) == 18, 'sum-zero norm-two root') + for w, z in rows: + gram, remainder = divmod(dot(v, z), 9) + require(remainder == 0, 'integral Gram entries') + require((u & w).bit_count() % 2 == (gram + 1) % 2, + 'binary label/Gram pairing') + live = [row for i, row in enumerate(rows) if i not in frame] + require(len(live) == 112 and rational_rank(v for _, v in live) == 8, + 'live roots span the eight-dimensional sum-zero space') + require(rank(u for u, _ in live) == 9, 'live labels span F2^9') + for k in range(9): + require(rank(u for u, v in live if v[k]) == 9, 'column support label rank nine') + return live + + +def tables(live): + words = [sum(((u & w).bit_count() % 2) << i + for i, (u, _) in enumerate(live)) for w in range(512)] + unequal = {(j, k): sum((v[j] != v[k]) << i for i, (_, v) in enumerate(live)) + for j, k in combinations(range(9), 2)} + return words, unequal + + +def compatibility_spaces(live, words, unequal, anchor): + others = [k for k in range(9) if k != anchor] + allowed, forced = {}, {} + for k in others: + different = unequal[min(k, anchor), max(k, anchor)] + allowed[k] = [sum(1 << z for z in range(1, 512) + if not (words[w] & words[z] & different)) + for w in range(512)] + for z in range(1, 512): + support = words[z] & different + forced[k, z] = binary_basis(u for i, (u, _) in enumerate(live) + if support >> i & 1) + return others, allowed, forced + + +def plane_configurations(others, allowed): + """Every plane has exactly one encoding 0= (a ^ b): + continue + planes += 1 + hs = tuple(allowed[k][a] & allowed[k][b] for k in others) + dimensions = [] + for h in hs: + vectors = list(members(h)) + require(len(vectors) in (0, 1, 3), 'partner space dimension at most two') + if len(vectors) == 3: + require(vectors[0] ^ vectors[1] == vectors[2], 'partner plane closure') + dimensions.append((len(vectors) + 1).bit_length() - 1) + histogram[tuple(sorted(dimensions))] += 1 + if hs not in configs: + configs[hs] = {'first_plane': (a, b), 'multiplicity': 0} + configs[hs]['multiplicity'] += 1 + require(planes == 43435 and sum(c['multiplicity'] for c in configs.values()) == planes, + 'complete plane coverage') + return configs, [{'dimensions': list(ds), 'planes': count} + for ds, count in sorted(histogram.items())] + + +def subspace_options(k, h, forced, words): + """All subspaces of H: zero, every line, and H itself if dim H=2.""" + vectors = list(members(h)) + require(len(vectors) in (0, 1, 3), 'unsupported partner dimension') + options = [((), (), 0)] + for z in vectors: + options.append(((z,), forced[k, z], words[z])) + if len(vectors) == 3: + require(vectors[0] ^ vectors[1] == vectors[2], 'partner plane closure') + options.append((binary_basis(vectors), + binary_basis(x for z in vectors for x in forced[k, z]), + words[vectors[0]] | words[vectors[1]])) + return options + + +def enumerate_configuration(others, hs, forced, words, unequal, mutual=True): + choices = [(k, subspace_options(k, h, forced, words)) for k, h in zip(others, hs)] + choices.sort(key=lambda item: -len(item[1])) + best, leaves, conflicts = 0, 0, 0 + + def visit(position, constraints, dimension_sum, selected): + nonlocal best, leaves, conflicts + if position == len(choices): + leaves += 1 + # K_anchor is contained in the annihilator of these constraints. + best = max(best, 9 - len(constraints) + dimension_sum) + return + k, options = choices[position] + for zs, fs, support in options: + if mutual and any(support & old_support & unequal[min(k, j), max(k, j)] + for j, old_support in selected): + conflicts += 1 + continue + visit(position + 1, binary_basis(constraints + fs), + dimension_sum + len(zs), selected + [(k, support)]) + + visit(0, (), 0, []) + return best, leaves, conflicts + + +def census(live, words, unequal): + result = [] + for anchor in range(9): + others, allowed, forced = compatibility_spaces(live, words, unequal, anchor) + configs, histogram = plane_configurations(others, allowed) + maxima = Counter() + leaves = conflicts = 0 + for hs in configs: + maximum, count, rejected = enumerate_configuration(others, hs, forced, words, unequal) + require(maximum <= 10, 'total deficiency exceeds ten') + maxima[maximum] += 1 + leaves += count + conflicts += rejected + result.append({'anchor': anchor, 'planes': 43435, 'configurations': len(configs), + 'partner_dimension_histogram': histogram, + 'maximum_histogram': dict(sorted(maxima.items())), + 'compatible_leaves': leaves, 'rejected_branches': conflicts}) + return result + + +def check_identity(live, coefficients): + require(len(coefficients) == len(live) and all(len(c) == 9 for c in coefficients), + 'decoder shape') + for (_, v), c in zip(live, coefficients): + for _, z in live: + require(dot(c, z) == 2 * dot(v, z), 'exact all-pairs identity') + + +def witness(live, all_active): + # The first live line is e_0-e_2. Switch its anchor to 2 to activate term 0. + c = [tuple(2 * (x - v[2 if all_active and i == 0 else 0]) for x in v) + for i, (_, v) in enumerate(live)] + check_identity(live, c) + costs = [rank(u for (u, _), row in zip(live, c) if row[k]) for k in range(9)] + require(sum(costs) == 71, 'witness cost must be seventy-one') + require(not all_active or min(costs) > 0, 'all nine terms must be active') + return c, costs + + +def semantic_controls(rows, live, words, unequal, c): + passed = [] + + def rejected(name, function): + try: + function() + except ValueError: + passed.append(name) + return + raise ValueError('control unexpectedly accepted: ' + name) + + bad = list(c) + bad[0] = tuple(x + (k == 0) for k, x in enumerate(bad[0])) + rejected('coefficient_perturbation', lambda: check_identity(live, bad)) + bad = list(c) + bad[0] = (0,) + bad[0][1:] + rejected('active_term_deleted', lambda: check_identity(live, bad)) + corrupt = list(rows) + corrupt[1] = (corrupt[1][0] ^ 1, corrupt[1][1]) + rejected('label_pairing_corrupted', lambda: check_model(corrupt)) + rejected('nonorthogonal_puncture', lambda: check_model(rows, (1,) + FRAME[1:])) + others, allowed, forced = compatibility_spaces(live, words, unequal, 0) + hs = tuple(allowed[k][1] & allowed[k][508] for k in others) + require(hs[0].bit_count() == 3, 'puncturing permits a partner plane') + rejected('unpunctured_dimension_lemma', lambda: require(hs[0].bit_count() <= 1, + 'false dimension-one inference')) + relaxed, _, _ = enumerate_configuration(others, hs, forced, words, unequal, mutual=False) + checked, _, _ = enumerate_configuration(others, hs, forced, words, unequal) + require(relaxed == 11 and checked == 10, 'mutual compatibility is necessary') + passed.append('omitted_mutual_compatibility_changes_bound') + rejected('false_cost_seventy', lambda: require(sum(rank(u for (u, _), row in zip(live, c) + if row[k]) for k in range(9)) == 70, + 'support ranks disagree with claimed cost')) + # A non-real shift C_i = 2v_i + 3i*1, checked using integer real/imaginary parts. + check_identity(live, [tuple(2 * x for x in v) for _, v in live]) + require(all(dot((3,) * 9, v) == 0 for _, v in live), 'imaginary shift is in the kernel') + require(9 * rank(u for u, _ in live) == 81, 'generic complex shift cost') + passed.append('nonreal_kernel_shift_positive') + return passed + + +def compute(): + rows = model() + require(first_frame(rows) == FRAME, 'declared frame is not lexicographically first') + live = check_model(rows) + words, unequal = tables(live) + anchors = census(live, words, unequal) + _, dropped = witness(live, False) + c, active = witness(live, True) + result = {'schema_version': 1, 'kind': 'scoped proof with exhaustive finite lemmas', + 'model': 'fixed A8 simplex; one P112 frame puncture; all-pairs; separate term costs', + 'frame_indices': list(FRAME), 'frame_labels': [rows[i][0] for i in FRAME], + 'coordinate_permutation_punctures': matching_frame_orbit(rows), + 'live_roots': 112, 'live_root_rank': 8, 'column_label_ranks': [9] * 9, + 'anchors': anchors, 'total_planes': sum(a['planes'] for a in anchors), + 'total_configurations': sum(a['configurations'] for a in anchors), + 'total_compatible_leaves': sum(a['compatible_leaves'] for a in anchors), + 'deficiency_upper_bound': 10, 'sharp_copy_cost': 71, + 'dropped_witness_costs': dropped, 'active_witness_costs': active, + 'all_pairs_checked_per_witness': 112 * 112, + 'semantic_controls': semantic_controls(rows, live, words, unequal, c)} + return json.loads(json.dumps(result)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='regenerate the deterministic certificate') + args = parser.parse_args() + path = HERE / 'CERTIFICATE.json' + expected = None if args.write else json.loads(path.read_text()) + result = compute() + if args.write: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + require(expected == result, 'certificate differs from exact replay') + print('PASS_A8_P112_DECODER_FLOOR planes=390915 configurations=19299 ' + 'compatible_leaves=462141 cost=71 controls=8') + + +if __name__ == '__main__': + main()