From a47e7e5b626c8dfde099b6d8aaab9b650e9ca30b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 08:04:16 +0000 Subject: [PATCH] feat(research): exclude the extremal E8 96-line complement --- research/e8-pseudoforest-line-sets/README.md | 198 +++++++++++++++ .../e8-pseudoforest-line-sets/SOURCES.json | 30 +++ research/e8-pseudoforest-line-sets/TASK.json | 81 ++++++ .../e8-pseudoforest-line-sets/VERIFY.json | 40 +++ research/e8-pseudoforest-line-sets/verify.py | 234 ++++++++++++++++++ 5 files changed, 583 insertions(+) create mode 100644 research/e8-pseudoforest-line-sets/README.md create mode 100644 research/e8-pseudoforest-line-sets/SOURCES.json create mode 100644 research/e8-pseudoforest-line-sets/TASK.json create mode 100644 research/e8-pseudoforest-line-sets/VERIFY.json create mode 100644 research/e8-pseudoforest-line-sets/verify.py diff --git a/research/e8-pseudoforest-line-sets/README.md b/research/e8-pseudoforest-line-sets/README.md new file mode 100644 index 0000000000..980d36bd5f --- /dev/null +++ b/research/e8-pseudoforest-line-sets/README.md @@ -0,0 +1,198 @@ +# A Hall obstruction in the extremal 96-line E8 complement + +The particular 96-line complement proposed in open question 1 of +[DreamingOfClouds's #6854](https://github.com/CrocSwap/integer-mult-bounds/pull/6854) +has no realisation of inner dimension `8k`, over any field and for any `k >= 1`. +It contains an explicit 14-line configuration with six pair lines supported on +five gauge coordinates. The inherited Hall rank argument gives `6k <= 5k`. + +This is a scoped written proof supported by an exact finite certificate of the +configuration. It answers the concrete complement case. Existence for other +96-line sets remains open here. No new kappa, word, invoice or supplier is claimed. + +## Hypothesis and exact set + +Use the label pattern of #6846 and #6854. For each line `T` in a set `S` of the +120 E8 root lines, let `U_T, W_T` be `k by d` matrices over a field `F`. Require +`W_S U_T^T = 0` for distinct non-orthogonal root lines and require each +`W_T U_T^T` to be invertible. The two matrices may differ. Non-orthogonality is +defined by the real root coordinates, including when `F` has characteristic 2. +This pattern is a hypothesis, not a property proved for a physical program. + +Index the roots as in the pinned `p104-e8-rank8-closure/check.py`. First list the +roots `2 a e_i + 2 b e_j`, with `i < j` lexicographic and `a, b` in `(1,-1)`. +Then list the sign vectors in `(1,-1)^8` with an even number of minus signs. +Retain the first representative of each pair `r, -r`. Coordinates are doubled, +so every root has squared norm 8. Set + +```text +D24 = [0,1,2,3,12,13,14,15,24,25,34,35, + 36,37,38,39,40,41,44,45,46,47,50,51] +S96 = {0,...,119} minus D24. +K = [4,6,8,10,56,72,88,104]. +``` + +`K` is a forced-zero clique inside `S96`. For a line `t` outside `K`, let +`A_K(t)` be the positions of the members of `K` orthogonal to `t`. Positions +are numbered 0 through 7, in the displayed order of `K`. The following lines +are also in `S96`. + +| Pair line `t` | `A_K(t)` | +|---|---| +| 90 | {2,5} | +| 92 | {1,5} | +| 96 | {0,5} | +| 106 | {2,4} | +| 108 | {1,4} | +| 112 | {0,4} | + +Their supports form `K_{2,3}` with parts `{4,5}` and `{0,1,2}`. Two of these +lines sharing a position are forced zero and share exactly one position. +The coordinate construction and every entry of this table are checked directly. + +## Proof + +The gauge and rank-sum mechanism below are due to DreamingOfClouds's #6846 and +#6854. The new step is the explicit configuration in `S96`, where the 13-line +family of #6854 is absent. No novelty is claimed for Hall's condition or the +general star-configuration method. + +Suppose a realisation with `d = 8k` exists. Multiply each block row `W_T` on the +left by `(W_T U_T^T)^{-1}`. This preserves all required zeros and makes every +diagonal block `I_k`. Stack the eight gauge rows as square matrices `W_K, U_K`. +They satisfy `W_K U_K^T = I_{8k}`, so both are invertible. Replacing +`U_T` by `U_T U_K^{-1}` and `W_T` by `W_T U_K^T` preserves every pairing and +makes `U_K = W_K = I_{8k}`. + +Divide the coordinates into eight blocks of width `k`. For a line `T` outside +`K`, a forced zero with the gauge line at position `c` now says both +`U_T[c] = 0` and `W_T[c] = 0`. Thus these matrices are supported on `A_K(T)`. + +Let `O` be the six displayed pair lines. For each of the five used coordinates +`c`, stack the matrices `W_T[c]`, and separately `U_T[c]`, over the lines +`T` whose supports contain `c`. The product of these two stacks is block +diagonal. Its off-diagonal blocks vanish because two such lines are forced +zero and their supports meet only at `c`. It factors through `k` dimensions, +so + +```text +sum over T incident to c of rank(W_T[c] U_T[c]^T) <= k. +``` + +For each `T` in `O`, its diagonal block is the sum of its two coordinate +products and is invertible. Rank subadditivity gives + +```text +k <= sum over c in A_K(T) of rank(W_T[c] U_T[c]^T). +``` + +Summing over six lines and then over their five used coordinates gives +`6k <= 5k`, impossible for `k >= 1`. Restriction of a realisation on `S96` +to `K union O` would give the forbidden realisation. This proves the claim. + +## Finite geometry and controls + +The verifier enumerates all **192** forced-zero eight-cliques contained in +`S96`. At each gauge, the pair-line graph of `S96` is exactly `K_{4,4}`. +In particular it contains `K_{2,3}`, but no `K_4` minus an edge. Every 13-line +witness of #6854 consists of a gauge plus pair lines forming `K_4` minus an +edge. Thus this census also explains why that family misses `S96`. + +For the displayed `K_{2,3}`, the verifier enumerates all 64 subsets of its six +edges and searches at most 64 endpoint assignments per subset. Exactly the 63 proper +subsets admit distinct serving coordinates. Giving each pair line the unit +vector at its serving coordinate and each gauge line its own unit vector +produces `U = W` with unit diagonal and the required zeros over the integers. +The checker multiplies these vectors exactly. Tensoring with `I_k` gives a +realisation in dimension `8k` over every field for each such proper subset. +Consequently the displayed obstruction disappears after removing any one of +its six pair lines while retaining `K`. No minimum size over all obstructions +is claimed. + +This endpoint test has the standard pseudoforest interpretation. A simple +graph admits an injection from edges to their incident vertices exactly when +every component has at most as many edges as vertices. The 64-subset check +compares both criteria. Necessity follows by counting within a component. +For sufficiency, root each tree and assign its edges to their child vertices; +in a unicyclic component, also assign cycle edges cyclically to their heads. +The all-`k` negative claim comes from the written +rank proof, not from finite-field searches. + +Three rejecting controls detect a singular diagonal, a nonzero forced-zero +pair and an incomplete `K_{4,4}` fixture. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error -X dev research/e8-pseudoforest-line-sets/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e8-pseudoforest-line-sets +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e8-pseudoforest-line-sets --check-source-history +``` + +Any CPython 3.12 can replace the displayed interpreter. The terminal line is + +```text +PASS_E8_S96_HALL gauges=192 witness_lines=14 repair_subsets=63 no_new_kappa +``` + +Both registered commands run the full verifier, normally and with `-O`. +Explicit exceptions keep all checks active in both modes. The verifier reads +the predecessor's `D24` assignment as data after checking the source SHA256; +it does not execute or replay the predecessor. Exact source commits, blobs +and hashes are in [SOURCES.json](SOURCES.json). + +## Limits and implementation bounds + +The conclusion concerns this specific complement, not every 96-line set or +a new universal cardinality threshold. The minimum hitting set for a larger +obstruction family is not computed. No largest realisable line set is claimed. +Ranks strictly between `8k` and `9k`, other masks, physical words, prices and +the full multiplication theorem are outside the result. No Lean, Docker, +solver or selected-frontier replay is required or claimed. + +The checker uses no recursion, network, subprocess, file writes or mutable +cache. Fixed dimensions bound the root construction by 240 roots and the +mask by 120 squared entries. Clique enumeration has a 2,000,000-pop limit, +a 960-entry worklist cap, depth eight and a 10,000-clique storage cap; exhaustion +fails explicitly. Endpoint matching has at most 64 choices for each of 64 +subsets. Every function is shorter than 60 lines. The registered warning and +development modes provide the available Python diagnostics; no external +static analyzer is claimed. + +Power of Ten rule 3 deviation: CPython allocates objects during this one-shot +checker. The fixed domains and explicit worklist/storage caps bound live data; +all data is released at process exit. Normal and optimized replays run within +these caps without leaving runtime files. A future steady-operation native +implementation would need preallocated storage to remove this deviation. + +## Sources, scope and credit + +The package was produced by Nick Petalas. Credit DreamingOfClouds for #6846, +the label pattern, Hall rank argument, explicit `D24` and open question in +#6854. The general window and star bounds of #6933 and open #7114 are prior +work. This package adds the explicit `S96` geometry and its concrete +14-line witness; it does not improve those general bounds. The related #7129 +studies stronger bounds on other star configurations and is not used here. + +The base is `e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8. +The changed scope of `complex-rank-shape-decoder` is recorded in [TASK.json](TASK.json). +This is a side result about a possible label set, not a decoder or paid-budget +gain. The selected record is historical provenance and is unchanged. +The advance [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19529936) +named the 96-line question. The delivered scope is its specified complement; +no global hitting-set optimum or largest construction is supplied. +New work is Apache-2.0. + +## Open next questions + +1. Can another 96-line set avoid both the 13-line family and these pair-line + Hall deficiencies? This is the unsettled part of #6854's question. First + step: classify the 24-line hitting sets of that family and inspect one + representative complement from each class. The classification is not + provided here. +2. What is the largest subset of the 120 E8 lines with an `8k` realisation + under this mask? Start with explicit candidate subsets and inspect all + gauges they contain. Passing every pair-line Hall condition is only a + necessary test and does not construct a realisation. diff --git a/research/e8-pseudoforest-line-sets/SOURCES.json b/research/e8-pseudoforest-line-sets/SOURCES.json new file mode 100644 index 0000000000..5446093841 --- /dev/null +++ b/research/e8-pseudoforest-line-sets/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-e8-rank8-closure/check.py", + "usage": "input", + "git_blob": "e072fad67d3a6f899dcad8e892d41de2c8f39db2", + "sha256": "6c9c13133942d811449a76a3489886cd30a96eee38a041105f33a104453e8a00" + }, + { + "path": "research/p104-e8-rank8-closure/README.md", + "usage": "provenance", + "git_blob": "bb5b6d3449b19439a73cf52d710fa362de420d40", + "sha256": "b0fe020b05024c6a9843d1815e9fa8315fd499c406385431a13242c7fbf92b86" + } + ] +} diff --git a/research/e8-pseudoforest-line-sets/TASK.json b/research/e8-pseudoforest-line-sets/TASK.json new file mode 100644 index 0000000000..4d3a58d4af --- /dev/null +++ b/research/e8-pseudoforest-line-sets/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "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": "Exclude the particular 96-line complement of the pinned D24 at inner dimension 8k under the complex label pattern, by an explicit K2,3 Hall witness; enumerate its gauge pair-line graphs.", + "scope_change_reason": "The assigned question is the concrete complement case of open question 1 in DreamingOfClouds PR6854. The card concerns a complete signed decoder invoice; this package is instead a label-set side result and does not compute such an invoice.", + "bottleneck_link": "A side result on which E8 line sets can support labels of width 8k. It removes one proposed 96-line candidate; it provides no legal decoder, paid supplier or kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified scoped improvement, within about 60 minutes. Do not seek a global hitting-set optimum or a larger realisation after the concrete complement is excluded.", + "outcome": "negative-result", + "evidence": "README.md gives the all-field, all-k Hall rank proof. verify.py checks the explicit 14-line witness, all 192 S96 gauges with pair graph K4,4, all 64 subsets of its six pair lines (63 exact integer repairs), source integrity and three rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a different 96-line set avoid both the F13 family and pair-line Hall deficiencies?", + "why_it_matters": "The supplied result excludes only the specific complement proposed in PR6854, not all sets of size 96.", + "first_step": "Classify the 24-line hitting sets of F13 and inspect representative complements.", + "blocked_by": "No classification of those hitting sets is supplied here." + }, + { + "question": "What is the largest E8 line subset admitting an 8k realisation under this mask?", + "why_it_matters": "It determines the realizability threshold rather than the threshold for one obstruction family.", + "first_step": "Construct an explicit candidate and inspect every contained gauge for pair-line Hall deficiencies.", + "blocked_by": "Passing these necessary tests does not construct a realization; general U and W remain unconstrained beyond the mask." + } + ] +} diff --git a/research/e8-pseudoforest-line-sets/VERIFY.json b/research/e8-pseudoforest-line-sets/VERIFY.json new file mode 100644 index 0000000000..e3ba8f1f88 --- /dev/null +++ b/research/e8-pseudoforest-line-sets/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-e8-rank8-closure/check.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source-bound D24, exact K2,3 witness and Hall hypotheses, all 192 S96 gauge pair graphs K4,4, 64 subset controls with 63 integer patterns, and three rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete finite certificate and controls with optimized Python; all explicit invariant checks remain active." + } + ] +} diff --git a/research/e8-pseudoforest-line-sets/verify.py b/research/e8-pseudoforest-line-sets/verify.py new file mode 100644 index 0000000000..d429a07f85 --- /dev/null +++ b/research/e8-pseudoforest-line-sets/verify.py @@ -0,0 +1,234 @@ +#!/usr/bin/env python3 +"""Check the explicit Hall obstruction in the extremal 96-line complement. + +Standard library only. No solver, predecessor execution, or file writes. +All contracts use exceptions and remain active under optimized Python. +""" + +import ast +import hashlib +import itertools +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SOURCE = HERE.parent / "p104-e8-rank8-closure" / "check.py" +SOURCE_SHA256 = "6c9c13133942d811449a76a3489886cd30a96eee38a041105f33a104453e8a00" +D24 = (0, 1, 2, 3, 12, 13, 14, 15, 24, 25, 34, 35, + 36, 37, 38, 39, 40, 41, 44, 45, 46, 47, 50, 51) +GAUGE = (4, 6, 8, 10, 56, 72, 88, 104) +WITNESS = (90, 92, 96, 106, 108, 112) +SUPPORTS = ((2, 5), (1, 5), (0, 5), (2, 4), (1, 4), (0, 4)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def e8_lines(): + """Doubled E8 coordinates, with the ordering of the pinned source.""" + roots = [] + for i, j in itertools.combinations(range(8), 2): + for a, b in itertools.product((2, -2), repeat=2): + row = [0] * 8 + row[i], row[j] = a, b + roots.append(tuple(row)) + roots.extend(row for row in itertools.product((1, -1), repeat=8) + if row.count(-1) % 2 == 0) + require(len(roots) == 240, "root count") + require(all(dot(row, row) == 8 for row in roots), "root norm") + seen, lines = set(), [] + for row in roots: + if row not in seen: + seen.update((row, tuple(-x for x in row))) + lines.append(row) + require(len(lines) == 120, "line count") + return lines + + +def read_deleted_set(): + require(SOURCE.stat().st_size <= 1_048_576, "source size bound") + data = SOURCE.read_bytes() + require(hashlib.sha256(data).hexdigest() == SOURCE_SHA256, + "predecessor source hash") + tree = ast.parse(data) + values = [ast.literal_eval(node.value) for node in tree.body + if isinstance(node, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == "D24" + for t in node.targets)] + require(values == [list(D24)], "pinned D24 assignment") + require(len(set(D24)) == 24 and set(D24) <= set(range(120)), "D24 domain") + return set(range(120)) - set(D24) + + +def eight_cliques(no, vertices): + """Enumerate increasing cliques by bounded iterative depth-first search.""" + require(len(no) == 120 and len(vertices) <= 120, "graph domain") + neighbors = [sum(1 << j for j in vertices if no[i][j]) for i in range(120)] + stack = [((), sum(1 << v for v in vertices))] + result = [] + for _ in range(2_000_000): + if not stack: + return result + clique, candidates = stack.pop() + if len(clique) == 8: + result.append(clique) + require(len(result) <= 10_000, "clique storage bound") + continue + if len(clique) + candidates.bit_count() < 8: + continue + for _ in range(120): + if not candidates: + break + bit = candidates & -candidates + vertex = bit.bit_length() - 1 + candidates ^= bit + stack.append((clique + (vertex,), candidates & neighbors[vertex])) + require(len(stack) <= 960, "depth-first worklist bound") + raise ValueError("clique enumeration exhausted its iteration bound") + + +def supports(gauge, no): + return {t: tuple(i for i, c in enumerate(gauge) if not no[t][c]) + for t in range(120) if t not in gauge} + + +def components(edges): + require(len(edges) <= 28, "edge domain") + require(all(len(e) == 2 and 0 <= e[0] < e[1] < 8 for e in edges), + "edge endpoints") + parent = list(range(8)) + for a, b in edges: + old, new = parent[b], parent[a] + parent = [new if p == old else p for p in parent] + return [(sum(p == root for p in parent), + sum(parent[a] == root for a, _ in edges)) + for root in sorted(set(parent))] + + +def pseudoforest(edges): + return all(e <= v for v, e in components(edges)) + + +def endpoint_matching(edges): + """Exhaust all at most 64 endpoint choices for the six-line fixture.""" + require(len(edges) <= 6, "matching enumeration domain") + for choices in itertools.product(*edges): + if len(set(choices)) == len(choices): + return choices + return None + + +def vectors_fit(vectors, no): + vertices = tuple(vectors) + require(len(vertices) <= 14, "fixture vector domain") + require(all(len(row) == 8 for row in vectors.values()), "vector width") + return (all(dot(vectors[t], vectors[t]) == 1 for t in vertices) + and all(not no[s][t] or dot(vectors[s], vectors[t]) == 0 + for s, t in itertools.combinations(vertices, 2))) + + +def check_fixture(no, live): + require(set(GAUGE + WITNESS) <= live, "fixture inside S96") + require(len(set(GAUGE + WITNESS)) == 14, "fixture distinct lines") + require(all(no[s][t] for s, t in itertools.combinations(GAUGE, 2)), + "gauge is a forced-zero clique") + masks = supports(GAUGE, no) + require(tuple(masks[t] for t in WITNESS) == SUPPORTS, "fixture support table") + for s, t in itertools.combinations(WITNESS, 2): + shared = set(masks[s]) & set(masks[t]) + require(len(shared) <= 1, "distinct pair supports") + require(not shared or no[s][t], "shared-coordinate forced zero") + vertices = set().union(*(set(edge) for edge in SUPPORTS)) + require(len(vertices) == 5 and len(SUPPORTS) == 6, "6k versus 5k") + require(not pseudoforest(SUPPORTS), "Hall deficiency") + require(endpoint_matching(SUPPORTS) is None, "scalar Hall deficiency") + + +def check_repairs(no): + """All 64 pair-line subsets; construct exact integer patterns when feasible.""" + basis = [tuple(int(i == j) for i in range(8)) for j in range(8)] + feasible = 0 + for mask in range(1 << 6): + indices = [i for i in range(6) if mask >> i & 1] + edges = [SUPPORTS[i] for i in indices] + choice = endpoint_matching(edges) + require((choice is not None) == pseudoforest(edges), "Hall control") + require((choice is not None) == (mask != 63), "minimal obstruction") + if choice is not None: + vectors = {t: basis[i] for i, t in enumerate(GAUGE)} + vectors.update({WITNESS[i]: basis[c] + for i, c in zip(indices, choice, strict=True)}) + require(vectors_fit(vectors, no), "integer repair pattern") + feasible += 1 + require(feasible == 63, "repair subset count") + vectors = {t: basis[i] for i, t in enumerate(GAUGE)} + vectors[GAUGE[0]] = (0,) * 8 + require(not vectors_fit(vectors, no), "singular diagonal control") + vectors[GAUGE[0]] = basis[1] + require(not vectors_fit(vectors, no), "forced-zero violation control") + return feasible + + +def is_k44(edges): + if len(edges) != 16 or not all(e == 16 for _, e in components(edges)): + return False + adjacency = [set() for _ in range(8)] + for a, b in edges: + adjacency[a].add(b) + adjacency[b].add(a) + if any(len(row) != 4 for row in adjacency): + return False + right = adjacency[0] + left = set(range(8)) - right + return (len(left) == len(right) == 4 + and all(adjacency[v] == right for v in left) + and all(adjacency[v] == left for v in right)) + + +def check_live_gauges(no, live): + gauges = eight_cliques(no, live) + require(len(gauges) == 192, "S96 eight-clique count") + require(GAUGE in gauges, "explicit gauge enumerated") + for gauge in gauges: + masks = supports(gauge, no) + require(Counter(map(len, masks.values())) == {2: 28, 5: 56, 6: 28}, + "outside-line support sizes") + pairs = {t: edge for t, edge in masks.items() if len(edge) == 2} + require(len(set(pairs.values())) == 28, "unique pair lines") + edges = [edge for t, edge in pairs.items() if t in live] + require(is_k44(edges), "S96 pair graph is K4,4") + for s, t in itertools.combinations(pairs, 2): + if set(pairs[s]) & set(pairs[t]): + require(no[s][t], "pair-line star mask") + require(not is_k44(edges[:-1]), "incomplete K4,4 control") + return len(gauges) + + +def main(): + live = read_deleted_set() + require(len(live) == 96, "live line count") + lines = e8_lines() + no = [[i != j and dot(lines[i], lines[j]) != 0 for j in range(120)] + for i in range(120)] + require(all(dot(lines[i], lines[j]) in (0, 4, -4) + for i, j in itertools.combinations(range(120), 2)), "root pairs") + check_fixture(no, live) + print("fixture: K =", list(GAUGE), "pair lines =", list(WITNESS)) + print("supports:", list(SUPPORTS), "; Hall contradiction: 6k <= 5k") + feasible = check_repairs(no) + gauges = check_live_gauges(no, live) + print("S96: 192 eight-cliques; every pair-line graph is K4,4") + print("controls: 63 proper pair-line subsets have exact integer patterns;") + print("singular diagonal, forced-zero violation and incomplete K4,4 rejected") + print(f"PASS_E8_S96_HALL gauges={gauges} witness_lines=14 " + f"repair_subsets={feasible} no_new_kappa") + + +if __name__ == "__main__": + main()