diff --git a/research/a8-p112-fano-frame-floor/CERTIFICATE.json b/research/a8-p112-fano-frame-floor/CERTIFICATE.json new file mode 100644 index 0000000000..2019fcfee8 --- /dev/null +++ b/research/a8-p112-fano-frame-floor/CERTIFICATE.json @@ -0,0 +1,3342 @@ +{ + "all_nine_terms_active": true, + "deficiency_upper_bound": 10, + "frame_pair_root_counts": { + "1": 1080, + "4": 945 + }, + "frames": 2025, + "orbits": [ + { + "active_witness_costs": [ + 1, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "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 + ], + "frame": [ + 0, + 15, + 26, + 33, + 42, + 89, + 112, + 119 + ], + "identity_entries": 12544, + "name": "matching", + "orbit_size": 945 + }, + { + "active_witness_costs": [ + 1, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "anchors": [ + { + "anchor": 0, + "compatible_leaves": 52829, + "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": 19816 + }, + { + "anchor": 1, + "compatible_leaves": 52829, + "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": 19816 + }, + { + "anchor": 2, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 3, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 4, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 5, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 6, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 7, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 8, + "compatible_leaves": 39482, + "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": 13904 + } + ], + "column_label_ranks": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "controls": { + "checked_deficiency_bound": 10, + "passed": [ + "coefficient_error", + "active_term_removed", + "label_pairing_error", + "nonorthogonal_puncture", + "mutual_compatibility_needed", + "nonreal_shift_positive" + ], + "relaxation_plane": [ + 1, + 508 + ], + "relaxed_deficiency_bound": 11 + }, + "frame": [ + 0, + 85, + 94, + 99, + 105, + 108, + 112, + 113 + ], + "identity_entries": 12544, + "name": "fano", + "orbit_size": 1080 + } + ], + "predecessor_verifier_sha256": "c8dff5ebf75511bf7c5e962a42189977ef5b20ce02e6f9734e4648e695ca3148", + "schema_version": 1, + "scope": "Fixed A8 simplex, all orthogonal eight-frame punctures, all-pairs, separate copies", + "sharp_copy_cost": 71, + "total_planes": 781830 +} diff --git a/research/a8-p112-fano-frame-floor/README.md b/research/a8-p112-fano-frame-floor/README.md new file mode 100644 index 0000000000..1666f6cd43 --- /dev/null +++ b/research/a8-p112-fano-frame-floor/README.md @@ -0,0 +1,264 @@ +# Independent check: A8 simplex cost 71 on every P112 frame puncture + +For the fixed A8 simplex nine-term all-pairs decoder, the minimum separate-term +binary pairing-rank cost is **71 on every orthogonal eight-frame puncture of +P120**. The minimum is attained with all nine terms active. This is a scoped +proof with exhaustive finite lemmas, not a new supplier or multiplication bound. + +[PR1304](https://github.com/CrocSwap/integer-mult-bounds/pull/1304), by +commdata2338, established 71 on the 945 matching-frame punctures and explicitly +left the other frame orbits open. This package proves 71 on the other 1,080 +frames and checks that these two coordinate-permutation orbits exhaust all +2,025 frames. It replays the earlier orbit as a positive control. Since 71 +exceeds the standard P112 copy cost 64, this family cannot lower that +copied-information bill. + +**Concurrent work:** the final overlap refresh found a +[claim for the same remaining orbit](https://github.com/CrocSwap/integer-mult-bounds/discussions/1241#discussioncomment-18914233), +posted at 03:38 UTC on October 14 after this session's entry snapshot. That +claim reported the same frame census and cost-71 witness, with the lower bound +still being checked. This submission is therefore **independent corroboration** +with a completed lower-bound replay, not a claim of unique discovery. Its +separate Gram-derived checker and all-anchor source-bound replay are the +reviewable contribution; no unpublished implementation from that session is +imported or assumed correct. + +## Reproduce + +From the repository root, using Python 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/a8-p112-fano-frame-floor +``` + +The registered replay runs the primary verifier, a separate implementation, +and six package failure controls. For a standalone source export, these commands +need only this directory and Python 3.10 or later: + +```sh +python3 -I -B research/a8-p112-fano-frame-floor/verify.py +python3 -I -B research/a8-p112-fano-frame-floor/independent.py +python3 -I -B research/a8-p112-fano-frame-floor/test_package.py +``` + +Expected markers: + +```text +PASS_A8_P112_ALL_FRAME_FLOOR frames=2025 orbits=945,1080 planes=781830 sharp_cost=71 active_terms=9 +PASS_A8_P112_INDEPENDENT frames=2025 anchors=4 transported=18 planes=173740 compatible_leaves=184628 sharp_cost=71 +``` + +`verify.py --write` explicitly regenerates `CERTIFICATE.json`. Normal replay +compares the entire recomputed receipt without writing it. The generic package +metadata check needs the base Git history; standalone mathematical replay does +not need Git, network access, or another research package. + +Local validation passed on macOS 27.0.1 arm64: the registered replay and all six +package controls on CPython 3.12.13, plus both mathematical checkers under +isolated, optimized CPython 3.14.6 from a relocated read-only package. The +selected-record integrity check also passed. Hosted CI and human review are +separate from this local evidence. + +## Model and quantified statement + +Use the sum-zero subspace V of C^9 and the 120 oriented E8 root lines: + +- `e_a-e_b`, for `0 <= a < b <= 8`, in lexicographic order; +- `1_S-(1/3)1`, for three-element subsets S, in lexicographic order. + +Remove an orthogonal frame F of eight lines and let R contain the 112 surviving +roots. Fix the nine simplex normals `b_k=e_k-(1/9)1`, so `T_ik=r_ik`. Allow +arbitrary complex D satisfying `D T^t = 2 R R^t` on **all** live pairs, with +ordinary transpose. Charge each term separately by the F2 rank of +`(r_i dot r_j + 1) mod 2` restricted to its actual nonzero row and column supports. + +**Theorem.** For every such F and D, the total charge is at least 71. For every +F there is a rational D attaining 71 with all nine terms active. + +This changes the eight-term hypothesis of the earlier decoder floor. It does +not relax exactness to a masked graph. The theorem concerns the fixed simplex +normals, not every nine-term decoder. + +## Proof + +### 1. Exactly two frame orbits + +Exhaustive increasing-index clique enumeration in the exact orthogonality graph +finds 2,025 frames. Adjacent coordinate transpositions generate S9. Closing the +following representatives under those generators gives disjoint sets of sizes +945 and 1,080, whose union equals the complete frame census: + +```text +matching: [0,15,26,33,42,89,112,119] +Fano: [0,85,94,99,105,108,112,113] +``` + +The matching representative has four pair roots. Its frames are described by +one singleton coordinate and a perfect matching of the other eight coordinates, +as in PR1304. The Fano representative has the pair root `e_0-e_1`, together with +triple roots on + +```text +234, 256, 278, 357, 368, 458, 467. +``` + +These are the seven lines of a Fano plane on coordinates 2 through 8. +Independently generating the 30 labelled Fano planes for each of 36 coordinate +pairs produces the same 1,080 frames. The separate checker also reconstructs all +945 matching frames and compares their union with its own orthogonality census. + +Coordinate permutations preserve the simplex family and root lines, possibly +reversing pair-root representatives. Apply the corresponding row signs to both +factors. This preserves the all-pairs identity and every support. Signs also +preserve the binary pairing since the Gram entries are integers. Thus proving +the cost statement for both representatives proves it for every frame. + +### 2. Deficiency spaces cover all complex shifts + +The live roots span V; each representative is checked exactly. Therefore + +```text +D_ik = 2r_ik + t_i, t_i arbitrary in C. +``` + +Indeed every row of `D-2R` annihilates V and is a multiple of the all-ones vector. +Use binary labels `u_ab=1+e_a+e_b` and `u_S=1_S`. Their dot product equals the +binary Gram pairing on all 14,400 root pairs. For both representatives and every +column k, the labels on `{i:r_ik != 0}` span F2^9. + +Let K_k be the annihilator of the labels on `{i:D_ik != 0}`, and write +`delta_k=dim K_k`. Full column span makes the cost exactly + +```text +81 - sum_k delta_k. +``` + +If `w in K_j` and `z in K_k` both evaluate nontrivially on a live label u_i, +then `D_ij=D_ik=0`, which forces `r_ij=r_ik`. This necessary compatibility +condition applies to arbitrary complex shifts, including shifts with no zeros. + +If every deficiency is at most one, their sum is at most nine. Otherwise choose +an anchor j and a binary plane U contained in K_j. There are exactly 43,435 +planes, represented uniquely by `0 i} + if len(rest) >= 7 - len(prefix): + extend(prefix + (i,), rest) + + extend((), set(range(120))) + return frames + + +def matchings(xs): + if not xs: + yield () + else: + for b in xs[1:]: + for tail in matchings(tuple(x for x in xs[1:] if x != b)): + yield ((xs[0], b),) + tail + + +def combinatorial_orbits(rs): + pairs = {tuple(i for i, x in enumerate(r) if x): n for n, r in enumerate(rs[:36])} + triples = {tuple(i for i, x in enumerate(r) if x == 2): n + for n, r in enumerate(rs) if n >= 36} + matching = set() + for singleton in range(9): + for blocks in matchings(tuple(i for i in range(9) if i != singleton)): + f = [pairs[b] for b in blocks] + f += [triples[tuple(sorted((*b, singleton)))] for b in blocks] + matching.add(tuple(sorted(f))) + template = [tuple(i - 2 for i, x in enumerate(rs[n]) if x == 2) for n in FANO[1:]] + systems = {tuple(sorted(tuple(sorted(p[i] for i in line)) for line in template)) + for p in permutations(range(7))} + check(len(systems) == 30, 'thirty labelled Fano planes') + fano = set() + for pair in pairs: + remaining = [i for i in range(9) if i not in pair] + for lines in systems: + f = [pairs[pair]] + [triples[tuple(remaining[i] for i in line)] for line in lines] + fano.add(tuple(sorted(f))) + check(len(matching) == 945 and len(fano) == 1080, 'combinatorial orbit counts') + check(not matching & fano, 'orbits disjoint') + check(matching | fano == all_frames(rs), 'all frames covered by explicit coordinate images') + return matching, fano + + +def stabilizer_orbits(rs, frame): + lookup = {r: n for n, r in enumerate(rs)} + lookup.update({tuple(-x for x in r): n for n, r in enumerate(rs)}) + actions = [] + if frame == FANO: + for tail in permutations(range(2, 9)): + p = (0, 1) + tail + image = {lookup[tuple(rs[n][p[i]] for i in range(9))] for n in frame} + if image == set(frame): + actions.append(p) + check(len(actions) == 168, 'Fano automorphism count') + actions.append((1, 0, 2, 3, 4, 5, 6, 7, 8)) + else: + for i in (0, 2, 4, 6): + p = list(range(9)) + p[i], p[i + 1] = p[i + 1], p[i] + actions.append(tuple(p)) + for i in (0, 2, 4): + p = list(range(9)) + p[i:i + 4] = p[i + 2:i + 4] + p[i:i + 2] + actions.append(tuple(p)) + for p in actions: + check({lookup[tuple(rs[n][p[i]] for i in range(9))] for n in frame} == set(frame), + 'anchor transport must preserve puncture') + result = [] + remaining = set(range(9)) + while remaining: + orbit = {min(remaining)} + while True: + expanded = orbit | {p[i] for i in orbit for p in actions} + if expanded == orbit: + break + orbit = expanded + result.append(sorted(orbit)) + remaining -= orbit + return result + + +def gram_model(rs, frame): + live = [r for n, r in enumerate(rs) if n not in frame] + check(all(sum(r) == 0 and dot(r, r) == 18 for r in rs), 'E8 norms and sum-zero space') + gram = [[dot(r, s) for s in live] for r in live] + check(all(g % 9 == 0 for row in gram for g in row), 'integral normalized Gram matrix') + parity = [sum(((g // 9 + 1) % 2) << j for j, g in enumerate(row)) for row in gram] + pivots = sorted(echelon(parity)) + check(len(pivots) == 9, 'Gram pairing rank nine') + labels = [sum(((row >> p) & 1) << j for j, p in enumerate(pivots)) for row in parity] + check(len(echelon(labels)) == 9, 'injective row-space coordinates') + for k in range(9): + check(len(echelon(l for l, r in zip(labels, live) if r[k])) == 9, + 'each column support spans nine') + # Rank modulo 101 proves rank at least eight over Q; sum zero proves at most eight. + basis = {} + for r in live: + v = [x % 101 for x in r] + for j in range(9): + if v[j]: + if j in basis: + c = v[j] + v = [(x - c * y) % 101 for x, y in zip(v, basis[j])] + else: + inv = pow(v[j], -1, 101) + basis[j] = [(x * inv) % 101 for x in v] + break + check(len(basis) == 8, 'live root rank eight') + return live, labels, parity + + +def anchor_census(live, labels, anchor): + evaluations = [sum(((l & w).bit_count() % 2) << i for i, l in enumerate(labels)) + for w in range(512)] + others = [k for k in range(9) if k != anchor] + unequal = {k: sum((r[k] != r[anchor]) << i for i, r in enumerate(live)) for k in others} + + @lru_cache(None) + def partner(cut): + h = annihilator(labels[i] for i in bits(cut)) + check(len(h) in (0, 1, 3), 'partner dimension exceeds two') + return h + + configurations = set() + plane_count = 0 + for a in range(1, 512): + for b in range(a + 1, 512): + if b < (a ^ b): + plane_count += 1 + cut = evaluations[a] | evaluations[b] + configurations.add(tuple(partner(cut & unequal[k]) for k in others)) + check(plane_count == 43435, 'exhaustive plane enumeration') + values = sorted({x for r in live for x in r}) + row_values = {k: [sum((r[k] == v) << i for i, r in enumerate(live)) for v in values] + for k in others} + + @lru_cache(None) + def options(k, h): + subspaces = [(0, ())] + [(1, (w,)) for w in h] + if len(h) == 3: + check(h[0] ^ h[1] == h[2], 'plane closure') + subspaces.append((2, h)) + result = [] + for dimension, vectors in subspaces: + forced = 0 + for w in vectors: + forced |= evaluations[w] + result.append((dimension, tuple(forced & m for m in row_values[k]), + forced & unequal[k])) + return tuple(result) + + @lru_cache(None) + def rank_cut(cut): + return len(echelon(labels[i] for i in bits(cut))) + + maxima = Counter() + leaves = 0 + for hs in configurations: + maximum = 0 + for choice in product(*(options(k, h) for k, h in zip(others, hs))): + assigned = [0] * len(values) + assigned_any = constraints = dimensions = 0 + valid = True + for dimension, masks, cut in choice: + if any(mask & (assigned_any ^ assigned[i]) for i, mask in enumerate(masks)): + valid = False + break + for i, mask in enumerate(masks): + assigned[i] |= mask + assigned_any |= mask + constraints |= cut + dimensions += dimension + if valid: + leaves += 1 + maximum = max(maximum, 9 - rank_cut(constraints) + dimensions) + check(maximum <= 10, 'total deficiency exceeds ten') + maxima[maximum] += 1 + return {'anchor': anchor, 'planes': plane_count, 'configurations': len(configurations), + 'compatible_leaves': leaves, 'maximum_histogram': dict(sorted(maxima.items()))} + + +def witness(live, parity): + coefficients = [tuple(2 * (x - r[2 if i == 0 else 0]) for x in r) + for i, r in enumerate(live)] + check(all(dot(c, s) == 2 * dot(r, s) for c, r in zip(coefficients, live) for s in live), + 'full all-pairs witness identity') + costs = [] + for k in range(9): + columns = sum((r[k] != 0) << i for i, r in enumerate(live)) + costs.append(len(echelon(row & columns for row, c in zip(parity, coefficients) if c[k]))) + check(costs == [1, 8, 8, 9, 9, 9, 9, 9, 9], 'direct pairing-submatrix costs') + return costs + + +def main(): + receipt = json.loads((HERE / 'CERTIFICATE.json').read_text()) + check(receipt['sharp_copy_cost'] == 71 and receipt['frames'] == 2025, 'headline receipt') + rs = roots() + matching, fano = combinatorial_orbits(rs) + total_planes = total_leaves = 0 + for name, frame, orbit in [('matching', MATCHING, matching), ('fano', FANO, fano)]: + expected = next(x for x in receipt['orbits'] if x['name'] == name) + check(expected['frame'] == list(frame) and expected['orbit_size'] == len(orbit), 'frame receipt') + coordinate_orbits = stabilizer_orbits(rs, frame) + check(coordinate_orbits == ([list(range(8)), [8]] if name == 'matching' else + [[0, 1], list(range(2, 9))]), 'anchor orbit partition') + live, labels, parity = gram_model(rs, frame) + check(witness(live, parity) == expected['active_witness_costs'], 'witness receipt') + check([a['anchor'] for a in expected['anchors']] == list(range(9)), 'all anchors recorded') + for orbit in coordinate_orbits: + result = anchor_census(live, labels, orbit[0]) + for a in orbit: + for key in ('planes', 'configurations', 'compatible_leaves', 'maximum_histogram'): + check(json.loads(json.dumps(result[key])) == expected['anchors'][a][key], + f'{name} anchor {a}: independent {key} mismatch') + total_planes += result['planes'] + total_leaves += result['compatible_leaves'] + print(f'PASS_A8_P112_INDEPENDENT frames=2025 anchors=4 transported=18 ' + f'planes={total_planes} compatible_leaves={total_leaves} sharp_cost=71') + + +if __name__ == '__main__': + main() diff --git a/research/a8-p112-fano-frame-floor/test_package.py b/research/a8-p112-fano-frame-floor/test_package.py new file mode 100644 index 0000000000..718de514ed --- /dev/null +++ b/research/a8-p112-fano-frame-floor/test_package.py @@ -0,0 +1,65 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Failure controls for source bindings and the public receipt-checking command.""" + +import importlib.util +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('frame_floor_verifier', HERE / 'verify.py') +verifier = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verifier) + + +class PackageControls(unittest.TestCase): + def test_changed_predecessor_rejected(self): + with tempfile.TemporaryDirectory() as directory: + path = Path(directory) / 'changed.py' + path.write_bytes((HERE / 'vendor/pr1304_verify.py').read_bytes() + b'\n') + with self.assertRaisesRegex(ValueError, 'source bytes changed'): + verifier.predecessor(path) + + def test_missing_predecessor_rejected(self): + with tempfile.TemporaryDirectory() as directory: + with self.assertRaises(FileNotFoundError): + verifier.predecessor(Path(directory) / 'absent.py') + + def rejected_receipt(self, text, expected_error): + with tempfile.TemporaryDirectory() as directory: + path = Path(directory) / 'receipt.json' + if text is not None: + path.write_text(text) + result = subprocess.run( + [sys.executable, '-I', '-O', '-B', str(HERE / 'verify.py'), + '--certificate', str(path)], cwd=directory, capture_output=True, + text=True, timeout=120) + self.assertNotEqual(result.returncode, 0) + self.assertIn(expected_error, result.stderr) + self.assertNotIn('PASS_A8_P112', result.stdout) + if text is not None: + self.assertEqual(path.read_text(), text) + + def test_false_cost_rejected_by_cli(self): + receipt = json.loads((HERE / 'CERTIFICATE.json').read_text()) + receipt['sharp_copy_cost'] = 70 + self.rejected_receipt(json.dumps(receipt), 'certificate differs') + + def test_omitted_anchor_rejected_by_cli(self): + receipt = json.loads((HERE / 'CERTIFICATE.json').read_text()) + receipt['orbits'][1]['anchors'].pop() + self.rejected_receipt(json.dumps(receipt), 'certificate differs') + + def test_missing_receipt_rejected_by_cli(self): + self.rejected_receipt(None, 'FileNotFoundError') + + def test_malformed_receipt_rejected_by_cli(self): + self.rejected_receipt('{broken', 'JSONDecodeError') + + +if __name__ == '__main__': + unittest.main() diff --git a/research/a8-p112-fano-frame-floor/vendor/pr1304_verify.py b/research/a8-p112-fano-frame-floor/vendor/pr1304_verify.py new file mode 100644 index 0000000000..188d3a8fda --- /dev/null +++ b/research/a8-p112-fano-frame-floor/vendor/pr1304_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() diff --git a/research/a8-p112-fano-frame-floor/verify.py b/research/a8-p112-fano-frame-floor/verify.py new file mode 100644 index 0000000000..62dbf9ae27 --- /dev/null +++ b/research/a8-p112-fano-frame-floor/verify.py @@ -0,0 +1,189 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Close the other A8 simplex P112 frame orbit using pinned PR1304 lemmas. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. +The exact predecessor implementation is retained unmodified and credited. +""" + +import argparse +from collections import Counter, deque +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +FANO_FRAME = (0, 85, 94, 99, 105, 108, 112, 113) +MATCHING_FRAME = (0, 15, 26, 33, 42, 89, 112, 119) +VENDOR_SHA256 = 'c8dff5ebf75511bf7c5e962a42189977ef5b20ce02e6f9734e4648e695ca3148' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def predecessor(path=HERE / 'vendor/pr1304_verify.py'): + require(hashlib.sha256(path.read_bytes()).hexdigest() == VENDOR_SHA256, + 'PR1304 source bytes changed') + spec = importlib.util.spec_from_file_location('pinned_pr1304', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def frame_census(p, rows): + """Enumerate all orthogonal eight-cliques, with increasing root indices.""" + adjacency = [sum(1 << j for j in range(i + 1, 120) + if p.dot(rows[i][1], rows[j][1]) == 0) for i in range(120)] + frames = set() + + def visit(prefix, candidates): + if len(prefix) == 8: + frames.add(prefix) + return + while candidates: + bit = candidates & -candidates + candidates ^= bit + i = bit.bit_length() - 1 + rest = candidates & adjacency[i] + if len(prefix) + 1 + rest.bit_count() >= 8: + visit(prefix + (i,), rest) + + visit((), (1 << 120) - 1) + require(len(frames) == 2025, 'complete E8 frame census count') + return frames + + +def coordinate_orbit(rows, start): + """Adjacent transpositions generate S9; signs of pair roots are immaterial.""" + lookup = {} + for i, (_, v) in enumerate(rows): + lookup[v] = lookup[tuple(-x for x in v)] = i + actions = [] + for k in range(8): + action = [] + for _, v in rows: + w = list(v) + w[k], w[k + 1] = w[k + 1], w[k] + action.append(lookup[tuple(w)]) + require(len(set(action)) == 120, 'coordinate action is a permutation') + actions.append(action) + orbit, queue = {start}, deque([start]) + while queue: + f = queue.popleft() + for action in actions: + image = tuple(sorted(action[i] for i in f)) + if image not in orbit: + orbit.add(image) + queue.append(image) + return orbit + + +def active_witness(p, live): + require(live[0][1] == (3, 0, -3, 0, 0, 0, 0, 0, 0), 'witness root is e0-e2') + coefficients = [tuple(2 * (x - v[2 if i == 0 else 0]) for x in v) + for i, (_, v) in enumerate(live)] + p.check_identity(live, coefficients) + costs = [p.rank(u for (u, _), c in zip(live, coefficients) if c[k]) + for k in range(9)] + require(costs == [1, 8, 8, 9, 9, 9, 9, 9, 9], 'active witness cost vector') + return coefficients, costs + + +def controls(p, rows, live, coefficients): + names = [] + + def rejects(name, action): + try: + action() + except ValueError: + names.append(name) + return + raise ValueError('control unexpectedly accepted: ' + name) + + bad = list(coefficients) + bad[0] = (bad[0][0] + 1,) + bad[0][1:] + rejects('coefficient_error', lambda: p.check_identity(live, bad)) + bad_term = [(0,) + c[1:] for c in coefficients] + rejects('active_term_removed', lambda: p.check_identity(live, bad_term)) + labels = list(rows) + labels[1] = (labels[1][0] ^ 1, labels[1][1]) + rejects('label_pairing_error', lambda: p.check_model(labels, FANO_FRAME)) + rejects('nonorthogonal_puncture', + lambda: p.check_model(rows, (1,) + FANO_FRAME[1:])) + words, unequal = p.tables(live) + others, allowed, forced = p.compatibility_spaces(live, words, unequal, 0) + configs, _ = p.plane_configurations(others, allowed) + for hs, data in configs.items(): + relaxed = p.enumerate_configuration(others, hs, forced, words, unequal, False)[0] + if relaxed > 10: + checked = p.enumerate_configuration(others, hs, forced, words, unequal)[0] + require(checked == 10, 'mutual compatibility control') + names.append('mutual_compatibility_needed') + control_plane = list(data['first_plane']) + break + else: + raise ValueError('missing relaxation counterexample') + # Exact real and imaginary parts of a generic complex kernel shift. + p.check_identity(live, [tuple(2 * x for x in v) for _, v in live]) + require(all(sum(v) == 0 for _, v in live), 'imaginary all-ones kernel') + require(p.rank(u for u, _ in live) == 9, 'generic complex shift cost 81') + names.append('nonreal_shift_positive') + return {'passed': names, 'relaxation_plane': control_plane, + 'relaxed_deficiency_bound': relaxed, 'checked_deficiency_bound': checked} + + +def compute(): + p = predecessor() + rows = p.model() + frames = frame_census(p, rows) + matching = coordinate_orbit(rows, MATCHING_FRAME) + fano = coordinate_orbit(rows, FANO_FRAME) + require(len(matching) == 945 and len(fano) == 1080, 'coordinate orbit sizes') + require(not matching & fano and matching | fano == frames, 'two orbits cover every frame') + require(all(sum(i < 36 for i in f) == 4 for f in matching), 'matching root types') + require(all(sum(i < 36 for i in f) == 1 for f in fano), 'Fano root types') + orbit_results = [] + for name, frame, size in [('matching', MATCHING_FRAME, 945), ('fano', FANO_FRAME, 1080)]: + live = p.check_model(rows, frame) + words, unequal = p.tables(live) + anchors = p.census(live, words, unequal) + coefficients, costs = active_witness(p, live) + result = {'name': name, 'frame': list(frame), 'orbit_size': size, + 'anchors': anchors, 'active_witness_costs': costs, + 'identity_entries': 112 * 112, 'column_label_ranks': [9] * 9} + if name == 'fano': + result['controls'] = controls(p, rows, live, coefficients) + orbit_results.append(result) + return json.loads(json.dumps({ + 'schema_version': 1, + 'scope': 'Fixed A8 simplex, all orthogonal eight-frame punctures, all-pairs, separate copies', + 'frames': len(frames), 'frame_pair_root_counts': dict(Counter(sum(i < 36 for i in f) for f in frames)), + 'orbits': orbit_results, 'total_planes': 2 * 9 * 43435, + 'deficiency_upper_bound': 10, 'sharp_copy_cost': 71, + 'all_nine_terms_active': True, 'predecessor_verifier_sha256': VENDOR_SHA256})) + + +def compare_certificate(expected, actual): + require(expected == actual, 'certificate differs from complete exact replay') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + parser.add_argument('--certificate', type=Path, default=HERE / 'CERTIFICATE.json') + args = parser.parse_args() + expected = None if args.write else json.loads(args.certificate.read_text()) + result = compute() + if args.write: + args.certificate.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + compare_certificate(expected, result) + print('PASS_A8_P112_ALL_FRAME_FLOOR frames=2025 orbits=945,1080 ' + 'planes=781830 sharp_cost=71 active_terms=9') + + +if __name__ == '__main__': + main()