From 7e4e01a281afa5c76930f6a211b381c653912d75 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 10 Nov 2026 21:30:11 +0000 Subject: [PATCH] feat(research): prove a closed form for E8 port counts in subspaces Answers the ports-per-dimension half of open question 1 of PR 6861: N(V) = 2^(e-2) + (sigma' - sigma)/4 with both character sums fixed up to sign by the radical of B|V, hence N(V) <= 2^(e-2) + 4 with three equality classes and N(V) <= 64 at dimension 8. The verifier requires every clause on all subspaces of F2^9 and checks seven P104 witnesses. --- .../CENSUS.json | 962 ++++++++++++++++++ .../p104-e8-port-count-closed-form/PROOF.md | 191 ++++ .../p104-e8-port-count-closed-form/README.md | 151 +++ .../SOURCES.json | 30 + .../p104-e8-port-count-closed-form/TASK.json | 145 +++ .../VERIFY.json | 23 + .../p104-e8-port-count-closed-form/verify.py | 325 ++++++ 7 files changed, 1827 insertions(+) create mode 100644 research/p104-e8-port-count-closed-form/CENSUS.json create mode 100644 research/p104-e8-port-count-closed-form/PROOF.md create mode 100644 research/p104-e8-port-count-closed-form/README.md create mode 100644 research/p104-e8-port-count-closed-form/SOURCES.json create mode 100644 research/p104-e8-port-count-closed-form/TASK.json create mode 100644 research/p104-e8-port-count-closed-form/VERIFY.json create mode 100644 research/p104-e8-port-count-closed-form/verify.py diff --git a/research/p104-e8-port-count-closed-form/CENSUS.json b/research/p104-e8-port-count-closed-form/CENSUS.json new file mode 100644 index 0000000000..c8231f24db --- /dev/null +++ b/research/p104-e8-port-count-closed-form/CENSUS.json @@ -0,0 +1,962 @@ +{ + "schema_version": 1, + "subspaces_total": 8283458, + "subspaces_inside_even_hyperplane": 417199, + "small_subspaces_by_dimension": [ + 1, + 511, + 43435, + 788035, + 3309747 + ], + "classes": [ + { + "dimension": 1, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 1, + "subspaces": 120 + }, + { + "dimension": 1, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 135 + }, + { + "dimension": 1, + "contains_all_ones": 1, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 1 + }, + { + "dimension": 2, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": -1, + "sign_sigma_prime": 1, + "ports": 2, + "subspaces": 3360 + }, + { + "dimension": 2, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 0, + "subspaces": 4320 + }, + { + "dimension": 2, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 1, + "subspaces": 8640 + }, + { + "dimension": 2, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 1, + "subspaces": 7560 + }, + { + "dimension": 2, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 2, + "subspaces": 3780 + }, + { + "dimension": 2, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 4725 + }, + { + "dimension": 2, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 1, + "subspaces": 120 + }, + { + "dimension": 2, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 135 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 3, + "subspaces": 30240 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": -1, + "sign_sigma_prime": 1, + "ports": 4, + "subspaces": 22680 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": -1, + "ports": 1, + "subspaces": 40320 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 2, + "subspaces": 120960 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 3, + "subspaces": 120960 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 0, + "subspaces": 37800 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 1, + "subspaces": 151200 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 2, + "subspaces": 75600 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 2, + "subspaces": 56700 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 4, + "subspaces": 9450 + }, + { + "dimension": 3, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 14175 + }, + { + "dimension": 3, + "contains_all_ones": 1, + "radical_dimension": 1, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 3, + "subspaces": 1120 + }, + { + "dimension": 3, + "contains_all_ones": 1, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 1, + "subspaces": 4320 + }, + { + "dimension": 3, + "contains_all_ones": 1, + "radical_dimension": 3, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 2, + "subspaces": 3780 + }, + { + "dimension": 3, + "contains_all_ones": 1, + "radical_dimension": 3, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 1575 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": -1, + "sign_sigma_prime": -1, + "ports": 4, + "subspaces": 120960 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": -1, + "sign_sigma_prime": 1, + "ports": 6, + "subspaces": 241920 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 2, + "subspaces": 403200 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 4, + "subspaces": 604800 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 6, + "subspaces": 37800 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": -1, + "sign_sigma_prime": 1, + "ports": 8, + "subspaces": 9450 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": -1, + "ports": 2, + "subspaces": 75600 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 4, + "subspaces": 831600 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 6, + "subspaces": 226800 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 0, + "subspaces": 28350 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 2, + "subspaces": 340200 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 4, + "subspaces": 56700 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 4, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 4, + "subspaces": 28350 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 4, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 8, + "subspaces": 2025 + }, + { + "dimension": 4, + "contains_all_ones": 0, + "radical_dimension": 4, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 4050 + }, + { + "dimension": 4, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 6, + "subspaces": 7560 + }, + { + "dimension": 4, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 4, + "subspaces": 40320 + }, + { + "dimension": 4, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 2, + "subspaces": 37800 + }, + { + "dimension": 4, + "contains_all_ones": 1, + "radical_dimension": 4, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 4, + "subspaces": 9450 + }, + { + "dimension": 4, + "contains_all_ones": 1, + "radical_dimension": 4, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 2025 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": -1, + "sign_sigma_prime": -1, + "ports": 8, + "subspaces": 37800 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 10, + "subspaces": 120960 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": -1, + "sign_sigma_prime": 1, + "ports": 12, + "subspaces": 75600 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": -1, + "ports": 6, + "subspaces": 241920 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 8, + "subspaces": 604800 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 10, + "subspaces": 403200 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 4, + "subspaces": 226800 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 6, + "subspaces": 604800 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 8, + "subspaces": 340200 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 0, + "sign_sigma_prime": -1, + "ports": 4, + "subspaces": 9450 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 8, + "subspaces": 255150 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 12, + "subspaces": 28350 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 0, + "subspaces": 2025 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 4, + "subspaces": 56700 + }, + { + "dimension": 5, + "contains_all_ones": 0, + "radical_dimension": 3, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 8, + "subspaces": 4050 + }, + { + "dimension": 5, + "contains_all_ones": 1, + "radical_dimension": 1, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 10, + "subspaces": 24192 + }, + { + "dimension": 5, + "contains_all_ones": 1, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 6, + "subspaces": 67200 + }, + { + "dimension": 5, + "contains_all_ones": 1, + "radical_dimension": 3, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 12, + "subspaces": 3150 + }, + { + "dimension": 5, + "contains_all_ones": 1, + "radical_dimension": 3, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 8, + "subspaces": 75600 + }, + { + "dimension": 5, + "contains_all_ones": 1, + "radical_dimension": 3, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 4, + "subspaces": 28350 + }, + { + "dimension": 5, + "contains_all_ones": 1, + "radical_dimension": 5, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 8, + "subspaces": 2025 + }, + { + "dimension": 5, + "contains_all_ones": 1, + "radical_dimension": 5, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 0, + "subspaces": 270 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": -1, + "sign_sigma_prime": -1, + "ports": 16, + "subspaces": 30240 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": -1, + "sign_sigma_prime": 1, + "ports": 20, + "subspaces": 40320 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 12, + "subspaces": 120960 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 16, + "subspaces": 151200 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": -1, + "ports": 12, + "subspaces": 22680 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 16, + "subspaces": 177660 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 20, + "subspaces": 37800 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 8, + "subspaces": 9450 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 12, + "subspaces": 75600 + }, + { + "dimension": 6, + "contains_all_ones": 0, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 16, + "subspaces": 14175 + }, + { + "dimension": 6, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 20, + "subspaces": 7560 + }, + { + "dimension": 6, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 16, + "subspaces": 40320 + }, + { + "dimension": 6, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 12, + "subspaces": 37800 + }, + { + "dimension": 6, + "contains_all_ones": 1, + "radical_dimension": 4, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 16, + "subspaces": 9450 + }, + { + "dimension": 6, + "contains_all_ones": 1, + "radical_dimension": 4, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 8, + "subspaces": 2025 + }, + { + "dimension": 7, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": -1, + "ports": 28, + "subspaces": 3360 + }, + { + "dimension": 7, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 32, + "subspaces": 7560 + }, + { + "dimension": 7, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 0, + "sign_sigma_prime": 1, + "ports": 36, + "subspaces": 4320 + }, + { + "dimension": 7, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 24, + "subspaces": 3780 + }, + { + "dimension": 7, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 28, + "subspaces": 8640 + }, + { + "dimension": 7, + "contains_all_ones": 0, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 32, + "subspaces": 4725 + }, + { + "dimension": 7, + "contains_all_ones": 1, + "radical_dimension": 1, + "sign_sigma": -1, + "sign_sigma_prime": 0, + "ports": 36, + "subspaces": 1120 + }, + { + "dimension": 7, + "contains_all_ones": 1, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 28, + "subspaces": 4320 + }, + { + "dimension": 7, + "contains_all_ones": 1, + "radical_dimension": 3, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 32, + "subspaces": 3780 + }, + { + "dimension": 7, + "contains_all_ones": 1, + "radical_dimension": 3, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 24, + "subspaces": 1575 + }, + { + "dimension": 8, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": 1, + "sign_sigma_prime": -1, + "ports": 56, + "subspaces": 120 + }, + { + "dimension": 8, + "contains_all_ones": 0, + "radical_dimension": 0, + "sign_sigma": 1, + "sign_sigma_prime": 1, + "ports": 64, + "subspaces": 135 + }, + { + "dimension": 8, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": 0, + "sign_sigma_prime": 0, + "ports": 64, + "subspaces": 120 + }, + { + "dimension": 8, + "contains_all_ones": 1, + "radical_dimension": 2, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 56, + "subspaces": 135 + }, + { + "dimension": 9, + "contains_all_ones": 1, + "radical_dimension": 1, + "sign_sigma": 1, + "sign_sigma_prime": 0, + "ports": 120, + "subspaces": 1 + } + ], + "max_ports_by_dimension": { + "1": 1, + "2": 2, + "3": 4, + "4": 8, + "5": 12, + "6": 20, + "7": 36, + "8": 64, + "9": 120 + }, + "maximizers_by_dimension": { + "1": 120, + "2": 7140, + "3": 32130, + "4": 11475, + "5": 107100, + "6": 85680, + "7": 5440, + "8": 255, + "9": 1 + }, + "p104_witness_bases": { + "1": [ + 416 + ], + "2": [ + 224, + 352 + ], + "3": [ + 48, + 208, + 336 + ], + "4": [ + 48, + 72, + 152, + 280 + ], + "5": [ + 1, + 12, + 22, + 36, + 196 + ], + "6": [ + 2, + 4, + 9, + 17, + 32, + 129 + ], + "7": [ + 1, + 2, + 8, + 20, + 100, + 132, + 260 + ] + } +} diff --git a/research/p104-e8-port-count-closed-form/PROOF.md b/research/p104-e8-port-count-closed-form/PROOF.md new file mode 100644 index 0000000000..5b61b6b7db --- /dev/null +++ b/research/p104-e8-port-count-closed-form/PROOF.md @@ -0,0 +1,191 @@ +# Proof: a closed form for E8 port counts in subspaces + +## Setting + +The setting is that of PR #6861 (`research/p104-e8-subspace-invariants`). +`F = F2^9`, `wt` is Hamming weight, `par(x) = wt(x) mod 2`, `x.y` is the +dot product, `1` is the all-ones vector and `E = ker par` is the even +hyperplane. The quadratic form is `q(x) = C(wt x, 2) mod 2`, with polar +form `B(x,y) = q(x+y) + q(x) + q(y) = wt(x) wt(y) + wt(x & y) mod 2`. The +radical of `B` is `<1>`, and `q(1) = 0`. The port set is + + P120 = { x : par(x) = 1 and q(x) = 1 } (weights 3 and 7), + +and `N(V) = |P120 ∩ V|` for a subspace `V`. + +Fix a subspace `V` of dimension `e`. Write + +- `R = { y in V : B(y,x) = 0 for all x in V }`, the radical of `B|V`, and + `rho = dim R`; +- `delta = 1` if `1` lies in `V`, otherwise `delta = 0`; +- `q' = q + par`, so `q'(x) = C(wt x + 1, 2) mod 2`; +- `sigma = sum over x in V of (-1)^q(x)` and + `sigma' = sum over x in V of (-1)^q'(x)`. + +Since `par` is linear, `q` and `q'` are quadratic forms on `V` with the +same polar form `B|V`. For `y, y'` in `R`, `B(y,y') = 0`, so both forms +are linear on `R`. + +Two identities are used throughout. + +**(I1)** `B(x,y) = x . tau(y)`, where `tau(y) = y + par(y) 1`. Indeed +`x . 1 = par(x)`, so `x . tau(y) = x.y + par(x) par(y)`. The map `tau` is +linear with kernel `<1>`. + +**(I2)** `sum over x in F of (-1)^q(x) = 32`. The weights with `q = 0` +are those congruent to 0 or 1 mod 4, which gives +`1 + 9 + 126 + 126 + 9 + 1 = 272` vectors, against `240` with `q = 1`. + +## Theorem 1 (closed form) + +Let `V` be a subspace of dimension `e` that is not contained in `E`. Then + + N(V) = 2^(e-2) + (sigma' - sigma) / 4, + + sigma^2 = 2^(e+rho) if q vanishes on R, and 0 otherwise, + sigma'^2 = 2^(e+rho) if q' vanishes on R, and 0 otherwise. + +So `N(V) = 2^(e-2) + (s' - s) 2^(t-2)` with `t = (e + rho)/2` and +`s, s'` in `{-1, 0, 1}`. The number `s` is zero exactly when `q` is +nonzero on `R`, and likewise for `s'` and `q'`. + +*Proof.* The indicator of a port is +`(1 - (-1)^par(x)) (1 - (-1)^q(x)) / 4`. Summing over `V`, + + 4 N(V) = 2^e - sum (-1)^par(x) - sigma + sigma'. + +`par` is a nonzero linear form on `V`, so the middle sum is zero. + +Let `Q` be `q` or `q'`. Substituting `y = x + z`, + + (sum_x (-1)^Q(x))^2 = sum_z sum_x (-1)^(Q(x) + Q(x+z)) + = sum_z (-1)^Q(z) sum_x (-1)^B(x,z). + +The inner sum is `2^e` if `z` lies in `R` and `0` otherwise. Hence the +square is `2^e sum over z in R of (-1)^Q(z)`. As `Q` is linear on `R`, +this last sum is `2^rho` if `Q` vanishes on `R` and `0` otherwise. The +rank `e - rho` of the alternating form `B|V` is even, so `t` is an +integer. ∎ + +## Theorem 2 (constraints) + +For every subspace `V` of dimension `e`: + +**(a)** `e + rho <= 8 + 2 delta`. + +**(b)** If `delta = 1` then `sigma' = 0`. + +**(c)** If `e + rho = 8 + 2 delta` and `q` vanishes on `R`, then +`sigma = 2^(4 + delta)`, which is positive. + +*Proof.* (a) By (I1), the `B`-orthogonal of `R` is the dot orthogonal of +`tau(R)`. Since `1` lies in the radical of `B`, it lies in `R` exactly +when it lies in `V`, so `dim tau(R) = rho - delta` and + + dim R^perp = 9 - rho + delta. + +`V` is contained in `R^perp`, hence `e + rho <= 9 + delta`. As `e + rho` +is even, this is `e + rho <= 8 + 2 delta`. + +(b) If `1` lies in `V` it lies in `R`, and `q'(1) = q(1) + par(1) = 1`. +So `q'` is nonzero on `R` and Theorem 1 gives `sigma' = 0`. + +(c) Let `T` be any subspace on which `q` vanishes; then `B` vanishes on +`T` as well. For `r` in `T`, `q(x + r) = q(x) + B(x,r)`. Averaging (I2) +over translations by `T`, + + 32 = (1/|T|) sum_x (-1)^q(x) sum_{r in T} (-1)^B(x,r) + = sum over x in T^perp of (-1)^q(x), + +because the inner sum is `|T|` when `x` lies in `T^perp` and `0` +otherwise. Take `T = R`. If `delta = 1` and `e + rho = 10`, then +`dim V = dim R^perp`, so `V = R^perp` and `sigma = 32`. If `delta = 0` +and `e + rho = 8`, then `V` has codimension one in `R^perp`, and `1` lies +in `R^perp` but not in `V`, so `R^perp` is the disjoint union of `V` and +`V + 1`. As `q(x + 1) = q(x)`, `sigma = 32/2 = 16`. ∎ + +## Theorem 3 (the bound and its equality cases) + +For every subspace `V` of `F2^9` of dimension `e`, + + N(V) <= 2^(e-2) + 4. + +Equality holds exactly in three cases: + +1. `delta = 1`, `e + rho = 8`, `q` vanishes on `R` and `sigma < 0`; +2. `delta = 0`, `e + rho = 8`, `q` is nonzero on `R`, `q'` vanishes on + `R` and `sigma' > 0`; +3. `delta = 0`, `e + rho = 6`, `q` and `q'` vanish on `R`, and + `sigma < 0 < sigma'`. + +Moreover `N(V) <= 64` when `e = 8`. + +*Proof.* If `V` lies in `E` then `N(V) = 0`. Otherwise use Theorem 1. + +`delta = 1`. By 2(b), `N(V) = 2^(e-2) - sigma/4`. If `e + rho = 10`, +then `sigma` is `0` or, by 2(c), `32`, so `N(V) <= 2^(e-2)`. Otherwise +`e + rho <= 8`, `|sigma| <= 16`, and `N(V) <= 2^(e-2) + 4` with equality +exactly in case 1. + +`delta = 0`. By 2(a), `e + rho <= 8`. If `e + rho = 8`, then `sigma` is +`0` or, by 2(c), `16`, while `sigma' <= 16`. So +`N(V) <= 2^(e-2) + 4`, with equality exactly when `sigma = 0` and +`sigma' = 16`, which is case 2. If `e + rho <= 6`, then +`|sigma|, |sigma'| <= 8` and `N(V) <= 2^(e-2) + 4`, with equality exactly +in case 3. + +`e = 8`. If `delta = 1`, then `rho >= 1`, `rho <= 2` by 2(a) and `rho` is +even, so `e + rho = 10` and `N(V) <= 64` by the first paragraph. If +`delta = 0`, then `rho = 0`, so `e + rho = 8` and `q` vanishes on +`R = 0`; by 2(c) `sigma = 16`, and `N(V) = 64 + (sigma' - 16)/4 <= 64`. ∎ + +## Corollary 4 (ports per dimension) + +Let `N_e(S)` be the largest number of elements of a port set `S` in a +subspace of dimension `e`. + +1. For every subset `S` of P120 and every `e`, + `N_e(S) <= min(2^(e-1), 2^(e-2) + 4)`, and `N_8(S) <= 64`. +2. `N_e(P120) = N_e(P104) = min(2^(e-1), 2^(e-2) + 4)` for `1 <= e <= 7`, + that is `1, 2, 4, 8, 12, 20, 36`. `N_8(P120) = 64` and + `N_9(P120) = 120`. + +*Proof.* A subspace not inside `E` has `2^(e-1)` odd vectors, which gives +the first term; Theorem 3 gives the second and the bound at `e = 8`. For +part 2, `CENSUS.json` lists one explicit basis for each `e = 1..7` whose +span contains the stated number of P104 ports; `verify.py` checks each by +direct enumeration. P104 is a subset of P120, so the same subspaces +attain the bound for P120. A hyperplane with 64 ports is found by the +census, and `N_9 = |P120| = 120`. ∎ + +## Why the bias is 4, and why the pattern stops at dimension 8 + +The bias `N(V) - 2^(e-2)` is `(s' - s) 2^(t-2)` with `t = (e + rho)/2`. +Theorem 2(a) caps `t` at `4 + delta`; the 4 is the Witt index of the form +that `q` induces on `F2^9/<1>`. At the cap, Theorem 2(c) gives +`sigma >= 0`: a subspace whose radical is as large as its dimension +allows has no negative character sum. Without 2(c) the estimates of +Theorem 1 alone would allow a bias of `+8`, from `sigma = -32` at +`t = 5` or from `sigma = -16, sigma' = 16` at `t = 4` with `delta = 0`. +With it the largest bias is `+4`. + +At `e = 8` every subspace not inside `E` has `e + rho = 8 + 2 delta`, +because `rho` is forced to `2 delta`. Every such subspace is in the +`sigma >= 0` regime, so the bias is at most `0` and `N_8 = 64 = 2^6` +rather than `68`. + +For `e <= 3` the bound `2^(e-2) + 4` exceeds the number `2^(e-1)` of odd +vectors, and at `e = 4` the two agree. Theorem 3 therefore also recovers +the saturation depth of PR #6861 Theorem 1: a saturated subspace of +dimension `e` needs `N(V) = 2^(e-1)`, which is impossible once +`2^(e-1) > 2^(e-2) + 4`, that is for `e >= 5`. + +## Exhaustive corroboration + +`verify.py` visits each of the 8,283,458 subspaces of `F2^9` once. For +the 7,866,259 that are not inside `E` it computes `N(V)`, `sigma`, +`sigma'` and `R` and requires every clause of Theorems 1 to 3. The +98 classes `(e, delta, rho, sign sigma, sign sigma', N)` and their sizes +are in `CENSUS.json`. This run is corroboration; the theorems do not +depend on it. Part 2 of Corollary 4 does depend on the seven explicit +witnesses and on one 64-port hyperplane, which are finite checks. diff --git a/research/p104-e8-port-count-closed-form/README.md b/research/p104-e8-port-count-closed-form/README.md new file mode 100644 index 0000000000..6c3ea60aec --- /dev/null +++ b/research/p104-e8-port-count-closed-form/README.md @@ -0,0 +1,151 @@ +# A closed form for E8 port counts in subspaces (no κ) + +**Scoped written proof with exhaustive finite corroboration. No new κ.** +This answers the first half of open question 1 of PR #6861 +(`research/p104-e8-subspace-invariants`, DreamingOfClouds): derive the +ports-per-dimension law `N_e = 2^(e-2) + 4` for `4 <= e <= 7` from the +radical of `B|V` and the restriction of `q` to `V`, and explain why it +stops at `e = 8`. Nothing is priced and no word is constructed. + +## Result + +Setting as in PR #6861: `F2^9`, `q(x) = C(wt x, 2) mod 2` with polar form +`B`, even hyperplane `E`, and P120 the odd vectors with `q = 1` (weights +3 and 7). `N(V)` is the number of ports in a subspace `V`. + +For a subspace `V` of dimension `e`, let `R` be the radical of `B|V`, +`rho = dim R`, `delta = 1` if the all-ones vector lies in `V` and `0` +otherwise, `q' = q + (wt mod 2)`, and let `sigma`, `sigma'` be the sums of +`(-1)^q` and `(-1)^q'` over `V`. + +1. **Closed form.** If `V` is not inside `E`, then + `N(V) = 2^(e-2) + (sigma' - sigma)/4`, where `sigma^2 = 2^(e+rho)` if + `q` vanishes on `R` and `0` otherwise, and the same for `sigma'` and + `q'`. So the bias `N(V) - 2^(e-2)` is `(s' - s) 2^((e+rho)/2 - 2)` with + `s, s'` in `{-1, 0, 1}`. +2. **Constraints.** `e + rho <= 8 + 2 delta`. If `delta = 1` then + `sigma' = 0`. If `e + rho = 8 + 2 delta` and `q` vanishes on `R`, then + `sigma = 2^(4 + delta) > 0`. +3. **Bound.** `N(V) <= 2^(e-2) + 4` for every subspace of every + dimension, with equality in exactly three listed radical classes, and + `N(V) <= 64` at `e = 8`. +4. **Ports per dimension.** For every subset `S` of P120, + `N_e(S) <= min(2^(e-1), 2^(e-2) + 4)`. For P120 and for P104 this is + attained at every `e = 1..7`: + + | e | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | + |---|---|---|---|---|---|---|---|---|---| + | `min(2^(e-1), 2^(e-2)+4)` | 1 | 2 | 4 | 8 | 12 | 20 | 36 | | | + | `N_e(P120)` | 1 | 2 | 4 | 8 | 12 | 20 | 36 | 64 | 120 | + +The pattern stops at `e = 8` because there `rho = 2 delta` is forced, so +every subspace is at the cap of item 2 and has `sigma >= 0`; the bias is +then at most `0`. Item 3 also recovers the saturation depth of PR #6861 +Theorem 1, since a saturated subspace needs `N(V) = 2^(e-1)`. + +Statements and proofs are in [PROOF.md](PROOF.md). The proofs use two +identities, `B(x,y) = x . (y + (wt y mod 2) 1)` and +`sum over F2^9 of (-1)^q = 32`, and no enumeration. Attainment in item 4 +uses seven explicit bases and is a finite check. + +## Census + +`verify.py` visits all 8,283,458 subspaces of `F2^9`. Of these 417,199 +lie inside `E` and have no port. The other 7,866,259 fall into 98 classes +`(e, delta, rho, sign sigma, sign sigma', N)`, listed with their sizes in +[CENSUS.json](CENSUS.json). Subspaces attaining `2^(e-2) + 4`, by the +equality case of Theorem 3: + +| e | case 1 (`delta=1`, `e+rho=8`) | case 2 (`delta=0`, `e+rho=8`) | case 3 (`delta=0`, `e+rho=6`) | total | +|---|---:|---:|---:|---:| +| 4 | 0 | 2,025 | 9,450 | 11,475 | +| 5 | 3,150 | 28,350 | 75,600 | 107,100 | +| 6 | 7,560 | 37,800 | 40,320 | 85,680 | +| 7 | 1,120 | 4,320 | 0 | 5,440 | + +At `e = 8`, 255 hyperplanes hold 64 ports. For `e = 1..4` the maximizers +are the saturated subspaces, and their counts 120, 7,140, 32,130 and +11,475 agree with the P120 row of PR #6861 Theorem 1. The `N_e(P120)` +row above agrees with PR #6861 Theorem 2. + +## Reproduce + +From the repository root, with CPython 3.12 (standard library only): + +```sh +/path/to/python3.12 -I -B -W error research/p104-e8-port-count-closed-form/verify.py +/path/to/python3.12 -B scripts/research_package.py --package research/p104-e8-port-count-closed-form +``` + +Expected last line: `PASS_P104_E8_PORT_COUNT_CLOSED_FORM`. One run takes +about 20 seconds. The verifier + +- checks the form facts and both identities on all 512 by 512 pairs; +- computes `N`, `sigma`, `sigma'` and `R` for every subspace and requires + each clause of Theorems 1 to 3; +- recomputes the same invariants from first principles, with no masks and + no use of the identity `B(x,y) = x . tau(y)`, on 3,094 subspaces: all + those of dimension 0, 1, 8 and 9 and a fixed-stride sample of the rest; +- requires the class census to equal `CENSUS.json`, and the equality + classification of Theorem 3 on every class; +- checks the seven P104 witnesses by direct enumeration; +- runs five rejecting controls: a wrong port count, a wrong radical, a + negative sign at the radical cap, a mutated census row, and a witness + with one of its ports removed from P104. + +`verify.py --write-census PATH` regenerates `CENSUS.json`. + +## Scope and limits + +- This is a statement about port sets. It supplies no word, helper + split, invoice or supplier, and the selected frontier is unchanged. +- The signs `s, s'` are determined by `V` but are not expressed here + through `rho` alone. They are the types of the nondegenerate forms that + `q` and `q'` induce on `V/R`; only the constraint at the cap (item 2) + is proved and used. +- For P104 the proof gives `N_8 <= 64`. The exact value 60 is PR #6861's + exhaustive result and is not derived here. +- The flag-rectangle masses, the second half of the same open question, + and the star law are not addressed. +- The 5561 port list is read from + `research/p104-designer-toolkit-v2/words/5561.json.gz`, pinned in + [SOURCES.json](SOURCES.json). It is used only for the seven witnesses. +- `verify.py` is iterative, with a node budget equal to the exact number + of subspaces of dimension at most 4. Its work stack peaks at 953 + frames of at most 16 elements each. Functions stay below 60 lines. + Python-managed allocation is bounded by those sizes. No separate + static type check was run. + +## Open next questions + +1. **Flag masses.** Does the class table give the flag-rectangle maxima + of PR #6861 Theorem 4 (32 at every level, 36 at level 5) in closed + form? The product `N(g) N(A^perp)` couples the class of `g` with that + of `A^perp`. A first step is to express the radical of `A^perp` + through `A` with `B(x,y) = x . tau(y)` and list which class pairs can + occur for a hyperplane `g` of `A`. The joint constraint is not derived + here. +2. **Star law.** The same question for `max N(V) N(V^perp)`, which + PR #6861 Theorem 3 finds equal to the port degree. The classes of `V` + and `V^perp` are linked by the same identity. +3. **P104 at dimension 8.** PR #6861 finds `N_8(P104) = 60`, so each + of the 255 hyperplanes with 64 ports of P120 loses at least four ports + in P104. Which property of the 16 removed ports forces that? Start by + splitting the 255 hyperplanes into their two classes (135 with + `delta = 0`, 120 with `delta = 1`) and counting removed ports in each. +4. **Other E8-type port sets.** The proof uses only the form, so the + bound holds for every subset of P120. For which punctures is it still + attained at every `e <= 7`? This is the witness side of PR #6861's + question 3. + +[TASK.json](TASK.json) gives the structured questions and scope change. + +## Credit + +This package was produced by Nick Petalas. The setting, the port sets, +the quadratic form `q`, the exhaustive `N_e` tables, the saturation +theorem and the open question answered here are from DreamingOfClouds, +PR #6861. The 5561 port list is from `research/p104-designer-toolkit-v2`. +New here: the closed form for `N(V)`, the constraints at the radical cap, +the bound `2^(e-2) + 4` with its equality classes, and the class census. +New work is Apache-2.0. diff --git a/research/p104-e8-port-count-closed-form/SOURCES.json b/research/p104-e8-port-count-closed-form/SOURCES.json new file mode 100644 index 0000000000..e1672e8c83 --- /dev/null +++ b/research/p104-e8-port-count-closed-form/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-designer-toolkit-v2/words/5561.json.gz", + "usage": "input", + "git_blob": "c367d865a154ffd2ae0b6f6053469580a139f487", + "sha256": "b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44" + }, + { + "path": "research/p104-e8-subspace-invariants/README.md", + "usage": "provenance", + "git_blob": "88f5a8c3aef552524ddfbe71b209d499ed12c843", + "sha256": "c99d0ee18debc63a6418b7a11ae93ef590543a0f73fa50d4087445c123c2c62a" + } + ] +} diff --git a/research/p104-e8-port-count-closed-form/TASK.json b/research/p104-e8-port-count-closed-form/TASK.json new file mode 100644 index 0000000000..2bf3484efd --- /dev/null +++ b/research/p104-e8-port-count-closed-form/TASK.json @@ -0,0 +1,145 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a closed form for the number of E8 ports (P120, and every subset such as P104) in a subspace V of F2^9: N(V) = 2^(e-2) + (sigma' - sigma)/4 with both character sums fixed up to sign by the radical of B|V; prove N(V) <= 2^(e-2) + 4 with its three equality classes and N(V) <= 64 at dimension 8; conclude N_e = min(2^(e-1), 2^(e-2)+4) for e = 1..7 on P120 and P104.", + "scope_change_reason": "The card asks for a helper-basis and causal-split construction on the complete invoice. This package takes open question 1 of PR #6861 instead, a statement about port sets only: it turns that package's exhaustive ports-per-dimension table into a written theorem. It constructs no word and prices nothing.", + "bottleneck_link": "A side result for the P104 complex helper track: the bound limits how many ports one subspace-shaped carrier can hold at each dimension, for every E8-type port set. No supplier, invoice or framework assumption changes.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original improvement: the ports-per-dimension law. Leave the flag masses and the star law open.", + "outcome": "completed", + "evidence": "PROOF.md (Theorems 1-3 and Corollary 4, written proofs); verify.py (all 8,283,458 subspaces of F2^9, every clause required on the 7,866,259 not inside the even hyperplane; first-principles recomputation on 3,094 subspaces; seven P104 witnesses; five rejecting controls); CENSUS.json (98 classes with sizes).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Do the flag-rectangle maxima of PR #6861 Theorem 4 (32 at every level, 36 at level 5) follow in closed form from the class table?", + "why_it_matters": "It is the second half of PR #6861's open question 1 and would make the flag bound valid for every E8-type port set.", + "first_step": "Express the radical of A^perp through A with B(x,y) = x.tau(y) and list which class pairs can occur for a hyperplane g of A.", + "blocked_by": "The joint constraint between the class of g and the class of A^perp is not derived." + }, + { + "question": "Does the star law max N(V) N(V^perp) = port degree of PR #6861 Theorem 3 follow from the same classes?", + "why_it_matters": "It bounds subspace bicliques of the orthogonality graph without enumeration.", + "first_step": "Relate the class of V^perp to that of V with the identity B(x,y) = x.tau(y), then maximise the product over compatible pairs.", + "blocked_by": "The class of the dot-orthogonal space is not determined here from the class of V." + }, + { + "question": "Which property of the 16 ports removed from P120 forces N_8(P104) = 60 rather than the proved bound 64?", + "why_it_matters": "It is the only dimension where P104 and P120 differ, and the proof here does not see it.", + "first_step": "Split the 255 hyperplanes with 64 ports into their two classes (135 with delta = 0, 120 with delta = 1) and count removed ports in each.", + "blocked_by": "No structural description of the removed 16 ports is used in this package." + }, + { + "question": "For which punctures of P120 is the bound min(2^(e-1), 2^(e-2)+4) still attained at every e <= 7?", + "why_it_matters": "The upper bound holds for every subset; attainment decides whether P104 is typical, which is PR #6861's question 3.", + "first_step": "For one puncture family, count the maximizers of each equality class that avoid the removed ports, using the maximizer counts in CENSUS.json as the total.", + "blocked_by": "A puncture family has to be chosen and its removed ports listed." + } + ], + "predecessor": { + "pr": 6861, + "package": "research/p104-e8-subspace-invariants", + "question": "README Open next question 1, first half", + "author": "DreamingOfClouds" + }, + "local_environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit" + } +} diff --git a/research/p104-e8-port-count-closed-form/VERIFY.json b/research/p104-e8-port-count-closed-form/VERIFY.json new file mode 100644 index 0000000000..78870bb705 --- /dev/null +++ b/research/p104-e8-port-count-closed-form/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-designer-toolkit-v2/words/5561.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Form facts and both identities; every clause of Theorems 1-3 on all subspaces of F2^9 not inside the even hyperplane; first-principles recomputation on a fixed sample; class census equal to CENSUS.json; equality classification; seven P104 witnesses; five rejecting controls." + } + ] +} diff --git a/research/p104-e8-port-count-closed-form/verify.py b/research/p104-e8-port-count-closed-form/verify.py new file mode 100644 index 0000000000..86f94a2283 --- /dev/null +++ b/research/p104-e8-port-count-closed-form/verify.py @@ -0,0 +1,325 @@ +#!/usr/bin/env python3 +"""Exhaustive corroboration of the closed form for E8 port counts. + +Python 3.12, standard library only. Run from the repository root: + + python3.12 -I -B -W error research/p104-e8-port-count-closed-form/verify.py + +Marker: PASS_P104_E8_PORT_COUNT_CLOSED_FORM + +Every subspace of F2^9 is visited once: X in reduced echelon form with +dim X <= 4, and its dot-product orthogonal V = X^perp of dimension >= 5. +For each one the port count, both character sums and the radical of the +polar form are computed from their definitions, and the clauses of +Theorems 1-3 of PROOF.md are required. The resulting class census must +equal CENSUS.json. `--write-census PATH` regenerates that file. +""" +import gzip +import json +import sys +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PORTS_FILE = HERE.parent / "p104-designer-toolkit-v2" / "words" / "5561.json.gz" +CENSUS_FILE = HERE / "CENSUS.json" +MARKER = "PASS_P104_E8_PORT_COUNT_CLOSED_FORM" +SIZE = 512 +ONE = SIZE - 1 +MAX_SMALL_DIM = 4 +NODE_BUDGET = 4_141_729 # subspaces of F2^9 of dimension 0..4 +SAMPLE_STRIDE = 4001 + +WT = [bin(x).count("1") for x in range(SIZE)] +PAR = [w & 1 for w in WT] +Q = [(w * (w - 1) // 2) & 1 for w in WT] +QP = [Q[x] ^ PAR[x] for x in range(SIZE)] +TAU = [x ^ (ONE if PAR[x] else 0) for x in range(SIZE)] +SQ = [1 - 2 * v for v in Q] +SQP = [1 - 2 * v for v in QP] +PORT = [PAR[x] & Q[x] for x in range(SIZE)] +P120 = [x for x in range(SIZE) if PORT[x]] + + +def require(ok, msg): + if not ok: + raise ValueError(msg) + + +def mask_of(vectors): + return sum(1 << x for x in vectors) + + +M120 = mask_of(P120) +MQ = mask_of(x for x in range(SIZE) if Q[x]) +MQP = mask_of(x for x in range(SIZE) if QP[x]) +MODD = mask_of(x for x in range(SIZE) if PAR[x]) +PERP = [mask_of(x for x in range(SIZE) if not WT[x & y] & 1) for y in range(SIZE)] + + +def polar(x, y): + return (WT[x] * WT[y] + WT[x & y]) & 1 + + +def check_form_facts(): + """The setting of PR 6861 plus the two identities the proof uses.""" + pairs = [(x, y) for x in range(SIZE) for y in range(SIZE)] + require(all(Q[x ^ y] == Q[x] ^ Q[y] ^ polar(x, y) for x, y in pairs), "q polarises to B") + require(all(polar(x, y) == WT[x & TAU[y]] & 1 for x, y in pairs), "B(x,y) = x.tau(y)") + radical = [x for x in range(SIZE) if all(polar(x, y) == 0 for y in range(SIZE))] + require(radical == [0, ONE] and Q[ONE] == 0 and PAR[ONE] == 1, "radical is <1>, q(1)=0, 1 odd") + require(all(TAU[x ^ y] == TAU[x] ^ TAU[y] for x, y in pairs), "tau is linear") + require([x for x in range(SIZE) if TAU[x] == 0] == [0, ONE], "kernel of tau is <1>") + require(len(P120) == 120 and all(WT[x] in (3, 7) for x in P120), "P120 is weight 3 or 7") + require(sum(SQ) == 32, "sum of (-1)^q over F2^9 is 32") + + +def sign(value): + return (value > 0) - (value < 0) + + +def clauses(e, delta, radical, sig, sigp, ports): + """Require Theorems 1-3 for one subspace not inside E; return its class.""" + rho = len(radical).bit_length() - 1 + require(len(radical) == 1 << rho, "radical size is a power of two") + a = int(all(Q[y] == 0 for y in radical)) + ap = int(all(QP[y] == 0 for y in radical)) + total = e + rho + require(total % 2 == 0 and total <= 8 + 2 * delta, "Theorem 2(a)") + require(sig * sig == a << total and sigp * sigp == ap << total, "Theorem 1 squares") + require(not (delta and ap), "Theorem 2(b)") + require(not (total == 8 + 2 * delta and a) or sig == 1 << (4 + delta), "Theorem 2(c)") + require(4 * ports == (1 << e) + sigp - sig, "Theorem 1 count") + require(4 * ports <= (1 << e) + 16 and 2 * ports <= 1 << e, "Theorem 3 bound") + require(e != 8 or ports <= 64, "Theorem 3 at dimension 8") + return (e, delta, rho, sign(sig), sign(sigp), ports) + + +def small_record(k, elems, vmask): + """Invariants of X (dimension k) from its element list; None inside E.""" + if not any(PAR[x] for x in elems): + return None + radical = [y for y in elems if (vmask >> TAU[y]) & 1] + sig = sum(SQ[x] for x in elems) + sigp = sum(SQP[x] for x in elems) + ports = sum(PORT[x] for x in elems) + return (k, int(ONE in elems), radical, sig, sigp, ports) + + +def dual_record(k, elems, vmask): + """Invariants of V = X^perp (dimension 9-k) from its mask; None inside E.""" + if not vmask & MODD: + return None + radical = [] + for z in elems: + if PAR[z]: + continue + if (vmask >> z) & 1: + radical.append(z) + if (vmask >> (z ^ ONE)) & 1: + radical.append(z ^ ONE) + size = 1 << (9 - k) + sig = size - 2 * (vmask & MQ).bit_count() + sigp = size - 2 * (vmask & MQP).bit_count() + return (9 - k, (vmask >> ONE) & 1, radical, sig, sigp, (vmask & M120).bit_count()) + + +def children(minp, pivmask): + """Echelon rows that extend a basis whose smallest pivot is minp.""" + rows = [] + for p in range(minp): + cands = [1 << p] + for c in range(p + 1, 9): + if not (pivmask >> c) & 1: + cands += [v | (1 << c) for v in cands] + rows.append((p, cands)) + return rows + + +def basis_of(vectors): + """Greedy basis of the span of at most 512 vectors.""" + basis, span = [], {0} + for v in vectors[:SIZE]: + if v not in span: + basis.append(v) + span |= {v ^ s for s in span} + return basis, span + + +def direct_record(vectors): + """The same invariants from first principles, without masks or tau.""" + basis, span = basis_of(vectors) + require(span == set(vectors), "vectors form a subspace") + if all(WT[x] % 2 == 0 for x in vectors): + return None + radical = sorted(y for y in vectors if all(polar(y, b) == 0 for b in basis)) + sig = sum(1 if (WT[x] * (WT[x] - 1) // 2) % 2 == 0 else -1 for x in vectors) + sigp = sum(1 if (WT[x] * (WT[x] + 1) // 2) % 2 == 0 else -1 for x in vectors) + ports = sum(1 for x in vectors if WT[x] in (3, 7)) + return (len(basis), int(ONE in span), radical, sig, sigp, ports) + + +def cross_check(record, vectors): + direct = direct_record(vectors) + if record is None or direct is None: + require(record is None and direct is None, "even-hyperplane test agrees") + return + fast = record[:2] + (sorted(record[2]),) + record[3:] + require(fast == direct, "mask invariants equal first-principles invariants") + + +def elements_of(mask): + return [x for x in range(SIZE) if (mask >> x) & 1] + + +def census(m104): + """Visit all 8,283,458 subspaces; return classes, node counts, witnesses.""" + classes, nodes, even, sampled = Counter(), [0] * (MAX_SMALL_DIM + 1), 0, 0 + witnesses = {} + stack = [(0, 9, 0, [0], (1 << SIZE) - 1)] + visited = 0 + while stack: + k, minp, pivmask, elems, vmask = stack.pop() + visited += 1 + require(visited <= NODE_BUDGET, "node budget exceeded") + nodes[k] += 1 + small, dual = small_record(k, elems, vmask), dual_record(k, elems, vmask) + if k <= 1 or visited % SAMPLE_STRIDE == 0: + cross_check(small, elems) + cross_check(dual, elements_of(vmask)) + sampled += 2 + for record, mask in ((small, None), (dual, vmask)): + if record is None: + even += 1 + continue + key = clauses(*record) + classes[key] += 1 + e = key[0] + if e <= 7 and e not in witnesses and 4 * key[5] == min(2 << e, (1 << e) + 16): + own = mask_of(elems) if mask is None else mask + if (own & m104).bit_count() == key[5]: + witnesses[e] = basis_of(elements_of(own))[0] + if k < MAX_SMALL_DIM: + for p, cands in children(minp, pivmask): + grown = pivmask | (1 << p) + for b in cands: + stack.append((k + 1, p, grown, elems + [x ^ b for x in elems], vmask & PERP[b])) + return classes, nodes, even, sampled, witnesses + + +def summarize(classes, nodes, even, witnesses): + rows = [ + {"dimension": e, "contains_all_ones": d, "radical_dimension": r, "sign_sigma": s, + "sign_sigma_prime": sp, "ports": n, "subspaces": count} + for (e, d, r, s, sp, n), count in sorted(classes.items()) + ] + best = {e: max(row["ports"] for row in rows if row["dimension"] == e) for e in range(1, 10)} + attaining = { + e: sum(row["subspaces"] for row in rows if row["dimension"] == e and row["ports"] == best[e]) + for e in range(1, 10) + } + return { + "schema_version": 1, + "subspaces_total": 2 * sum(nodes), + "subspaces_inside_even_hyperplane": even, + "small_subspaces_by_dimension": nodes, + "classes": rows, + "max_ports_by_dimension": {str(e): best[e] for e in best}, + "maximizers_by_dimension": {str(e): attaining[e] for e in attaining}, + "p104_witness_bases": {str(e): witnesses[e] for e in sorted(witnesses)}, + } + + +def check_summary(doc): + """Statements of Theorem 3 and Corollary 4 read off the census.""" + require(doc["small_subspaces_by_dimension"] == [1, 511, 43435, 788035, 3309747], "Gaussian binomials") + require(doc["subspaces_total"] == 8_283_458 and doc["subspaces_inside_even_hyperplane"] == 417_199, "totals") + counted = sum(row["subspaces"] for row in doc["classes"]) + require(counted + doc["subspaces_inside_even_hyperplane"] == doc["subspaces_total"], "census is complete") + best = [doc["max_ports_by_dimension"][str(e)] for e in range(1, 10)] + require(best == [1, 2, 4, 8, 12, 20, 36, 64, 120], "N_e table") + require(all(best[e - 1] == min(1 << (e - 1), (1 << (e - 2)) + 4) for e in range(2, 8)), "closed form") + for row in doc["classes"]: + e, total = row["dimension"], row["dimension"] + row["radical_dimension"] + s, sp, d = row["sign_sigma"], row["sign_sigma_prime"], row["contains_all_ones"] + require(4 * row["ports"] == (1 << e) + (sp - s) * (1 << (total // 2)), "class formula") + equality = ( + (d == 1 and total == 8 and s == -1) + or (d == 0 and total == 8 and s == 0 and sp == 1) + or (d == 0 and total == 6 and s == -1 and sp == 1) + ) + require(equality == (4 * row["ports"] == (1 << e) + 16), "equality classification") + + +def span_of(basis): + span = [0] + for b in basis[:9]: + span += [x ^ b for x in span] + return span + + +def check_witnesses(doc, p104): + """One explicit subspace per dimension 1..7 attains the bound inside P104.""" + ports = set(p104) + for e in range(1, 8): + basis = doc["p104_witness_bases"][str(e)] + span = span_of(basis) + require(len(basis) == e and len(set(span)) == 1 << e, "witness has dimension e") + target = min(1 << (e - 1), (1 << (e - 2)) + 4) if e > 1 else 1 + require(sum(1 for x in span if x in ports) == target, "witness attains the bound in P104") + require(sum(PORT[x] for x in span) == target, "witness attains the bound in P120") + + +def expect_failure(action, label): + try: + action() + except ValueError: + return + raise ValueError("control did not reject: " + label) + + +def run_controls(doc, p104): + radical = [0, ONE] + require(clauses(9, 1, radical, 32, 0, 120) == (9, 1, 1, 1, 0, 120), "whole space is accepted") + expect_failure(lambda: clauses(9, 1, radical, 32, 0, 121), "wrong port count") + expect_failure(lambda: clauses(9, 1, [0], 32, 0, 120), "wrong radical") + expect_failure(lambda: clauses(9, 1, radical, -32, 0, 136), "negative sign at full radical") + mutated = json.loads(json.dumps(doc)) + mutated["classes"][0]["ports"] += 1 + expect_failure(lambda: check_summary(mutated), "mutated class row") + basis = doc["p104_witness_bases"]["7"] + dropped = next(x for x in span_of(basis) if x in set(p104)) + expect_failure(lambda: check_witnesses(doc, [x for x in p104 if x != dropped]), "port removed from witness") + + +def load_p104(): + with gzip.open(PORTS_FILE) as handle: + p104 = json.load(handle)["ports"] + require(len(p104) == 104 and len(set(p104)) == 104 and set(p104) <= set(P120), "P104 inside P120") + return p104 + + +def main(argv): + require(len(argv) in (1, 3) and (len(argv) == 1 or argv[1] == "--write-census"), "usage") + check_form_facts() + p104 = load_p104() + classes, nodes, even, sampled, witnesses = census(mask_of(p104)) + doc = summarize(classes, nodes, even, witnesses) + check_summary(doc) + check_witnesses(doc, p104) + run_controls(doc, p104) + if len(argv) == 3: + Path(argv[2]).write_text(json.dumps(doc, indent=1) + "\n") + print("WROTE", argv[2]) + return 0 + require(json.loads(CENSUS_FILE.read_text()) == doc, "census equals CENSUS.json") + print(json.dumps({"subspaces": doc["subspaces_total"], "classes": len(doc["classes"]), + "first_principles_samples": sampled, + "max_ports": doc["max_ports_by_dimension"], + "maximizers": doc["maximizers_by_dimension"]}, sort_keys=True)) + print(MARKER) + return 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv))