Prove a sharp degree-eight tree barrier for a Boolean table (no new κ)

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<a<d,
+
+```text
+2^min(a,d-a) = rank(T_A) <= 2^k_e,
+k_e >= 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.

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.

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."
+    }
+  ]
+}

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)"
+}