From 277ff2c230937460aae5d2b19d83be37d0d60a5b Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Tue, 3 Nov 2026 10:14:29 +0000
Subject: [PATCH] feat(research): prove root-low E8 basis tariff 78

---
 research/e8-root-low-plane/PROOF.md     | 167 +++++++++++++++
 research/e8-root-low-plane/README.md    | 100 +++++++++
 research/e8-root-low-plane/SOURCES.json |  36 ++++
 research/e8-root-low-plane/TASK.json    | 121 +++++++++++
 research/e8-root-low-plane/VERIFY.json  |  34 +++
 research/e8-root-low-plane/verify.py    | 272 ++++++++++++++++++++++++
 6 files changed, 730 insertions(+)
 create mode 100644 research/e8-root-low-plane/PROOF.md
 create mode 100644 research/e8-root-low-plane/README.md
 create mode 100644 research/e8-root-low-plane/SOURCES.json
 create mode 100644 research/e8-root-low-plane/TASK.json
 create mode 100644 research/e8-root-low-plane/VERIFY.json
 create mode 100644 research/e8-root-low-plane/verify.py

diff --git a/research/e8-root-low-plane/PROOF.md b/research/e8-root-low-plane/PROOF.md
new file mode 100644
index 0000000000..0db52efc82
--- /dev/null
+++ b/research/e8-root-low-plane/PROOF.md
@@ -0,0 +1,167 @@
+# A root-low correction plane has exact basis tariff 78
+
+Scoped proof and finite exact certificate produced by Nick Petalas.
+Apache-2.0. The fixed root/label model and the 29-neighbor opening credit
+conorholds' PR3755 and PR4052. No predecessor threshold or scientific
+checker is replayed as a deliverable.
+
+## 1. Fixed space and claim
+
+Let K be any field of characteristic zero. Use the following rational
+nine-coordinate realization of the 120 E8 root lines. Write R_x for the
+listed vectors, and r_x=R_x/3 for the norm-two representatives.
+
+- For 0<=i<j<=8, take R_x=3(e_i-e_j), with label
+  u_x=511 XOR 2^i XOR 2^j.
+- For each three-element subset A of {0,...,8}, take R_x with entry 2
+  on A and -1 elsewhere, with label u_x=sum_{i in A}2^i.
+
+The pairing on the binary nine-space is ordinary dot product. The labels
+are distinct and span that space. They give the dense COPY pairing used
+in PR4052. This is the A8 model from its retained geometry definitions.
+
+Fix v=(0,1) and a=(0,2), the first two pair roots. Their labels are
+u_v=508 and u_a=506. Their scalar inner product is one. Set
+
+```
+E_a(x) = r_x dot r_a = (R_x dot R_a)/9,
+C = span_K of the eight columns R_x[0],...,R_x[7],
+H_v = {x : u_v dot u_x = 0},
+e = delta_a,
+d = E_a restricted to H_v,
+g = d-2e,
+f = E_a-d,
+D = span_K(e,d) = span_K(e,g),
+S = C+D,                 T = span_K(e,g,f).
+```
+
+The code C has dimension eight and S has dimension ten. The correction d
+has exactly 29 nonzero entries. This is the natural root-low correction
+from PR4052's opening, supplemented by its own root coordinate. The
+quantifier here concerns this one fixed space, not every correction space
+on 29 neighbors.
+
+For q in K^120 let w(q) be the dimension over F2 of the labels at its
+nonzero scalar entries. The new result is the exact ordered minimum basis
+profile of S:
+
+```
+(1,7,7,9,9,9,9,9,9,9).
+```
+
+Every basis has sorted weights at least these values coordinate by
+coordinate, and a basis attains them. In particular its minimum linear
+bill is 78. More generally, for every nondecreasing tariff F on {1,...,9},
+the exact minimum is F(1)+2F(7)+7F(9). This includes every positive power
+tariff. The statement prices a basis; it is not a complete supplier invoice.
+
+## 2. Complete character-kernel certificate
+
+For a nonzero binary character z define
+
+```
+O_z = {x : z dot u_x = 1},
+K_z = {q in S : q vanishes on O_z}.
+```
+
+Use parameter coordinates (h_0,...,h_7,s,t), with
+q_x=sum_j R_x[j]h_j+s delta_a(x)+t d(x). The 120-by-10 matrix M of this
+map is injective. Each K_z is therefore the kernel of the submatrix of M
+on O_z. The complete exact table is:
+
+| Character condition | K_z | Number |
+| --- | --- | ---: |
+| z=508 | span(e,g) | 1 |
+| z=506 | span(g,f) | 1 |
+| z=505 | span(e,f) | 1 |
+| z=6 | span(g) | 1 |
+| z=3 | span(f) | 1 |
+| z dot 506=0, excluding 508 and 505 | span(e) | 253 |
+| Every remaining nonzero character | zero | 253 |
+
+These disjoint rows account for all 511 nonzero characters. The executable
+certificate constructs each integer submatrix and verifies the listed
+kernel by two exact methods:
+
+1. Rational elimination constructs its entire kernel and compares subspaces.
+2. Direct integer products show that the prescribed vectors vanish. A
+   separately implemented elimination modulo 101 proves matrix rank
+   10-dim(K_z). This is a rational rank lower bound; the displayed kernel
+   gives the matching upper bound. The prime is fixed and no random rank
+   inference is used.
+
+All matrices and displayed vectors are rational. The rational rank and
+kernel remain unchanged under extension to K, so this finite certificate
+proves the table over every characteristic-zero field. Positive
+characteristics are outside the claim.
+
+The pairwise disjoint supports of e,g,f have sizes 1,28,28. Exact binary
+elimination gives ranks 1,7,7 on the individual supports, rank eight on
+each two-support union, and rank nine on the three-support union. Since
+the supports are disjoint, nonzero scalar coefficients cannot cancel
+between them. Thus these ranks apply to every coefficient choice, not
+only to the displayed rational samples.
+
+## 3. The whole deficient locus and its span
+
+The binary pairing is nondegenerate. Hence w(q)<=8 if and only if there
+is a nonzero character z with q in K_z. The table proves
+
+```
+{q in S : w(q)<=8}
+  = span(e,g) union span(e,f) union span(g,f).
+```
+
+Every vector outside this union has weight nine, including a vector in T
+whose three coefficients are all nonzero. Within the union, the only
+nonzero weight below seven is the e-axis, of weight one. The g- and
+f-axes have weight seven. A vector with exactly two nonzero coefficients
+has weight eight.
+
+Writing V_k=span_K{q in S : w(q)<=k}, including zero, gives
+
+```
+dim V_0 = 0,
+dim V_k = 1 for k=1,...,6,
+dim V_7 = dim V_8 = 3,
+dim V_9 = 10.
+```
+
+This is the new structural obstruction. Allowing the mixed weight-seven
+word f does not supply eight cheap scalar normal directions. All deficient
+words together still span only T. In particular, being a span of deficient
+words does not make every member deficient.
+
+## 4. Exact basis bill and attainment
+
+In any basis of S, the number of members of weight at most k cannot
+exceed dim V_k. Consequently the first sorted weight is at least one,
+the second and third at least seven, and the other seven at least nine.
+Equivalently, the integer sum is at least
+
+```
+9 dim(S) - sum_{k=0}^8 dim(V_k) = 90-(6+3+3) = 78.
+```
+
+The ten vectors e,g,f and the seven code columns indexed
+0,1,3,4,5,6,7 form a basis. The missing code column 2 is recovered using
+E_a=d+f=2e+g+f and E_a=(R[0]-R[2])/3. The certificate independently checks
+their rank ten and exact weights (1,7,7,9,9,9,9,9,9,9). This proves
+attainment. The sorted coordinate bounds also prove the nondecreasing
+tariff statement without an analytic root search.
+
+## 5. A conditional coupled consequence
+
+Under PR4052's singleton-encoder hypotheses, an exact scalar-active
+factorization with actual reader space S has COPY at least 77, provided
+each exceptional left ray occurs at most once. The target and transpose
+conventions must be those of that source. This follows from its strict-floor
+corollary with L=77 and the new basis floor L+1=78. It is a lower bound,
+not an exact COPY optimum or an attaining factorization. The source's
+singleton classification and coupling argument are cited premises.
+
+This leaves at least five units above 72 in that coupled model. It closes
+this natural two-dimensional candidate at the first mixed-low boundary;
+it does not extend the general 28-neighbor theorem to arbitrary 29-site
+partial quotients. No native realization, physical access/restoration,
+compiler, stock, precision/tape or outer-cost obligation is discharged.
diff --git a/research/e8-root-low-plane/README.md b/research/e8-root-low-plane/README.md
new file mode 100644
index 0000000000..9dafb592b0
--- /dev/null
+++ b/research/e8-root-low-plane/README.md
@@ -0,0 +1,100 @@
+# Exact basis tariff 78 for the first root-low E8 quotient
+
+Scoped proof with an exact finite certificate, produced by Nick Petalas.
+No new kappa or selected-frontier change.
+
+For the explicit adjacent roots v=(0,1), a=(0,2) in the A8 E8 model, let
+d be E_a restricted to the nonorthogonal neighbors H_v. It has 29 nonzero
+entries and creates the mixed weight-seven word E_a-d. The natural
+two-dimensional correction space D=span(delta_a,d) gives a ten-dimensional
+reader space S=C+D with exact minimum basis profile
+
+```
+1, 7, 7, 9, 9, 9, 9, 9, 9, 9       sum = 78.
+```
+
+[PROOF.md](PROOF.md) proves that every basis has sorted weights at least
+this profile, over every characteristic-zero field. The exact minimum for
+every nondecreasing tariff F is F(1)+2F(7)+7F(9). All deficient vectors
+lie in three specified planes inside one three-dimensional space. The
+new mixed low direction therefore fails to make the complete reader
+basis cheap. Under conorholds' PR4052 singleton-encoder hypotheses, its
+strict-floor corollary gives the new conditional COPY lower bound 77
+for this actual reader space. No exact COPY optimum is claimed.
+
+The source question is [PR4052](https://github.com/CrocSwap/integer-mult-bounds/pull/4052),
+Open next question 2, at `7541aca683b1c40881a478b9d0bb2b63291949f9`.
+Its thresholds and COPY theorem are cited, not audited. The card changes
+from a complete signed-moment experiment to this scoped negative result
+on one named algebraic decoder candidate. It does not meet the physical
+supplier acceptance gate. [TASK.json](TASK.json) retains the original card.
+
+## Reproduction and evidence
+
+From the repository root, CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e8-root-low-plane/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/e8-root-low-plane/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e8-root-low-plane
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e8-root-low-plane --check-source-history
+```
+
+Other hosts can substitute their CPython 3.12 path. Direct checks are
+read-only and print `PASS_E8_ROOT_LOW_PLANE` in JSON bound to all six
+package hashes. An optional `--receipt PATH` creates a new receipt and
+refuses to overwrite an existing file. No receipt is hand-written or
+committed. No predecessor executable is imported or run.
+
+The new certificate covers all 511 nonzero characters, with rational
+kernel construction and separate integer/modulo-101 rank certificates.
+It checks the seven nonempty support unions, the ten-vector attaining
+basis, and seven controls. The controls reject incomplete, incorrect and
+oversized kernels and distinguish the deficient locus, its span, the
+unpunctured correction and the false bill 77. The finite table plus the
+written scalar-extension and filtration arguments proves the quantified
+claim; finite coefficient sampling alone would not do so.
+
+## Limitations
+
+The main result concerns exactly D=span(delta_a,E_a restricted to H_v)
+at the displayed root pair. Arbitrary 29-coordinate spaces, other fields,
+masked targets and shared or dynamic delivery are outside scope. The
+conditional COPY consequence retains PR4052's normalization and singleton
+classification premises. The selected #6030 record and all five framework
+assumptions remain unchanged. No selected cold replay, Lean, Docker,
+independent human or formal proof-kernel review is claimed.
+
+The verifier has no recursion, dynamic code execution or external
+dependencies. All matrix sizes are bounded by 120 rows and ten columns;
+the complete character loop has 511 iterations. Functions are below sixty
+lines. Python's managed allocation is a Power-of-Ten deviation, bounded
+here by the fixed matrix and certificate sizes. Warning-strict normal and
+optimized commands are registered. Ruff, mypy, Pyright and Pylint are
+unavailable in the local PATH and interpreter environment; stronger static
+analysis remains unclaimed.
+
+## Open next questions
+
+- Does a different correction space containing one 29-neighbor root-low
+  word admit a reader basis at or below 72? Start by adding one explicitly
+  independent correction to D and recomputing its character-kernel
+  filtration. The present result shows that this particular D is too costly;
+  it supplies no uniform answer for larger spaces.
+- What is the exact coupled COPY optimum with actual reader space S?
+  Start from the proved lower bound 77 and the source's exceptional-ray
+  identities. An exact factorization attaining that bill or a stronger
+  actual-basis argument is missing. Physical costs would still be separate.
+
+## Credit
+
+New quotient classification, basis tariff and verifier produced by Nick
+Petalas. conorholds supplied PR4052's 29-neighbor opening, relative
+thresholds and actual-basis coupling, building on PR3755's singleton and
+one-coset results and PR3166's weighted root swaps. Retain DreamingOfClouds'
+decoder programme and prefix relaxation, adamgall's concave accounting,
+the original E8 root/label geometry and all predecessor notices. Linear
+algebra, annihilator tests and rank filtrations are classical. No global
+literature-priority claim is made. New files are Apache-2.0; predecessor
+files and credit are unchanged. [SOURCES.json](SOURCES.json) pins the cited
+proofs and model as historical provenance, not executable dependencies.
diff --git a/research/e8-root-low-plane/SOURCES.json b/research/e8-root-low-plane/SOURCES.json
new file mode 100644
index 0000000000..5095945ed7
--- /dev/null
+++ b/research/e8-root-low-plane/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/e8-coupled-coordinate-floor/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "1c246d0689dec12e6fe1ebd8f20894839ae13399",
+      "sha256": "21dad21baa2f3bd2caad1dafb3945868327ec54b0fcdc63ffccfda73e93dc601"
+    },
+    {
+      "path": "research/e8-coupled-coordinate-floor/RELATIVE.md",
+      "usage": "provenance",
+      "git_blob": "9801ef8feb42f8534754cc6f602ca3fe4a834185",
+      "sha256": "eef835999b7fe56a80306e22e9cf3b386672a7c22fda260eb21759a7a61a1250"
+    },
+    {
+      "path": "research/e8-coupled-coordinate-floor/vendor/pr3755/geometry.py",
+      "usage": "provenance",
+      "git_blob": "9b4a3844d1c0c0e126f54ca9991f1cb158f358e0",
+      "sha256": "c783f6ddaf0bd5381b2345a62fe01f13e3e101ca33d70bc0495c406034782b91"
+    }
+  ]
+}
diff --git a/research/e8-root-low-plane/TASK.json b/research/e8-root-low-plane/TASK.json
new file mode 100644
index 0000000000..aca7f672b8
--- /dev/null
+++ b/research/e8-root-low-plane/TASK.json
@@ -0,0 +1,121 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "Determine the exact basis tariff of C+span(delta_a,E_a restricted to H_v) at the fixed adjacent A8 roots (0,1),(0,2), and its conditional singleton COPY consequence.",
+  "scope_change_reason": "This is a scoped algebraic obstruction at the 29-neighbor opening in PR4052, not a completed native supplier or a full signed-moment construction.",
+  "bottleneck_link": "Side result for changed decoder geometry. It rules out this explicit natural two-dimensional root-low reader space as a route below the COPY-72 baseline, under the stated singleton-encoder contract. No physical supplier admission follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first exact original basis tariff. Leave larger correction spaces and the exact coupled optimum open.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md; verify.py exhausts 511 character kernels using rational elimination and separate integer/modulo-101 rank certificates, seven support unions, an attaining ten-vector basis and seven controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a different correction space containing a 29-neighbor root-low word have basis tariff at most 72?",
+      "why_it_matters": "The natural two-dimensional space here costs 78, leaving other partial quotients unresolved.",
+      "first_step": "Add one named independent correction to D and determine the new character-kernel filtration.",
+      "blocked_by": "No useful larger space or complete physical budget is supplied."
+    },
+    {
+      "question": "What is the exact coupled COPY optimum with actual reader space S?",
+      "why_it_matters": "The new inherited-coupling consequence is a lower bound of 77, not an optimum.",
+      "first_step": "Seek an exact factorization or a stronger actual-basis cut argument under the same exceptional-ray contract.",
+      "blocked_by": "An attaining factorization and physical delivery are missing."
+    }
+  ],
+  "source_question": {
+    "pr": 4052,
+    "author": "conorholds",
+    "head": "7541aca683b1c40881a478b9d0bb2b63291949f9",
+    "location": "README.md Open next questions 2; RELATIVE.md section 8"
+  },
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371199",
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  },
+  "result": {
+    "minimum_basis_profile": [
+      1,
+      7,
+      7,
+      9,
+      9,
+      9,
+      9,
+      9,
+      9,
+      9
+    ],
+    "minimum_basis_bill": 78,
+    "conditional_copy_lower_bound": 77,
+    "field": "characteristic zero",
+    "complete_multiplication_theorem": false,
+    "new_kappa": false
+  },
+  "freshness": {
+    "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "checked_utc": "2026-11-03T10:13:47.800098+00:00",
+    "priority_revision": 8,
+    "selected_pr": 6030,
+    "open_prs_snapshot_records": 522,
+    "discussion_snapshot_records": 6535,
+    "coverage_limits": "Targeted current-main README and merged PR searches supplement complete open/discussion metadata. Sparse notes, arbitrary historical diffs and unpublished work remain outside coverage."
+  }
+}
diff --git a/research/e8-root-low-plane/VERIFY.json b/research/e8-root-low-plane/VERIFY.json
new file mode 100644
index 0000000000..c4c414fdf8
--- /dev/null
+++ b/research/e8-root-low-plane/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "All 511 rational kernels; separate modulo-101 rank certificates; support-union ranks; attaining basis; seven controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat the complete new certificate with assertions disabled; explicit proof checks remain active."
+    }
+  ]
+}
diff --git a/research/e8-root-low-plane/verify.py b/research/e8-root-low-plane/verify.py
new file mode 100644
index 0000000000..beb9403aa6
--- /dev/null
+++ b/research/e8-root-low-plane/verify.py
@@ -0,0 +1,272 @@
+"""Exact basis tariff for one root-low E8 quotient, produced by Nick Petalas.
+
+Apache-2.0. The A8 root/label model credits conorholds PR3755/4052 and
+the retained E8 decoder lineage. No predecessor executable is imported.
+"""
+
+import argparse
+from collections import Counter
+from fractions import Fraction
+from hashlib import sha256
+from itertools import combinations
+import json
+from pathlib import Path
+import sys
+
+
+WIDTH = 10
+PACKAGE_FILES = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json",
+                 "VERIFY.json", "verify.py")
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def dot(left, right):
+    need(len(left) == len(right), "dot-product shape")
+    return sum(x * y for x, y in zip(left, right))
+
+
+def row_basis(rows, width):
+    """Forward rational elimination; at most 120 input rows of width ten."""
+    need(0 <= width <= WIDTH and len(rows) <= 120, "rational matrix capacity")
+    need(all(len(row) == width for row in rows), "rational matrix shape")
+    pivots = {}
+    for initial in rows:
+        row = [Fraction(x) for x in initial]
+        for column, old in sorted(pivots.items()):
+            factor = row[column]
+            row = [x - factor * y for x, y in zip(row, old)]
+        column = next((j for j in range(width) if row[j]), None)
+        if column is not None:
+            scale = row[column]
+            pivots[column] = tuple(x / scale for x in row)
+    return pivots
+
+
+def nullspace(rows):
+    pivots = row_basis(rows, WIDTH)
+    result = []
+    for free in range(WIDTH):
+        if free in pivots:
+            continue
+        vector = [Fraction(j == free) for j in range(WIDTH)]
+        for column, row in sorted(pivots.items(), reverse=True):
+            vector[column] = -sum(row[j] * vector[j]
+                                  for j in range(column + 1, WIDTH))
+        result.append(tuple(vector))
+    need(len(result) + len(pivots) == WIDTH, "rank-nullity")
+    need(all(dot(row, vector) == 0 for row in rows for vector in result),
+         "computed kernel is not annihilated")
+    return result
+
+
+def modular_rank(rows):
+    """Separate column elimination modulo 101 supplies a rational rank lower bound."""
+    need(len(rows) <= 120 and all(len(row) == WIDTH for row in rows),
+         "modular matrix capacity")
+    work = [[int(x) % 101 for x in row] for row in rows]
+    rank = 0
+    for column in range(WIDTH):
+        pivot = next((i for i in range(rank, len(work)) if work[i][column]), None)
+        if pivot is None:
+            continue
+        work[rank], work[pivot] = work[pivot], work[rank]
+        inverse = pow(work[rank][column], -1, 101)
+        work[rank] = [x * inverse % 101 for x in work[rank]]
+        for i in range(rank + 1, len(work)):
+            factor = work[i][column]
+            for j in range(column, WIDTH):
+                work[i][j] = (work[i][j] - factor * work[rank][j]) % 101
+        rank += 1
+    return rank
+
+
+def binary_rank(values):
+    need(len(values) <= 120 and all(type(x) is int and 0 <= x < 512
+                                  for x in values), "binary input capacity")
+    pivots = [0] * 9
+    for initial in values:
+        value = initial
+        for bit in range(8, -1, -1):
+            if value & (1 << bit):
+                if pivots[bit]:
+                    value ^= pivots[bit]
+                else:
+                    pivots[bit] = value
+                    break
+    return sum(bool(x) for x in pivots)
+
+
+def model():
+    roots, labels = [], []
+    for i, j in combinations(range(9), 2):
+        row = [0] * 9
+        row[i], row[j] = 3, -3
+        roots.append(tuple(row))
+        labels.append(511 ^ (1 << i) ^ (1 << j))
+    for subset in combinations(range(9), 3):
+        roots.append(tuple(2 if i in subset else -1 for i in range(9)))
+        labels.append(sum(1 << i for i in subset))
+    need(len(roots) == len(set(roots)) == len(set(labels)) == 120, "root inventory")
+    need(all(sum(row) == 0 and dot(row, row) == 18 for row in roots), "root norms")
+    need((labels[0], labels[1]) == (508, 506), "distinguished root labels")
+    evaluation = [dot(row, roots[1]) // 9 for row in roots]
+    need(all(dot(row, roots[1]) % 9 == 0 for row in roots), "root evaluation scale")
+    correction = [x if (label & labels[0]).bit_count() % 2 == 0 else 0
+                  for label, x in zip(labels, evaluation)]
+    matrix = [row[:8] + (int(i == 1), correction[i])
+              for i, row in enumerate(roots)]
+    need(len(row_basis(matrix, WIDTH)) == WIDTH, "actual quotient dimension")
+    return matrix, labels
+
+
+def special_vectors():
+    unit = tuple(int(j == 8) for j in range(WIDTH))
+    neighbor = tuple(-2 if j == 8 else int(j == 9) for j in range(WIDTH))
+    outside = (1, 0, -1, 0, 0, 0, 0, 0, 0, -3)  # Three times E_a-d.
+    return unit, neighbor, outside
+
+
+def expected_kernel(character, vectors):
+    unit, neighbor, outside = vectors
+    if character == 508:
+        return "eg", [unit, neighbor]
+    if character == 506:
+        return "gf", [neighbor, outside]
+    if character == 505:
+        return "ef", [unit, outside]
+    if character == 6:
+        return "g", [neighbor]
+    if character == 3:
+        return "f", [outside]
+    if (character & 506).bit_count() % 2 == 0:
+        return "e", [unit]
+    return "zero", []
+
+
+def validate_kernel(rows, claimed):
+    need(len(claimed) <= 2, "claimed kernel capacity")
+    need(len(row_basis(claimed, WIDTH)) == len(claimed), "claimed kernel dependence")
+    need(all(dot(row, vector) == 0 for row in rows for vector in claimed),
+         "claimed kernel annihilation")
+    need(modular_rank(rows) == WIDTH - len(claimed), "modular rank certificate")
+
+
+def kernel_census(matrix, labels, vectors):
+    counts, records = Counter(), []
+    for character in range(1, 512):
+        rows = [row for row, label in zip(matrix, labels)
+                if (character & label).bit_count() % 2]
+        tag, expected = expected_kernel(character, vectors)
+        actual = nullspace(rows)
+        need(len(actual) == len(expected), "rational kernel dimension")
+        need(len(row_basis(actual + expected, WIDTH)) == len(expected),
+             "rational kernel subspace")
+        validate_kernel(rows, expected)
+        counts[tag] += 1
+        records.append([character, tag, len(rows), WIDTH - len(actual)])
+    need(dict(counts) == {"zero": 253, "e": 253, "f": 1, "g": 1,
+                         "ef": 1, "gf": 1, "eg": 1}, "character census")
+    return dict(sorted(counts.items())), records
+
+
+def support(matrix, vector):
+    return [i for i, row in enumerate(matrix) if dot(row, vector)]
+
+
+def weight(matrix, labels, vector):
+    return binary_rank([labels[i] for i in support(matrix, vector)])
+
+
+def support_certificate(matrix, labels, vectors):
+    sets = [set(support(matrix, vector)) for vector in vectors]
+    need([len(part) for part in sets] == [1, 28, 28], "disjoint support sizes")
+    need(all(not sets[i] & sets[j] for i, j in combinations(range(3), 2)),
+         "special supports intersect")
+    ranks = {}
+    for mask in range(1, 8):
+        union = set().union(*(sets[j] for j in range(3) if mask & (1 << j)))
+        ranks[str(mask)] = binary_rank([labels[i] for i in sorted(union)])
+    need(ranks == {"1": 1, "2": 7, "3": 8, "4": 7,
+                   "5": 8, "6": 8, "7": 9}, "support-union ranks")
+    return ranks
+
+
+def attaining_basis(matrix, labels, vectors):
+    # Retain seven coordinate evaluation columns complementary to E_a.
+    result = list(vectors)
+    result.extend(tuple(int(j == i) for j in range(WIDTH))
+                  for i in (0, 1, 3, 4, 5, 6, 7))
+    need(len(row_basis(result, WIDTH)) == WIDTH, "attaining basis dependence")
+    weights = [weight(matrix, labels, vector) for vector in result]
+    need(weights == [1, 7, 7] + [9] * 7, "attaining basis weights")
+    return weights
+
+
+def controls(matrix, labels, vectors):
+    count = 0
+    rows = [row for row, label in zip(matrix, labels) if (508 & label).bit_count() % 2]
+    broken = list(vectors[1])
+    broken[0] += 1
+    trials = ([vectors[0]], [vectors[0], tuple(broken)],
+              [vectors[0], vectors[1], vectors[2]])
+    for claimed in trials:
+        try:
+            validate_kernel(rows, claimed)
+        except ValueError:
+            count += 1
+        else:
+            raise ValueError("false kernel was accepted")
+    need(weight(matrix, labels, tuple(x + y for x, y in zip(vectors[1], vectors[2]))) == 8,
+         "two weight-seven directions were incorrectly closed under addition")
+    count += 1
+    need(weight(matrix, labels, tuple(sum(xs) for xs in zip(*vectors))) == 9,
+         "the span of deficient words was mistaken for the deficient locus")
+    count += 1
+    need(weight(matrix, labels, tuple(int(j == 9) for j in range(WIDTH))) == 8,
+         "the unpunctured correction was incorrectly priced seven")
+    count += 1
+    need(sum(attaining_basis(matrix, labels, vectors)) != 77, "false tariff 77 accepted")
+    return count + 1
+
+
+def verify():
+    matrix, labels = model()
+    vectors = special_vectors()
+    counts, records = kernel_census(matrix, labels, vectors)
+    unions = support_certificate(matrix, labels, vectors)
+    weights = attaining_basis(matrix, labels, vectors)
+    dimensions = [len(row_basis([vector for vector in vectors
+                                if weight(matrix, labels, vector) <= cutoff], WIDTH))
+                  for cutoff in range(1, 9)]
+    need(dimensions == [1] * 6 + [3, 3], "weight-filtration dimensions")
+    need(9 * WIDTH - sum(dimensions) == sum(weights) == 78, "filtration tariff identity")
+    directory = Path(__file__).resolve().parent
+    hashes = {name: sha256((directory / name).read_bytes()).hexdigest()
+              for name in PACKAGE_FILES}
+    return {"status": "PASS_E8_ROOT_LOW_PLANE", "claim_type": "scoped proof with finite certificate",
+            "characters": len(records), "kernel_types": counts,
+            "character_records_sha256": sha256(json.dumps(records, separators=(",", ":")).encode()).hexdigest(),
+            "support_union_ranks": unions, "filtration_dimensions": dimensions,
+            "minimum_basis_profile": weights, "minimum_basis_bill": sum(weights),
+            "conditional_copy_lower_bound": 77, "controls": controls(matrix, labels, vectors),
+            "package_sha256": hashes}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--receipt", type=Path, help="write a new hash-bound JSON receipt")
+    arguments = parser.parse_args()
+    result = verify()
+    output = json.dumps(result, indent=2, sort_keys=True) + "\n"
+    if arguments.receipt is not None:
+        with arguments.receipt.open("x", encoding="utf-8") as stream:
+            need(stream.write(output) == len(output), "short receipt write")
+    sys.stdout.write(output)
+
+
+if __name__ == "__main__":
+    main()