From 2a804fcb32f46d66018185194b55f1f2b217523d Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 16:25:33 +0000 Subject: [PATCH] feat(research): extend E8 span inputs to every odd characteristic --- research/e8-odd-characteristic-spans/PROOF.md | 132 ++++++++++ .../e8-odd-characteristic-spans/README.md | 95 +++++++ .../e8-odd-characteristic-spans/SOURCES.json | 54 ++++ .../e8-odd-characteristic-spans/TASK.json | 87 ++++++ .../e8-odd-characteristic-spans/VERIFY.json | 39 +++ .../e8-odd-characteristic-spans/verify.py | 248 ++++++++++++++++++ 6 files changed, 655 insertions(+) create mode 100644 research/e8-odd-characteristic-spans/PROOF.md create mode 100644 research/e8-odd-characteristic-spans/README.md create mode 100644 research/e8-odd-characteristic-spans/SOURCES.json create mode 100644 research/e8-odd-characteristic-spans/TASK.json create mode 100644 research/e8-odd-characteristic-spans/VERIFY.json create mode 100644 research/e8-odd-characteristic-spans/verify.py diff --git a/research/e8-odd-characteristic-spans/PROOF.md b/research/e8-odd-characteristic-spans/PROOF.md new file mode 100644 index 0000000000..df57b12669 --- /dev/null +++ b/research/e8-odd-characteristic-spans/PROOF.md @@ -0,0 +1,132 @@ +# E8 span lemmas over every field of odd characteristic + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let L be the 120 standard norm-two E8 root lines, with representatives in +Z[1/2]^8. For a line u write O_u for the root lines orthogonal to u. Evaluate +these representatives in a field K of characteristic different from two. +The ambient dot product is the ordinary nondegenerate form on K^8. + +The following four facts hold over every such field, including characteristic +zero. There is no exceptional odd prime. + +1. **S1.** The roots in O_f span f-perp, of dimension seven. +2. **S2.** For distinct root lines f,u, the roots in O_f intersect O_u span + span(f,u)-perp, of dimension six. +3. **S3prime.** Suppose u,v are distinct root lines nonorthogonal to f, neither + equal to f, and f,u,v are independent over Q. The roots in O_f intersect + O_u intersect O_v span span(f,u,v)-perp, of dimension five. The three + anchors remain independent over K. +4. **W2.** Project the 56 lines nonorthogonal to f, other than f itself, onto + f-perp by w_u = r_u - (r_u dot r_f) r_f/2. Their projective images are + exactly 28 distinct directions. Every three distinct directions are + linearly independent over K. Consequently a two-dimensional subspace + contains at most two of them. + +The S3prime admissibility condition uses the rational root configuration. +The conclusion proves that its admissible triples remain independent after +reduction. It does not silently change the domain at a special prime. + +These are the span inputs named in DreamingOfClouds's PR2819 and its PR2784 +lineage. PR2819 establishes them in characteristic zero and explicitly leaves +positive characteristic outside its classification. This proof supplies the +new field range of those inputs. It does not assert the full rank-nine +classification in positive characteristic. + +## Integer certificates + +Use doubled roots R_u = 2 r_u. Their entries are integral, their squared norm +is eight, and distinct root-line products are 0 or +/-4. All those nonzero +products remain nonzero over every odd-characteristic field, so the +orthogonality pattern itself does not change. + +For an integer matrix A, a k-by-k minor with determinant +/-2^a certifies +rank(A) >= k over every field of characteristic different from two. This +follows because its determinant is a unit in Z[1/2], hence is nonzero in K. +The same certificate also applies to characteristic zero. No extrapolation +from finitely many primes is involved. + +The verifier fixes f = e_0+e_1. It constructs the entire root inventory +explicitly and generates one such minor for each of the following matrices. + +| Matrix family | Matrices | Certified lower rank | +| --- | ---: | ---: | +| R[O_f] | 1 | 7 | +| Two anchors (f,u) | 119 | 2 | +| R[O_f intersect O_u] | 119 | 6 | +| Admissible three anchors (f,u,v) | 1512 | 3 | +| R[O_f intersect O_u intersect O_v] | 1512 | 5 | +| Three distinct projected directions | 3276 | 3 | + +There are 6539 minors. Their absolute determinants are powers of two between +2 and 256. `select_minor` uses elimination modulo three only to choose row +and column indices. `determinant` then evaluates the selected original +integer square matrix by fraction-free elimination, checking every division. +Only that exact integer determinant establishes the all-field claim. + +All rows of the first, third and fifth families are orthogonal to their +respective anchor rows. The certified anchor ranks and nondegeneracy of the +ambient dot product bound their ranks above by seven, six and five. Thus the +lower bounds give the exact spans in S1, S2 and S3prime. + +For W2 the verifier forms integer projected rows + + D_u = 2 R_u - (R_u dot R_f)/4 R_f = 4 w_u. + +It divides each by its positive coordinate gcd and chooses its sign by its +first nonzero coordinate. Every divisor is a power of two. These operations +remain invertible over every K in the statement. The 56 rows form 28 rational +directions with two rows per direction. Their 3276 triples have certified +rank three. This also proves nonvanishing and pairwise distinction after +reduction, since any pair belongs to such a triple. No extra direction can +arise by reducing two proportional vectors. + +For the S3prime inventory, f,u,v are rationally dependent precisely when +the two nonzero projections have the same projective direction. The verifier +omits exactly those pairs and certifies every other anchor triple separately. +This accounts for every rationally admissible pair in its stated domain. + +## Transport to every anchor + +For a doubled root a, the reflection is + + H_a = I - a a^T/4. + +Since a^T a = 8, direct multiplication gives H_a^T H_a = I and H_a^2 = I. +Its coefficients are in Z[1/2], so these identities hold over every K under +consideration. On a doubled root R its image is + + R - (a dot R)/4 a. + +The verifier checks all 14400 root images, including divisibility by four +and membership in the signed root set. Each reflection gives a permutation +of the 120 root lines. A bounded traversal of these permutations proves +that the orbit of f contains all 120 lines. Each resulting product is an +invertible isometry over Z[1/2], hence over K. + +These products transport root orthogonality, anchor independence, spans and +orthogonal projection. Therefore the complete fixed-anchor certificates +prove S1, S2, S3prime and W2 for every root line f. Multiplication by any +representative sign has no effect on these assertions. + +## Scope and remaining obligations + +This is a scoped algebraic proof supported by an exhaustive finite integer +certificate. The executable certificate and the written transport argument +jointly establish the quantified field statement. The executable is not a +formal proof-kernel check. + +The rank-nine pinning/classification argument, its sign logic, SAT encodings, +refutations and other finite facts are inherited research and were not +replayed. Applying this new lemma to a positive-characteristic classification +still requires checking all remaining characteristic assumptions in that +argument. No decoder COPY floor, native operation, physical caller, signed +invoice, new kappa or complete multiplication theorem follows here. + +Power-of-two minors and integral root-reflection transport are established +methods. CubeJerry's PR3095 and conorholds's PR3755 use them for different +root/character span statements. They retain that methodological credit. +The new result here is the complete all-odd-field S1/S2/S3prime/W2 input set +and its explicit bounded integer certificates. diff --git a/research/e8-odd-characteristic-spans/README.md b/research/e8-odd-characteristic-spans/README.md new file mode 100644 index 0000000000..564aa89503 --- /dev/null +++ b/research/e8-odd-characteristic-spans/README.md @@ -0,0 +1,95 @@ +# E8 span inputs have no exceptional odd prime + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with an exhaustive finite integer certificate. No new kappa.** +The E8 facts S1, S2, S3prime and W2 used by DreamingOfClouds's +[PR2819](https://github.com/CrocSwap/integer-mult-bounds/pull/2819) hold over +**every field of characteristic different from two**. This supplies a new +field range for the span inputs that its section 7 leaves open. The existing +characteristic-zero classification and SAT work are cited, not audited. + +[PROOF.md](PROOF.md) states the exact domains. Orthogonal roots span the +seven-, six- and five-dimensional complements of the specified one-, two- +and three-root anchor sets. The 56 nonorthogonal neighbors of any root +project to 28 distinct directions, with every three independent. No odd +prime changes those conclusions. + +The new verifier constructs 6539 integer minors with absolute determinants +in {2,4,8,16,32,64,128,256}. Each remains nonzero over every odd-characteristic +field. Its complete fixed-anchor domain consists of one S1 matrix, 119 S2 +matrices and their 119 anchor pairs, 1512 S3prime matrices and their 1512 +anchor triples, and all 3276 projected-direction triples. It checks all +14400 root images under the 120 integral reflections and verifies a +120-line orbit to transport the result to every anchor. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/e8-odd-characteristic-spans/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e8-odd-characteristic-spans +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e8-odd-characteristic-spans --check-source-history +``` + +Local checks used CPython 3.12.15 on macOS 27.0.1 arm64. The two registered +commands took 0.13 and 0.14 seconds locally, below their 60-second limits. + +The principal marker is `PASS_E8_ODD_CHARACTERISTIC_SPANS`. The verifier +writes a JSON receipt to stdout, binding its certificate digest to SHA256 +hashes of the package and declared input files. Redirect outputs outside the +checkout. It writes no files and executes no predecessor program. + +Modular elimination only selects minors. Exact fraction-free determinants +supply the proof certificates. The checks include 673 comparisons with an +independent Leibniz determinant formula, rejection of a singular matrix and +odd-torsion matrices at three and five, and two dyadic-unit/power controls. +All checks remain active under `-O`. + +## Limitations + +This does not extend the complete rank-nine classification to positive +characteristic. Its remaining sign logic, pinning implications, other finite +facts, SAT encodings and refutations were not assessed or replayed here. +There is no decoder floor, native supplier, caller, signed invoice or +selected-frontier change. The five selected framework assumptions remain. +Independent human and formal proof-kernel review are unclaimed. + +The executable uses bounded exact integer arithmetic, without recursion. +Every matrix has at most 63 rows and eight columns; every determinant has +order at most seven. Managed Python allocation is a documented deviation +from fixed-capacity allocation. Finite inventories bound live data. The +certificate digest is generated, not a hand-written receipt. Historical +source checks are byte bindings only. + +## Open next questions + +- Which remaining PR2819 classification implications require a further + characteristic restriction? Start by listing those implications and their + denominators. This matters because the new span inputs alone cannot admit + the classification in a new field; those implications remain the blocker. +- Does an explicitly missing span input for P112 or P104 admit dyadic-unit + minors? First identify its exact incidence domain in a source package. + This could help the supplier geometries, but is blocked by that distinct + target specification. No punctured-unit result is claimed here. + +The same questions are structured in [TASK.json](TASK.json). + +## Credit and related work + +DreamingOfClouds retains PR2819's classification, naming and characteristic-zero +span inputs, with its PR2784 lineage. The standard E8 root coordinates are +also retained there. No predecessor source or credit line is changed. +CubeJerry's [PR3095](https://github.com/CrocSwap/integer-mult-bounds/pull/3095) +and conorholds's [PR3755](https://github.com/CrocSwap/integer-mult-bounds/pull/3755) +use power-of-two minors and integral reflection transport for different +root/character span questions. Those methods are established background. +The new contribution is the all-odd-field S1/S2/S3prime/W2 input set and its +complete bounded certificate. No literature-priority claim is made. + +The overlap check covered all 310 open PR bodies and complete Discussion +pagination at the recorded snapshot, targeted merged-PR searches, and +canonical-main README searches for the facts, their field range and more +general formulations. The sparse local-note corpus was incomplete. No +matching open PR was found. Unpublished work remains outside that coverage. diff --git a/research/e8-odd-characteristic-spans/SOURCES.json b/research/e8-odd-characteristic-spans/SOURCES.json new file mode 100644 index 0000000000..a5a83b70c7 --- /dev/null +++ b/research/e8-odd-characteristic-spans/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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-rank9-realisations/README.md", + "usage": "input", + "git_blob": "62c6efd17a3439e79c2eb4f260df00ef8c22eba8", + "sha256": "dd4d1f54ec6e0f41da85c5862304d8bcb8b252f50425f13467f230b69098568a" + }, + { + "path": "research/e8-rank9-realisations/checks/e8lib.py", + "usage": "input", + "git_blob": "d802266a2850fe2d4941bd49154e5ae976443289", + "sha256": "b1a0339383cc4ae6957caec6a9feffb9fb344679cceeff8eca49996ff21bcf4d" + }, + { + "path": "research/e8-rank9-realisations/checks/spans.py", + "usage": "input", + "git_blob": "1c2f7615972a06e45f57e72f19b8e4c1e8d6655d", + "sha256": "780d373d518e6c1830594d550f408cc7eac9da32a1527504efb6c32afd9e5e0a" + }, + { + "path": "research/e8-rank9-realisations/checks/spans3.py", + "usage": "input", + "git_blob": "db00d69635acb9a973764fb6b273515c96b88bfa", + "sha256": "8d5b0c0270c916e9ce5136a2d95f06c4eff4769008534b8d2d83c402694e1d2d" + }, + { + "path": "research/one-sided-padding-audit/README.md", + "usage": "provenance", + "git_blob": "f5a61bd2c3f30d24b6926667a015229c132671c3", + "sha256": "6291af467140df3cb9ca701c9f02e92b25b99869818589dc5b544a5d60eaff80" + }, + { + "path": "research/e8-one-coset-deficiency/PROOF.md", + "usage": "provenance", + "git_blob": "89c328853b8a7a49dbbd9d8e4a842e1e209974df", + "sha256": "d3dcc35205225547c13f8bc0ec3175da7aab41e54c7adc06f0c35c86f00b93e4" + } + ] +} diff --git a/research/e8-odd-characteristic-spans/TASK.json b/research/e8-odd-characteristic-spans/TASK.json new file mode 100644 index 0000000000..5cd296e76c --- /dev/null +++ b/research/e8-odd-characteristic-spans/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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": "All-odd-characteristic E8 orthogonal-complement span facts S1, S2, S3prime and projected-direction fact W2, certified by integral dyadic-unit minors.", + "scope_change_reason": "Answer PR2819 section 7 positive-characteristic boundary for its finite span inputs. This is an arithmetic side result rather than a physical decoder or signed-moment improvement.", + "bottleneck_link": "Removes the field-transfer obstacle for four algebraic inputs used in rank-nine decoder classification. It supplies no physical decoder or improvement to the binding complex invoice.", + "budget_minutes": 60, + "stop_rule": "Ship the first all-odd-field span certificate; leave classification, SAT and physical realization obligations open.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-field implication and reflection transport; verify.py generates 6539 exact power-of-two minors and a file-hash-bound JSON receipt without writing files.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Do all remaining PR2819 classification steps hold over every odd characteristic?", + "why_it_matters": "The new span theorem alone does not extend the rank-nine classification.", + "first_step": "List each remaining field assumption in the pinning and sign-logic arguments before any new finite run.", + "blocked_by": "The remaining algebraic implications and finite proof obligations have not been assessed in that field range." + }, + { + "question": "Can the same integer-unit approach cover span inputs for punctured P112 or P104 classification?", + "why_it_matters": "Those geometries are closer to the productive suppliers but have different available root sets.", + "first_step": "Identify one explicitly missing span proposition in an existing punctured-unit package.", + "blocked_by": "A distinct valid target and its complete incidence domain must first be specified." + } + ], + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS 27.0.1 arm64", + "dependencies": "standard library only", + "playbook": "Autonomous local run" + } +} diff --git a/research/e8-odd-characteristic-spans/VERIFY.json b/research/e8-odd-characteristic-spans/VERIFY.json new file mode 100644 index 0000000000..96b1a1e5ae --- /dev/null +++ b/research/e8-odd-characteristic-spans/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-rank9-realisations/README.md", + "research/e8-rank9-realisations/checks/e8lib.py", + "research/e8-rank9-realisations/checks/spans.py", + "research/e8-rank9-realisations/checks/spans3.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Generate every fixed-anchor integer minor, all root-reflection images, exact determinant differentials and singular/odd-torsion rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat the complete certificate and rejection controls with Python assertions disabled." + } + ] +} diff --git a/research/e8-odd-characteristic-spans/verify.py b/research/e8-odd-characteristic-spans/verify.py new file mode 100644 index 0000000000..91a927b464 --- /dev/null +++ b/research/e8-odd-characteristic-spans/verify.py @@ -0,0 +1,248 @@ +#!/usr/bin/env python3 +"""Exact all-odd-characteristic certificates; produced by Nick Petalas. + +Integer minors certify ranks. Modular elimination only selects minors. +No predecessor program is executed and no file is written. +""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations, permutations, product +from math import gcd +from pathlib import Path +import json + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def power_of_two(value): + return value > 0 and value & (value - 1) == 0 + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right, strict=True)) + + +def canonical(row): + require(any(row), "zero projective vector") + return tuple(-x for x in row) if next(x for x in row if x) < 0 else row + + +def roots(): + lines = [] + for i, j in combinations(range(8), 2): + for sign in (1, -1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + lines.append(tuple(row)) + for signs in product((1, -1), repeat=7): + row = (1,) + signs + if row.count(-1) % 2 == 0: + lines.append(row) + require(len(lines) == len(set(lines)) == 120, "root inventory") + require(all(dot(row, row) == 8 for row in lines), "root norm") + return tuple(lines) + + +def determinant(matrix): + """Bareiss elimination with checked exact divisions; order at most seven.""" + size = len(matrix) + require(1 <= size <= 7, "minor order") + require(all(len(row) == size for row in matrix), "nonsquare minor") + work = [list(row) for row in matrix] + previous, sign = 1, 1 + for col in range(size - 1): + pivot = next((i for i in range(col, size) if work[i][col]), None) + if pivot is None: + return 0 + if pivot != col: + work[col], work[pivot] = work[pivot], work[col] + sign = -sign + current = work[col][col] + for i in range(col + 1, size): + for j in range(col + 1, size): + numerator = current * work[i][j] - work[i][col] * work[col][j] + require(numerator % previous == 0, "inexact Bareiss division") + work[i][j] = numerator // previous + work[i][col] = 0 + previous = current + return sign * work[-1][-1] + + +def select_minor(rows, rank, prime): + """Return original row and column IDs of a nonzero modular minor.""" + require(1 <= len(rows) <= 63 and 1 <= rank <= 7, "matrix bounds") + require(all(len(row) == 8 for row in rows), "coordinate count") + work = [[x % prime for x in row] for row in rows] + indices = list(range(len(rows))) + columns = [] + for col in range(8): + height = len(columns) + pivot = next((i for i in range(height, len(rows)) if work[i][col]), None) + if pivot is None: + continue + work[height], work[pivot] = work[pivot], work[height] + indices[height], indices[pivot] = indices[pivot], indices[height] + inverse = pow(work[height][col], -1, prime) + for i in range(height + 1, len(rows)): + factor = work[i][col] * inverse % prime + for j in range(col, 8): + work[i][j] = (work[i][j] - factor * work[height][j]) % prime + columns.append(col) + if len(columns) == rank: + return indices[:rank], columns + raise ValueError(f"rank below {rank} in characteristic {prime}") + + +def rank_certificate(rows, rank): + """Select and exactly verify one power-of-two minor.""" + row_ids, col_ids = select_minor(rows, rank, 3) + minor = [[rows[i][j] for j in col_ids] for i in row_ids] + value = determinant(minor) + require(power_of_two(abs(value)) and abs(value) <= 2**20, "nonunit minor") + return [[row_ids, col_ids, value]], abs(value) + + +def reflection_orbit(lines): + ids = {row: i for i, row in enumerate(lines)} + maps = [] + for alpha in lines: + image = [] + for row in lines: + pairing = dot(alpha, row) + require(pairing % 4 == 0, "reflection integrality") + reflected = tuple(x - pairing // 4 * a for x, a in zip(row, alpha)) + require(canonical(reflected) in ids, "reflection left root set") + image.append(ids[canonical(reflected)]) + require(len(set(image)) == 120, "reflection is not a permutation") + maps.append(image) + orbit, seen = [0], {0} + for position in range(120): + if position == len(orbit): + break + for image in maps: + target = image[orbit[position]] + if target not in seen: + seen.add(target) + orbit.append(target) + require(len(orbit) == 120, "reflection transitivity") + return len(maps) * len(lines) + + +def geometry(lines): + orthogonal = [{j for j, other in enumerate(lines) if dot(row, other) == 0} + for row in lines] + neighbors = [u for u in range(1, 120) if dot(lines[0], lines[u]) != 0] + directions, projected_ids = [], {} + for u in neighbors: + pairing = dot(lines[0], lines[u]) + require(pairing in (-4, 4), "neighbor pairing") + projected = tuple(2 * x - pairing // 4 * y + for x, y in zip(lines[u], lines[0])) + scale = gcd(*projected) + require(power_of_two(scale), "nonunit projection rescaling") + direction = canonical(tuple(x // scale for x in projected)) + require(dot(direction, lines[0]) == 0, "projection is not orthogonal") + if direction not in directions: + directions.append(direction) + projected_ids[u] = directions.index(direction) + require(len(neighbors) == 56 and len(directions) == 28, "projection inventory") + require(set(Counter(projected_ids.values()).values()) == {2}, "antipodal fibers") + return orthogonal, neighbors, directions, projected_ids + + +def certificates(lines, orthogonal, neighbors, directions, projected_ids): + yield "S1", [lines[i] for i in sorted(orthogonal[0])], 7 + for u in range(1, 120): + yield "S2-anchor", [lines[0], lines[u]], 2 + yield "S2", [lines[i] for i in sorted(orthogonal[0] & orthogonal[u])], 6 + for u, v in combinations(neighbors, 2): + if projected_ids[u] == projected_ids[v]: + continue + yield "S3-anchor", [lines[0], lines[u], lines[v]], 3 + common = orthogonal[0] & orthogonal[u] & orthogonal[v] + yield "S3", [lines[i] for i in sorted(common)], 5 + for indices in combinations(range(28), 3): + yield "W2", [directions[i] for i in indices], 3 + + +def leibniz(matrix): + total = 0 + for order in permutations(range(len(matrix))): + inversions = sum(order[i] > order[j] for i, j in combinations(range(len(order)), 2)) + term = (-1) ** inversions + for i, j in enumerate(order): + term *= matrix[i][j] + total += term + return total + + +def controls(): + count = 0 + for values in product(range(-2, 3), repeat=4): + matrix = [list(values[:2]), list(values[2:])] + require(determinant(matrix) == leibniz(matrix), "determinant differential") + count += 1 + for size in (3, 4, 5): + for offset in range(16): + matrix = [[((i + 2) * (j + 3) + offset * (i == j)) % 7 - 3 + for j in range(size)] for i in range(size)] + require(determinant(matrix) == leibniz(matrix), "larger determinant differential") + count += 1 + for coefficient in (0, 3, 5): + try: + rank_certificate([[coefficient] + [0] * 7], 1) + except ValueError: + count += 1 + else: + raise ValueError("accepted singular or odd-torsion matrix") + require(rank_certificate([[2] + [0] * 7], 1)[1] == 2, "dyadic unit control") + require(not power_of_two(0) and not power_of_two(12), "power-of-two control") + return count + 2 + + +def source_bindings(package): + manifest = json.loads((package / "SOURCES.json").read_text()) + root, hashes = package.parent.parent, {} + for item in manifest["files"]: + if item["usage"] == "input": + observed = sha256((root / item["path"]).read_bytes()).hexdigest() + require(observed == item["sha256"], "source byte mismatch: " + item["path"]) + hashes[item["path"]] = observed + for path in sorted(package.iterdir()): + if path.is_file() and path.suffix in (".py", ".md", ".json"): + hashes[path.name] = sha256(path.read_bytes()).hexdigest() + return hashes + + +def main(): + package = Path(__file__).resolve().parent + hashes = source_bindings(package) + lines = roots() + images = reflection_orbit(lines) + orthogonal, neighbors, directions, projected_ids = geometry(lines) + counts, gcds, digest = Counter(), Counter(), sha256() + minor_count, largest = 0, 0 + for name, rows, rank in certificates(lines, orthogonal, neighbors, directions, projected_ids): + witnesses, divisor = rank_certificate(rows, rank) + digest.update(json.dumps([name, rows, rank, witnesses, divisor], separators=(",", ":")).encode()) + counts[name] += 1 + gcds[str(divisor)] += 1 + minor_count += len(witnesses) + largest = max(largest, *(abs(witness[2]) for witness in witnesses)) + require(dict(counts) == {"S1": 1, "S2-anchor": 119, "S2": 119, + "S3-anchor": 1512, "S3": 1512, "W2": 3276}, "case inventory") + print(json.dumps({"status": "PASS_E8_ODD_CHARACTERISTIC_SPANS", + "claim_type": "scoped proof with finite integer-minor certificate", + "cases": dict(counts), "minor_count": minor_count, + "gcd_histogram": dict(sorted(gcds.items())), + "largest_absolute_minor": largest, + "certificate_sha256": digest.hexdigest(), + "reflection_images": images, "controls": controls(), + "source_sha256": hashes, "exceptional_odd_primes": []}, sort_keys=True)) + + +if __name__ == "__main__": + main()