diff --git a/research/e8-minimal-mixed-port/README.md b/research/e8-minimal-mixed-port/README.md new file mode 100644 index 0000000000..49a72ef2fb --- /dev/null +++ b/research/e8-minimal-mixed-port/README.md @@ -0,0 +1,206 @@ +# The minimal E8 mixed-port extension is saturated + +**Scoped negative result.** Delete at most 14 of the 120 E8 root lines and +retain their inherited nine-dimensional binary labels. If a compatible +non-root port can be added, exactly 14 lines were deleted. Up to Weyl symmetry, +they are the integer root lines involving coordinate eight. There is exactly +one compatible non-root port type. After adding it, no further nonzero port +of any direction can be added with these labels. + +The resulting 107-port unit has star copy cost **72**, not the root-only +puncture's cost 64. Every nonzero reader now spans all eight physical +dimensions. Its ratio `72/107` is worse than both the full-root unit's `72/120` +and the known punctured-star benchmark `63/111`. + +This adds an equality classification and simultaneous-port obstruction to +Chi Zhao's [#631](https://github.com/CrocSwap/integer-mult-bounds/pull/631). +GamingPuzzled's #620 already computed the coordinate-axis example's roughly +0.67 ratio. That numerical example is predecessor evidence, not a new result +claimed here. The new statement covers every minimum-deletion mixed extension +in the stated model, including arbitrarily many proposed added ports. + +No new supplier word, exponent or kappa is claimed. + +## Model and exact scope + +Let `L` contain the 120 E8 root-line representatives in doubled standard +coordinates, of squared norm eight. Integer lines are `2e_i +/- 2e_j`; +the other 64 representatives have first coordinate one and an even number +of minus signs. Put `G_st = L_s dot L_t / 4` and `B = (J + G) mod 2`. +The rank-nine binary form gives inherited labels `u_t` with +`u_s dot u_t = B_st`. + +A new port consists of a **nonzero rational vector** `n` in eight-dimensional +Euclidean space and a label `z` in the **same nine-dimensional binary space**. +Compatibility requires odd self-pairing `z dot z = 1`, and, for distinct ports, + + physical inner product nonzero => binary label pairing zero. + +Thus all surviving roots in the reader `R(z) = {t : z dot u_t = 1}` must lie +in `n`'s orthogonal hyperplane. New ports must satisfy the same condition +against each other. "Non-root" means that `n` is not proportional to any of +the original E8 root lines. Rational rescaling of a nonzero port is immaterial. + +The theorem fixes surviving root labels. It permits no added binary label +dimensions, zero physical vectors, relabelling of old ports, or different +ambient form. It makes no assertion for more than 14 punctures or for other +decoder families. + +## Why every equality case is D7 + +Use the simple E8 system explicitly listed in `verify.py`. Move an arbitrary +normal into its closed fundamental Weyl chamber. A positive root is a +nonnegative integral combination of simple roots, so its pairing with this +normal vanishes exactly when it uses only vanishing simple roots. Its root +section therefore lies in a standard parabolic section. + +The eight maximal sections have the following reader-deletion minima. Each +minimum is over all 511 nonzero label functionals, so allowing an even label +in this lower bound cannot invalidate it for the required odd labels. + +| Root lines in section | 63 | 42 | 37 | 28 | 23 | 22 | 16 | 14 | +| --- | --- | --- | --- | --- | --- | --- | --- | --- | +| Minimum deletions | 1 | 14 | 27 | 28 | 33 | 35 | 40 | 43 | + +These minima reproduce #631's table independently. Only the 63-line E7 +section has a root normal. If a chamber normal has just that omitted simple +root with positive pairing, it is a root normal and is excluded. Otherwise +choose a positive-pairing simple root whose omission gives one of the other +seven maximal sections. The actual root section is contained in that section. +At most 14 punctures therefore forces the 42-line D7 section and its unique +minimizing reader. + +That reader consists of all 56 integer root lines. The 14 outside D7 are +exactly `2e_i +/- 2e_8`, for `i=1,...,7`, and all must be deleted. The other +42 span the D7 hyperplane. Since the actual normal annihilates these 42 roots, +it is proportional to `e_8`. This last rank argument rules out a proper +subsection of D7 attaining equality. It also proves that the puncture and +reader are forced, rather than merely exhibiting one 14-deletion example. + +The checker verifies integral common-sign simple coordinates, all eight +simple-reflection permutations, and preservation of the binary Gram form. +Weyl permutations consequently preserve its row space, induced nondegenerate +label pairing and odd self-pairing. Transporting the enumeration through these +permutations preserves every compatibility and rank statement used here. +The chamber reduction is a written mathematical argument; enumerating eight +sections alone is not advertised as a formal proof of it. + +## All compatible ports at equality + +For that fixed puncture, the exact rational ranks of all 511 reader spans are + + 15 readers of rank 7; 496 readers of rank 8. + +All 15 deficient readers have odd self-pairing. Fourteen are precisely the +labels of the deleted roots, with those roots as their unique normal lines. +The remaining reader, denoted `z`, selects all integer roots and has unique +normal line `e_8`. No reader has smaller rank. Therefore the only possible +non-root port is `(e_8, z)`, up to nonzero rational rescaling. + +Two copies of this type cannot coexist. Their geometric inner product is +nonzero, but their binary pairing is `z dot z = 1`. + +There is a stronger saturation certificate. Each of the 14 root-normal +readers pairs to one with `z`, and `e_8` lies outside its hyperplane. The +reader `z` itself also reads the added port, because it is odd, and `e_8` +lies outside D7. Adding the port raises all 15 ranks from seven to eight. +The other 496 ranks were already eight. A further nonzero port would need +to annihilate an eight-dimensional reader span, which is impossible. + +The live label rank remains nine. In the star label-decoder model, the +functionals must span the dual label space; a minimum-weight basis gives +the optimum, since extra nonnegative-cost totals cannot improve on a contained +basis. Before augmentation the 15 rank-seven functionals span dimension eight, +giving `8*7 + 8 = 64`. Afterwards all 511 nonzero functionals cost eight, +so the exact optimum is `9*8 = 72`. + +This already fails the optimistic copy-cost comparison. No circuit search +was launched. Helper preparation, source access, frame changes, restoration, +recursive calls, hosting and assembly have not been implemented or priced. +The ratio result excludes this proposed improvement to copied information; +it does not exclude a separate helper-saving tradeoff at a worse copy ratio. + +## Reproduce and verification boundary + +From the repository root, with Python 3.9 or later and no third-party packages: + +```sh +python3 -B research/e8-minimal-mixed-port/verify.py +``` + +Expected output: + +```text +PASS: 8 maximal flats; 511 readers before and after augmentation; one non-root candidate; 5 negative-control categories +star costs: 64 on 106 ports; 72 on 107 ports +``` + +Every run regenerates the census and compares its full deterministic JSON +encoding with `results.json`. `--print-receipt` also prints that encoding. +All validations remain active under `python3 -O`; the checker uses explicit +exceptions, not removable assertions. + +The independent implementation works directly in a basis of rows of `B`, +rather than constructing #620's orthonormal label factor. If the chosen root +indices are `I` and a functional has basis coefficients `a`, its support is +`a * B[I,:]`. Its pairing with `b` is `a * B[I,I] * b^T`. This avoids assuming +that ordinary bitwise dot products are valid in a nonorthonormal basis. +Rational spans use integer elimination with content reduction; normal +vectors and simple-root coordinates use exact fractions. + +The five negative-control categories reject two identical non-root ports, +an even added label, restoration of each of the 14 deleted roots while +retaining the new port, a rank-eight input to the normal calculation, and a +malformed simple-root system. The domain is exhaustive for eight maximal +sections and all 511 readers before and after this forced augmentation. +There is no annealing, heuristic stopping condition, or claim based on a failed +search. The finite arithmetic supports the stated proof and does not prove +the full multiplication theorem. + +Validation on 2026-10-13 passed with Python 3.14.8 and Python 3.11.15, the +latter with `-O`. A separate AI-assisted check generated all 240 signed roots, +quotiented signs in a different order, chose a different binary basis, and +computed reader ranks over GF(3). It confirmed all 511 augmented spans have +rank eight. For the 15 deficient original readers, exact integer annihilators +give rank-at-most-seven certificates and the modular ranks give the matching +lower bounds. Their binary span has dimension eight. The selected-record +binding check, source hashes and staged whitespace check also passed. +The expensive repository-wide supplier replays were not repeated because +no supplier, assembly, generator or existing file changes. + +## Sprint record, source pins and credit + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected conditional +result there is #626 on #622/#623 with #543, +`kappa = 51110230636731/31250000000000000`. It is unchanged. Its all-size, +physical realization, restoration, precision and analytic obligations remain. + +The OS-random assignment seed was **40**, selecting structural decoder +research. It also selects root row 40 as the start of the cyclic row ordering +for the independent binary Gram basis. Three candidates were considered: +deeper star punctures beyond 35, pairing-rank decoders on another nine-line +puncture, and simultaneous non-root additions at the sharp 14-puncture +threshold. The last addresses an explicit omission from #631's scope. + +The local claim was recorded at 04:29 UTC on 2026-10-13 with an expected +finish of 05:01 UTC. There was no pinned sprint issue; the only open issue +was #650. Related #620, #631 and #669 were checked before claiming. +#669 treats paired hypercubes, not this E8 geometry. See `SOURCES.json` for +immutable predecessor pins and content hashes. No external package or PR +checkout is needed to run the checker. + +The final overlap scan at 04:38 UTC covered 528 open PRs through #709. +#620 and #631 retained the recorded heads. New #703 concerns ten quaternionic +lines and asymmetric copy accounting; it does not cover this real E8 +minimum-puncture equality case. + +Credit to Joel Pulikkan / GamingPuzzled for #620's mixed-port model and +coordinate-axis experiment; Chi Zhao for #631's exact threshold and chamber +argument; DreamingOfClouds and artuskg for the format-limit work; eumemic +for the E8 suppliers; and the upstream OpenAI #109 framework and cumulative +community work. The selected frontier also retains the construction and +allocation credit recorded in its maintainer review. + +Prepared by **Sagar Thakrar / @thakrarsagar**, with substantial **OpenAI Codex +assistance** in research, implementation, proof review and documentation. +Apache-2.0, following the repository license. No archived source was changed. diff --git a/research/e8-minimal-mixed-port/SOURCES.json b/research/e8-minimal-mixed-port/SOURCES.json new file mode 100644 index 0000000000..0d7ff8fbf2 --- /dev/null +++ b/research/e8-minimal-mixed-port/SOURCES.json @@ -0,0 +1,49 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 40, + "track": "structural decoder research", + "runtime_dependencies": "Python standard library only; no imports from predecessor packages", + "base_files_sha256": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "research/community-k492-audit/pr626/replay/ASSEMBLY.json": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/REPORT.md": "16c53bf8afd9f91eca02b2af9c9f5f09385823fc705dd1a48153508cfdff28b6", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/e8units.py": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/mixed.py": "088ac53c0842d20b1ecbf807b6e800a585e34b580c15aa8737c4539db84ec551", + "research/e8-decoder-floors-and-cold14-notes/s2-decoder/mixed_d8.py": "f6333bcecf93383c6900b864cadd57b330574a4b64e24b6a3f874f4fafd0e96d" + }, + "predecessor_prs": [ + { + "number": 620, + "head": "e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87", + "author": "Joel Pulikkan / GamingPuzzled", + "role": "Mixed-port compatibility model and coordinate-axis example; not claiming its sampled ratio as new" + }, + { + "number": 631, + "head": "fb893b5ee1317c2da3b297e6fe78eca0857d1a76", + "author": "Chi Zhao / vectorsss", + "role": "Sharp 14-deletion threshold and chamber argument; our checker independently rebuilds the maximal-flat minima", + "files_sha256": { + "research/e8-continuation-20261013/punctures/README.md": "281f706bf29d1f91dd64ba096f9d66d622f49e9d82d0ff306fb9374f77ba7333", + "research/e8-continuation-20261013/punctures/verify.py": "9add2f1d71466f00963652b818e168fe2e2a4fa6e62cafa9811389fdba7000c2" + } + }, + { + "number": 669, + "head": "308f1e6ec3bb0b6ec0584cf7bfe219addc219b1e", + "role": "Overlap check only: paired-hypercube decoder result, not an E8 dependency" + } + ], + "claim": { + "recorded_utc": "2026-10-13T04:29:00Z", + "expected_finish_utc": "2026-10-13T05:01:00Z", + "coordination": "No pinned issue; recorded locally after checking open issues and PRs", + "object": "All simultaneous non-root port additions at the sharp E8 14-puncture threshold, with inherited nine-dimensional labels", + "method": "Exact maximal-parabolic census and exhaustive reader-span classification in a Gram-row basis", + "stopping_rule": "Complete all eight maximal sections, all 511 nonzero readers before/after augmentation, and controls; stop after pricing the copy cost" + }, + "license": "Apache-2.0", + "contributor": "Sagar Thakrar / thakrarsagar", + "ai_assistance": "Substantial OpenAI Codex assistance in research, implementation, proof review and documentation" +} diff --git a/research/e8-minimal-mixed-port/results.json b/research/e8-minimal-mixed-port/results.json new file mode 100644 index 0000000000..a222166a89 --- /dev/null +++ b/research/e8-minimal-mixed-port/results.json @@ -0,0 +1,463 @@ +{ + "added_label_coefficients": 56, + "added_normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "assignment_seed": 40, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "binary_gram_basis_root_indices": [ + 40, + 41, + 42, + 44, + 46, + 50, + 56, + 72, + 88 + ], + "cheap_readers": [ + { + "functional": 4, + "normal": [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 7, + "normal": [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + -1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 21, + "normal": [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 22, + "normal": [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + -1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 37, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 38, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + -1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 56, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "odd": true, + "root_normal": false + }, + { + "functional": 61, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 62, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 248, + "normal": [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + -1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 251, + "normal": [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 376, + "normal": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + -1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 379, + "normal": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 433, + "normal": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "odd": true, + "root_normal": true + }, + { + "functional": 434, + "normal": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1 + ], + "odd": true, + "root_normal": true + } + ], + "equality_puncture": [ + 12, + 13, + 24, + 25, + 34, + 35, + 42, + 43, + 48, + 49, + 52, + 53, + 54, + 55 + ], + "label_dimension": 9, + "maximal_parabolic_flats": [ + { + "minimizer_count": 1, + "minimum_deletions": 14, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "odd_minimizer_count": 1, + "omitted_simple_root": 0, + "root_lines": 42 + }, + { + "minimizer_count": 1, + "minimum_deletions": 28, + "normal": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 5 + ], + "odd_minimizer_count": 1, + "omitted_simple_root": 1, + "root_lines": 28 + }, + { + "minimizer_count": 2, + "minimum_deletions": 35, + "normal": [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + -7 + ], + "odd_minimizer_count": 2, + "omitted_simple_root": 2, + "root_lines": 22 + }, + { + "minimizer_count": 2, + "minimum_deletions": 43, + "normal": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 5 + ], + "odd_minimizer_count": 2, + "omitted_simple_root": 3, + "root_lines": 14 + }, + { + "minimizer_count": 1, + "minimum_deletions": 40, + "normal": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 4 + ], + "odd_minimizer_count": 1, + "omitted_simple_root": 4, + "root_lines": 16 + }, + { + "minimizer_count": 1, + "minimum_deletions": 33, + "normal": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 3 + ], + "odd_minimizer_count": 1, + "omitted_simple_root": 5, + "root_lines": 23 + }, + { + "minimizer_count": 1, + "minimum_deletions": 27, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "odd_minimizer_count": 1, + "omitted_simple_root": 6, + "root_lines": 37 + }, + { + "minimizer_count": 1, + "minimum_deletions": 1, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "odd_minimizer_count": 1, + "omitted_simple_root": 7, + "root_lines": 63 + } + ], + "negative_controls": { + "corrupt_simple_system": true, + "duplicate_nonroot_port": true, + "even_added_label": true, + "rank_eight_has_no_normal": true, + "restored_deleted_root": true + }, + "nonzero_readers": 511, + "one_added_port": { + "comparison_ratio": "21/37", + "ports": 107, + "rank_histogram": { + "8": 511 + }, + "ratio": "72/107", + "ratio_strictly_worse": true, + "star_basis": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "star_cost": 72 + }, + "reader_weight_histogram": { + "56": 255, + "64": 255, + "120": 1 + }, + "root_lines": 120, + "root_only": { + "ports": 106, + "rank_histogram": { + "7": 15, + "8": 496 + }, + "star_basis": [ + 4, + 7, + 21, + 37, + 56, + 61, + 248, + 376, + 64 + ], + "star_cost": 64 + }, + "simple_reflections_checked": 8 +} diff --git a/research/e8-minimal-mixed-port/verify.py b/research/e8-minimal-mixed-port/verify.py new file mode 100644 index 0000000000..bf3d61e0e4 --- /dev/null +++ b/research/e8-minimal-mixed-port/verify.py @@ -0,0 +1,265 @@ +#!/usr/bin/env python3 +"""Exact census of the sharp 14-puncture E8 mixed-port equality case. + +Prepared by thakrarsagar with substantial OpenAI Codex assistance. Apache-2.0. +Uses a row basis of the binary Gram matrix, not an orthonormal label factor. +""" + +import argparse +from collections import Counter +from fractions import Fraction +from itertools import combinations, product +import json +from math import gcd +from pathlib import Path + +SEED = 40 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +def parity(x): + return bin(x).count("1") % 2 + + +def primitive(v): + den = 1 + for x in v: + den = den * x.denominator // gcd(den, x.denominator) + w = [int(x * den) for x in v] + content = 0 + for x in w: + content = gcd(content, x) + require(content != 0, "zero normal") + w = [x // content for x in w] + if next(x for x in w if x) < 0: + w = [-x for x in w] + return tuple(w) + + +def echelon(rows): + basis = [] + for row in rows: + row = list(row) + for pivot, b in basis: + if row[pivot]: + a, c = row[pivot], b[pivot] + row = [c * x - a * y for x, y in zip(row, b)] + content = 0 + for x in row: + content = gcd(content, x) + if content: + row = [x // content for x in row] + pivot = next((j for j, x in enumerate(row) if x), None) + if pivot is not None: + basis.append((pivot, row)) + return basis + + +def normal(rows): + basis = echelon(rows) + require(len(basis) == 7, "normal requires rank seven") + pivots = {i for i, _ in basis} + free = next(i for i in range(8) if i not in pivots) + v = [Fraction(int(i == free)) for i in range(8)] + for pivot, row in reversed(basis): + v[pivot] = -sum(row[j] * v[j] for j in range(8) if j != pivot) / row[pivot] + out = primitive(v) + require(all(dot(out, row) == 0 for row in rows), "incorrect normal") + return out + + +def binary_basis(rows): + basis = {} + chosen = [] + for i, row in enumerate(rows): + while row: + pivot = row.bit_length() - 1 + if pivot not in basis: + basis[pivot] = row + chosen.append(i) + break + row ^= basis[pivot] + return chosen + + +def roots(): + out = [] + for i, j in combinations(range(8), 2): + for sign in (1, -1): + v = [0] * 8 + v[i], v[j] = 2, 2 * sign + out.append(tuple(v)) + out.extend((1,) + s for s in product((1, -1), repeat=7) if s.count(-1) % 2 == 0) + require(len(out) == 120 and len(set(out)) == 120, "root count") + require(all(dot(v, v) == 8 for v in out), "root norm") + require(all(dot(v, w) in (-4, 0, 4) for i, v in enumerate(out) for w in out[i + 1:]), "root pairing") + return out + + +def simple_system(): + out = [(1, -1, -1, -1, -1, -1, -1, 1), (2, 2, 0, 0, 0, 0, 0, 0)] + for j in range(6): + v = [0] * 8 + v[j], v[j + 1] = -2, 2 + out.append(tuple(v)) + return out + + +def check_simple_coordinates(lines, simple): + # Invert the simple-root column matrix to certify the positive-root premise. + a = [[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 a[i][j]) + a[j], a[pivot] = a[pivot], a[j] + c = a[j][j] + a[j] = [x / c for x in a[j]] + for i in range(8): + if i != j: + c = a[i][j] + a[i] = [x - c * y for x, y in zip(a[i], a[j])] + inverse = [row[8:] for row in a] + for line in lines: + coords = [dot(row, line) for row in inverse] + require(all(x.denominator == 1 for x in coords), "nonintegral simple coordinate") + require(all(x >= 0 for x in coords) or all(x <= 0 for x in coords), "mixed-sign simple coordinates") + + +def census(): + lines = roots() + gram = [sum(((1 + dot(v, w) // 4) % 2) << j for j, w in enumerate(lines)) for v in lines] + basis_order = list(range(SEED, 120)) + list(range(SEED)) + indices = [basis_order[i] for i in binary_basis([gram[j] for j in basis_order])] + require(len(indices) == 9, "binary Gram rank") + generators = [gram[i] for i in indices] + words = [0] + for g in generators: + words += [w ^ g for w in words] + require(len(set(words)) == 512, "reader word independence") + labels = [words.index(g) for g in gram] + + def pairing(a, b): + return sum(((a >> i) & 1) * parity(words[b] & (1 << indices[i])) for i in range(9)) % 2 + + require(all(pairing(a, a) == 1 for a in labels), "odd root labels") + + def compatible(geometry, lab): + require(all(pairing(a, a) == 1 for a in lab), "even port label") + require(all(not dot(v, w) or not pairing(lab[i], lab[j]) + for i, v in enumerate(geometry) for j, w in enumerate(geometry) if i < j), "incompatible port pair") + + compatible(lines, labels) + simple = simple_system() + check_simple_coordinates(lines, simple) + root_directions = {primitive(v): i for i, v in enumerate(lines)} + for root in simple: + permutation = [root_directions[primitive(tuple(x - dot(v, root) // 4 * y for x, y in zip(v, root)))] for v in lines] + require(len(set(permutation)) == 120, "simple reflection is not a permutation") + require(all(((gram[i] >> j) & 1) == ((gram[permutation[i]] >> permutation[j]) & 1) + for i in range(120) for j in range(120)), "reflection changes binary Gram form") + flat_receipts = [] + equality = None + for omitted in range(8): + n = normal([v for j, v in enumerate(simple) if j != omitted]) + outside = sum((dot(v, n) != 0) << j for j, v in enumerate(lines)) + counts = [bin(w & outside).count("1") for w in words[1:]] + minimum = min(counts) + minimizers = [a for a in range(1, 512) if counts[a - 1] == minimum] + require((n in root_directions) == (minimum == 1), "root-normal exception is not the E7 flat") + flat_receipts.append({"omitted_simple_root": omitted, "normal": n, + "root_lines": 120 - bin(outside).count("1"), + "minimum_deletions": minimum, "minimizer_count": len(minimizers), + "odd_minimizer_count": sum(pairing(a, a) for a in minimizers)}) + if minimum == 14: + require(equality is None and len(minimizers) == 1, "nonunique D7 equality") + z = minimizers[0] + puncture = words[z] & outside + equality = n, z, puncture + require(sorted(x["minimum_deletions"] for x in flat_receipts) == [1, 14, 27, 28, 33, 35, 40, 43], "hyperplane thresholds") + n, z, puncture = equality + live = [i for i in range(120) if not (puncture >> i) & 1] + geometry = [lines[i] for i in live] + lab = [labels[i] for i in live] + require(len(live) == 106 and len(binary_basis(lab)) == 9, "live label rank") + + def reader_data(geometry, lab): + spans = [[v for v, u in zip(geometry, lab) if pairing(a, u)] for a in range(1, 512)] + ranks = [len(echelon(rows)) for rows in spans] + order = sorted(range(1, 512), key=lambda a: (ranks[a - 1], a)) + chosen = [order[j] for j in binary_basis(order)] + return spans, ranks, chosen, sum(ranks[a - 1] for a in chosen) + + spans, ranks, chosen, cost = reader_data(geometry, lab) + cheap = [] + nonroot = [] + for a, rank in enumerate(ranks, 1): + if rank < 8: + require(rank == 7, "reader below rank seven") + direction = normal(spans[a - 1]) + record = {"functional": a, "odd": bool(pairing(a, a)), "normal": direction, + "root_normal": direction in root_directions} + cheap.append(record) + if not record["root_normal"]: + nonroot.append(record) + require(len(nonroot) == 1 and nonroot[0]["functional"] == z and nonroot[0]["normal"] == n, "nonroot candidate classification") + compatible(geometry + [n], lab + [z]) + _, mixed_ranks, mixed_chosen, mixed_cost = reader_data(geometry + [n], lab + [z]) + require(set(mixed_ranks) == {8} and mixed_cost == 72, "augmented reader ranks") + require(pairing(z, z) == 1 and dot(n, n) != 0, "duplicate-port obstruction") + + def rejects(action): + try: + action() + except ValueError: + return True + raise ValueError("negative control was accepted") + + deleted = [i for i in range(120) if (puncture >> i) & 1] + controls = { + "duplicate_nonroot_port": rejects(lambda: compatible(geometry + [n, n], lab + [z, z])), + "even_added_label": rejects(lambda: compatible(geometry + [n], lab + [0])), + "restored_deleted_root": all(rejects(lambda i=i: compatible(geometry + [lines[i], n], lab + [labels[i], z])) for i in deleted), + "rank_eight_has_no_normal": rejects(lambda: normal(lines)), + "corrupt_simple_system": rejects(lambda: check_simple_coordinates(lines, simple[:-1] + [(0, 0, 0, 0, 0, -2, 0, 2)])), + } + return { + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", "assignment_seed": SEED, + "binary_gram_basis_root_indices": indices, + "root_lines": 120, "label_dimension": 9, "nonzero_readers": 511, + "simple_reflections_checked": 8, + "reader_weight_histogram": dict(sorted(Counter(bin(w).count("1") for w in words[1:]).items())), + "maximal_parabolic_flats": flat_receipts, + "equality_puncture": deleted, "added_normal": n, "added_label_coefficients": z, + "cheap_readers": cheap, + "root_only": {"ports": 106, "rank_histogram": dict(sorted(Counter(ranks).items())), "star_basis": chosen, "star_cost": cost}, + "one_added_port": {"ports": 107, "rank_histogram": dict(sorted(Counter(mixed_ranks).items())), "star_basis": mixed_chosen, "star_cost": mixed_cost, + "ratio": str(Fraction(mixed_cost, 107)), "comparison_ratio": "21/37", + "ratio_strictly_worse": Fraction(mixed_cost, 107) > Fraction(63, 111)}, + "negative_controls": controls, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--print-receipt", action="store_true") + args = parser.parse_args() + result = census() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + expected = Path(__file__).with_name("results.json") + require(encoded == expected.read_text(), "receipt mismatch") + if args.print_receipt: + print(encoded, end="") + else: + print("PASS: 8 maximal flats; 511 readers before and after augmentation; one non-root candidate; 5 negative-control categories") + print("star costs:", result["root_only"]["star_cost"], "on 106 ports;", result["one_added_port"]["star_cost"], "on 107 ports") + + +if __name__ == "__main__": + main()