Prove weighted E8 query limits and low-redundancy obstructions

research/e8-hyperplane-minrank/README.md

@@ -0,0 +1,65 @@
+# A thirteen-line certificate for the E8 hyperplane floor
+
+For every proper real linear hyperplane H in the eight-dimensional E8
+root space, every binary fitting matrix on the root lines outside H has
+rank at least nine. The fitting convention is diagonal one and entry
+zero for each distinct pair with nonzero real inner product. Entries on
+orthogonal pairs are free. Symmetry is not assumed. This floor is prior work: [PR #3045](https://github.com/CrocSwap/integer-mult-bounds/pull/3045)
+proves the stronger mixed-normal statement in
+[Theorem 6 at its pinned source](https://github.com/CrocSwap/integer-mult-bounds/blob/16feea078f5542964ae85ca1b1f35bb94314ae78/research/nondense-pairing-square-floors/README.md).
+Set its two real normals equal. This annex supplies compact explicit
+thirteen-line certificates and a separate Schur-complement proof for that
+established slice, with no SAT solver in the replay. It claims no new
+floor, comparison of verification speed, circuit or kappa gain.
+
+The [proof](historical/work/p518-next/bit/weighted/rank9/parabolic/PROOF.md)
+uses a thirteen-line certificate in each of eight maximal parabolic
+complements. Eight anchors have identity fitting block. Five witnesses
+encode five edges on four anchor indices. A rank-eight Schur factorization
+would orient each edge toward its unique nonzero binary product. Incident
+edges cannot share an endpoint, which is impossible for five edges on four
+vertices. The Weyl-chamber argument then covers every real hyperplane.
+
+The later [dense-table rigidity theorem](https://github.com/CrocSwap/integer-mult-bounds/blob/cef4b52f2a59009865bf8eabde1be3f159063703/research/decoder-floors-frontier-format/README.md)
+and [tensor copy-floor theorem](https://github.com/CrocSwap/integer-mult-bounds/blob/cef4b52f2a59009865bf8eabde1be3f159063703/research/tensor-e8-copy-floor/README.md)
+cover the earlier full-E8 rank-nine support and minimum-nine-term cost
+consequences. Those consequences are not new claims here. This annex
+preserves an alternative proof of the induced-complement theorem: its matrix need only
+fit the lines outside H and need not extend to a rank-nine full-E8 matrix.
+The other new E8 small-redundancy package fixes the canonical full matrix;
+it does not prove this arbitrary fitting statement on each complement.
+
+From this package directory, with Python 3.10 or later:
+
+```sh
+python3 -B verify.py --build /tmp/e8-hyperplane-minrank-replay
+```
+
+The output path must not exist. Only the standard library is required.
+The final line must be:
+
+```text
+PASS_E8_HYPERPLANE_MINRANK 240 8 13
+```
+
+The independent checker constructs all 240 signed roots, checks the simple
+basis, integral positive/negative root coordinates and simple reflections,
+and verifies all eight thirteen-line certificates by integer arithmetic.
+It compares the complete result with the saved receipt. The wrapper rejects
+optimized Python and runs the child with Python environment options ignored.
+No search runs. The written Weyl-chamber and Schur-complement arguments are
+necessary proof steps; the finite replay alone does not prove the theorem.
+
+`SOURCE-MANIFEST.json` binds the unchanged proof, certificate and checker.
+`replayed-receipt.json` and `replay.log` record the fresh cleanup replay.
+The standalone proof uses the standard E8 root system and the existing
+local 13-line fitting certificate. The original local proof and checks were
+prepared with substantial OpenAI Codex and research-agent assistance under
+the user's direction. No independent human review is claimed.
+
+## Open next questions
+
+Can an induced E8 set with no such thirteen-line certificate have binary
+fitting rank below nine? A first step is to compare a specified removed set
+with the eight stored certificates. This package makes no assertion about
+arbitrary punctures, larger fields, or a physical construction.

research/e8-hyperplane-minrank/SOURCE-MANIFEST.json

@@ -0,0 +1,29 @@
+{
+  "main_pin": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "files": [
+    {
+      "original": "work/p518-next/bit/weighted/rank9/quick.json",
+      "package": "historical/work/p518-next/bit/weighted/rank9/quick.json",
+      "sha256": "621cc49f29bf382cbca0cc49f3a9091173de683c52357efdc264f55c1c105256",
+      "bytes": 15906
+    },
+    {
+      "original": "work/p518-next/bit/weighted/rank9/parabolic/PROOF.md",
+      "package": "historical/work/p518-next/bit/weighted/rank9/parabolic/PROOF.md",
+      "sha256": "c4f7fbe4851d52e4f7daf6389e2b2b0ad758bb9a9cf5be60a70df3234b2ecb67",
+      "bytes": 4259
+    },
+    {
+      "original": "work/p518-next/bit/weighted/rank9/parabolic/independent_check.py",
+      "package": "historical/work/p518-next/bit/weighted/rank9/parabolic/independent_check.py",
+      "sha256": "8c41c12c044ab5bc515a1f6f1dc44dce6550ff3051f77262942873f5e5bb5f45",
+      "bytes": 4072
+    },
+    {
+      "original": "work/p518-next/bit/weighted/rank9/parabolic/INDEPENDENT.json",
+      "package": "historical/work/p518-next/bit/weighted/rank9/parabolic/INDEPENDENT.json",
+      "sha256": "b80c137491fe45c4e7c8a28987581047fb05ca139685d14c094e43f23b6fc1e7",
+      "bytes": 1599
+    }
+  ]
+}

research/e8-hyperplane-minrank/VALIDATION.json

@@ -0,0 +1,18 @@
+{
+  "cwd": "/Users/aliromman/Projects/IntegerMultiplicationBounds",
+  "command": [
+    "python3",
+    "-E",
+    "-B",
+    "work/project-final-cleanup-20261022/early-projects-audit/packages/e8-hyperplane-minrank/verify.py",
+    "--build",
+    "/tmp/e8-hyperplane-cleanup-20261023"
+  ],
+  "exit_code": 0,
+  "fresh_output_required": true,
+  "log": "replay.log",
+  "log_sha256": "b2e9cbe5c104028fd32942d900443b30debcf7dbd7bd8b7e05ea14400429b376",
+  "receipt": "replayed-receipt.json",
+  "receipt_sha256": "b80c137491fe45c4e7c8a28987581047fb05ca139685d14c094e43f23b6fc1e7",
+  "note": "Literal output is retained. Original source files are unchanged. No new discovery search ran."
+}

research/e8-hyperplane-minrank/historical/work/p518-next/bit/weighted/rank9/parabolic/INDEPENDENT.json

@@ -0,0 +1,66 @@
+{
+  "status": "PASS",
+  "input_sha256": "621cc49f29bf382cbca0cc49f3a9091173de683c52357efdc264f55c1c105256",
+  "integer_root_count": 240,
+  "simple_basis_and_reflection_checks": true,
+  "all_eight_certificates_checked": true,
+  "parabolics": [
+    {
+      "node": 1,
+      "type": "D7",
+      "root_lines_inside": 42,
+      "certificate_lines": 13,
+      "incident_zero_constraints": 8
+    },
+    {
+      "node": 2,
+      "type": "A7",
+      "root_lines_inside": 28,
+      "certificate_lines": 13,
+      "incident_zero_constraints": 8
+    },
+    {
+      "node": 3,
+      "type": "A6+A1",
+      "root_lines_inside": 22,
+      "certificate_lines": 13,
+      "incident_zero_constraints": 8
+    },
+    {
+      "node": 4,
+      "type": "A4+A2+A1",
+      "root_lines_inside": 14,
+      "certificate_lines": 13,
+      "incident_zero_constraints": 8
+    },
+    {
+      "node": 5,
+      "type": "A4+A3",
+      "root_lines_inside": 16,
+      "certificate_lines": 13,
+      "incident_zero_constraints": 8
+    },
+    {
+      "node": 6,
+      "type": "D5+A2",
+      "root_lines_inside": 23,
+      "certificate_lines": 13,
+      "incident_zero_constraints": 8
+    },
+    {
+      "node": 7,
+      "type": "E6+A1",
+      "root_lines_inside": 37,
+      "certificate_lines": 13,
+      "incident_zero_constraints": 8
+    },
+    {
+      "node": 8,
+      "type": "E7",
+      "root_lines_inside": 63,
+      "certificate_lines": 13,
+      "incident_zero_constraints": 8
+    }
+  ],
+  "scope": "Finite certificates and simple roots. The universal theorem also uses the Weyl chamber and fitting rank arguments in PROOF.md."
+}

research/e8-hyperplane-minrank/historical/work/p518-next/bit/weighted/rank9/parabolic/PROOF.md

@@ -0,0 +1,91 @@
+# A rank-nine obstruction after each hyperplane removal
+
+Let R be the 120 E8 root lines. A binary fitting matrix F has F(r,r)=1.
+For distinct roots r,s with r dot s nonzero, it has F(r,s)=0. Entries for
+orthogonal roots are free. The matrix need not be symmetric.
+
+For every linear hyperplane H through the origin, the fitting matrices
+on R outside H have binary rank at least nine. The finite part of this
+statement uses eight certificates in `../quick.json`. Each certificate
+has thirteen root lines. `independent_check.py` checks each certificate
+with integer arithmetic. It also checks the simple-root basis and the
+root counts. `INDEPENDENT.json` records the result and the input hash.
+
+## The thirteen-root certificate
+
+The first eight roots are pairwise nonorthogonal anchors. Their fitting
+block is the identity I8. Each of the five other roots is a witness for a
+distinct pair of anchors. It is orthogonal to exactly those two anchors.
+The five pairs use only four anchor indices. Witnesses for incident pairs
+are nonorthogonal.
+
+Suppose the fitting matrix on these thirteen roots has rank at most eight.
+Write it in block form as [[I8,B],[C,D]]. The Schur complement gives D=CB.
+For the witness for e={i,j}, its column in B and its row in C have support
+contained in {i,j}. Its diagonal entry gives
+
+    C[e,i] B[i,e] + C[e,j] B[j,e] = 1.
+
+Over F2, exactly one product is one. Assign the pair to that endpoint.
+If two incident pairs e,f are assigned to their common endpoint i, then
+
+    (CB)[e,f] = C[e,i] B[i,f] = 1.
+
+Their witnesses are nonorthogonal, so D[e,f] must be zero. This is a
+contradiction. Each of the four endpoints can receive at most one pair.
+There are five pairs. Thus the fitting rank is at least nine.
+
+## The eight maximal parabolic subsystems
+
+Use the simple roots in `../quick.json`. Their Dynkin edges are
+1-3, 2-4, 3-4, 4-5, 5-6, 6-7, and 7-8. All roots are scaled by two.
+Delete one simple root at a time. The types and root-line counts are:
+
+| Deleted node | Type | Root lines |
+| --- | --- | ---: |
+| 1 | D7 | 42 |
+| 2 | A7 | 28 |
+| 3 | A6+A1 | 22 |
+| 4 | A4+A2+A1 | 14 |
+| 5 | A4+A3 | 16 |
+| 6 | D5+A2 | 23 |
+| 7 | E6+A1 | 37 |
+| 8 | E7 | 63 |
+
+For each row, its certificate has all thirteen roots outside the span of
+the retained seven simple roots. The normal in the input is orthogonal
+to those seven roots and has nonzero inner product with the deleted root.
+Thus each of the eight complements has fitting rank at least nine.
+
+## All hyperplanes
+
+Write H=v-perp, where v is nonzero. A Weyl transformation puts v in the
+closed dominant chamber. In that chamber each simple-root inner product
+is nonnegative. A positive root is a sum of simple roots with nonnegative
+integer coefficients. Its inner product with v is zero exactly when each
+simple root in its support has zero inner product with v.
+
+Thus the roots in H form a standard parabolic subsystem after that Weyl
+transformation. Since v is nonzero and the simple roots span the ambient
+space, at least one simple-root inner product is positive. Delete such a
+node. The roots in H lie in the rank-seven subsystem for that deletion.
+The complement of H therefore contains the complement of that subsystem.
+Fitting rank cannot decrease when more vertices are present, since the
+smaller fitting matrix is a principal submatrix. Weyl transformations
+preserve orthogonality. The eight finite certificates now give the claim.
+This argument also applies to real hyperplanes.
+
+## Consequence for rank-nine fitting matrices
+
+Let F be a fitting matrix on all 120 roots, with binary rank nine. For a
+proper hyperplane H, let O be the indices outside H. The principal matrix
+F[O,O] has rank at least nine, and hence exactly nine. The rows F[O,*]
+therefore span the complete row space of F. The columns F[*,O] span the
+complete column space.
+
+If a column-space vector Fu has support in H, then F[O,*]u=0. Since those
+rows span all rows, Fu=0. Apply the transpose argument to the row space.
+Consequently, every nonzero vector in either space has support with
+rational span dimension eight. In particular, a rank-nine factorization
+cannot have a nonzero factor row or column with support rank at most seven.
+This does not rule out factorizations with more than nine factors.

research/e8-hyperplane-minrank/historical/work/p518-next/bit/weighted/rank9/parabolic/independent_check.py

@@ -0,0 +1,95 @@
+"""Check the eight finite certificates with integer arithmetic."""
+from fractions import Fraction
+from itertools import combinations, product
+from pathlib import Path
+import hashlib
+import json
+
+BASE = Path(__file__).resolve().parent
+source = BASE.parent / 'quick.json'
+raw = source.read_bytes()
+data = json.loads(raw)
+roots = set()
+for i in range(8):
+    for j in range(i + 1, 8):
+        for u, v in product((-2, 2), repeat=2):
+            row = [0] * 8
+            row[i], row[j] = u, v
+            roots.add(tuple(row))
+roots.update(row for row in product((-1, 1), repeat=8)
+             if row.count(-1) % 2 == 0)
+assert len(roots) == 240
+simple = [(1,-1,-1,-1,-1,-1,-1,1), (2,2,0,0,0,0,0,0),
+          (-2,2,0,0,0,0,0,0)]
+for j in range(1, 6):
+    row = [0] * 8
+    row[j], row[j + 1] = -2, 2
+    simple.append(tuple(row))
+assert data['simple_roots'] == list(map(list, simple))
+assert all(root in roots for root in simple)
+
+def dot(a, b):
+    return sum(x * y for x, y in zip(a, b))
+
+# Invert the column matrix of the simple roots.
+matrix = [[Fraction(simple[j][i]) for j in range(8)]
+          + [Fraction(i == j) for j in range(8)] for i in range(8)]
+for j in range(8):
+    pivot = next(i for i in range(j, 8) if matrix[i][j])
+    matrix[j], matrix[pivot] = matrix[pivot], matrix[j]
+    scale = matrix[j][j]
+    matrix[j] = [x / scale for x in matrix[j]]
+    for i in range(8):
+        if i != j:
+            scale = matrix[i][j]
+            matrix[i] = [x - scale * y for x, y in zip(matrix[i], matrix[j])]
+inverse = [row[8:] for row in matrix]
+for root in roots:
+    coordinates = [dot(row, root) for row in inverse]
+    assert all(x.denominator == 1 for x in coordinates)
+    assert all(x >= 0 for x in coordinates) or all(x <= 0 for x in coordinates)
+    for alpha in simple:
+        inner = dot(root, alpha)
+        assert inner % 4 == 0
+        reflected = tuple(x - inner // 4 * y for x, y in zip(root, alpha))
+        assert reflected in roots
+assert all(dot(alpha, alpha) == 8 for alpha in simple)
+cartan = [[dot(a, b) // 4 for b in simple] for a in simple]
+assert [(i + 1, j + 1) for i, j in combinations(range(8), 2)
+        if cartan[i][j] == -1] == [(1,3),(2,4),(3,4),(4,5),(5,6),(6,7),(7,8)]
+
+pairs = [tuple(pair) for pair in data['pairs']]
+assert len(pairs) == 5 and len(set(pairs)) == 5
+assert len(set().union(*map(set, pairs))) == 4
+counts = [42,28,22,14,16,23,37,63]
+types = ['D7','A7','A6+A1','A4+A2+A1','A4+A3','D5+A2','E6+A1','E7']
+items = []
+assert len(data['parabolics']) == 8
+for item in data['parabolics']:
+    node = item['node']
+    n = item['normal']
+    assert [i + 1 for i, a in enumerate(simple) if dot(n, a)] == [node]
+    inside = sum(dot(n, r) == 0 for r in roots) // 2
+    assert inside == item['roots_in_hyperplane'] == counts[node - 1]
+    rows = list(map(tuple, item['certificate']))
+    assert len(rows) == 13
+    assert len({min(r, tuple(-x for x in r)) for r in rows}) == 13
+    assert all(r in roots and dot(r, n) != 0 for r in rows)
+    anchors, witnesses = rows[:8], rows[8:]
+    assert all(dot(a, b) != 0 for a, b in combinations(anchors, 2))
+    for pair, witness in zip(pairs, witnesses):
+        assert tuple(i for i, a in enumerate(anchors) if dot(a, witness) == 0) == pair
+    checks = 0
+    for (p, u), (q, v) in combinations(list(zip(pairs, witnesses)), 2):
+        if set(p) & set(q):
+            assert dot(u, v) != 0
+            checks += 1
+    assert checks == 8
+    items.append({'node':node, 'type':types[node - 1], 'root_lines_inside':inside,
+                  'certificate_lines':13, 'incident_zero_constraints':checks})
+result = {'status':'PASS', 'input_sha256':hashlib.sha256(raw).hexdigest(),
+          'integer_root_count':240, 'simple_basis_and_reflection_checks':True,
+          'all_eight_certificates_checked':True, 'parabolics':items,
+          'scope':'Finite certificates and simple roots. The universal theorem also uses the Weyl chamber and fitting rank arguments in PROOF.md.'}
+(BASE / 'INDEPENDENT.json').write_text(json.dumps(result, indent=2) + '\n')
+print(json.dumps(result, indent=2))