From 114eafd694efcfae1f811cbaccf7962385919386 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 08:01:26 +0000 Subject: [PATCH] feat(research): prove the exact small-deletion E8 Gram floor --- .../p104-gram-class-exact-floor/README.md | 222 +++++++++ .../p104-gram-class-exact-floor/SOURCES.json | 30 ++ .../p104-gram-class-exact-floor/TASK.json | 135 ++++++ .../p104-gram-class-exact-floor/VERIFY.json | 38 ++ .../build_designs.py | 73 +++ .../data/designs.json | 30 ++ .../p104-gram-class-exact-floor/verify.py | 428 ++++++++++++++++++ 7 files changed, 956 insertions(+) create mode 100644 research/p104-gram-class-exact-floor/README.md create mode 100644 research/p104-gram-class-exact-floor/SOURCES.json create mode 100644 research/p104-gram-class-exact-floor/TASK.json create mode 100644 research/p104-gram-class-exact-floor/VERIFY.json create mode 100644 research/p104-gram-class-exact-floor/build_designs.py create mode 100644 research/p104-gram-class-exact-floor/data/designs.json create mode 100644 research/p104-gram-class-exact-floor/verify.py diff --git a/research/p104-gram-class-exact-floor/README.md b/research/p104-gram-class-exact-floor/README.md new file mode 100644 index 0000000000..c5beb404c6 --- /dev/null +++ b/research/p104-gram-class-exact-floor/README.md @@ -0,0 +1,222 @@ +# Exact E8 Gram-class floor through 24 deleted lines + +No new kappa, supplier word or multiplication theorem is claimed. + +For the Gram class of DreamingOfClouds's [PR #6888](https://github.com/CrocSwap/integer-mult-bounds/pull/6888), +let `g(d)` be the minimum cost over **both** the deleted set `D` with `|D| = d` +and all Gram-class designs on its complement. This package proves + +```text +g(d) = 72 - 2 min(d, 8), 0 <= d <= 24. +``` + +The claim is a scoped written proof with exact finite certificates. The new +lower-bound step treats `d <= 7`. Explicit designs attain the bound for every +`d <= 24`, including the previously uncovered range below 16. The lower bound +56 for `8 <= d <= 24` uses the argument already in #6888, Theorem O, whose +codimension-two census applies throughout `d <= 24`. + +In particular, deleting the eight simple-root lines gives `c = 56`, with eight +terms of price 7 and `det M = 65536`. Its 112 live ports have `v - c = 56`. +Thus `c >= 72 - |D|` and `v - c <= 48` do not hold for arbitrary deleted sets +in this enlarged Gram class. This set has the **size** of P112. It is not the +fixed P112 unit obtained by deleting an orthogonal frame. The example has +`M` nonscalar, so it does not contradict the exact-decoder floors in #2338. + +## Model and precise quantifiers + +Use doubled coordinates for the 240 E8 roots, of squared norm 8. Let `L` be +their 120 unoriented lines and choose a representative `l_p` on each line. +Set `N[p,q] = 1` over F2 when `(l_p . l_q)/4` is even. It has rank 9 and +admits a factorization `N = A G A^T`, with nine-column label matrix `A` and +invertible symmetric `G` over F2. + +A design on `P = L \ D` is a finite family of pairs `u_k,w_k` in C^8 such +that `M = sum_k u_k w_k^T` is invertible. Its supports and prices are + +```text +S_D(u) = {p in L \ D : l_p . u != 0}, +rho_D(u,w) = rank_F2 N[S_D(u), S_D(w)], +c = sum_k rho_D(u_k,w_k). +``` + +The dot product is bilinear, with no complex conjugation. The theorem says +that **every** such design for **every** `D` of size `d <= 24` has cost at +least `72 - 2 min(d,8)`, and for **some** `D` of each size there is a design +with equality. It does not give the optimum for each individual deleted set. + +## Proof + +Write `a_D(u) = 9 - dim_F2 span{A[p] : p in S_D(u)}` for nonzero `u`. +Zero terms may be discarded. + +### 1. Eight independent pairs and their price bound + +Let `U,W` have the term vectors as columns. Cauchy-Binet expands +`det(U W^T)` as a sum over eight-element subsets `K` of +`det(U_K) det(W_K)`. Since the sum is nonzero, some `K` makes both selected +families bases of C^8. Discarding other terms can only lower the total price. +Sylvester's inequality in the nine-dimensional label space gives, termwise, + +```text +rho_D(u,w) >= 9 - a_D(u) - a_D(w). +``` + +These are the Cauchy-Binet and Sylvester steps of #6888, Theorem O. + +### 2. The finite geometric inputs + +The ray census in #6888 gives the following numbers. Here `T(r)=S_empty(r)`; +`cost_j` is the least number of lines removed from `T(r)` to make its label +span have codimension at least `j`. + +| `|T(r)|` | `cost_1` | `cost_2` | +|---:|---:|---:| +| 57 | 1 | 25 | +| 78 | 14 | 42 | +| 83 | 27 | 51 | +| 92 | 28 | 56 | +| 97 | 33 | 61 | +| 98 | 35 | 62 | +| 104 | 40 | 68 | +| 106 | 43 | 70 | + +These are the eight fundamental-weight rays up to the E8 Weyl group. Only +`omega_8`, which is a root, has `cost_1 < 14`. The standalone verifier +reconstructs the Cartan matrix and its inverse, constructs the rays, and +computes this table by enumerating all label hyperplanes and all two-dimensional +annihilator subspaces. This checks a dependency of the new argument; the +census and the general `a_D(u) <= 1` consequence for `d <= 24` are credited +to #6888, rather than claimed as new results. + +The verifier also checks the following root-specific fact over all 120 roots +and all 511 nonzero label functionals. For a root line `r`, exactly one label +hyperplane omits just `{r}` from `T(r)`; every other label hyperplane omits at +least 24 lines. The 63 roots orthogonal to `r` have rational rank 7. +Consequently, when `|D| <= 7`, + +```text +a_D(r) = 1 if r belongs to D, and 0 otherwise. +``` + +Indeed, label-span deficiency means that some nonzero functional vanishes +on every surviving label. With at most seven deletions, its omitted set must +be the unique singleton `{r}`. Removing that singleton gives rank exactly 8. + +### 3. Only deleted root directions can be deficient at small d + +First take `x` real and nonzero, with `|D| <= 7` and `a_D(x) > 0`. Move it +by an E8 Weyl transformation into the closed fundamental chamber, moving `D` +as well. This preserves the mask and all relevant ranks. Write +`x = sum_i t_i omega_i`, with `t_i >= 0`. + +Every positive root has nonnegative simple-root coefficients. Hence its +pairing with this sum vanishes exactly when its pairing with every active +`omega_i` vanishes. Thus `T(x)` is the union of `T(omega_i)` over `t_i > 0`. +Each active ray must therefore have deficient surviving label span. Its +`cost_1` is at most seven. The table forces every active index to be 8. +It follows that `x` is proportional to a root. + +For complex nonzero `u`, choose a complex scalar `z` so that +`x = Re(z u)` has the same support on all 120 root lines as `u`. Such a scalar +exists because each nonzero root pairing forbids only a real line of choices +for `z`, and there are finitely many pairings. The real argument makes `x` +a root direction. Every root orthogonal to that direction is then also +orthogonal to `u`. Since these roots span its seven-dimensional orthogonal +complement, `u` is a complex multiple of the same root. The root-specific +fact in step 2 now forces that root line to lie in `D`, with deficiency 1. + +### 4. Lower-bound assembly + +For `d <= 7`, a basis contains at most one vector on each deleted root line. +Step 3 therefore gives `sum_{k in K} a_D(u_k) <= d` and the same bound for +bottoms. Step 1 implies `c >= 72 - 2d`. + +For `8 <= d <= 24`, #6888's domination and `cost_2 >= 25` give +`a_D(u) <= 1` for every nonzero direction, including complex directions. +For completeness, its domination step replaces the root-hyperplane flat of +`u` by a real arrangement ray in that flat. The ray support is contained +in the original support. A deficiency of two would therefore force at least +25 deletions on that ray. Every selected term costs at least 7, so `c >= 56`. + +### 5. Attainment + +Take the Bourbaki simple-root basis `a_1,...,a_8`, whose doubled coordinates +are recorded in `build_designs.py`. Its Dynkin diagram has the perfect matching + +```text +(1,3), (2,4), (5,6), (7,8). +``` + +For even `d <= 8`, delete the endpoints of the first `d/2` matching edges, +and pair their endpoints by transposition. Pair each remaining root with +itself. For odd `d < 8`, also delete one endpoint of the next edge and +transpose it with an unused simple root. Use the eight terms +`(u_k,w_k) = (a_k,a_tau(k))`. Both families are bases, so `M` is invertible. +For `d >= 8`, keep the `d=8` terms and append `d-8` other deleted lines. + +`data/designs.json` lists all 25 resulting designs. The verifier independently +rebuilds every support from integer dot products and every term price from +the corresponding binary submatrix of `N`. It checks invertibility by exact +Bareiss determinants. The costs equal the stated floor at every `d=0,...,24`. +This finite enumeration proves attainment for the full asserted range. + +## Reproduce and evidence limits + +From the repository root, any CPython 3.12 can replace the interpreter below. +No third-party dependencies are needed. + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-gram-class-exact-floor +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-gram-class-exact-floor --check-source-history +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error -X dev research/p104-gram-class-exact-floor/verify.py +``` + +The direct check ends with +`PASS_P104_GRAM_CLASS_EXACT_FLOOR designs=25 root_hyperplanes=61320 no_new_kappa`. +The registered commands run normal and optimized Python. Controls detect a +singular term family and compare the price-7 construction with identity pairing +on the same deleted set, which costs 64, and with restored lines, which costs 72. + +To regenerate the committed design data without writing replay output into the +checkout, run `build_designs.py /absolute/scratch/designs.json` with the same +interpreter, then compare that JSON with `data/designs.json`. + +No solver, Lean, Docker, selected supplier replay, physical COPY implementation +or complete multiplication theorem was run or established. The written proof +uses the usual E8 Weyl chambers and positive-root expansion. Its finite inputs +are checked exactly; independent human and formal proof-kernel acceptance +remain unclaimed. The theorem excludes `d >= 25`, non-Gram carriers and other +line systems. It gives no new floor for the subclass `M` proportional to `I`. + +The verifier has bounded loops on at most 120 lines, 512 labels, eight-dimensional +matrices and 25 certificates. Python's managed allocation is the power-of-ten +memory-allocation deviation; all collections have these finite bounds. The +largest elimination matrices are 120 by 8 over integers and 8 by 16 over rationals. +Diagnostics use `-W error -X dev`; there is no separate configured static analyzer. + +## Open next questions + +1. For a fixed deleted set with `d <= 7`, determine when equality `72-2d` + is attained. The first test is the odd-inner-product matching graph on + independent deleted roots. This distinguishes the global minimum proved + here from a statement about every deleted set. The pairing constraint + after Cauchy-Binet is the remaining issue. +2. Determine the minimum under `M` proportional to `I` for nonorthogonal small + deleted sets. Start with the eight-simple-root set, impose the exact matrix + identity and reprice every term. The nonscalar construction here does not + answer that decoder question. + +Both questions and their first steps are in [TASK.json](TASK.json). + +## Credit and provenance + +This package was produced by Nick Petalas. New work is Apache-2.0. +DreamingOfClouds's #6888 supplies the Gram model, Theorem O's Cauchy-Binet, +Sylvester and domination argument, the ray census and the open question below +16 deletions. The new contribution is the small-deletion deficient-direction +argument and the attaining designs, giving the exact minimum over deleted sets. +DreamingOfClouds's #2338 and its credited decoder lineage concern the stronger +exact-decoder constraints and are cited for context, without replaying them. +Source commits, blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). +The selected record and catalogue remain historical provenance. diff --git a/research/p104-gram-class-exact-floor/SOURCES.json b/research/p104-gram-class-exact-floor/SOURCES.json new file mode 100644 index 0000000000..f3789e2197 --- /dev/null +++ b/research/p104-gram-class-exact-floor/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-duality-ceiling-flag-note/README.md", + "usage": "provenance", + "git_blob": "d5fe91d99174118343bd23651690dd301c8e991a", + "sha256": "79f37525b4e765eb2c1a685fcf7aba0494c59f783b9ab3fd507800e03c3060bf" + }, + { + "path": "research/p104-duality-ceiling-flag-note/THEOREM.md", + "usage": "provenance", + "git_blob": "90d1e224b6a4183a2d0004e3d11af8da4d5e5433", + "sha256": "720b9b803d07e5217f5ca6b5511ec2727a74413034773ccab587cf20777a67dc" + } + ] +} diff --git a/research/p104-gram-class-exact-floor/TASK.json b/research/p104-gram-class-exact-floor/TASK.json new file mode 100644 index 0000000000..d2c0c3f279 --- /dev/null +++ b/research/p104-gram-class-exact-floor/TASK.json @@ -0,0 +1,135 @@ +{ + "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": "Determine the minimum over all deleted sets D of each size d <= 24 and all invertible-M E8 Gram-class designs.", + "scope_change_reason": "Answer the fewer-than-16-deletions part of open question 1 in DreamingOfClouds PR #6888. This is a geometric side result, not a helper split or paid-word improvement.", + "bottleneck_link": "A scoped E8 mask-rank floor identifies what Gram-class arguments can exclude. Nonscalar M is allowed, so attainment does not supply an exact decoder or physical COPY improvement.", + "budget_minutes": 60, + "stop_rule": "Ship the exact floor through 24 deletions once the written lower bound and all 25 attaining certificates pass; leave fixed-D and scalar-M questions open.", + "outcome": "completed", + "evidence": "README.md proof, 25 data/designs.json certificates, full root/hyperplane census and direct exact integer/F2/rational verifier. No new kappa or multiplication theorem.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "For a fixed deleted set with d <= 7, when is the lower bound 72-2d attained?", + "why_it_matters": "The theorem optimizes over deleted sets and does not identify every fixed-set minimum.", + "first_step": "Analyze the odd-inner-product matching graph on independent deleted root lines and complete the top and bottom bases.", + "blocked_by": "The paired-basis constraint beyond the global lower bound." + }, + { + "question": "What is the minimum with M proportional to I on the eight-simple-root deleted set?", + "why_it_matters": "The cost-56 design has nonscalar M and therefore does not implement the exact decoder identity.", + "first_step": "Impose the exact matrix identity, construct a finite term family and recompute all binary support-pairing ranks.", + "blocked_by": "The scalar-matrix constraint couples the eight term pairs." + } + ], + "source_question": { + "pr": 6888, + "author": "DreamingOfClouds", + "item": 1, + "scope": "15 or fewer deleted lines" + }, + "overlap_checkpoint": { + "upstream_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "priority_revision": 8, + "checked_utc": "2026-11-11T07:57:00Z", + "coverage": "Live open PRs, account PRs, handoff comments, merged-title searches and origin/main README search. Cached overlap had 466 open PRs and 7089 discussion records with complete pagination; sparse local coverage was 171/10178 notes, supplemented by git grep on origin/main. No novelty guarantee." + } +} diff --git a/research/p104-gram-class-exact-floor/VERIFY.json b/research/p104-gram-class-exact-floor/VERIFY.json new file mode 100644 index 0000000000..da222cdc37 --- /dev/null +++ b/research/p104-gram-class-exact-floor/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact E8 labels, ray-census proof inputs, all 61320 root-hyperplane cases, 25 attaining designs and singular/support controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat all finite checks with Python assertions disabled." + } + ] +} diff --git a/research/p104-gram-class-exact-floor/build_designs.py b/research/p104-gram-class-exact-floor/build_designs.py new file mode 100644 index 0000000000..e281b9b38f --- /dev/null +++ b/research/p104-gram-class-exact-floor/build_designs.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Write the 25 explicit Gram designs to a requested output file. + +Run from the repository root with an output path outside the checkout. +The independent verifier recomputes every price and determinant. +""" +import argparse +import itertools +import json +from pathlib import Path + +SIMPLE = [ + None, + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + (0, -2, 2, 0, 0, 0, 0, 0), + (0, 0, -2, 2, 0, 0, 0, 0), + (0, 0, 0, -2, 2, 0, 0, 0), + (0, 0, 0, 0, -2, 2, 0, 0), + (0, 0, 0, 0, 0, -2, 2, 0), +] +PAIRS = [(1, 3), (2, 4), (5, 6), (7, 8)] + + +def root_lines(): + lines = set() + for i, j in itertools.combinations(range(8), 2): + for sign in (2, -2): + root = [0] * 8 + root[i], root[j] = 2, sign + lines.add(tuple(root)) + for tail in itertools.product((1, -1), repeat=7): + if tail.count(-1) % 2 == 0: + lines.add((1,) + tail) + if len(lines) != 120: + raise ValueError("wrong E8 line count") + return sorted(lines) + + +def design(d, lines): + deleted_indices = set() + tau = {i: i for i in range(1, 9)} + for a, b in PAIRS[:min(d // 2, 4)]: + deleted_indices.update((a, b)) + tau[a], tau[b] = b, a + if d < 8 and d % 2: + a = PAIRS[d // 2][0] + deleted_indices.add(a) + b = min(i for i in range(1, 9) if i not in deleted_indices) + tau[a], tau[b] = b, a + deleted = [SIMPLE[i] for i in sorted(deleted_indices)] + extras = [v for v in lines if v not in deleted and tuple(-x for x in v) not in deleted] + if d >= 8: + deleted.extend(extras[:d - 8]) + return {"d": d, "claimed_c": 72 - 2 * min(d, 8), "D": deleted, + "terms": [(SIMPLE[k], SIMPLE[tau[k]]) for k in range(1, 9)]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("output", type=Path) + args = parser.parse_args() + lines = root_lines() + rows = [json.dumps(design(d, lines), sort_keys=True, separators=(",", ":")) for d in range(25)] + payload = ('{\n "format": "Gram-class E8 designs in doubled integer coordinates",\n' + ' "designs": [\n' + ",\n".join(rows) + '\n ]\n}\n') + args.output.write_text(payload, encoding="utf-8") + print("WROTE_GRAM_DESIGNS designs=25") + + +if __name__ == "__main__": + main() diff --git a/research/p104-gram-class-exact-floor/data/designs.json b/research/p104-gram-class-exact-floor/data/designs.json new file mode 100644 index 0000000000..b7d5c3bda7 --- /dev/null +++ b/research/p104-gram-class-exact-floor/data/designs.json @@ -0,0 +1,30 @@ +{ + "format": "Gram-class E8 designs in doubled integer coordinates", + "designs": [ +{"D":[],"claimed_c":72,"d":0,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[1,-1,-1,-1,-1,-1,-1,1]],[[2,2,0,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0]],[[0,-2,2,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,-2,2,0,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,0,-2,2,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1]],"claimed_c":70,"d":1,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[-2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0]],[[0,-2,2,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,-2,2,0,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,0,-2,2,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],"claimed_c":68,"d":2,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,-2,2,0,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,0,-2,2,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0]],"claimed_c":66,"d":3,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,-2,2,0,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,0,-2,2,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],"claimed_c":64,"d":4,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,-2,2,0,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,0,-2,2,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0]],"claimed_c":62,"d":5,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,-2,2,0,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,0,-2,2,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],"claimed_c":60,"d":6,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,-2,2,0,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,0,-2,2,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0]],"claimed_c":58,"d":7,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],"claimed_c":56,"d":8,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2]],"claimed_c":56,"d":9,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2]],"claimed_c":56,"d":10,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2]],"claimed_c":56,"d":11,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2]],"claimed_c":56,"d":12,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0]],"claimed_c":56,"d":13,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0]],"claimed_c":56,"d":14,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2]],"claimed_c":56,"d":15,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2]],"claimed_c":56,"d":16,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,2,0]],"claimed_c":56,"d":17,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,2,0],[0,0,0,0,2,2,0,0]],"claimed_c":56,"d":18,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,2,0],[0,0,0,0,2,2,0,0],[0,0,0,2,0,-2,0,0]],"claimed_c":56,"d":19,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,2,0],[0,0,0,0,2,2,0,0],[0,0,0,2,0,-2,0,0],[0,0,0,2,0,0,-2,0]],"claimed_c":56,"d":20,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,2,0],[0,0,0,0,2,2,0,0],[0,0,0,2,0,-2,0,0],[0,0,0,2,0,0,-2,0],[0,0,0,2,0,0,0,-2]],"claimed_c":56,"d":21,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,2,0],[0,0,0,0,2,2,0,0],[0,0,0,2,0,-2,0,0],[0,0,0,2,0,0,-2,0],[0,0,0,2,0,0,0,-2],[0,0,0,2,0,0,0,2]],"claimed_c":56,"d":22,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,2,0],[0,0,0,0,2,2,0,0],[0,0,0,2,0,-2,0,0],[0,0,0,2,0,0,-2,0],[0,0,0,2,0,0,0,-2],[0,0,0,2,0,0,0,2],[0,0,0,2,0,0,2,0]],"claimed_c":56,"d":23,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]}, +{"D":[[1,-1,-1,-1,-1,-1,-1,1],[2,2,0,0,0,0,0,0],[-2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0],[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0],[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0],[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,-2],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,2,0],[0,0,0,0,2,2,0,0],[0,0,0,2,0,-2,0,0],[0,0,0,2,0,0,-2,0],[0,0,0,2,0,0,0,-2],[0,0,0,2,0,0,0,2],[0,0,0,2,0,0,2,0],[0,0,0,2,0,2,0,0]],"claimed_c":56,"d":24,"terms":[[[1,-1,-1,-1,-1,-1,-1,1],[-2,2,0,0,0,0,0,0]],[[2,2,0,0,0,0,0,0],[0,-2,2,0,0,0,0,0]],[[-2,2,0,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1]],[[0,-2,2,0,0,0,0,0],[2,2,0,0,0,0,0,0]],[[0,0,-2,2,0,0,0,0],[0,0,0,-2,2,0,0,0]],[[0,0,0,-2,2,0,0,0],[0,0,-2,2,0,0,0,0]],[[0,0,0,0,-2,2,0,0],[0,0,0,0,0,-2,2,0]],[[0,0,0,0,0,-2,2,0],[0,0,0,0,-2,2,0,0]]]} + ] +} diff --git a/research/p104-gram-class-exact-floor/verify.py b/research/p104-gram-class-exact-floor/verify.py new file mode 100644 index 0000000000..791b660727 --- /dev/null +++ b/research/p104-gram-class-exact-floor/verify.py @@ -0,0 +1,428 @@ +#!/usr/bin/env python3 +"""Exact finite evidence for the E8 Gram-class floor in README.md. + +Standard library only. Supports and all design prices use integer dot products +and binary submatrix ranks. The ray census supplies the finite data in the proof. +""" +import itertools +import json +import os +from fractions import Fraction +from math import gcd + +HERE = os.path.dirname(os.path.abspath(__file__)) + + +DATA = os.path.join(HERE, "data", "designs.json") + + +def require(cond, msg): + # Not `assert`, so the checks survive python -O. + if not cond: + raise SystemExit("FAIL: " + msg) + + +def ok(name, detail=""): + print("PASS %s%s" % (name, (": " + detail) if detail else "")) + + +def parity(x): + return bin(x).count("1") & 1 + + +def f2_rank(rows): + basis = [] + for x in rows: + for b in basis: + x = min(x, x ^ b) + if x: + basis.append(x) + return len(basis) + + +def f2_inverse(rows, n): + """Inverse of an n x n F2 matrix given as n row bit-masks.""" + aug = [(rows[i], 1 << i) for i in range(n)] + for c in range(n): + piv = next((i for i in range(c, n) if (aug[i][0] >> c) & 1), None) + require(piv is not None, "singular F2 matrix") + aug[c], aug[piv] = aug[piv], aug[c] + for i in range(n): + if i != c and (aug[i][0] >> c) & 1: + aug[i] = (aug[i][0] ^ aug[c][0], aug[i][1] ^ aug[c][1]) + return [aug[i][1] for i in range(n)] + + +def det_q(m): + """Exact determinant of an integer matrix (Bareiss fraction-free elimination).""" + n = len(m) + a = [[int(x) for x in row] for row in m] + sign, prev = 1, 1 + for k in range(n - 1): + if a[k][k] == 0: + sw = next((i for i in range(k + 1, n) if a[i][k] != 0), None) + if sw is None: + return 0 + a[k], a[sw] = a[sw], a[k] + sign = -sign + for i in range(k + 1, n): + for j in range(k + 1, n): + numerator = a[i][j] * a[k][k] - a[i][k] * a[k][j] + require(numerator % prev == 0, "exact Bareiss division") + a[i][j] = numerator // prev + prev = a[k][k] + return sign * a[n - 1][n - 1] + + +def rank_q(vectors): + """Exact rank over Q of integer vectors (fraction-free elimination with gcd reduction).""" + m = [[int(x) for x in v] for v in vectors] + rk = 0 + for c in range(len(m[0]) if m else 0): + piv = next((r for r in range(rk, len(m)) if m[r][c] != 0), None) + if piv is None: + continue + m[rk], m[piv] = m[piv], m[rk] + for r in range(len(m)): + if r != rk and m[r][c] != 0: + a, b = m[rk][c], m[r][c] + row = [a * x - b * y for x, y in zip(m[r], m[rk])] + g = 0 + for x in row: + g = gcd(g, x) + m[r] = [x // g for x in row] if g > 1 else row + rk += 1 + return rk + + +def canon(v): + for x in v: + if x > 0: + return tuple(v) + if x < 0: + return tuple(-y for y in v) + raise ValueError("zero vector") + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +class Model: + """120 root lines of E8 in doubled coordinates (norm 8; <,>/4 in {0,+-1,+-2}).""" + + def __init__(self): + roots = [] + for i in range(8): + for j in range(i + 1, 8): + for si in (2, -2): + for sj in (2, -2): + v = [0] * 8 + v[i], v[j] = si, sj + roots.append(tuple(v)) + for signs in itertools.product((1, -1), repeat=8): + if signs.count(-1) % 2 == 0: + roots.append(tuple(signs)) + require(len(roots) == 240, "240 roots") + self.lines = sorted({canon(v) for v in roots}) + require(len(self.lines) == 120, "120 root lines") + self.index = {v: i for i, v in enumerate(self.lines)} + n = 120 + self.n = n + self.ip = [[dot(self.lines[p], self.lines[q]) for q in range(n)] for p in range(n)] + for p in range(n): + for q in range(n): + require(self.ip[p][q] % 4 == 0 and abs(self.ip[p][q]) <= 8, "ip/4 in {0,+-1,+-2}") + self.nrow = [0] * n + for p in range(n): + b = 0 + for q in range(n): + if (self.ip[p][q] // 4) % 2 == 0: + b |= 1 << q + self.nrow[p] = b + self.set_labels() + + def set_labels(self): + """Factor the rank-nine symmetric mask through a nonsingular block.""" + n = self.n + # Independent rows of a symmetric matrix select a nonsingular principal block. + basis, rows_idx = [], [] + for p in range(n): + x = self.nrow[p] + for b in basis: + x = min(x, x ^ b) + if x: + basis.append(x) + rows_idx.append(p) + self.rank_n = len(rows_idx) + k = self.rank_n + self.label = [] + for p in range(n): + x = 0 + for t, q in enumerate(rows_idx): + if (self.nrow[p] >> q) & 1: + x |= 1 << t + self.label.append(x) + block = [] + for a in rows_idx: + r = 0 + for t, q in enumerate(rows_idx): + if (self.nrow[a] >> q) & 1: + r |= 1 << t + block.append(r) + self.G = f2_inverse(block, k) # row masks of the inverse Gram form + + # --- supports and prices ------------------------------------------------- + def top(self, u, deleted=()): + """Lines of P not orthogonal to u (u an integer 8-vector).""" + dele = set(deleted) + return [p for p in range(self.n) if p not in dele and dot(self.lines[p], u) != 0] + + def price(self, u, w, deleted=()): + s = self.top(u, deleted) + t = self.top(w, deleted) + mask = 0 + for q in t: + mask |= 1 << q + return f2_rank([self.nrow[p] & mask for p in s]) + + def span_dim(self, lines_subset): + return f2_rank([self.label[p] for p in lines_subset]) + + def deficiency(self, u, deleted=()): + """a(u; D) = 9 - dim span of labels of T(u) minus D.""" + return self.rank_n - self.span_dim(self.top(u, deleted)) + + def line_of(self, v): + return self.index[canon(v)] + + def design_cost(self, deleted_lines, terms): + """Exact (c, prices, det M) of a Gram-class design on P = lines minus D.""" + dele = set(deleted_lines) + prices = [self.price(u, w, dele) for (u, w) in terms] + m = [[0] * 8 for _ in range(8)] + for (u, w) in terms: + for i in range(8): + for j in range(8): + m[i][j] += u[i] * w[j] + return sum(prices), prices, det_q(m) + + +def self_checks(M): + n = M.n + require(M.rank_n == 9, "rank_F2 N = 9") + # labels reproduce N: N[p,q] = label(p)^T G label(q) + for p in range(n): + gp = 0 + for i in range(9): + if parity(M.G[i] & M.label[p]): + gp |= 1 << i + for q in range(n): + bit = parity(gp & M.label[q]) + require(bit == ((M.nrow[p] >> q) & 1), "N = L G L^T at (%d,%d)" % (p, q)) + ok("e8-model", "120 lines, rank_F2 N = 9, N = L G L^T on all 14400 pairs") + + +SIMPLE = [ + None, + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + (0, -2, 2, 0, 0, 0, 0, 0), + (0, 0, -2, 2, 0, 0, 0, 0), + (0, 0, 0, -2, 2, 0, 0, 0), + (0, 0, 0, 0, -2, 2, 0, 0), + (0, 0, 0, 0, 0, -2, 2, 0), +] + + +def cartan_inverse(): + c = [[dot(SIMPLE[i], SIMPLE[j]) // 4 for j in range(1, 9)] for i in range(1, 9)] + # Bourbaki E8 Cartan matrix: chain 1-3-4-5-6-7-8 with node 2 on node 4 + edges = {(1, 3), (3, 4), (4, 5), (5, 6), (6, 7), (7, 8), (2, 4)} + for i in range(1, 9): + for j in range(1, 9): + want = 2 if i == j else (-1 if (i, j) in edges or (j, i) in edges else 0) + require(c[i - 1][j - 1] == want, "Cartan entry (%d,%d)" % (i, j)) + # exact inverse by Gauss-Jordan over the rationals + a = [[Fraction(c[i][j]) for j in range(8)] + [Fraction(1 if i == j else 0) for j in range(8)] + for i in range(8)] + for col in range(8): + piv = next(r for r in range(col, 8) if a[r][col] != 0) + a[col], a[piv] = a[piv], a[col] + pv = a[col][col] + a[col] = [x / pv for x in a[col]] + for r in range(8): + if r != col and a[r][col] != 0: + f = a[r][col] + a[r] = [x - f * y for x, y in zip(a[r], a[col])] + inv = [[a[i][8 + j] for j in range(8)] for i in range(8)] + for i in range(8): + for j in range(8): + require(inv[i][j].denominator == 1, "E8 Cartan inverse is integral (det 1)") + return [[int(x) for x in row] for row in inv] + + +def fundamental_weights(cinv): + ws = [] + for i in range(8): + v = [0] * 8 + for j in range(8): + for t in range(8): + v[t] += cinv[i][j] * SIMPLE[j + 1][t] + ws.append(tuple(v)) + return ws + + +def wht512(cnt): + a = list(cnt) + require(len(a) == 512, "nine-bit Walsh transform") + for stage in range(9): + h = 1 << stage + for i in range(0, 512, 2 * h): + for j in range(i, i + h): + x, y = a[j], a[j + h] + a[j], a[j + h] = x + y, x - y + return a + + +def census(M, weights): + """For each fundamental-weight ray: |T|, cost_1, cost_2. + + cost_a = |T| - max over codimension-a subspaces W of F2^9 of #{p in T: label(p) in W} + = the fewest lines of T whose deletion can make the labels of T minus D fall in a + codimension-a subspace. Counted by characters: #{x in W} = (1/2^a) sum_{h in H} S[h]. + """ + rows = [] + for w in weights: + t = M.top(w) + cnt = [0] * 512 + for p in t: + cnt[M.label[p]] += 1 + s = wht512(cnt) + best1 = max(s[h] for h in range(1, 512)) + cost1 = len(t) - (len(t) + best1) // 2 + best2 = None + for h1 in range(1, 512): + for h2 in range(h1 + 1, 512): + h3 = h1 ^ h2 + if h3 <= h2: + continue + val = len(t) + s[h1] + s[h2] + s[h3] + if best2 is None or val > best2: + best2 = val + cost2 = len(t) - best2 // 4 + rows.append((len(t), cost1, cost2)) + return rows + + +PREDECESSOR_CENSUS = [ + (57, 1, 25), (78, 14, 42), (83, 27, 51), (92, 28, 56), + (97, 33, 61), (98, 35, 62), (104, 40, 68), (106, 43, 70), +] + + +def check_census(M): + cinv = cartan_inverse() + weights = fundamental_weights(cinv) + rows = census(M, weights) + require(sorted(rows) == PREDECESSOR_CENSUS, "census table %r" % (sorted(rows),)) + root_type = [i for i, r in enumerate(rows) if r[0] == 57] + require(len(root_type) == 1, "one ray type with |T| = 57") + theta = weights[root_type[0]] + require(canon(theta) in M.index, "the 57-type fundamental weight is a root") + require(root_type[0] == 7, "that weight is omega_8, the highest root") + other = [r for i, r in enumerate(rows) if i != root_type[0]] + require(all(r[1] >= 14 for r in other), "cost_1 >= 14 off the root type") + require(rows[root_type[0]][1] == 1 and rows[root_type[0]][2] == 25, "root type costs (1, 25)") + ok("ray-census", "(|T|, cost_1, cost_2) = %s; only the root type has cost_1 < 14, cost_2 >= 25 everywhere" + % (sorted(rows),)) + + +def scalar_matrix(terms): + m = [[0] * 8 for _ in range(8)] + for (u, w) in terms: + for i in range(8): + for j in range(8): + m[i][j] += u[i] * w[j] + lam = m[0][0] + return lam != 0 and all(m[i][j] == (lam if i == j else 0) for i in range(8) for j in range(8)) + + +def check_root_hyperplanes(model): + """Check every label hyperplane on every root support, with no sampling.""" + for r in range(120): + support = model.top(model.lines[r]) + orthogonal = [model.lines[p] for p in range(120) if model.ip[p][r] == 0] + require(len(support) == 57 and len(orthogonal) == 63, "root support sizes") + require(rank_q(orthogonal) == 7, "orthogonal roots span r-perp") + singleton = [] + other_sizes = [] + for h in range(1, 512): + outside = [p for p in support if parity(model.label[p] & h)] + if outside == [r]: + singleton.append(h) + else: + other_sizes.append(len(outside)) + require(len(singleton) == 1, "unique hyperplane deleting just r") + require(min(other_sizes) == 24, "all other hyperplanes need at least 24 deletions") + require(model.deficiency(model.lines[r], [r]) == 1, "deleted root loses one dimension") + ok("root-hyperplanes", "120 roots x 511 hyperplanes; unique singleton {r}, other costs >= 24; orthogonal rank 7") + + +def read_designs(model): + with open(DATA, encoding="utf-8") as stream: + data = json.load(stream) + designs = data["designs"] + require(len(designs) == 25, "one design for every d in 0..24") + results = {} + for row in designs: + d = row["d"] + require(type(d) is int and 0 <= d <= 24 and d not in results, "distinct valid d") + require(len(row["D"]) == d and len(row["terms"]) == 8, "certificate sizes") + vectors = row["D"] + [v for pair in row["terms"] for v in pair] + require(all(len(v) == 8 and all(type(x) is int for x in v) for v in vectors), "integer 8-vectors") + deleted = [model.line_of(v) for v in row["D"]] + require(len(deleted) == len(set(deleted)) == d, "distinct deleted lines") + terms = [(tuple(u), tuple(w)) for u, w in row["terms"]] + require(len(terms) == 8, "eight terms") + require(all(len(u) == len(w) == 8 and any(u) and any(w) for u, w in terms), "term dimensions") + cost, prices, determinant = model.design_cost(deleted, terms) + expected = 72 - 2 * min(d, 8) + require(cost == row["claimed_c"] == expected, "exact attained floor") + require(determinant != 0, "invertible M") + results[d] = (cost, prices, determinant) + ok("designs", "25 exact certificates: c = 72 - 2 min(d,8), d=0..24, all det M != 0") + return designs, results + + +def check_controls(model, designs, results): + terms = [(tuple(u), tuple(w)) for u, w in designs[8]["terms"]] + simple = [model.line_of(SIMPLE[k]) for k in range(1, 9)] + require(set(simple) == {model.line_of(v) for v in designs[8]["D"]}, "d=8 deletes the simple roots") + require(results[8] == (56, [7] * 8, 65536), "d=8 determinant and prices") + require(not scalar_matrix(terms), "the example has nonscalar M") + require(112 - results[8][0] == 56 and results[8][0] < 72 - 8, "c >= 72-d is false here") + same = [(SIMPLE[k], SIMPLE[k]) for k in range(1, 9)] + cost, prices, determinant = model.design_cost(simple, same) + require(cost == 64 and prices == [8] * 8 and determinant != 0, "identity pairing costs 64") + cost, prices, determinant = model.design_cost([], terms) + require(cost == 72 and prices == [9] * 8 and determinant != 0, "restoring D costs 72") + singular = [(SIMPLE[1], SIMPLE[1])] * 8 + require(model.design_cost([], singular)[2] == 0, "singular repeated terms rejected") + require(rank_q([SIMPLE[1], SIMPLE[1]]) == 1, "parallel deficient directions cannot enter a basis twice") + ok("controls", "identity pairing 64; no deletions 72; singular terms detected; d=8 M is nonscalar") + + +def main(): + model = Model() + self_checks(model) + check_census(model) + check_root_hyperplanes(model) + designs, results = read_designs(model) + check_controls(model, designs, results) + print("PASS_P104_GRAM_CLASS_EXACT_FLOOR designs=25 root_hyperplanes=61320 no_new_kappa") + + +if __name__ == "__main__": + main()