From 8dbf33d72f181af5986b3f703f9a827d64d18688 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 23:22:27 +0100 Subject: [PATCH] feat(research): prove partial-axis root-code decoder floor --- .../axis-punctured-root-code-floor/PROOF.md | 150 + .../axis-punctured-root-code-floor/README.md | 132 + .../RESULT.json | 6890 +++++++++++++++++ .../SOURCES.json | 36 + .../axis-punctured-root-code-floor/TASK.json | 115 + .../VERIFY.json | 32 + .../axis-punctured-root-code-floor/verify.py | 270 + 7 files changed, 7625 insertions(+) create mode 100644 research/axis-punctured-root-code-floor/PROOF.md create mode 100644 research/axis-punctured-root-code-floor/README.md create mode 100644 research/axis-punctured-root-code-floor/RESULT.json create mode 100644 research/axis-punctured-root-code-floor/SOURCES.json create mode 100644 research/axis-punctured-root-code-floor/TASK.json create mode 100644 research/axis-punctured-root-code-floor/VERIFY.json create mode 100644 research/axis-punctured-root-code-floor/verify.py diff --git a/research/axis-punctured-root-code-floor/PROOF.md b/research/axis-punctured-root-code-floor/PROOF.md new file mode 100644 index 0000000000..19aa02d8b7 --- /dev/null +++ b/research/axis-punctured-root-code-floor/PROOF.md @@ -0,0 +1,150 @@ +# Dense root-code floor with any subset of axes + +This scoped proof was produced by Nick Petalas. The coefficient field K has +characteristic other than two. Binary support ranks are always over F2. +Ordinary transpose is used throughout. + +## Statement + +Let n>=4 and A be any subset of {0,...,n-1}, with k=|A|. Let R have rows + + e_i+e_j, e_i-e_j for every i= n(n-1)+k. Coordinate factors attain equality. Every optimum +has exactly n nonzero terms. In particular, deleting arbitrary axis lines +while keeping all signed edges cannot make the cost smaller than the +number of retained lines. + +The cases k=0 and k=n are the previously established full Dn and Bn/Cn +floors. The new result is the intermediate-axis family 0=n. All nonzero +vectors have nonzero root-code factors. + +Call a term marked when both x_j restricted to A and y_j restricted to A +are nonzero. Restricting the last identity to its A-by-A block gives + + I_k = sum_(marked j) (x_j|A)(y_j|A)^T. + +Rank subadditivity therefore forces at least k marked terms. This is a +rank argument, not merely k separate nonzero diagonal entries; one term +can contribute to several diagonal entries without supplying their rank. + +Each marked term costs at least n. Indeed choose a retained axis i with +x_ji nonzero, and a retained axis h with y_jh nonzero. The axis entries +are supported. For every t!=i at least one of x_ji+x_jt and x_ji-x_jt is +nonzero; otherwise 2x_ji=0. The analogous fact holds on the other side. +Thus both supports contain complete axis stars. The cited cross-star +minor is a submatrix of the actual punctured rectangle. Its rank n is +retained because none of its two axes or signed edges was deleted. + +Write e for the number of marked terms, so e>=k. Restricting any actual +rectangle to the signed edges also retains the cited Dn lower bound. + +## All finite numbers of terms + +For even n, every term costs at least n-1 and each marked term costs at +least n. Hence + + sum c_j >= m(n-1)+e >= n(n-1)+k. + +If m>n, this inequality is strict. + +For odd n, n>=5. Call a term cheap when x_j and y_j are nonzero multiples +of distinct coordinate vectors. The cited Dn tariff implies that an +unmarked noncheap term costs at least n-1, a cheap term costs at least +n-2, and a marked term costs at least n. A cheap term is never marked +unless both of its distinct axes are retained, in which case the marked +bound n applies instead. In the estimates below it is safe to subtract +the count c of all cheap terms, including any marked cheap terms: + + sum c_j >= m(n-1)-c+e. (1) + +For m=n, Y^T X=I_n follows from XY^T=I_n. Thus y_j^T x_j=1 for every j, +which excludes every cheap term. Equation (1) proves the desired floor. + +For m=n+1, the credited one-extra coupling argument bounds c by two. +Here is its application, included to specify every hypothesis. H=Y^T X +is an idempotent of rank n. Therefore I-H=u v^T for nonzero vectors u,v, +with v^T u=1. A cheap index j has H_jj=0, so u_j v_j=1. For distinct +cheap indices j,l, H_jl=-u_j v_l is nonzero. Write the cheap factors as +x_j=alpha_j e_(a_j), y_j=beta_j e_(b_j), with a_j!=b_j. Then H_jl!=0 +forces b_j=a_l. Three cheap indices j,l,t would force +a_l=b_j=a_t and a_j=b_l=a_t, hence a_j=a_l=b_j, a contradiction. +Thus (1) gives + + sum c_j >= (n+1)(n-1)-2+k + = n(n-1)+k+(n-3) > n(n-1)+k. + +For m>=n+2 use the universal signed-edge floor n-2 and charge two more +for each marked term: + + sum c_j >= m(n-2)+2e + >= (n+2)(n-2)+2k + = n(n-1)+k+(n+k-4) > n(n-1)+k. + +The last strict inequality uses n>=5 and k>=0. These three cases exhaust +all finite m, without assuming a bounded coefficient alphabet or m<=n+1. + +## Attainment and scope + +Take x_j=y_j=e_j, j=0,...,n-1. The support for j contains the two signs +on each of its n-1 incident edges, and its own axis precisely when j is +retained. After removing identical sign rows and columns, its pairing +rectangle is I_(n-1+[j in A]). The exact Gram expansion therefore costs + + sum_j (n-1+[j in A]) = n(n-1)+k. + +This proves attainment and, with the strict inequalities above, the +exactly-n-terms statement. It is an algebraic separate-term rank invoice. +Sparse pairings, deleted signed edges, non-root-code factors, different +targets and characteristic two are outside the theorem. No physical +frames, access, dirty restoration, compiler, precision or recursive +supplier budget is supplied. These costs remain unknown, rather than +being set to zero. No new multiplication theorem or kappa follows. diff --git a/research/axis-punctured-root-code-floor/README.md b/research/axis-punctured-root-code-floor/README.md new file mode 100644 index 0000000000..357ba27e81 --- /dev/null +++ b/research/axis-punctured-root-code-floor/README.md @@ -0,0 +1,132 @@ +# Sharp root-code floor after arbitrary axis punctures + +For every n>=4, retain all signed edge lines e_i+e_j and e_i-e_j and any +k coordinate-axis lines. With the fixed dense binary orthogonality pairing, +the exact root-code Gram decoder costs at least + + n(n-1)+k = number of retained lines. + +Coordinate factors attain the bound. Every optimum has exactly n nonzero +terms, even when arbitrary finite term counts and arbitrary coefficients +over a field of characteristic other than two are allowed. + +This is a **scoped proof with finite corroboration**. The new case is +0=4; 0=4 and finite term count over any field of characteristic other than two.", + "scope_change_reason": "Take the explicit puncture question of ywz65 PR2582. The new result adds the intermediate-axis all-term obstruction; it does not claim the original constructive five-percent gate.", + "bottleneck_link": "A scoped negative screen prevents spending synthesis effort on axis deletion alone in this larger mixed-length alphabet. It is an algebraic side result, not a complete recursive invoice.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved partial-axis floor with bounded exact support and factorization corroboration; do not extend the family.", + "outcome": "negative-result", + "evidence": "PROOF.md and generated RESULT.json; finite mixed-axis supports, coordinate attainments, exact rational expansions, all-term inequality controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which specified signed-edge deletion permits a strict exact root-code Gram gain?", + "why_it_matters": "All signed edges are essential to the cited tariff; axis deletion alone is closed by this result.", + "first_step": "Choose one n=4 mixed-axis set, remove specified signed edges and exhibit a complete exact factorization with all literal support ranks.", + "blocked_by": "A new support tariff and complete physical consumer are not supplied." + }, + { + "question": "Can one sparse fitting pairing lower the intermediate-axis coordinate bill?", + "why_it_matters": "The theorem fixes the dense pairing; deleting entries is not rank-monotone.", + "first_step": "At n=4,k=1 enumerate one shared fitting pairing and compute every coordinate-term rectangle.", + "blocked_by": "Shared-pairing compatibility, global optimum and physical realization remain open." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133737", + "base_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "scope_coverage": "Live open PRs and 60 recent account PRs; last 50 handoff comments; distinctive merged/main README/proof searches. Cached search pending at claim time. No complete unpublished/code-diff coverage.", + "cached_overlap": { + "searched_at": "2026-10-22T22:16:39.878065+00:00", + "coverage": { + "local": { + "head": "624de9dc66858af0945e5f8a0942488d62280d43", + "records": 115, + "head_records": 6319, + "complete_head_inventory": false + }, + "open_prs": { + "fetched_at": "2026-10-22T22:14:21.920233+00:00", + "complete_pagination": true, + "records": 379 + }, + "discussions": { + "fetched_at": "2026-10-22T22:16:39.717321+00:00", + "complete_pagination": true, + "records": 3855 + } + }, + "matches_total": 215, + "limitations": [ + "local: 6204 HEAD note paths were not searched; inspect coverage.local.unsearched_head_paths in --json output and materialize relevant notes before treating a lack of matches as evidence." + ] + } + }, + "submission_refresh": { + "checked_at": "2026-10-22T22:20:53.722937+00:00", + "main_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "live_overlap": "Newest 100 open PRs and latest 30 handoff comments checked. No competing partial-axis root-code target found; merged exact-formula search returned no records. Full README/proof searches included axis-puncture and missing-axis terminology." + }, + "claim_type": "scoped proof with finite corroboration" +} diff --git a/research/axis-punctured-root-code-floor/VERIFY.json b/research/axis-punctured-root-code-floor/VERIFY.json new file mode 100644 index 0000000000..61cd2e2d7b --- /dev/null +++ b/research/axis-punctured-root-code-floor/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact mixed-axis support census, coordinate attainments, rational expansions, count bounds, controls and hash-bound generated receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Repeat every finite check and receipt comparison with assertions optimized out." + } + ] +} diff --git a/research/axis-punctured-root-code-floor/verify.py b/research/axis-punctured-root-code-floor/verify.py new file mode 100644 index 0000000000..e50c0be578 --- /dev/null +++ b/research/axis-punctured-root-code-floor/verify.py @@ -0,0 +1,270 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration for the partial-axis theorem; standard library.""" + +import argparse +import copy +import hashlib +import itertools +import json +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +BOUND_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py" +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank2(rows, width): + """At most len(rows)*width pivot steps, no mutable shared basis.""" + basis = [0] * width + rank = 0 + for original in rows: + value = original + for pivot in range(width - 1, -1, -1): + if not (value >> pivot) & 1: + continue + if basis[pivot]: + value ^= basis[pivot] + else: + basis[pivot] = value + rank += 1 + break + return rank + + +def geometry(n, axes, scale=1): + require(4 <= n <= 12, "finite checker dimension must be 4..12") + require(0 <= axes < (1 << n), "axis mask outside dimension") + require(scale != 0, "axis scale must be nonzero") + roots = [] + for i in range(n): + if (axes >> i) & 1: + roots.append(tuple(scale * (j == i) for j in range(n))) + for i, j in itertools.combinations(range(n), 2): + for sign in (1, -1): + roots.append(tuple((h == i) + sign * (h == j) for h in range(n))) + pairing = [] + for i, row in enumerate(roots): + bits = 0 + for j, col in enumerate(roots): + if i == j or sum(a * b for a, b in zip(row, col)) == 0: + bits |= 1 << j + pairing.append(bits) + return roots, pairing + + +def support(roots, vector, prime=0): + bits = 0 + for i, row in enumerate(roots): + value = sum(a * b for a, b in zip(row, vector)) + if prime: + value %= prime + if value: + bits |= 1 << i + return bits + + +def cost(pairing, left, right): + rows = [row & right for i, row in enumerate(pairing) if (left >> i) & 1] + return rank2(rows, len(pairing)) + + +def projective_vectors(n, prime): + require((n, prime) in ((4, 3), (5, 3), (4, 5)), "unregistered census") + vectors = [] + for vector in itertools.product(range(prime), repeat=n): + nonzero = [v for v in vector if v] + if nonzero and nonzero[0] == 1: + vectors.append(vector) + require(len(vectors) == (prime ** n - 1) // (prime - 1), "projective count") + return vectors + + +def axis_index(vector): + indices = [i for i, v in enumerate(vector) if v] + return indices[0] if len(indices) == 1 else None + + +def local_bound(n, axes, x, y): + marked = any(v and ((axes >> i) & 1) for i, v in enumerate(x)) and any( + v and ((axes >> i) & 1) for i, v in enumerate(y) + ) + if marked: + return n + if n % 2 == 0: + return n - 1 + a, b = axis_index(x), axis_index(y) + if a is not None and b is not None and a != b: + return n - 2 + return n if a is None and b is None else n - 1 + + +def mixed_support_census(n, prime): + """Every intermediate axis mask and projective pair in the finite field.""" + vectors = projective_vectors(n, prime) + comparisons = 0 + digest = hashlib.sha256() + histogram = {} + for axes in range(1, (1 << n) - 1): + roots, pairing = geometry(n, axes) + supports = [support(roots, x, prime) for x in vectors] + for i, x in enumerate(vectors): + for j, y in enumerate(vectors): + actual = cost(pairing, supports[i], supports[j]) + require(actual >= local_bound(n, axes, x, y), "mixed-axis tariff") + histogram[actual] = histogram.get(actual, 0) + 1 + digest.update(bytes((axes, i, j, actual))) + comparisons += 1 + return {"n": n, "prime": prime, "projective_vectors": len(vectors), + "axis_masks": (1 << n) - 2, "support_pairs": comparisons, + "rank_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "sha256": digest.hexdigest()} + + +def coordinate_attainments(): + records = [] + for n in range(4, 13): + # Every mask through n=6, then all cardinalities by permutation symmetry. + masks = range(1, (1 << n) - 1) if n <= 6 else ((1 << k) - 1 for k in range(1, n)) + for axes in masks: + for scale in (1, 2): + roots, pairing = geometry(n, axes, scale) + prices = [] + for i in range(n): + vector = tuple(int(j == i) for j in range(n)) + side = support(roots, vector) + price = cost(pairing, side, side) + require(price == n - 1 + ((axes >> i) & 1), "coordinate price") + prices.append(price) + expected = n * (n - 1) + axes.bit_count() + require(sum(prices) == expected, "attained punctured floor") + records.append({"n": n, "axes": axes, "scale": scale, + "prices": prices, "total": expected}) + return records + + +def endpoint(terms, n): + return [[sum(x[i] * y[j] for x, y in terms) for j in range(n)] for i in range(n)] + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def expansion_fixtures(): + records = [] + for n in range(4, 9): + unit = [tuple(Fraction(i == j) for i in range(n)) for j in range(n)] + base = [(x, x) for x in unit] + difference = tuple(unit[0][i] - unit[1][i] for i in range(n)) + two_cheap = [(unit[0], unit[1]), (unit[1], unit[0]), + (difference, difference)] + base[2:] + minus = tuple(-v for v in unit[0]) + cancel = base + [(unit[0], unit[1]), (minus, unit[1])] + # A noncoordinate rational dual pair, plus a split one-extra variant. + left = tuple(unit[0][i] + Fraction(2, 3) * unit[1][i] for i in range(n)) + dual = tuple(unit[1][i] - Fraction(2, 3) * unit[0][i] for i in range(n)) + shear = [(left, unit[0]), (unit[1], dual)] + base[2:] + half = tuple(v / 2 for v in left) + split = [(half, unit[0]), (half, unit[0])] + shear[1:] + for k in range(1, n): + axes = ((1 << k) - 1) << (n - k) + roots, pairing = geometry(n, axes) + for name, terms in (("coordinate", base), ("two-cheap", two_cheap), + ("cancel", cancel), ("rational-shear", shear), + ("split", split)): + require(endpoint(terms, n) == identity(n), "exact Gram coefficient identity") + prices = [cost(pairing, support(roots, x), support(roots, y)) for x, y in terms] + floor = n * (n - 1) + k + require(sum(prices) >= floor, "expansion price below floor") + require(len(terms) == n or sum(prices) > floor, "overcomplete equality") + records.append({"n": n, "k": k, "name": name, "terms": len(terms), + "prices": prices, "cost": sum(prices), "floor": floor}) + return records + + +def term_count_bounds(): + checked = 0 + for n in range(4, 129): + for k in range(n + 1): + floor = n * (n - 1) + k + for m in range(n, n + 7): + if n % 2 == 0: + bound = m * (n - 1) + k + elif m == n: + bound = n * (n - 1) + k + elif m == n + 1: + bound = m * (n - 1) - 2 + k + else: + bound = m * (n - 2) + 2 * k + require(bound >= floor, "count lower bound") + require(m == n or bound > floor, "strict excess for additional terms") + checked += 1 + return checked + + +def canonical(value): + """JSON spelling distinguishes booleans from integers in receipts.""" + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def controls(): + n, axes = 5, 0b11100 + roots, pairing = geometry(n, axes) + unit = [tuple(int(i == j) for i in range(n)) for j in range(n)] + x, y = unit[0], unit[1] + sx, sy = support(roots, x), support(roots, y) + require(cost(pairing, sx, sy) == n - 2, "unmatched missing-axis cheap witness") + require(endpoint([(x, y)], n) != identity(n), "cheap term is not an exact expansion") + require(sum(x[i] * y[i] for i in range(n)) == 0, "cheap term excluded from square dual") + require(local_bound(n, axes, unit[2], unit[3]) == n, "retained stars need extra charge") + require(n * (n - 1) < n * (n - 1) + axes.bit_count(), "unmarked-only bill loses axes") + edge_roots, _ = geometry(4, 0) + require(support(edge_roots, (1, 1, 1, 1), 2) == 0, "characteristic two loses injection") + sparse = [1 << i for i in range(len(pairing))] + require(cost(sparse, sx, sy) != cost(pairing, sx, sy), "sparse mask changes tariff") + require(canonical({"cost": 1}) != canonical({"cost": True}), "typed receipt control") + return 8 + + +def evidence(): + return {"schema": "axis-punctured-root-code-floor/v1", + "claim_type": "scoped proof with finite corroboration", + "scope": "n>=4; 0