From 6bce04acf6ffe10ba2b649c060c37701fb913db6 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:48:38 +0000 Subject: [PATCH] feat(research): prove a sharp Boolean table tree-degree barrier --- research/boolean-table-tree-degree/PROOF.md | 140 +++++++++ research/boolean-table-tree-degree/README.md | 126 ++++++++ .../boolean-table-tree-degree/SOURCES.json | 35 +++ research/boolean-table-tree-degree/TABLE.json | 5 + research/boolean-table-tree-degree/TASK.json | 109 +++++++ .../boolean-table-tree-degree/VERIFY.json | 34 +++ research/boolean-table-tree-degree/verify.py | 280 ++++++++++++++++++ 7 files changed, 729 insertions(+) create mode 100644 research/boolean-table-tree-degree/PROOF.md create mode 100644 research/boolean-table-tree-degree/README.md create mode 100644 research/boolean-table-tree-degree/SOURCES.json create mode 100644 research/boolean-table-tree-degree/TABLE.json create mode 100644 research/boolean-table-tree-degree/TASK.json create mode 100644 research/boolean-table-tree-degree/VERIFY.json create mode 100644 research/boolean-table-tree-degree/verify.py diff --git a/research/boolean-table-tree-degree/PROOF.md b/research/boolean-table-tree-degree/PROOF.md new file mode 100644 index 0000000000..bbd1a963c9 --- /dev/null +++ b/research/boolean-table-tree-degree/PROOF.md @@ -0,0 +1,140 @@ +# A sharp degree obstruction for tree table splitting + +produced by Nick Petalas. Apache-2.0. + +## Contract + +Let F be a field of characteristic zero, or F_101. A table T has d>=1 +external Boolean indices and entries in F. An exact tree realization has +a finite nonempty tree of tensor vertices. Each external index attaches +to exactly one vertex. An internal tree edge carries k_e Boolean wires, +where k_e is a nonnegative integer. Contracting their indices produces T +on every external input. Internal tensor coefficients are unrestricted +elements of F. The degree of a vertex is its number of external wires +plus the sum of k_e over its incident edges. Parallel wires count +separately. A bundle of zero wires has dimension one. + +The tree is the graph after replacing parallel internal wires by one +edge. Vertex count, topology and bundle widths have no imposed upper +bound. Every realization is finite. External indices cannot be copied +to multiple vertices without including the corresponding copy tensors +and wires in this graph. + +## General lemma + +Suppose every nonempty proper bipartition A | A-complement of the d +external indices has matrix rank 2^min(|A|,d-|A|). Then the minimum +possible maximum vertex degree in this contract is exactly d. + +Remove an internal tree edge e. If its two components have a and d-a +external indices, contracting each component first expresses the +corresponding flattening as a product of matrices with inner dimension +2^k_e. Consequently, when 0= min(a,d-a). +``` + +For a=0 or a=d, the same final inequality is just k_e>=0. +This is the classical tensor flattening cut bound. It holds over the +stated field regardless of signs, zero coefficients or cancellations. + +Give each tree vertex weight equal to its number of attached external +indices. A weighted centroid v has at most d/2 weight in every component +of the tree after v is removed. Such a vertex exists. Orient an edge +toward a component of weight greater than d/2 whenever one exists. An +edge cannot be oriented both ways. In a finite tree, following outgoing +edges cannot form a cycle, so there is a vertex with no outgoing edge. +This vertex is a weighted centroid. If no edge is oriented, any vertex +works. + +Write a_v for its external degree and b_1,...,b_t for the external weights +of its incident components. They partition the external indices, so +a_v+sum(b_i)=d, and b_i<=d/2. The edge inequalities give + +```text +degree(v) = a_v + sum(k_i) + >= a_v + sum(min(b_i,d-b_i)) + = a_v + sum(b_i) = d. +``` + +The original table stored at one vertex has degree d and attains the +bound. This proves the lemma for all finite trees, rather than only +for enumerated topologies. + +## The explicit Boolean table + +Take d=8 and the 32 bytes encoded in TABLE.json. For an input x in +{0,1}^8 set i=sum(x_j 2^j), with j starting at zero. T(x) is bit i%8 of +byte i//8, with the low bit numbered zero. This specifies all 256 values; +121 are one. The hex string is a literal witness, not a hash-only +description of an unknown table. + +The finite certificate checks every unordered nontrivial bipartition. +Choose its representative mask m with 1<=m<128; complementation gives +the other member. For each cut choose the smaller side as rows. The +complete census is + +```text +smaller side size 1 2 3 4 +number of cuts 8 28 56 35 +certified matrix rank 2 4 8 16 +``` + +The verifier finds pivot columns by elimination modulo the prime 101. +It then reconstructs the selected square minor separately by scanning +all complete input words, and computes its integer determinant using +fraction-free elimination. All 127 determinants are nonzero modulo 101. +Thus each determinant is nonzero over F_101 and over every field of +characteristic zero. The number of rows is already an upper bound on +rank, proving equality on every cut. + +Apply the general lemma. Every exact tree realization of this Boolean +membership table has a vertex of degree at least eight. One vertex +holding T attains eight. No tree replacement with maximum degree seven +exists, even with unbounded vertex count, arbitrary internal coefficients +and arbitrarily wide Boolean bundles. + +This explicit table and its application to the table-splitting question +are the new result. The flattening method and weighted centroid argument +are standard. No claim of literature priority for those methods is made. + +## Why the graph hypothesis matters + +The verifier contracts a four-site cycle as a boundary control. Each +vertex has one external Boolean index and two internal Boolean indices, +hence degree three. Site i has the two 2-by-2 matrix slices written +literally in cycle_boundary(). Its external table is + +```text +42 62 52 48 26 36 30 32 16 24 16 16 12 16 12 16. +``` + +All seven nontrivial bipartitions of that four-index table have full rank, +certified by exact integer minors. Thus full flattening ranks alone do +not give degree at least d for cyclic networks. This is a contract control, +not a Boolean membership-table construction for the open cyclic case. + +## Relation to the question and limits + +Jacob Sussman's PR #5817 asks whether vector tables can be split into +low-degree tensor vertices while keeping the total wire count small. +The present result excludes exact acyclic replacements as a universal +degree-reducing method for arbitrary tables. It needs neither a wire-count +cap nor a particular tensor-contraction algorithm. Its proof does not +assume any unreviewed complexity-theoretic claim from that source. + +The explicit Boolean table has eight axes. There is no claim here that +Boolean tables with the same full-cut-rank property exist at every larger +dimension, or that the degree cap of a particular asymptotic contraction +theorem is violated by this fixed-size instance. Cyclic networks, +approximations, structured table families, duplicated external inputs +with a different contract and non-Boolean internal alphabets require +their own analysis. In particular this is not a general Orthogonal +Vectors lower bound, an impossibility of all vector-table splitting, +a new multiplication exponent or a complete multiplication theorem. + +The universal tree implication is a written proof. The table-rank claim +is a finite exact computation. Independent human and formal proof-kernel +review are unclaimed. diff --git a/research/boolean-table-tree-degree/README.md b/research/boolean-table-tree-degree/README.md new file mode 100644 index 0000000000..7e84d20f8c --- /dev/null +++ b/research/boolean-table-tree-degree/README.md @@ -0,0 +1,126 @@ +# A Boolean table that cannot lower its degree by tree splitting + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped proof with a finite exact certificate. The explicit eight-bit +membership table in [TABLE.json](TABLE.json) has exact minimum maximum +vertex degree **eight** among all exact tree tensor realizations over +fields of characteristic zero or F_101. Seven is impossible. The original +single tensor attains eight. + +The contract permits arbitrary internal coefficients, any finite tree, +arbitrarily many vertices and arbitrary bundles of internal Boolean +wires. Every wire in a bundle counts toward vertex degree; each external +bit attaches once. This settles the acyclic universal-splitting route for +this table in Jacob Sussman's [PR #5817](https://github.com/CrocSwap/integer-mult-bounds/pull/5817), +Open next question 2. It does not settle the full cyclic or asymptotic +vector-table question. + +## Proof and evidence + +[PROOF.md](PROOF.md) proves that a table with full matrix rank on every +nontrivial cut must retain a vertex of degree at least its number of +external bits. The proof factors each cut through its internal wires, +then sums the resulting rank bounds at a weighted tree centroid. + +The verifier establishes the hypothesis for the literal 256-entry Boolean +table, which contains 121 ones. It checks every one of its 127 unordered +nontrivial cuts. The cut-size counts are 8, 28, 56 and 35, with ranks +2, 4, 8 and 16. For each cut, modular elimination finds a square minor; +a separate input-word scan rebuilds it and fraction-free elimination +computes its exact integer determinant. All are nonzero modulo 101. + +Further checks enumerate 2,785 weighted trees on one through four labeled +vertices with eight external legs. These corroborate the centroid +argument; the written proof covers arbitrary finite trees. Twelve +controls reject malformed tables, false low-rank witnesses, an incomplete +cut domain, an empty cut, a nonsquare minor and a cyclic graph passed as +a tree. A literal four-site integer-valued cycle has all seven full cut +ranks at degree three, demonstrating why the graph hypothesis matters. + +The new contribution is the explicit Boolean witness and its sharp +application to this table-splitting question. Classical tensor unfolding +ranks, including [Oseledets's tensor-train work](https://doi.org/10.1137/090752286), +and weighted tree centroids retain their credit. The cut argument is +proved here. No literature priority is claimed for those methods. + +## Reproduce + +From the repository root, using the CPython 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/boolean-table-tree-degree/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/boolean-table-tree-degree/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/boolean-table-tree-degree +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/boolean-table-tree-degree --check-source-history +``` + +Another CPython 3.12 installation can replace the absolute interpreter +path. Direct verification also works from a Git-free package export. +Expected marker is `PASS_BOOLEAN_TABLE_TREE_DEGREE`, with `cuts=127`, +`degree_minimum=8`, `small_weighted_trees=2785` and `controls=12` in the +generated JSON receipt. The receipt binds all seven package files by +SHA256 and is printed to stdout. Verification writes no files. Both +registered commands have 60-second limits and use explicit exceptions, +so checks remain active under optimization. + +## Scope and provenance + +Base is canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, +priority revision 8. The original `formal-interface-lemma` card is +explicitly changed to this mathematical side question in [TASK.json](TASK.json). +Selected source-binding orientation passed. It authenticates metadata, +not a supplier or this theorem. Selected kappa remains `62009/20000000`. + +Jacob Sussman's source head is `be98f61484415d75197ed6218ad0239306e7b1a2`. +[SOURCES.json](SOURCES.json) records the exact question-source README blob +and SHA256. It is external historical motivation, with no runtime or +proof dependency on its conditional claims, code or unmerged Git objects. +The pinned catalogue and selected record are provenance only. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216917) +followed live account/open-PR, Discussion, main-tree and merged-PR checks +and a local reservation. Cached coverage included 459 open PRs and +5,407 Discussion records with complete remote pagination; sparse local +coverage was 190 of 7,845 HEAD notes. Targeted all-main searches supplement +that limitation. Unpublished work and arbitrary historical diffs remain +outside coverage. No predecessor result was replayed as the deliverable. + +This fixed eight-axis example does not establish such Boolean witnesses +at every larger dimension or violate a stated asymptotic degree cap. +Cyclic networks, approximation, structured inputs and different wire +alphabets remain outside the claim. No general Orthogonal Vectors lower +bound, physical supplier, recursive invoice improvement, new kappa, +selected-frontier change or complete multiplication theorem is supplied. +Lean, Docker and selected scientific cold replay were not run. +Independent human and formal proof-kernel review are unclaimed. + +## Implementation bounds + +The verifier has no recursion, subprocess, network or write path. Its +flattenings have at most 16 rows and 128 columns, with 256 entries; +square minors have order at most 16. The tree controls have at most four vertices and three edges. +All enumeration ranges are explicit and finite, and functions are below +60 physical lines. Bounded file reads cover seven fixed paths, at most +256 KiB each. Python runtime allocation is a managed-runtime deviation +from static allocation; the finite dimensions bound live collections. +Twelve immediately executed control callbacks have five fixed targets +and retain no state after execution, a bounded deviation from avoiding +indirect calls. Warning-strict normal and optimized runs and in-memory +compilation provide diagnostics without changing shared build settings. +Any larger input domain needs new bounds before these limits change. + +## Open next questions + +- Can a cyclic network represent this specific table at maximum degree + seven with a useful total wire count? Start with one fixed graph and + its complete 256-entry endpoint. A cyclic factorization and complete + wire budget remain missing. +- Which structured membership families permit low-degree tree + factorizations with few wires? Start with one explicit family, its + exact cut ranks and a complete tensor factorization. The proposed + consumer currently supplies no structural promise that avoids this + obstruction. + +These are follow-on questions; the investigation stops at the first +explicit witness above. diff --git a/research/boolean-table-tree-degree/SOURCES.json b/research/boolean-table-tree-degree/SOURCES.json new file mode 100644 index 0000000000..7acd15c9b5 --- /dev/null +++ b/research/boolean-table-tree-degree/SOURCES.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ], + "external_provenance": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5817", + "author": "Jacob Sussman", + "commit": "be98f61484415d75197ed6218ad0239306e7b1a2", + "path": "research/eth-claim-fft-impact/README.md", + "git_blob": "92600dd0ad418122b720be283fcc32badf5c6fe5", + "sha256": "2d6fcb3edb8eea26ba6ec89856b784165d30a75794552f28712e97e69a395366", + "usage": "Question source only, Open next question 2. No source code, result, theorem or unmerged Git object is a runtime or proof dependency." + }, + { + "url": "https://doi.org/10.1137/090752286", + "author": "I. V. Oseledets", + "title": "Tensor-Train Decomposition", + "usage": "Classical unfolding-rank background only; the cut factorization used here is proved in PROOF.md." + } + ] +} diff --git a/research/boolean-table-tree-degree/TABLE.json b/research/boolean-table-tree-degree/TABLE.json new file mode 100644 index 0000000000..3bdcc92709 --- /dev/null +++ b/research/boolean-table-tree-degree/TABLE.json @@ -0,0 +1,5 @@ +{ + "axes": 8, + "hex": "22706d02039748a6b630c864fcf62dbf44af30d22af79151d31288cb03fd9393", + "encoding": "byte i//8, bit i%8, input i=sum(x_j*2^j)" +} diff --git a/research/boolean-table-tree-degree/TASK.json b/research/boolean-table-tree-degree/TASK.json new file mode 100644 index 0000000000..3fc2c598c1 --- /dev/null +++ b/research/boolean-table-tree-degree/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Give one explicit eight-bit Boolean membership table whose exact tree tensor realizations have minimum possible maximum Boolean-wire degree eight, using full flattening ranks on every cut.", + "scope_change_reason": "Take the acyclic vector-table-splitting subquestion from Jacob Sussman PR5817. This is a mathematical side result, rather than a formalization or audit of a selected supplier interface.", + "bottleneck_link": "Tests an explicit acyclic table-splitting route suggested for bounded-degree tensor contraction. Full-cut-rank tables require a degree-preserving vertex; cyclic or structured alternatives require new analysis. No selected recursive invoice is changed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified explicit table and package the sharp tree obstruction; do not search larger dimensions or extend the construction.", + "outcome": "completed", + "evidence": "PROOF.md gives a cut-rank and weighted-centroid proof for every finite tree. verify.py certifies all 127 cuts with exact nonzero integer minors, enumerates 2785 small weighted trees, contracts a cyclic boundary control and checks 12 rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a cyclic Boolean-wire network represent this specific eight-bit table with maximum degree seven and a useful total wire count?", + "why_it_matters": "Acyclic universal splitting is excluded, but the cycle control shows why the proof does not cover cyclic replacements.", + "first_step": "State a fixed cyclic graph and count every internal Boolean wire, then check its complete 256-entry endpoint.", + "blocked_by": "No cyclic factorization or complete wire budget for this table is supplied." + }, + { + "question": "Which structured vector-table families admit bounded-degree acyclic factorizations with near-linear wire count in the number of external indices?", + "why_it_matters": "The obstruction uses full ranks on every cut; structured tables may have low-rank separators and avoid it.", + "first_step": "Choose one concrete structured membership family and give its exact cut ranks and full tensor factorization.", + "blocked_by": "No structural promise on the tables in the proposed consumer has been specified." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216917", + "source_pr": 5817, + "source_head": "be98f61484415d75197ed6218ad0239306e7b1a2", + "upstream_checked_at": "2026-10-27T12:48:38.243861+00:00", + "upstream_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "overlap_coverage": "459 open PRs and 5407 Discussion records, complete remote pagination at 12:37:58Z/12:39:05Z; 190 local notes of 7845 HEAD notes. Distinctive all-main and merged-PR searches supplement sparse local coverage. No search establishes global novelty." + } +} diff --git a/research/boolean-table-tree-degree/VERIFY.json b/research/boolean-table-tree-degree/VERIFY.json new file mode 100644 index 0000000000..b1a340c8b9 --- /dev/null +++ b/research/boolean-table-tree-degree/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": "Every bipartition of the explicit Boolean table, 127 exact integer minors, complete small weighted-tree domain, literal cyclic boundary and twelve semantic/input controls. Explicit exceptions remain enabled under optimization." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Every bipartition of the explicit Boolean table, 127 exact integer minors, complete small weighted-tree domain, literal cyclic boundary and twelve semantic/input controls. Explicit exceptions remain enabled under optimization." + } + ] +} diff --git a/research/boolean-table-tree-degree/verify.py b/research/boolean-table-tree-degree/verify.py new file mode 100644 index 0000000000..dfcc9887dc --- /dev/null +++ b/research/boolean-table-tree-degree/verify.py @@ -0,0 +1,280 @@ +#!/usr/bin/env python3 +"""Exact cut certificates and tree-degree controls. + +produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import itertools +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parent +FILES = ("README.md", "PROOF.md", "TABLE.json", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") +PRIME = 101 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_bounded(name, limit): + with (ROOT / name).open("rb") as stream: + data = stream.read(limit + 1) + require(len(data) <= limit, "package file capacity") + return data + + +def decode_table(record): + require(type(record) is dict, "table must be an object") + require(set(record) == {"axes", "hex", "encoding"}, "table fields") + require(type(record["axes"]) is int and record["axes"] == 8, "eight axes") + require(record["encoding"] == "byte i//8, bit i%8, input i=sum(x_j*2^j)", + "table encoding") + word = record["hex"] + require(type(word) is str and len(word) == 64, "32-byte table") + require(all(c in "0123456789abcdef" for c in word), "canonical hex") + raw = bytes.fromhex(word) + return tuple((raw[i // 8] >> (i % 8)) & 1 for i in range(256)) + + +def flatten(values, axes, mask): + require(type(axes) is int and 2 <= axes <= 8, "axis bound") + require(len(values) == 1 << axes, "table size") + require(type(mask) is int and 0 < mask < (1 << axes) - 1, "proper cut") + left = tuple(i for i in range(axes) if mask >> i & 1) + right = tuple(i for i in range(axes) if not mask >> i & 1) + rows = tuple(sum(((x >> j) & 1) << i for j, i in enumerate(left)) + for x in range(1 << len(left))) + cols = tuple(sum(((x >> j) & 1) << i for j, i in enumerate(right)) + for x in range(1 << len(right))) + return [[values[x | y] for y in cols] for x in rows] + + +def modular_pivots(matrix): + work = [[x % PRIME for x in row] for row in matrix] + rows, cols = len(work), len(work[0]) + require(1 <= rows <= 16 and rows <= cols <= 128, "matrix capacity") + pivots = [] + for col in range(cols): + row = len(pivots) + found = next((i for i in range(row, rows) if work[i][col]), None) + if found is None: + continue + work[row], work[found] = work[found], work[row] + inverse = pow(work[row][col], -1, PRIME) + work[row] = [x * inverse % PRIME for x in work[row]] + for i in range(row + 1, rows): + factor = work[i][col] + work[i] = [(a - factor * b) % PRIME + for a, b in zip(work[i], work[row])] + pivots.append(col) + if len(pivots) == rows: + break + return tuple(pivots) + + +def exact_determinant(matrix): + """Fraction-free elimination, separate from the modular rank algorithm.""" + size = len(matrix) + require(1 <= size <= 16 and all(len(r) == size for r in matrix), "square minor") + work = [row[:] for row in matrix] + previous, sign = 1, 1 + for k in range(size - 1): + found = next((i for i in range(k, size) if work[i][k]), None) + if found is None: + return 0 + if found != k: + work[k], work[found] = work[found], work[k] + sign = -sign + pivot = work[k][k] + for i in range(k + 1, size): + for j in range(k + 1, size): + numerator = work[i][j] * pivot - work[i][k] * work[k][j] + require(numerator % previous == 0, "Bareiss exact division") + work[i][j] = numerator // previous + work[i][k] = 0 + previous = pivot + return sign * work[-1][-1] + + +def independent_minor(values, axes, mask, columns): + """Rebuild the selected integer minor by scanning complete input words.""" + left = [i for i in range(axes) if mask & (1 << i)] + right = [i for i in range(axes) if not mask & (1 << i)] + require(len(left) <= 4, "minor row capacity") + cells = [[None] * len(columns) for _ in range(1 << len(left))] + column_positions = {value: i for i, value in enumerate(columns)} + for word in range(1 << axes): + row = sum(((word >> bit) & 1) * 2 ** i for i, bit in enumerate(left)) + col = sum(((word >> bit) & 1) * 2 ** i for i, bit in enumerate(right)) + if col in column_positions: + cells[row][column_positions[col]] = values[word] + require(all(x is not None for row in cells for x in row), "complete minor") + return cells + + +def cut_certificate(values, axes, cuts): + require(tuple(cuts) == tuple(range(1, 1 << (axes - 1))), "complete cut domain") + histogram = {size: 0 for size in range(1, axes // 2 + 1)} + determinants = [] + full = (1 << axes) - 1 + for original in cuts: + mask = original if original.bit_count() <= axes // 2 else full ^ original + matrix = flatten(values, axes, mask) + pivots = modular_pivots(matrix) + require(len(pivots) == len(matrix), "rank-deficient cut") + minor = independent_minor(values, axes, mask, pivots) + determinant = exact_determinant(minor) + require(determinant % PRIME != 0, "nonzero integer minor") + histogram[mask.bit_count()] += 1 + determinants.append((original, pivots, determinant)) + return histogram, determinants + + +def prufer_tree(vertices, code): + require(1 <= vertices <= 4, "tree capacity") + if vertices == 1: + return () + degrees = [1 + code.count(i) for i in range(vertices)] + edges = [] + for target in code: + leaf = next(i for i in range(vertices) if degrees[i] == 1) + edges.append((leaf, target)) + degrees[leaf] -= 1 + degrees[target] -= 1 + ends = tuple(i for i in range(vertices) if degrees[i] == 1) + require(len(ends) == 2, "two final leaves") + return tuple(edges) + (ends,) + + +def component_weight(weights, edges, start, blocked): + reached, frontier = {start}, {start} + for _ in range(len(weights)): + following = set() + for a, b in edges: + if a in frontier and b != blocked and b not in reached: + following.add(b) + if b in frontier and a != blocked and a not in reached: + following.add(a) + reached.update(following) + frontier = following + require(not frontier, "bounded traversal exhausted") + return sum(weights[i] for i in reached) + + +def centroid_degree(weights, edges): + vertices, total = len(weights), sum(weights) + require(1 <= vertices <= 4 and total == 8, "eight external legs") + require(all(type(x) is int and x >= 0 for x in weights), "external weights") + require(len(edges) == vertices - 1, "tree edge count") + for root in range(vertices): + neighbours = [b if a == root else a for a, b in edges if root in (a, b)] + branches = [component_weight(weights, edges, v, root) for v in neighbours] + require(weights[root] + sum(branches) == total, "tree components partition") + if all(b <= total // 2 for b in branches): + bound = weights[root] + sum(min(b, total - b) for b in branches) + require(bound == total, "centroid degree floor") + return root, bound + raise ValueError("no weighted centroid") + + +def check_trees(): + count = 0 + for vertices in range(1, 5): + codes = itertools.product(range(vertices), repeat=max(0, vertices - 2)) + for code in codes: + edges = prufer_tree(vertices, code) + for bars in itertools.combinations(range(8 + vertices - 1), vertices - 1): + stops = (-1,) + bars + (8 + vertices - 1,) + weights = tuple(stops[i + 1] - stops[i] - 1 for i in range(vertices)) + _, degree = centroid_degree(weights, edges) + require(degree == 8, "tree degree") + count += 1 + require(count == 2785, "complete small-tree domain") + return count + + +def cycle_boundary(): + cores = ( + (((1, 1), (1, 2)), ((2, 0), (2, 1))), + (((1, 2), (1, 0)), ((2, 0), (0, 2))), + (((1, 2), (2, 2)), ((0, 2), (1, 1))), + (((0, 2), (1, 2)), ((0, 0), (2, 0))), + ) + values = [] + for word in range(16): + state = [[1, 0], [0, 1]] + for site in range(4): + gate = cores[site][(word >> site) & 1] + state = [[sum(state[i][k] * gate[k][j] for k in range(2)) + for j in range(2)] for i in range(2)] + values.append(state[0][0] + state[1][1]) + require(values == [42, 62, 52, 48, 26, 36, 30, 32, + 16, 24, 16, 16, 12, 16, 12, 16], "cycle contraction") + histogram, _ = cut_certificate(values, 4, range(1, 8)) + require(histogram == {1: 4, 2: 3}, "full-rank cycle boundary") + return len(values) + + +def rejected(call, message): + try: + call() + except ValueError as error: + require(message in str(error), "unexpected rejection cause") + return 1 + raise ValueError("false certificate accepted") + + +def controls(record, values): + count = 0 + for field, value, message in ( + ("axes", True, "eight axes"), ("axes", 9, "eight axes"), + ("hex", "00", "32-byte table"), ("hex", "g" * 64, "canonical hex"), + ("encoding", "big endian", "table encoding"), + ): + changed = dict(record, **{field: value}) + count += rejected(lambda: decode_table(changed), message) + for bad in ((0,) * 256, (1,) * 256, + tuple(i.bit_count() % 2 for i in range(256))): + count += rejected(lambda: cut_certificate(bad, 8, range(1, 128)), + "rank-deficient cut") + count += rejected(lambda: cut_certificate(values, 8, range(1, 127)), + "complete cut domain") + count += rejected(lambda: flatten(values, 8, 0), "proper cut") + count += rejected(lambda: exact_determinant([[1, 2]]), "square minor") + count += rejected(lambda: centroid_degree((2, 2, 2, 2), + ((0, 1), (1, 2), (2, 3), (3, 0))), "tree edge count") + return count + + +def main(): + raw = read_bounded("TABLE.json", 4096) + record = json.loads(raw) + values = decode_table(record) + require(sum(values) == 121, "membership count") + histogram, minors = cut_certificate(values, 8, range(1, 128)) + require(histogram == {1: 8, 2: 28, 3: 56, 4: 35}, "bipartition census") + require(len(minors) == 127, "minor census") + trees = check_trees() + cycle_entries = cycle_boundary() + count = controls(record, values) + require(count == 12, "control census") + hashes = {} + for name in FILES: + data = read_bounded(name, 262144) + hashes[name] = hashlib.sha256(data).hexdigest() + print(json.dumps({"status": "PASS_BOOLEAN_TABLE_TREE_DEGREE", "axes": 8, + "members": sum(values), "cuts": len(minors), + "cut_sizes": histogram, "exact_integer_minors": len(minors), + "degree_minimum": 8, "small_weighted_trees": trees, + "cycle_boundary_entries": cycle_entries, "controls": count, + "claim_type": "scoped proof with finite exact certificate", + "package_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()