From d57696c77de68ce61431e81cf4104e3379cc4f16 Mon Sep 17 00:00:00 2001 From: just-mn <77879381+just-mn@users.noreply.github.com> Date: Tue, 13 Oct 2026 20:59:00 +0200 Subject: [PATCH 1/3] Preserve pinned PR845 geometry and attribution [skip ci] --- .../p112-masked-walsh/vendor/pr845-NOTICE.md | 31 +++ .../p112-masked-walsh/vendor/pr845-PROOF.md | 161 ++++++++++++++++ .../vendor/pr845-geometry.py | 177 ++++++++++++++++++ 3 files changed, 369 insertions(+) create mode 100644 research/p112-masked-walsh/vendor/pr845-NOTICE.md create mode 100644 research/p112-masked-walsh/vendor/pr845-PROOF.md create mode 100644 research/p112-masked-walsh/vendor/pr845-geometry.py diff --git a/research/p112-masked-walsh/vendor/pr845-NOTICE.md b/research/p112-masked-walsh/vendor/pr845-NOTICE.md new file mode 100644 index 0000000000..eb811ef7e6 --- /dev/null +++ b/research/p112-masked-walsh/vendor/pr845-NOTICE.md @@ -0,0 +1,31 @@ +# Attribution and license + +Prepared for Mihir Srivastava (@mihir-s-05), with substantial OpenAI Codex +assistance in the proof, experiments, implementation, verification and +writing. No independent human review or proof-assistant verification is +claimed. New work is under the repository's Apache-2.0 license. + +- DreamingOfClouds' PR717, pinned at + `4150829a2cb66b823f4282da98985959ee448a90`, supplies the P112 decoder + model, root and simple-basis conventions, and the open mixed-beta question. + `reference/pr717_e8model.py` is an unchanged copy. `geometry.py` adapts + its geometry definition using exact standard-library arithmetic. + `reference-geometry.json` is a snapshot of its arrays as described in + SOURCES.json. The original notice is retained in + `reference/PR717-NOTICE.md`, including its Claude assistance disclosure. +- Joel Pulikkan / GamingPuzzled's PR620 records the coordinate P112 copy + cost 64. This contribution claims neither priority for that value nor + verification of all other claims in that package. +- DreamingOfClouds' PR446 Theorem C supplies the inherited copy-tree + interpretation. Its proof and physical correspondence have not been + newly audited here. +- Jacob Sussman, Zhihao Chen (jacklightChen), Dylan Crow + (utcorvusvolat-dotcom), icekylinx, eumemic, Jeremy Kothe, Chafik Boukhalfa + and the wider cited community retain credit for the E8 geometry, + label/frame calculus, supplier and compiler lineage. The selected + #741/#589 construction is context, not a result of this package. + +The new contribution is the single-lift annihilator obstruction, its compact +functional-support reduction, exact finite certificates, independent +checking implementation and scoped proof. All source-specific notices and +the repository license continue to apply. diff --git a/research/p112-masked-walsh/vendor/pr845-PROOF.md b/research/p112-masked-walsh/vendor/pr845-PROOF.md new file mode 100644 index 0000000000..609a2b1f83 --- /dev/null +++ b/research/p112-masked-walsh/vendor/pr845-PROOF.md @@ -0,0 +1,161 @@ +# One additional total cannot lower the coordinate P112 copy-rank cost + +This is a theorem about the precise finite algebraic model below. Its finite +premises have exact executable certificates. The all-real-parameter argument +is written mathematics, not a proof-assistant formalization. + +## Model and result + +Use DreamingOfClouds' PR717 P112 model, pinned in `SOURCES.json`: the 120 real +E8 root lines with the eight mutually orthogonal frame lines +`e_(2j) +/- e_(2j+1)` removed. Roots have squared norm 2. Let `G` be their +112 by 112 Gram matrix, and let `X_ij = ` for the deleted frame. +Then `X X^T = 2G`, `rank_R X = 8`, and every entry of X is 0 or +/-1. +Write x_j for column j of X. + +Labels l_i belong to F2^9, with a nondegenerate symmetric bilinear form S +such that `l_i S l_t^T = 1 + G_it (mod 2)`. The code stores the labels and +their duals `v_i = l_i S` as nine-bit integers. For a real column d let +`V(d) = span_F2 {v_i : d_i != 0}`. Define + + beta(d,t) = rank_F2 (l_i S l_u^T)_{i in supp(d), u in supp(t)}. + +This is the inherited per-total pairing-rank copy cost. The eight coordinate +terms `x_j x_j^T` each have beta 8, for total 64. Priority for this value +belongs to PR620 and its construction predecessors. + +**Theorem.** For every `a in R^8` and **every** `z in R^112`, + + sum_(j=0)^7 beta(x_j, x_j - a_j z) + beta(Xa, z) >= 64. (1) + +These terms always give the exact identity + + X X^T = sum_j x_j (x_j-a_j z)^T + (Xa) z^T. (2) + +Thus an added total with an arbitrary source vector cannot improve the copy +rank while the eight coordinate reader columns are retained. The class +allows asymmetric factors, arbitrary real magnitudes, negative coefficients, +source vectors outside col(X), and terms of pairing rank below 8. +Equality is attained by z=0. The transposed statement follows from the +symmetry of beta and X X^T. + +This includes every exact nine-term factorization retaining those eight +reader columns: if the ninth source z is nonzero, reducing the identity +modulo col(X) forces its reader d into col(X), so d=Xa. Since X has full +column rank, the remaining source matrix must be X-za^T. Independent +nonzero rescaling of the original reader columns can be absorbed into their +source columns. A zero ninth source is harmless. + +This last characterization requires exact equality to 2G on **all** entries. +It does not cover a masked completion corrected by additional zero-cost +terms, simultaneous changes of the original reader columns, two or more +additional totals, or interacting copy programs outside this cost model. + +## Finite geometry lemma + +For each j, the space `V_j = V(x_j)` has dimension 8, and +`beta(x_j,x_j)=8`. If a has at least two nonzero coordinates, `V(Xa)=F2^9`. + +Here is a short exact certificate for the second claim. For every nonzero +binary functional q on the dual-label space, form + + I_q = {i : q dot v_i = 1}. + +Of the 511 matrices `X[I_q,:]`, 503 have rational rank 8. The other eight +have rank 7; each has one identically zero column, and these columns run +through all eight coordinates exactly once. `RESULTS.json` provides +independent row indices for every matrix. The second checker verifies the +511 nonzero integer minors by fraction-free Bareiss elimination. In the +rank-7 cases it also checks the zero column on the entire support, proving +that the real kernel is exactly the associated coordinate axis. + +If V(Xa) were proper, a nonzero q would annihilate it, whence +`X[I_q,:] a=0`. The census forces a=0 or a on a coordinate axis. This is +impossible when a has at least two nonzero coordinates. Rational rank equals +real rank for these integer matrices, so this reasoning covers all real a, +not only a finite coefficient search. + +## Annihilators convert cost into a dimension bound + +Let J be the support of a, of size k>=2, and put + + H_j = {q in V_j : q dot l_i = 0 whenever x_ij-a_j z_i != 0}, + H_0 = {q in F2^9 : q dot l_i = 0 whenever z_i != 0}. + +Rank-nullity gives + + beta(x_j,x_j-a_j z) = 8 - dim H_j, + beta(Xa,z) = 9 - dim H_0. + +We prove that the addition map from the **external** direct sum +`(direct_sum_(j in J) H_j) direct_sum H_0` into F2^9 is injective. This gives +`sum dim H_j + dim H_0 <= 9`, so the k changed terms and the extra term +cost at least 8k. The remaining 8-k terms cost 8 each, proving (1). + +Suppose `(q_j,q_0)` is in the kernel of this addition map. At a port i +write `b_ij = q_j dot l_i`. If b_ij=1, the definition of H_j forces + + x_ij = a_j z_i. (3) + +If z_i!=0, membership in H_0 gives `q_0 dot l_i=0`. Hence an even number +of the b_ij are 1, and all their nonzero values `x_ij sign(a_j)` have the +same sign, namely sign(z_i). If z_i=0, every selected x_ij is zero. +In either case, for each sign epsilon=+1,-1 we have the binary equation + + sum_{j in J : x_ij sign(a_j)=epsilon} b_ij = 0. (4) + +These equations are necessary for every real a and z, regardless of the +magnitudes of a_j. They form a binary matrix on the 8k coefficients of +the q_j in the certified bases of V_j. A common sign reversal only exchanges +the two equations at each port. It therefore suffices to enumerate sign +vectors in {-1,0,1}^8 with at least two nonzero entries and first nonzero +entry positive. There are exactly 3,272, all checked (seed 40 changes the +traversal order only). + +| k | sign cases | rank of (4) | +|---:|---:|---:| +| 2 | 56 | 16 | +| 3 | 224 | 24 | +| 4 | 560 | 32 | +| 5 | 896 | 40 | +| 6 | 896 | 48 | +| 7 | 512 | 56 | +| 8 | 128 | 63 | + +For k<=7 the full column rank forces every q_j=0, and then q_0=0. + +**The k=8 case needs an additional check.** For every one of its 128 sign +patterns the one-dimensional kernel of (4) is explicitly recorded. At +exactly 56 ports its nonzero vector selects j's with at least two distinct +values in `{x_ij sign(a_j)}` (values 0,+1,-1 are distinguished). These demand +incompatible signs or zero/nonzero values of z_i in (3). Consequently that +nonzero vector cannot belong to the actual direct-sum kernel. The zero +vector is again the only possibility. The checkers regenerate every such +conflict, not only the first witness. The linear system alone does **not** +prove the k=8 case, and a negative control rejects that mistaken argument. + +This proves injectivity in all cases k>=2 and completes the main argument. + +## Boundary cases and proof boundary + +If a=0, the original eight terms are unchanged and the ninth reader is zero. +If only a_j is nonzero, the two affected reader spaces are both V_j. +The support of x_j is contained in the union of the supports of +`x_j-a_j z` and z. The rank of a union of column sets is at most the sum +of their ranks, so these two terms cost at least `beta(x_j,x_j)=8`. +Thus (1) also holds at k=0 and k=1. + +The finite checks certify the stated P112 geometry and the necessary +linear/conflict facts. The written rank-nullity argument, not sampled +vectors or a solver's failure to find a candidate, proves the quantified +result. No SAT/CP-SAT solver, floating-point rank, proof assistant, physical +circuit compilation, or new multiplication exponent is claimed. + +Under PR446 Theorem C's inherited separate-total copy-tree assumptions, +the result blocks a decrease in this copied-information charge. Additional +preparation, source access, frame changes, cleanup/restoration, and recursive +children were optimistically granted zero extra cost before construction. +Even that relaxation cannot make the **copy-rank sum** smaller than 64. +It does not rule out benefits in helper work, scheduling, hosting, or the +distribution of recursive ranks at the same sum. No complete cost recurrence +or physical realization is offered for an allegedly improved supplier. diff --git a/research/p112-masked-walsh/vendor/pr845-geometry.py b/research/p112-masked-walsh/vendor/pr845-geometry.py new file mode 100644 index 0000000000..34c1abf059 --- /dev/null +++ b/research/p112-masked-walsh/vendor/pr845-geometry.py @@ -0,0 +1,177 @@ +"""Exact P112 geometry, following DreamingOfClouds' pinned PR717 model. + +Apache-2.0. Prepared for Mihir Srivastava with substantial OpenAI Codex +assistance. No NumPy, floating-point solves, or predecessor imports. +""" + +from fractions import Fraction +from itertools import combinations, product + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def mask(values): + out = 0 + for value in values: + out = (out << 1) | (value % 2) + return out + + +def parity(value): + return value.bit_count() & 1 + + +def binary_basis(rows): + pivots = {} + for value in rows: + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + return [pivots[p] for p in sorted(pivots, reverse=True)] + + +def binary_kernel(rows, width): + basis = binary_basis(rows) + pivots = {v.bit_length() - 1: v for v in basis} + result = [] + for free in range(width): + if free in pivots: + continue + vector = 1 << free + for pivot, row in sorted(pivots.items()): + if parity(vector & row): + vector |= 1 << pivot + result.append(vector) + require(all(parity(r & v) == 0 for r in rows for v in result), + 'invalid binary kernel') + return result + + +def rational_basis_indices(rows): + """Select independent original rows using exact rational elimination.""" + basis = {} + selected = [] + for index, original in enumerate(rows): + row = list(map(Fraction, original)) + for pivot, previous in sorted(basis.items()): + coefficient = row[pivot] + if coefficient: + row = [a - coefficient * b for a, b in zip(row, previous)] + pivot = next((j for j, value in enumerate(row) if value), None) + if pivot is not None: + coefficient = row[pivot] + basis[pivot] = [value / coefficient for value in row] + selected.append(index) + if len(basis) == len(original): + break + return selected + + +def inverse(matrix): + size = len(matrix) + rows = [[Fraction(x) for x in row] + + [Fraction(i == j) for j in range(size)] + for i, row in enumerate(matrix)] + for col in range(size): + pivot = next(i for i in range(col, size) if rows[i][col]) + rows[col], rows[pivot] = rows[pivot], rows[col] + divisor = rows[col][col] + rows[col] = [x / divisor for x in rows[col]] + for i in range(size): + if i != col: + coefficient = rows[i][col] + rows[i] = [x - coefficient * y + for x, y in zip(rows[i], rows[col])] + return [row[size:] for row in rows] + + +def build(): + roots = [] + for i, j in combinations(range(8), 2): + for si, sj in product((1, -1), repeat=2): + vector = [0] * 8 + vector[i], vector[j] = 2 * si, 2 * sj + roots.append(vector) + roots.extend(list(s) for s in product((1, -1), repeat=8) + if s.count(-1) % 2 == 0) + simple = [[1, -1, -1, -1, -1, -1, -1, 1], + [2, 2, 0, 0, 0, 0, 0, 0], + [-2, 2, 0, 0, 0, 0, 0, 0]] + for k in range(1, 6): + vector = [0] * 8 + vector[k], vector[k + 1] = -2, 2 + simple.append(vector) + inv = inverse(simple) + gram = [[dot(a, b) // 4 for b in simple] for a in simple] + frame = [] + for j in range(4): + for sign in (1, -1): + vector = [0] * 8 + vector[2 * j], vector[2 * j + 1] = 2, 2 * sign + frame.append(vector) + lines, seen = [], set() + for root in roots: + key = max(tuple(root), tuple(-v for v in root)) + if key not in seen: + seen.add(key) + lines.append(root) + kept = [r for r in lines if r not in frame and [-v for v in r] not in frame] + labels, duals, columns = [], [], [] + for root in kept: + coordinates = [sum(root[k] * inv[k][j] for k in range(8)) + for j in range(8)] + require(all(x.denominator == 1 for x in coordinates), 'nonintegral E8 coordinates') + coordinates = [int(x) for x in coordinates] + require([sum(coordinates[k] * simple[k][j] for k in range(8)) + for j in range(8)] == root, 'root reconstruction') + labels.append(mask(coordinates + [1])) + duals.append(mask([sum(coordinates[k] * gram[k][j] for k in range(8)) + for j in range(8)] + [1])) + columns.append([dot(root, f) // 4 for f in frame]) + return {'roots': kept, 'frame': frame, 'labels': labels, + 'duals': duals, 'X': columns} + + +def check_geometry(data): + roots, frame = data['roots'], data['frame'] + labels, duals, x = data['labels'], data['duals'], data['X'] + require(len(roots) == len(labels) == len(duals) == len(x) == 112, 'P112 size') + require(len(frame) == 8 and len({tuple(r) for r in roots}) == 112, 'distinct geometry') + require(all(len(r) == 8 and dot(r, r) == 8 for r in roots), 'root norms') + require(all(len(row) == 8 and set(row) <= {-1, 0, 1} + and dot(row, row) == 4 for row in x), 'coordinate alphabet') + require(len(binary_basis(labels)) == 9, 'label span') + require(len(rational_basis_indices(x)) == 8, 'coordinate rank') + for i in range(112): + require(x[i] == [dot(roots[i], f) // 4 for f in frame], 'coordinate binding') + for j in range(112): + require(dot(roots[i], roots[j]) % 4 == 0, 'integral Gram') + gram = dot(roots[i], roots[j]) // 4 + require(dot(x[i], x[j]) == 2 * gram, 'XX^T = 2G') + require(parity(duals[i] & labels[j]) == (1 + gram) % 2, + 'binary label pairing') + + +def reader_space(values, duals): + return binary_basis(dual for value, dual in zip(values, duals) if value) + + +def evaluate(space, label): + return sum(parity(q & label) << j for j, q in enumerate(space)) + + +def term_cost(readers, sources, data): + space = reader_space(readers, data['duals']) + return len(binary_basis(evaluate(space, label) + for value, label in zip(sources, data['labels']) if value)) From efeb7a1526ca3c4c9701453cdcac3642f22b9413 Mon Sep 17 00:00:00 2001 From: just-mn <77879381+just-mn@users.noreply.github.com> Date: Tue, 13 Oct 2026 21:01:27 +0200 Subject: [PATCH 2/3] Research: exclude two masked Walsh P112 totals Exact support-cell bound for arbitrary real coefficients, 572320-case finite census, independent direct-pairing replay and corruption controls. Scoped negative result; no new kappa. Prepared for Denis (@just-mn) with substantial OpenAI Codex assistance. --- research/p112-masked-walsh/CLAIM.json | 35 ++ research/p112-masked-walsh/GEOMETRY.json | 1 + research/p112-masked-walsh/NOTICE.md | 19 + research/p112-masked-walsh/OVERLAP.json | 314 +++++++++++ research/p112-masked-walsh/README.md | 164 ++++++ research/p112-masked-walsh/RESULT.json | 499 ++++++++++++++++++ research/p112-masked-walsh/SOURCES.json | 30 ++ research/p112-masked-walsh/VALIDATION.md | 36 ++ .../p112-masked-walsh/independent_check.py | 374 +++++++++++++ research/p112-masked-walsh/test_verify.py | 65 +++ research/p112-masked-walsh/verify.py | 258 +++++++++ 11 files changed, 1795 insertions(+) create mode 100644 research/p112-masked-walsh/CLAIM.json create mode 100644 research/p112-masked-walsh/GEOMETRY.json create mode 100644 research/p112-masked-walsh/NOTICE.md create mode 100644 research/p112-masked-walsh/OVERLAP.json create mode 100644 research/p112-masked-walsh/README.md create mode 100644 research/p112-masked-walsh/RESULT.json create mode 100644 research/p112-masked-walsh/SOURCES.json create mode 100644 research/p112-masked-walsh/VALIDATION.md create mode 100644 research/p112-masked-walsh/independent_check.py create mode 100644 research/p112-masked-walsh/test_verify.py create mode 100644 research/p112-masked-walsh/verify.py diff --git a/research/p112-masked-walsh/CLAIM.json b/research/p112-masked-walsh/CLAIM.json new file mode 100644 index 0000000000..6e7fdd5fdc --- /dev/null +++ b/research/p112-masked-walsh/CLAIM.json @@ -0,0 +1,35 @@ +{ + "track": "structural decoder research", + "seed": 48, + "seed_source": "secrets.randbelow(100), operating-system randomness", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "claimed_at": "2026-10-13T11:43:53.824293+00:00", + "expected_finish": "2026-10-13T13:00:00Z", + "candidates": [ + "Two additional P112 decoder totals", + "Asymmetric higher-dimensional cube decoder", + "Restored-total reuse across decoder stages" + ], + "choice": "Two masked Walsh totals; seed 48 selects the P112 branch from the three candidates (48 mod 3 = 0).", + "object": "P112 exact 2G factorization retaining all eight coordinate reader columns, adding two cut-supported Walsh sources and two unimodular mixed readers.", + "domain": "28 coordinate pairs \u00d7 511 nonzero F2^9 label functionals \u00d7 40 matrices in {-1,0,1}^{2x2} with determinant +/-1", + "method": "Exact pairing ranks; seed-shuffled cut order; exhaust all 572320 cases, no early success stop.", + "deliverable": "Scoped complete finite cost census, deterministic certificate, exact endpoint identity, negative controls and independent replay. No new kappa.", + "coordination": "REST search returned only open issue 650 (Discussions), so no open sprint issue exists; local claim.", + "overlap": "695 open PRs inspected through #904; #845 covers one total; #717 covers in-column-space/gauge families and reports unfinished mixed-beta searches; #669 and #772 already cover asymmetric proper-star geometry; #848 covers restored R439 sharing. None covers the declared masked-Walsh family.", + "revised_expected_finish": "2026-10-13T19:30:00Z", + "refinement": "The finite census revealed a support-cell reduction: additionally certify an optimistic lower bound for arbitrary real coefficient matrices with both columns nonzero, using six scalar and five reader-support representatives.", + "continuation_recorded_at": "2026-10-13T18:46:49Z", + "outcome": { + "status": "completed scoped negative result", + "result": "README.md", + "certificate": "RESULT.json", + "all_real_copy_lower_bound": 72, + "all_real_nonzero_sources_lower_bound": 77, + "finite_cases": 572320, + "finite_minimum": 72, + "finite_nonzero_sources_minimum": 78, + "independent_replay": "passed; direct binary pairing matrices match all histograms", + "publication_branch": "https://github.com/just-mn/integer-mult-bounds/tree/codex/p112-masked-walsh/research/p112-masked-walsh" + } +} diff --git a/research/p112-masked-walsh/GEOMETRY.json b/research/p112-masked-walsh/GEOMETRY.json new file mode 100644 index 0000000000..cc6fe0ece6 --- /dev/null +++ b/research/p112-masked-walsh/GEOMETRY.json @@ -0,0 +1 @@ +{"X":[[1,1,1,1,0,0,0,0],[1,1,-1,-1,0,0,0,0],[1,1,1,-1,0,0,0,0],[1,1,-1,1,0,0,0,0],[1,1,0,0,1,1,0,0],[1,1,0,0,-1,-1,0,0],[1,1,0,0,1,-1,0,0],[1,1,0,0,-1,1,0,0],[1,1,0,0,0,0,1,1],[1,1,0,0,0,0,-1,-1],[1,1,0,0,0,0,1,-1],[1,1,0,0,0,0,-1,1],[1,-1,1,1,0,0,0,0],[1,-1,-1,-1,0,0,0,0],[1,-1,1,-1,0,0,0,0],[1,-1,-1,1,0,0,0,0],[1,-1,0,0,1,1,0,0],[1,-1,0,0,-1,-1,0,0],[1,-1,0,0,1,-1,0,0],[1,-1,0,0,-1,1,0,0],[1,-1,0,0,0,0,1,1],[1,-1,0,0,0,0,-1,-1],[1,-1,0,0,0,0,1,-1],[1,-1,0,0,0,0,-1,1],[0,0,1,1,1,1,0,0],[0,0,1,1,-1,-1,0,0],[0,0,1,1,1,-1,0,0],[0,0,1,1,-1,1,0,0],[0,0,1,1,0,0,1,1],[0,0,1,1,0,0,-1,-1],[0,0,1,1,0,0,1,-1],[0,0,1,1,0,0,-1,1],[0,0,1,-1,1,1,0,0],[0,0,1,-1,-1,-1,0,0],[0,0,1,-1,1,-1,0,0],[0,0,1,-1,-1,1,0,0],[0,0,1,-1,0,0,1,1],[0,0,1,-1,0,0,-1,-1],[0,0,1,-1,0,0,1,-1],[0,0,1,-1,0,0,-1,1],[0,0,0,0,1,1,1,1],[0,0,0,0,1,1,-1,-1],[0,0,0,0,1,1,1,-1],[0,0,0,0,1,1,-1,1],[0,0,0,0,1,-1,1,1],[0,0,0,0,1,-1,-1,-1],[0,0,0,0,1,-1,1,-1],[0,0,0,0,1,-1,-1,1],[1,0,1,0,1,0,1,0],[1,0,1,0,1,0,-1,0],[1,0,1,0,0,1,0,1],[1,0,1,0,0,1,0,-1],[1,0,1,0,0,-1,0,1],[1,0,1,0,0,-1,0,-1],[1,0,1,0,-1,0,1,0],[1,0,1,0,-1,0,-1,0],[1,0,0,1,1,0,0,1],[1,0,0,1,1,0,0,-1],[1,0,0,1,0,1,1,0],[1,0,0,1,0,1,-1,0],[1,0,0,1,0,-1,1,0],[1,0,0,1,0,-1,-1,0],[1,0,0,1,-1,0,0,1],[1,0,0,1,-1,0,0,-1],[1,0,0,-1,1,0,0,1],[1,0,0,-1,1,0,0,-1],[1,0,0,-1,0,1,1,0],[1,0,0,-1,0,1,-1,0],[1,0,0,-1,0,-1,1,0],[1,0,0,-1,0,-1,-1,0],[1,0,0,-1,-1,0,0,1],[1,0,0,-1,-1,0,0,-1],[1,0,-1,0,1,0,1,0],[1,0,-1,0,1,0,-1,0],[1,0,-1,0,0,1,0,1],[1,0,-1,0,0,1,0,-1],[1,0,-1,0,0,-1,0,1],[1,0,-1,0,0,-1,0,-1],[1,0,-1,0,-1,0,1,0],[1,0,-1,0,-1,0,-1,0],[0,1,1,0,1,0,0,1],[0,1,1,0,1,0,0,-1],[0,1,1,0,0,1,1,0],[0,1,1,0,0,1,-1,0],[0,1,1,0,0,-1,1,0],[0,1,1,0,0,-1,-1,0],[0,1,1,0,-1,0,0,1],[0,1,1,0,-1,0,0,-1],[0,1,0,1,1,0,1,0],[0,1,0,1,1,0,-1,0],[0,1,0,1,0,1,0,1],[0,1,0,1,0,1,0,-1],[0,1,0,1,0,-1,0,1],[0,1,0,1,0,-1,0,-1],[0,1,0,1,-1,0,1,0],[0,1,0,1,-1,0,-1,0],[0,1,0,-1,1,0,1,0],[0,1,0,-1,1,0,-1,0],[0,1,0,-1,0,1,0,1],[0,1,0,-1,0,1,0,-1],[0,1,0,-1,0,-1,0,1],[0,1,0,-1,0,-1,0,-1],[0,1,0,-1,-1,0,1,0],[0,1,0,-1,-1,0,-1,0],[0,1,-1,0,1,0,0,1],[0,1,-1,0,1,0,0,-1],[0,1,-1,0,0,1,1,0],[0,1,-1,0,0,1,-1,0],[0,1,-1,0,0,-1,1,0],[0,1,-1,0,0,-1,-1,0],[0,1,-1,0,-1,0,0,1],[0,1,-1,0,-1,0,0,-1]],"duals":[241,497,217,473,205,461,199,455,195,451,449,193,465,209,505,249,493,237,487,231,483,227,225,481,317,61,311,55,307,51,49,305,277,21,287,31,283,27,25,281,271,15,13,269,261,5,7,263,385,387,391,133,397,143,139,137,409,155,159,157,149,151,147,401,433,179,183,181,189,191,187,441,169,171,175,429,165,423,419,417,353,99,103,101,109,111,107,361,121,123,127,381,117,375,371,369,81,83,87,341,93,351,347,345,73,331,335,333,325,327,323,65],"frame":[[2,2,0,0,0,0,0,0],[2,-2,0,0,0,0,0,0],[0,0,2,2,0,0,0,0],[0,0,2,-2,0,0,0,0],[0,0,0,0,2,2,0,0],[0,0,0,0,2,-2,0,0],[0,0,0,0,0,0,2,2],[0,0,0,0,0,0,2,-2]],"labels":[161,97,177,113,185,121,189,125,191,127,235,43,225,33,241,49,249,57,253,61,255,63,171,107,217,25,221,29,223,31,139,75,201,9,205,13,207,15,155,91,199,7,147,83,195,3,151,87,491,383,381,297,377,301,303,443,369,293,295,435,291,439,437,481,353,309,311,419,307,423,421,497,315,431,429,505,425,509,511,363,321,277,279,387,275,391,389,465,283,399,397,473,393,477,479,331,267,415,413,457,409,461,463,347,401,453,455,339,451,343,341,257],"roots":[[2,0,2,0,0,0,0,0],[2,0,-2,0,0,0,0,0],[2,0,0,2,0,0,0,0],[2,0,0,-2,0,0,0,0],[2,0,0,0,2,0,0,0],[2,0,0,0,-2,0,0,0],[2,0,0,0,0,2,0,0],[2,0,0,0,0,-2,0,0],[2,0,0,0,0,0,2,0],[2,0,0,0,0,0,-2,0],[2,0,0,0,0,0,0,2],[2,0,0,0,0,0,0,-2],[0,2,2,0,0,0,0,0],[0,2,-2,0,0,0,0,0],[0,2,0,2,0,0,0,0],[0,2,0,-2,0,0,0,0],[0,2,0,0,2,0,0,0],[0,2,0,0,-2,0,0,0],[0,2,0,0,0,2,0,0],[0,2,0,0,0,-2,0,0],[0,2,0,0,0,0,2,0],[0,2,0,0,0,0,-2,0],[0,2,0,0,0,0,0,2],[0,2,0,0,0,0,0,-2],[0,0,2,0,2,0,0,0],[0,0,2,0,-2,0,0,0],[0,0,2,0,0,2,0,0],[0,0,2,0,0,-2,0,0],[0,0,2,0,0,0,2,0],[0,0,2,0,0,0,-2,0],[0,0,2,0,0,0,0,2],[0,0,2,0,0,0,0,-2],[0,0,0,2,2,0,0,0],[0,0,0,2,-2,0,0,0],[0,0,0,2,0,2,0,0],[0,0,0,2,0,-2,0,0],[0,0,0,2,0,0,2,0],[0,0,0,2,0,0,-2,0],[0,0,0,2,0,0,0,2],[0,0,0,2,0,0,0,-2],[0,0,0,0,2,0,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,0,-2],[0,0,0,0,0,2,2,0],[0,0,0,0,0,2,-2,0],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,0,-2],[1,1,1,1,1,1,1,1],[1,1,1,1,1,1,-1,-1],[1,1,1,1,1,-1,1,-1],[1,1,1,1,1,-1,-1,1],[1,1,1,1,-1,1,1,-1],[1,1,1,1,-1,1,-1,1],[1,1,1,1,-1,-1,1,1],[1,1,1,1,-1,-1,-1,-1],[1,1,1,-1,1,1,1,-1],[1,1,1,-1,1,1,-1,1],[1,1,1,-1,1,-1,1,1],[1,1,1,-1,1,-1,-1,-1],[1,1,1,-1,-1,1,1,1],[1,1,1,-1,-1,1,-1,-1],[1,1,1,-1,-1,-1,1,-1],[1,1,1,-1,-1,-1,-1,1],[1,1,-1,1,1,1,1,-1],[1,1,-1,1,1,1,-1,1],[1,1,-1,1,1,-1,1,1],[1,1,-1,1,1,-1,-1,-1],[1,1,-1,1,-1,1,1,1],[1,1,-1,1,-1,1,-1,-1],[1,1,-1,1,-1,-1,1,-1],[1,1,-1,1,-1,-1,-1,1],[1,1,-1,-1,1,1,1,1],[1,1,-1,-1,1,1,-1,-1],[1,1,-1,-1,1,-1,1,-1],[1,1,-1,-1,1,-1,-1,1],[1,1,-1,-1,-1,1,1,-1],[1,1,-1,-1,-1,1,-1,1],[1,1,-1,-1,-1,-1,1,1],[1,1,-1,-1,-1,-1,-1,-1],[1,-1,1,1,1,1,1,-1],[1,-1,1,1,1,1,-1,1],[1,-1,1,1,1,-1,1,1],[1,-1,1,1,1,-1,-1,-1],[1,-1,1,1,-1,1,1,1],[1,-1,1,1,-1,1,-1,-1],[1,-1,1,1,-1,-1,1,-1],[1,-1,1,1,-1,-1,-1,1],[1,-1,1,-1,1,1,1,1],[1,-1,1,-1,1,1,-1,-1],[1,-1,1,-1,1,-1,1,-1],[1,-1,1,-1,1,-1,-1,1],[1,-1,1,-1,-1,1,1,-1],[1,-1,1,-1,-1,1,-1,1],[1,-1,1,-1,-1,-1,1,1],[1,-1,1,-1,-1,-1,-1,-1],[1,-1,-1,1,1,1,1,1],[1,-1,-1,1,1,1,-1,-1],[1,-1,-1,1,1,-1,1,-1],[1,-1,-1,1,1,-1,-1,1],[1,-1,-1,1,-1,1,1,-1],[1,-1,-1,1,-1,1,-1,1],[1,-1,-1,1,-1,-1,1,1],[1,-1,-1,1,-1,-1,-1,-1],[1,-1,-1,-1,1,1,1,-1],[1,-1,-1,-1,1,1,-1,1],[1,-1,-1,-1,1,-1,1,1],[1,-1,-1,-1,1,-1,-1,-1],[1,-1,-1,-1,-1,1,1,1],[1,-1,-1,-1,-1,1,-1,-1],[1,-1,-1,-1,-1,-1,1,-1],[1,-1,-1,-1,-1,-1,-1,1]]} diff --git a/research/p112-masked-walsh/NOTICE.md b/research/p112-masked-walsh/NOTICE.md new file mode 100644 index 0000000000..c539578f6f --- /dev/null +++ b/research/p112-masked-walsh/NOTICE.md @@ -0,0 +1,19 @@ +# Attribution and license + +Prepared for Denis (@just-mn), with substantial OpenAI Codex assistance in +research, proof development, implementation, verification and documentation. +An economical separate Codex worker implemented the independent pairing-matrix +replay. This is AI-assisted independent implementation, not human peer review. + +New files are under the repository's Apache-2.0 license. +`vendor/pr845-geometry.py`, `vendor/pr845-PROOF.md` and `vendor/pr845-NOTICE.md` +are unchanged copies from Mihir Srivastava (@mihir-s-05), PR845 at +125ce25bdae421627b56077adc14940c2d0aa52f. Their original notice is retained. +They credit DreamingOfClouds' PR717 model and PR446 copy interpretation and +Joel Pulikkan / GamingPuzzled's PR620 baseline. All remain predecessor work. +GEOMETRY.json is generated from that exact geometry implementation. + +The context of the selected construction retains Jeremy Kothe's PR799, +Chafik Boukhalfa's PR741, DreamingOfClouds' PR589, eumemic's PR555 and the +repository's cumulative contributor lineage. No priority for their results, +or a new selected kappa, is claimed here. diff --git a/research/p112-masked-walsh/OVERLAP.json b/research/p112-masked-walsh/OVERLAP.json new file mode 100644 index 0000000000..0450dc951a --- /dev/null +++ b/research/p112-masked-walsh/OVERLAP.json @@ -0,0 +1,314 @@ +{ + "checked_at": "2026-10-13T18:52:13.509613+00:00", + "scope": "latest 200 updated open PR records; non-atomic de-duplicated snapshot", + "records": 200, + "relevant": [ + { + "number": 1125, + "title": "Research: exact asynchronous P104 carrier bound across 7,168 decoders", + "head": "9f7c0679d64bab954b7161d8586dc626a59b92ee", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1125" + }, + { + "number": 1119, + "title": "Finite complex construction: two-sided Markowitz LPR cleanup refactorization on U8 (-2,580 macros, -37,320 real prims per orientation, seed 30, no new kappa)", + "head": "bc0140e016bd865fffc7fdf64e12158183d52339", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1119" + }, + { + "number": 1084, + "title": "Research: bit E8 decoder witness and 9/17 pairing-cost floor", + "head": "ac8bd04538e692efa9c9b16bd79de5a45edcc9a5", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1084" + }, + { + "number": 1079, + "title": "Scoped negative result: R439 source-substitution census has one known survivor", + "head": "bb20dab261884412f2d2a7955cdb2fd8e2e64a16", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1079" + }, + { + "number": 1071, + "title": "Research: delivery lower bounds for #968's frame-pair centers (no new \u03ba)", + "head": "ce9531beba1ce115fdcdc44925ded995a29b8bac", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1071" + }, + { + "number": 1070, + "title": "Research audit: sharp arbitrary-mask affine agreement (no new kappa)", + "head": "8a4291875449f3e46f952465e200e7fe2c620958", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1070" + }, + { + "number": 956, + "title": "Research: close the PR390 heterogeneous physical provider in exact RAM", + "head": "fa4df77c9dfdbac93368d95dcb361e69b3b65464", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/956" + }, + { + "number": 1060, + "title": "Construction: exact complex P111 COPY word with a smaller paid recursive moment", + "head": "d27499553138bde007f5b1163e65e71da1b18899", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1060" + }, + { + "number": 1048, + "title": "Research: the bit paid profile is the whole bit supplier \u2014 exact pricer, and the reframing class is exhausted at #589 (no \u03ba claim)", + "head": "07730cd8302c378607259a9ad0efb73e0b57a2f2", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1048" + }, + { + "number": 1014, + "title": "Research note: 30 all-dimension parity edge obstructions beyond local frames", + "head": "830842d08c48d7b7f6847882d065157b3e978b3c", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1014" + }, + { + "number": 993, + "title": "Research note: exact incident-safe parity frame dimensions (no new kappa)", + "head": "76b71ff5bea1088fb5019dea25fe89698287e673", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/993" + }, + { + "number": 669, + "title": "Research: exact star-decoder hierarchies, target budgets, and COPY bounds", + "head": "8f4600b41bf1f0f5d07f209e5d3950eb22ef5cad", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/669" + }, + { + "number": 620, + "title": "Research notes (no \u03ba claim): E8 decoder floors are tight; #615 levers exhausted; +1.1e-7 \u03ba owner-map headroom on #617", + "head": "8f0150e0d0a8a02370907be35cccd3ca69cdd941", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/620" + }, + { + "number": 757, + "title": "Research: solver-free P111 copied-rank certificate and source-order correction", + "head": "e2ec7d7e719031e8f8b8012a4ab5b20faed074ce", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/757" + }, + { + "number": 933, + "title": "Scoped negative result: no relocation or Steinberg rewrite with exact reframing raises PR589's bit c (no new kappa)", + "head": "b9348c6907516e55dc07e135ad4d7a480d4f9840", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/933" + }, + { + "number": 647, + "title": "Research: paid-copy E8 exact-RAM realization with an attributed DFT corollary", + "head": "3b3fda9c602fbe4b45d02d1ead0b757b3c94f52c", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/647" + }, + { + "number": 912, + "title": "Research/seed42 decoder", + "head": "945b3da1f1dd87cebd456b3a0459601b15f7ea8b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/912" + }, + { + "number": 899, + "title": "Helper minimality (no \u03ba claim): the shipped helper layers of #656 / #799 are minimal for their op multiset", + "head": "75e7699a691f321861ab8fe303f8bd8e6a6fc393", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/899" + }, + { + "number": 895, + "title": "No new \u03ba: BW16 as a unit \u2014 window c \u2265 72 puts its ceiling at 0.649\u00d7 E8's (checked)", + "head": "3bf6fccaf17521ffdb9b3bec2740ba4886478556", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/895" + }, + { + "number": 888, + "title": "Research: Gaussian nonlinear message copy floor 40b under explicit width pricing", + "head": "8c9964b7ab4419409d20762c8d78591701008d04", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/888" + }, + { + "number": 717, + "title": "Format limits part 2 (no \u03ba claim): erratum to #595, exact invoice prices, frontier-word censuses, decoder floors, spec requirements, centre and fragmentation walls", + "head": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/717" + }, + { + "number": 878, + "title": "[Lean] Verify selected PR589 B boundaries and XOR interfaces", + "head": "7b3241566ddfd50548e6b113ede9333826b86313", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/878" + }, + { + "number": 868, + "title": "Research: Gaussian E8 all-clique certificate ceiling is 40 (no new kappa)", + "head": "54cbbea75b587bdf43a1c123e52220f936641d6f", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/868" + }, + { + "number": 831, + "title": "Research audit: F4 alternating trace is not by itself a phase-compilation obstruction (no new kappa)", + "head": "66c3bc5c2eb5a2c066b1119310b29d26350e1dde", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/831" + }, + { + "number": 825, + "title": "Research theorem: common-flag rational-frame obstruction (no new kappa)", + "head": "421db1ca2eb26056e82797f94b8c4eecd0120620", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/825" + }, + { + "number": 814, + "title": "Research: Eisenstein nonlinear message copy floor 22b under explicit width pricing", + "head": "d91c5152b314391406b0ec792b6765a5cf0af2f1", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/814" + }, + { + "number": 810, + "title": "Research construction: shorten R420 phase-B block 8 from 47 to 30 XORs (no new kappa)", + "head": "6e1fd9c00c1b0463debaac343db2948e02bcede7", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/810" + }, + { + "number": 801, + "title": "Research: certified format ceilings for Eisenstein/Gaussian/Hurwitz E8 copy floors (no \u03ba claim)", + "head": "f0758653a5a1f72c3b59e58d6fe8d658db20b50b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/801" + }, + { + "number": 673, + "title": "Research: dirty echo, verifier repair, and priced bit-sharing boundaries", + "head": "0b4f514c60d9bc7786415d7cbc24754f24d6dc3b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/673" + }, + { + "number": 798, + "title": "Research note: Eisenstein E8 copy cost \u226522 and sharp clique-method limit", + "head": "0aea3382e49abd9a59d3cb6676cdb26fd15b04e5", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/798" + }, + { + "number": 794, + "title": "Research construction: R420 target-basis compensation saves 7,879 XORs within the existing 192-bit nine-stage prefix charge (no new \u03ba)", + "head": "6be7364e0245c5a1c931cb1c43b3da991b755850", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/794" + }, + { + "number": 782, + "title": "independent verification: r420 lattice parity and 480 added incidences", + "head": "a4ef6ed2f33834e4599bf84317ae9d98ba2d9547", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/782" + }, + { + "number": 790, + "title": "Research note: factor R420 block 9 from 38 to 24 XORs (28 fewer native ADDs, no new \u03ba)", + "head": "08b4a039ba4938dd4f4c89a69759f49ed21923ef", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/790" + }, + { + "number": 785, + "title": "Scoped negative result: Hurwitz copy floor for fixed-support nonlinear messages", + "head": "83e78085ae9c110a34bff87e71387292d85e47c0", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/785" + }, + { + "number": 775, + "title": "Scoped negative result: coupled partial read exchanges on P6k4", + "head": "d4c60b58d48310ffd5b65bc99ff5b40ed2e59b14", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/775" + }, + { + "number": 770, + "title": "Research: Gaussian E8 weighted maximal-clique ceiling 40 and independent replay", + "head": "48d027a664288ea1d4e987de63cb79588b8b936b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/770" + }, + { + "number": 767, + "title": "Scoped negative result: Gaussian E8 planar and incidence decoder obstructions", + "head": "96b4b74677d1bef99e8346bfb6a4ed0531e58a62", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/767" + }, + { + "number": 765, + "title": "Scoped negative result: tensor E8 basis mixing cannot lower 72^d copy rank", + "head": "d8eaa3db32f76111b39db9b930f347ef30118a28", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/765" + }, + { + "number": 761, + "title": "Scoped negative result: algebraic P111 bit pairing-cost floor of 63", + "head": "287758702129e6cbca187356b92b311e8a1c843d", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/761" + } + ], + "initial_snapshot": "695 open PRs through #904 examined before the claim; current refresh examines newest activity.", + "conclusion": "No duplicate masked-Walsh two-total family found. Refreshed #912 is Hurwitz routing, #1070 XOR-affine agreement, #1084 bit punctures, #1125 P104 carriers. PR845 and PR717 heads unchanged.", + "focused_search": { + "query": "repo:CrocSwap/integer-mult-bounds is:pr P112", + "matches": 9, + "prs": [ + { + "number": 1133, + "title": "Research consolidation: rational support descent for fixed-reader single lifts (no new kappa)", + "state": "open" + }, + { + "number": 620, + "title": "Research notes (no \u03ba claim): E8 decoder floors are tight; #615 levers exhausted; +1.1e-7 \u03ba owner-map headroom on #617", + "state": "open" + }, + { + "number": 1071, + "title": "Research: delivery lower bounds for #968's frame-pair centers (no new \u03ba)", + "state": "open" + }, + { + "number": 717, + "title": "Format limits part 2 (no \u03ba claim): erratum to #595, exact invoice prices, frontier-word censuses, decoder floors, spec requirements, centre and fragmentation walls", + "state": "open" + }, + { + "number": 1098, + "title": "Independent verification: label-free P112 Gram support spectra (no new kappa)", + "state": "closed" + }, + { + "number": 998, + "title": "Scoped negative result: complex single lifts cannot lower P112 copy cost", + "state": "closed" + }, + { + "number": 845, + "title": "Scoped negative result: one added P112 total cannot reduce fixed-reader copy cost", + "state": "closed" + }, + { + "number": 1035, + "title": "Research consolidation: certify PR620 free P112 sink exclusions with exact minors", + "state": "closed" + }, + { + "number": 968, + "title": "Research: frame-pair decoders and the exact 8-term complex copy-cost floor (no new kappa)", + "state": "closed" + } + ] + }, + "upstream_head": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "selected_on_refresh": { + "kappa": "836330098538459/500000000000000000", + "decimal": "0.001672660197076918", + "source_prs": [ + 1094, + 1087, + 1082, + 1074, + 1068, + 1065, + 1063, + 1061 + ] + }, + "additional_review": { + "number": 1133, + "head": "8301a4698152cf63d3b4992145ecc8621942a6cd", + "scope": "rational support descent for fixed-reader single lifts; distinct from masked-Walsh two-total support cells" + } +} diff --git a/research/p112-masked-walsh/README.md b/research/p112-masked-walsh/README.md new file mode 100644 index 0000000000..3f06d674fc --- /dev/null +++ b/research/p112-masked-walsh/README.md @@ -0,0 +1,164 @@ +# Two masked Walsh totals cannot improve P112's copy bill + +**Scoped negative result; no new kappa.** Two source totals cut from a Walsh +pair do leave the original coordinate column space, but this family still +costs at least **72**, against the original **64**, for every real coefficient +matrix with two nonzero columns. If both masked sources are nonzero, the +certified lower bound is **77**. These are lower bounds, not claims that the +continuous optima are attained. + +The separate complete census of 572,320 small unimodular cases has exact minimum +72, or 78 when both sources are nonzero. Its cost distribution is +`{72:672, 73:448, 78:28672, 79:288064, 80:254464}`. +The written reduction below, plus exact finite premises, establishes the +all-real statement; a failed search is not its proof. + +## Reproduce + +Python 3.10+ and the standard library suffice. From the repository root: + +```sh +python3 -I -B research/p112-masked-walsh/verify.py +python3 -I -B research/p112-masked-walsh/independent_check.py +``` + +The first prints +`PASS_P112_MASKED_WALSH cases=572320 minimum=72 baseline=64 no_new_kappa`. +The second independently reconstructs the direct binary pairing matrices, +checks the full census and the continuous-class relaxation, and prints +`PASS_P112_MASKED_WALSH_INDEPENDENT`. Both compare against [RESULT.json](RESULT.json). +`verify.py --write /new/file.json` exports a fresh receipt and refuses an +existing path. [GEOMETRY.json](GEOMETRY.json) is regenerated and checked against +the pinned geometry implementation, not accepted as an unverified input. + +## Model and exact identity + +Use the P112 model of DreamingOfClouds' [PR717](https://github.com/CrocSwap/integer-mult-bounds/pull/717), +as independently implemented by Mihir Srivastava's +[PR845](https://github.com/CrocSwap/integer-mult-bounds/pull/845). +The scaled E8 roots, frame, labels and dual labels are in GEOMETRY.json. +Write `X=(x_0,...,x_7)`, with entries `0,+1,-1` and `XX^T=2G`. +For reader/source vectors d,t, define + + beta(d,t) = rank_F2 (l_i S l_j^T)_{i in supp(d), j in supp(t)}. + +Every original coordinate term has cost 8. For any pair `p> (8-k)) & 1 for k in range(9)] for v in label_masks] + else: + labels = [[int(x) for x in row] for row in raw_labels] + label_masks = [sum((v & 1) << (8-k) for k, v in enumerate(row)) + for row in labels] + if raw_duals and isinstance(raw_duals[0], int): + dual_masks = [int(v) for v in raw_duals] + duals = [[(v >> (8-k)) & 1 for k in range(9)] for v in dual_masks] + else: + duals = [[int(x) for x in row] for row in raw_duals] + dual_masks = [sum((v & 1) << (8-k) for k, v in enumerate(row)) + for row in duals] + x = as_int_rows(data, "X", ("x",)) + need(len(roots) == len(labels) == len(duals) == len(x) == N, + "geometry row count must be 112") + need(len(frame) == 8 and all(len(r) == 8 for r in frame), + "frame must contain eight 8-coordinate roots") + need(all(len(r) == 8 for r in roots), "roots must have eight coordinates") + need(all(len(r) == 9 for r in labels + duals), "labels/duals must be 9-bit rows") + need(all(len(r) == 8 for r in x), "X must have eight columns") + + # Independent binding of X and the binary pairing to the supplied roots. + need(all(dot(r, r) == 8 for r in roots), "scaled root norm is not 8") + need(all(dot(f, f) == 8 for f in frame), "scaled frame-root norm is not 8") + need(all(set(row) <= {-1, 0, 1} for row in x), "X has entries outside {-1,0,1}") + for i, root in enumerate(roots): + for j, f in enumerate(frame): + need(dot(root, f) == 4 * x[i][j], f"X/root-frame mismatch at ({i},{j})") + + # For scaled-by-2 E8 roots, G_ij=/4 and XX^T=2G. + gram = [[dot(roots[i], roots[j]) // 4 for j in range(N)] for i in range(N)] + for i in range(N): + for j in range(N): + ip = dot(roots[i], roots[j]) + need(ip % 4 == 0, f"nonintegral E8 Gram entry at ({i},{j})") + need(dot(x[i], x[j]) == ip // 2, + f"XX^T != 2G at ({i},{j})") + + # Pairing stored as dual_i = label_i S. This checks all 112^2 entries + # against the independently reconstructed Gram matrix. + for i in range(N): + need(len(duals[i]) == 9, "bad dual label width") + for j in range(N): + actual = parity(dual_masks[i] & label_masks[j]) + expected = (1 + gram[i][j]) & 1 + need(actual == expected, f"binary label pairing mismatch at ({i},{j})") + + xcols = [[x[i][j] for i in range(N)] for j in range(8)] + return roots, frame, labels, duals, x, label_masks, dual_masks, xcols + + +def run_census(geometry): + roots, frame, labels, duals, x, label_masks, dual_masks, xcols = geometry + + # Direct pairing table, independent of any packed-matrix helper in the + # source package. Rows encode L_i S L_j^T in port order. + pairing_rows = [] + for i in range(N): + row = 0 + for j in range(N): + row |= parity(dual_masks[i] & label_masks[j]) << j + pairing_rows.append(row) + + beta_cache = {} + projected_source_cache = {} + + def beta(reader_support, source_support): + key = (reader_support, source_support) + found = beta_cache.get(key) + if found is not None: + return found + projected = projected_source_cache.get(source_support) + if projected is None: + sources = [j for j in range(N) if (source_support >> j) & 1] + projected = [] + for i in range(N): + packed = 0 + for k, j in enumerate(sources): + packed |= ((pairing_rows[i] >> j) & 1) << k + projected.append(packed) + projected_source_cache[source_support] = projected + rows = [] + readers = reader_support + while readers: + bit = readers & -readers + i = bit.bit_length() - 1 + rows.append(projected[i]) + readers ^= bit + value = matrix_rank(rows) + beta_cache[key] = value + return value + + col_support = [] + for col in xcols: + col_support.append(sum((v != 0) << i for i, v in enumerate(col))) + + small_pairs = list(product((-1, 0, 1), repeat=2)) + + def support(values): + return sum((value != 0) << i for i, value in enumerate(values)) + + matrices = [] + for ap, bp, aq, bq in product((-1, 0, 1), repeat=4): + if ap * bq - bp * aq in (-1, 1): + matrices.append((ap, bp, aq, bq)) + need(len(matrices) == 40, f"expected 40 unimodular matrices, got {len(matrices)}") + + total_hist = Counter() + per_pair = [] + minima = [] + max_identity_checked = 0 + expected_count = 0 + + for p, q in combinations(range(8), 2): + hist = Counter() + min_cost = 10**9 + max_cost = -1 + min_cases = [] + xp, xq = xcols[p], xcols[q] + xps, xqs = col_support[p], col_support[q] + d_support = {uv: support([uv[0]*xp[i] + uv[1]*xq[i] for i in range(N)]) + for uv in small_pairs} + + for h in range(1, 512): + z = [((xp[i] + xq[i]) if parity(h & label_masks[i]) == 0 else 0) + for i in range(N)] + w = [((xp[i] - xq[i]) if parity(h & label_masks[i]) == 1 else 0) + for i in range(N)] + zs, ws = support(z), support(w) + rp_support = {uv: support([2*xp[i] - uv[0]*z[i] - uv[1]*w[i] + for i in range(N)]) for uv in small_pairs} + rq_support = {uv: support([2*xq[i] - uv[0]*z[i] - uv[1]*w[i] + for i in range(N)]) for uv in small_pairs} + + for ap, bp, aq, bq in matrices: + cost = (48 + beta(xps, rp_support[(ap, bp)]) + + beta(xqs, rq_support[(aq, bq)]) + + beta(d_support[(ap, aq)], zs) + + beta(d_support[(bp, bq)], ws)) + hist[cost] += 1 + total_hist[cost] += 1 + expected_count += 1 + if cost < min_cost: + min_cost, min_cases = cost, [] + if cost == min_cost and len(min_cases) < 4: + min_cases.append((h, (ap, bp, aq, bq))) + max_cost = max(max_cost, cost) + + need(sum(hist.values()) == 511 * 40, f"wrong count for pair {(p,q)}") + # Independently multiply the full matrix identity for one actual + # minimizer per coordinate pair, after the support-only census. + h0, a0 = min_cases[0] + ap, bp, aq, bq = a0 + z0 = [((xp[i] + xq[i]) if parity(h0 & label_masks[i]) == 0 else 0) + for i in range(N)] + w0 = [((xp[i] - xq[i]) if parity(h0 & label_masks[i]) == 1 else 0) + for i in range(N)] + rp0 = [2*xp[i] - ap*z0[i] - bp*w0[i] for i in range(N)] + rq0 = [2*xq[i] - aq*z0[i] - bq*w0[i] for i in range(N)] + d10 = [ap*xp[i] + aq*xq[i] for i in range(N)] + d20 = [bp*xp[i] + bq*xq[i] for i in range(N)] + for i in range(N): + for j in range(N): + lhs2 = 2 * sum(x[i][k] * x[j][k] for k in range(8)) + rhs2 = sum(2*xcols[k][i]*xcols[k][j] + for k in range(8) if k not in (p, q)) + rhs2 += xp[i]*rp0[j] + xq[i]*rq0[j] + rhs2 += d10[i]*z0[j] + d20[i]*w0[j] + need(rhs2 == lhs2, + f"exact identity failed for pair {(p,q)}, h={h0}, A={a0}") + max_identity_checked += 1 + + per_pair.append({"pair": [p, q], "histogram": dict(sorted(hist.items())), + "minimum": min_cost, "maximum": max_cost}) + minima.append((min_cost, p, q, min_cases)) + + need(expected_count == 28 * 511 * 40 == 572320, + f"wrong total candidate count: {expected_count}") + result = {"global_histogram": dict(sorted(total_hist.items())), + "per_pair": per_pair, "count": expected_count, + "minimum": min(total_hist), "maximum": max(total_hist), + "minimizers": [{"pair": [p, q], "h": h, "A": list(a)} + for value, p, q, cases in minima if value == min(total_hist) + for h, a in cases], + "beta_cache_entries": len(beta_cache), + "endpoint_identity_checks": max_identity_checked} + + # Relax coefficients to all reals. For fixed cut, a residual coordinate + # can vanish only when its active scalar is in {-2,-1,0,1,2}; every other + # real value has the same support as the representative 3. Thus six + # representatives per active coefficient give the exact minimum of each + # original residual beta term. A nonzero real combination of xp,xq has + # only five support types, represented by the listed coefficient pairs. + # Minimize these four terms independently, which is optimistic because it + # ignores that one coefficient matrix must realize all four choices. + residual_coefficients = (-2, -1, 0, 1, 2, 3) + reader_types = ((1, 0), (0, 1), (1, 1), (1, -1), (1, 3)) + relaxation_hist = Counter() + relaxation_nonzero_min = 10**9 + for p, q in combinations(range(8), 2): + xp, xq = xcols[p], xcols[q] + xps, xqs = col_support[p], col_support[q] + reader_supports = [support([u*xp[i] + v*xq[i] for i in range(N)]) + for u, v in reader_types] + for h in range(1, 512): + z = [((xp[i] + xq[i]) if parity(h & label_masks[i]) == 0 else 0) + for i in range(N)] + w = [((xp[i] - xq[i]) if parity(h & label_masks[i]) == 1 else 0) + for i in range(N)] + zs, ws = support(z), support(w) + best_p = min(beta(xps, support([2*xp[i] - a*z[i] - b*w[i] + for i in range(N)])) + for a in residual_coefficients + for b in residual_coefficients) + best_q = min(beta(xqs, support([2*xq[i] - a*z[i] - b*w[i] + for i in range(N)])) + for a in residual_coefficients + for b in residual_coefficients) + best_z = min(beta(ds, zs) for ds in reader_supports) + best_w = min(beta(ds, ws) for ds in reader_supports) + lower = 48 + best_p + best_q + best_z + best_w + relaxation_hist[lower] += 1 + if zs and ws: + relaxation_nonzero_min = min(relaxation_nonzero_min, lower) + need(sum(relaxation_hist.values()) == 28 * 511, + "wrong all-real relaxation cut count") + need(relaxation_nonzero_min < 10**9, + "no cuts with both Walsh sources nonzero") + result["relaxation"] = { + "histogram": dict(sorted(relaxation_hist.items())), + "minimum": min(relaxation_hist), + "nonzero_sources_minimum": relaxation_nonzero_min, + "cut_pairs": sum(relaxation_hist.values()), + "critical_coefficients": [-2, -1, 0, 1, 2], + "generic_representative": 3, + } + return result + + +def normalize_hist(hist): + return {str(k): int(v) for k, v in sorted(hist.items(), key=lambda kv: int(kv[0]))} + + +def compare_parent(result, path): + parent = json.loads(path.read_text()) + parent_hist = parent.get("global_histogram", parent.get("histogram")) + need(parent_hist is not None, "RESULT.json missing global_histogram/histogram") + need(normalize_hist(parent_hist) == normalize_hist(result["global_histogram"]), + "global histogram differs from RESULT.json") + for parent_key, own_key in (("cases", "count"), ("minimum", "minimum"), + ("maximum", "maximum")): + need(parent[parent_key] == result[own_key], f"summary field differs: {parent_key}") + parent_pairs = parent.get("per_pair") + need(parent_pairs is not None, "RESULT.json missing per_pair") + need(len(parent_pairs) == 28 and len({tuple(row["pair"]) for row in parent_pairs}) == 28, + "missing or duplicated pair receipts") + mine = {(tuple(row["pair"]), row["minimum"], row.get("maximum"), + tuple(normalize_hist(row["histogram"]).items())) + for row in result["per_pair"]} + theirs = {(tuple(row["pair"]), row["minimum"], row.get("maximum"), + tuple(normalize_hist(row["histogram"]).items())) + for row in parent_pairs} + need(mine == theirs, "per-pair census differs from RESULT.json") + print("RESULT.json comparison: global histogram and per-pair histograms/min/max match") + need("relaxation" in parent, "missing all-real relaxation receipt") + if "relaxation" in parent: + expected_relax = parent["relaxation"] + actual_relax = result["relaxation"] + need(normalize_hist(expected_relax["histogram"]) == + normalize_hist(actual_relax["histogram"]), + "all-real relaxation histogram differs from RESULT.json") + for key in ("minimum", "nonzero_sources_minimum", "cut_pairs", + "critical_coefficients", "generic_representative"): + need(expected_relax[key] == actual_relax[key], + f"all-real relaxation field differs: {key}") + print("RESULT.json comparison: all-real relaxation fields match") + + +def main(): + rank_self_checks() + geometry_path = Path(sys.argv[1]) if len(sys.argv) > 1 else HERE / "GEOMETRY.json" + result_path = Path(sys.argv[2]) if len(sys.argv) > 2 else HERE / "RESULT.json" + geometry = load_geometry(geometry_path) + print(f"Geometry verified: {geometry_path}") + result = run_census(geometry) + encoded = json.dumps(result["global_histogram"], sort_keys=True).encode() + print(f"Candidates: {result['count']}") + print(f"Cost range: {result['minimum']}..{result['maximum']}") + print(f"Global histogram: {json.dumps(result['global_histogram'], sort_keys=True)}") + print(f"Histogram SHA256: {hashlib.sha256(encoded).hexdigest()}") + print(f"Beta cache entries: {result['beta_cache_entries']}") + print(f"Exact identity checks at running minima: {result['endpoint_identity_checks']}") + print(f"Global minimum witnesses (first 4): {json.dumps(result['minimizers'][:4], sort_keys=True)}") + print(f"All-real relaxation: {json.dumps(result['relaxation'], sort_keys=True)}") + compare_parent(result, result_path) + print("PASS_P112_MASKED_WALSH_INDEPENDENT") + + +if __name__ == "__main__": + main() diff --git a/research/p112-masked-walsh/test_verify.py b/research/p112-masked-walsh/test_verify.py new file mode 100644 index 0000000000..58059f28dd --- /dev/null +++ b/research/p112-masked-walsh/test_verify.py @@ -0,0 +1,65 @@ +"""Portable replay and corruption controls; standard library only.""" + +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + + +HERE = Path(__file__).resolve().parent + + +class PackageChecks(unittest.TestCase): + def test_portability_and_rejections(self): + with tempfile.TemporaryDirectory(prefix="p112 replay with spaces ") as directory: + target = Path(directory) / "standalone" + shutil.copytree(HERE, target, ignore=shutil.ignore_patterns("__pycache__")) + + def run(*args): + return subprocess.run([sys.executable, "-I", "-O", "-B", + str(target / "verify.py"), *map(str, args)], + cwd=directory, text=True, capture_output=True, timeout=120) + + result = run() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("cases=572320 minimum=72", result.stdout) + receipt = target / "RESULT.json" + original = receipt.read_bytes() + changed = json.loads(original) + changed["minimum"] = 64 + receipt.write_text(json.dumps(changed)) + result = run() + self.assertNotEqual(result.returncode, 0) + self.assertIn("certificate mismatch", result.stderr) + receipt.write_bytes(original) + + source = target / "vendor/pr845-geometry.py" + source_bytes = source.read_bytes() + source.write_bytes(source_bytes + b"\n# corruption control\n") + result = run() + self.assertNotEqual(result.returncode, 0) + self.assertIn("source mismatch", result.stderr) + source.write_bytes(source_bytes) + + geometry = target / "GEOMETRY.json" + geometry_bytes = geometry.read_bytes() + changed = json.loads(geometry_bytes) + changed["X"][0][0] += 1 + geometry.write_text(json.dumps(changed)) + result = run() + self.assertNotEqual(result.returncode, 0) + self.assertIn("source mismatch", result.stderr) + geometry.write_bytes(geometry_bytes) + + protected = Path(directory) / "existing.json" + protected.write_text("keep this file\n") + result = run("--write", protected) + self.assertNotEqual(result.returncode, 0) + self.assertEqual(protected.read_text(), "keep this file\n") + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-masked-walsh/verify.py b/research/p112-masked-walsh/verify.py new file mode 100644 index 0000000000..48aaa40093 --- /dev/null +++ b/research/p112-masked-walsh/verify.py @@ -0,0 +1,258 @@ +"""Exact finite masked-Walsh census. Apache-2.0; substantial Codex assistance.""" + +import argparse +from collections import Counter +import hashlib +import importlib.util +from itertools import combinations, product +import json +from pathlib import Path +import random +from fractions import Fraction + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("p112_geometry", HERE / "vendor/pr845-geometry.py") +geometry = importlib.util.module_from_spec(spec) +spec.loader.exec_module(geometry) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows, limit=9): + pivots = [0] * 9 + size = 0 + for row in rows: + while row: + p = row.bit_length() - 1 + if pivots[p]: + row ^= pivots[p] + else: + pivots[p] = row + size += 1 + if size == limit: + return size + break + return size + + +def support(values): + return sum(1 << i for i, value in enumerate(values) if value) + + +def beta(readers, sources, data): + return geometry.term_cost(readers, sources, data) + + +def recipe(data, p, q, h, matrix): + xp, xq = ([row[j] for row in data["X"]] for j in (p, q)) + z = [a + b if (label & h).bit_count() % 2 == 0 else 0 + for a, b, label in zip(xp, xq, data["labels"])] + w = [a - b if (label & h).bit_count() % 2 else 0 + for a, b, label in zip(xp, xq, data["labels"])] + ap, bp, aq, bq = matrix + rp = [2*x - ap*u - bp*v for x, u, v in zip(xp, z, w)] + rq = [2*x - aq*u - bq*v for x, u, v in zip(xq, z, w)] + d1 = [ap*x + aq*y for x, y in zip(xp, xq)] + d2 = [bp*x + bq*y for x, y in zip(xp, xq)] + return xp, xq, z, w, rp, rq, d1, d2 + + +def check_endpoint(values): + xp, xq, z, w, rp, rq, d1, d2 = values + for i in range(112): + for j in range(112): + require(xp[i]*rp[j] + xq[i]*rq[j] + d1[i]*z[j] + d2[i]*w[j] + == 2*(xp[i]*xp[j] + xq[i]*xq[j]), "endpoint identity") + + +def controls(data): + require(rank([0, 3, 5, 6]) == 2, "dependent rank control") + require(rank([1, 2, 4]) == 3, "independent rank control") + cols = list(map(list, zip(*data["X"]))) + require(sum(beta(c, c, data) for c in cols) == 64, "baseline") + values = recipe(data, 0, 1, 48, (1, 1, 0, 1)) + check_endpoint(values) + broken = [list(v) for v in values] + broken[4][0] += 1 + try: + check_endpoint(broken) + except ValueError: + pass + else: + raise ValueError("corrupted residual accepted") + broken = [list(v) for v in values] + broken[6] = [0] * 112 + try: + check_endpoint(broken) + except ValueError: + pass + else: + raise ValueError("omitted added total accepted") + require(beta([0]*112, cols[0], data) == 0, "zero reader cost") + require(beta(cols[0], [0]*112, data) == 0, "zero source cost") + # Unmasked orthogonal Walsh replacement zeroes both old columns, but costs 18. + plus = [a+b for a, b in zip(cols[0], cols[1])] + minus = [a-b for a, b in zip(cols[0], cols[1])] + require(beta(plus, plus, data) + beta(minus, minus, data) == 18, + "unmasked Walsh cost") + # Check the support-cell reduction at rational points outside the grid. + critical = {-2, -1, 0, 1, 2} + rational_points = {Fraction(n, d) for n in range(-15, 16) for d in (1, 2, 3, 5)} + for cut in (1, 2, 48, 511): + xp, xq, z, w, *_ = recipe(data, 0, 1, cut, (1, 0, 0, 1)) + require(not any(a*b for a, b in zip(z, w)), "disjoint masked sources") + for a in rational_points: + representative = a if a in critical else 3 + for source in (z, w): + require(support([2*x-a*u for x, u in zip(xp, source)]) + == support([2*x-representative*u for x, u in zip(xp, source)]), + "residual support-cell control") + if a not in (0, 1, -1): + require(support([x+a*y for x, y in zip(xp, xq)]) + == support([x+3*y for x, y in zip(xp, xq)]), + "reader support-cell control") + require(support([2*x-2*zv for x, zv in zip(xp, z)]) + != support([2*x-3*zv for x, zv in zip(xp, z)]), + "coefficient 2 must not be treated as generic") + return {"baseline": 64, "unmasked_walsh_total": 66, + "rank_controls": 2, "endpoint_rejections": 2, "zero_term_controls": 2, + "rational_support_points": len(rational_points), "support_cuts": 4, + "critical_two_distinguished": True} + + +def census(data): + matrices = [m for m in product((-1, 0, 1), repeat=4) + if abs(m[0]*m[3] - m[1]*m[2]) == 1] + require(len(matrices) == 40, "matrix count") + cuts = list(range(1, 512)) + random.Random(48).shuffle(cuts) + columns = list(map(list, zip(*data["X"]))) + all_histogram = Counter() + pairs = [] + witness = None + best = 100 + zero_source_pairs = 0 + grid_nonzero_minimum = 100 + relaxed_histogram = Counter() + nonzero_sources_minimum = 100 + # Membership in col(X) is tested with exact rank below for a frozen witness; + # the census itself depends only on nonzero scalar supports. + for p, q in combinations(range(8), 2): + xp, xq = columns[p], columns[q] + reader_values = {(a, b): [a*x + b*y for x, y in zip(xp, xq)] + for a, b in product((-1, 0, 1), repeat=2) if a or b} + # Project source labels against an exact basis of each reader space. + projections = {} + dimensions = {} + for key, values in reader_values.items(): + space = geometry.reader_space(values, data["duals"]) + projections[key] = [geometry.evaluate(space, lab) for lab in data["labels"]] + dimensions[key] = len(space) + generic = (1, 3) + space = geometry.reader_space([x+3*y for x, y in zip(xp, xq)], data["duals"]) + projections[generic] = [geometry.evaluate(space, lab) for lab in data["labels"]] + dimensions[generic] = len(space) + cache = {} + + def cost(key, values): + mask = support(values) + cache_key = (key, mask) + if cache_key not in cache: + cache[cache_key] = rank((v for i, v in enumerate(projections[key]) + if mask >> i & 1), dimensions[key]) + return cache[cache_key] + + hist = Counter() + for h in cuts: + z = [x+y if (h & label).bit_count() % 2 == 0 else 0 + for x, y, label in zip(xp, xq, data["labels"])] + w = [x-y if (h & label).bit_count() % 2 else 0 + for x, y, label in zip(xp, xq, data["labels"])] + if not any(z) or not any(w): + zero_source_pairs += 1 + residual_costs = {} + for row, key in ((xp, (1, 0)), (xq, (0, 1))): + for a, b in product((-1, 0, 1), repeat=2): + if a or b: + residual = [2*x-a*u-b*v for x, u, v in zip(row, z, w)] + residual_costs[key, a, b] = cost(key, residual) + added_z = {key: cost(key, z) for key in reader_values} + added_w = {key: cost(key, w) for key in reader_values} + representatives = (-2, -1, 0, 1, 2, 3) + lower_original = [min(cost(key, [2*x-a*u-b*v for x, u, v in zip(row, z, w)]) + for a, b in product(representatives, repeat=2)) + for row, key in ((xp, (1, 0)), (xq, (0, 1)))] + reader_types = ((1, 0), (0, 1), (1, 1), (1, -1), generic) + lower_added = [min(cost(key, src) for key in reader_types) for src in (z, w)] + lower = 48 + sum(lower_original + lower_added) + relaxed_histogram[lower] += 1 + if any(z) and any(w): + nonzero_sources_minimum = min(nonzero_sources_minimum, lower) + for matrix in matrices: + ap, bp, aq, bq = matrix + terms = [residual_costs[(1, 0), ap, bp], residual_costs[(0, 1), aq, bq], + added_z[ap, aq], added_w[bp, bq]] + total = 48 + sum(terms) + hist[total] += 1 + if any(z) and any(w): + grid_nonzero_minimum = min(grid_nonzero_minimum, total) + if total < best: + best = total + witness = {"pair": [p, q], "cut": h, "matrix": list(matrix), + "changed_term_costs": terms, "unchanged_cost": 48, + "total": total} + pair_result = {"pair": [p, q], "histogram": dict(sorted(hist.items())), + "minimum": min(hist), "maximum": max(hist)} + pairs.append(pair_result) + all_histogram.update(hist) + require(sum(all_histogram.values()) == 572320, "incomplete census") + values = recipe(data, *witness["pair"], witness["cut"], witness["matrix"]) + check_endpoint(values) + direct_costs = [beta(values[a], values[b], data) for a, b in ((0, 4), (1, 5), (6, 2), (7, 3))] + require(direct_costs == witness["changed_term_costs"], "witness direct cost") + # Seed-chosen nondegenerate cut demonstrates that this is outside PR717's code-only class. + outside = recipe(data, 0, 1, 48, (1, 1, 0, 1)) + ranks = [len(geometry.rational_basis_indices([row + [v] for row, v in zip(data["X"], vec)])) + for vec in outside[2:4]] + require(ranks == [9, 9], "masked sources must leave col(X) in escape control") + return {"status": "complete finite census; no new kappa", "seed": 48, + "cases": sum(all_histogram.values()), "histogram": dict(sorted(all_histogram.items())), + "minimum": min(all_histogram), "maximum": max(all_histogram), "per_pair": pairs, + "nonzero_sources_minimum": grid_nonzero_minimum, + "minimum_witness": witness, "zero_source_cut_pairs": zero_source_pairs, + "outside_colX_control": {"pair": [0, 1], "cut": 48, "augmented_ranks": ranks}, + "relaxation": {"histogram": dict(sorted(relaxed_histogram.items())), + "minimum": min(relaxed_histogram), + "nonzero_sources_minimum": nonzero_sources_minimum, + "cut_pairs": sum(relaxed_histogram.values()), + "critical_coefficients": [-2, -1, 0, 1, 2], + "generic_representative": 3}, + "controls": controls(data)} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", type=Path, help="write a fresh certificate; refuse existing paths") + args = parser.parse_args() + pins = json.loads((HERE / "SOURCES.json").read_text()) + for path, expected in pins["files"].items(): + require(hashlib.sha256((HERE / path).read_bytes()).hexdigest() == expected, + "source mismatch: " + path) + data = geometry.build() + geometry.check_geometry(data) + require(data == json.loads((HERE / "GEOMETRY.json").read_text()), "geometry mismatch") + report = census(data) + encoded = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.write: + with args.write.open("x") as stream: + stream.write(encoded) + else: + require(encoded == (HERE / "RESULT.json").read_text(), "certificate mismatch") + print(f"PASS_P112_MASKED_WALSH cases={report['cases']} minimum={report['minimum']} baseline=64 no_new_kappa") + + +if __name__ == "__main__": + main() From f87724057cc5fc5192fe2904675a563273612851 Mon Sep 17 00:00:00 2001 From: just-mn <77879381+just-mn@users.noreply.github.com> Date: Wed, 14 Oct 2026 09:04:33 +0200 Subject: [PATCH 3/3] Document current P112 overlap and open questions --- research/p112-masked-walsh/NOTICE.md | 5 ++ research/p112-masked-walsh/OVERLAP.json | 108 ++++++++++++++++++++++++ research/p112-masked-walsh/README.md | 41 ++++++++- 3 files changed, 152 insertions(+), 2 deletions(-) diff --git a/research/p112-masked-walsh/NOTICE.md b/research/p112-masked-walsh/NOTICE.md index c539578f6f..7f616c8ddc 100644 --- a/research/p112-masked-walsh/NOTICE.md +++ b/research/p112-masked-walsh/NOTICE.md @@ -17,3 +17,8 @@ The context of the selected construction retains Jeremy Kothe's PR799, Chafik Boukhalfa's PR741, DreamingOfClouds' PR589, eumemic's PR555 and the repository's cumulative contributor lineage. No priority for their results, or a new selected kappa, is claimed here. + +The final overlap review also credits concurrent work by Philipp / @mightyOil +(PR1191 and PR1197), @thakrarsagar (PR1327), and the free-rectangle work in +PR1375, PR1460 and PR1473. Their statements are compared in README.md and +heads recorded in OVERLAP.json; their implementations are not imported. diff --git a/research/p112-masked-walsh/OVERLAP.json b/research/p112-masked-walsh/OVERLAP.json index 0450dc951a..25f4966697 100644 --- a/research/p112-masked-walsh/OVERLAP.json +++ b/research/p112-masked-walsh/OVERLAP.json @@ -310,5 +310,113 @@ "number": 1133, "head": "8301a4698152cf63d3b4992145ecc8621942a6cd", "scope": "rational support descent for fixed-reader single lifts; distinct from masked-Walsh two-total support cells" + }, + "final_refresh": { + "checked_at": "2026-10-14T07:02:49.501627+00:00", + "upstream_head": "5e554ff58d01921747d27177045c0061f31e1ad1", + "selected_decimal": "0.001672660197076918", + "selected_source_pr": 1094, + "consumed_predecessor_heads_unchanged": true, + "search": "repo:CrocSwap/integer-mult-bounds is:pr P112", + "matches_at_search": 71, + "relevant": [ + { + "number": 1197, + "title": "Scoped negative result: two P112 totals need overlapping independent lifts (no new kappa)", + "head": "a0935afff6cc5540a582c5881bc8d5f98b587357", + "created_at": "2026-10-13T19:57:09Z", + "state": "closed", + "user": "mightyOil", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1197" + }, + { + "number": 1327, + "title": "Scoped negative result: copy-rank floor for two-sided P112 parity lifts", + "head": "0462379659388acdb271f2e769986475d8a0646c", + "created_at": "2026-10-13T22:44:07Z", + "state": "closed", + "user": "thakrarsagar", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1327" + }, + { + "number": 1375, + "title": "Research: COPY floor 64 for two-coordinate P112 mixing with small free rectangles (no new kappa)", + "head": "4a533aff2a7a87c9b36e077a31774b332a7f64bd", + "created_at": "2026-10-13T23:46:30Z", + "state": "closed", + "user": "commdata2338", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1375" + }, + { + "number": 1460, + "title": "Scoped negative result: arbitrary free rectangles retain COPY64 for P112 pair (4,6)", + "head": "8d53667d9bb09d9b1ffb0f865b5c8dc230eb02f6", + "created_at": "2026-10-14T00:58:37Z", + "state": "closed", + "user": "bbMisk", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1460" + }, + { + "number": 1473, + "title": "Scoped negative result: two-anchor span preservation for P112 decoders", + "head": "ea2f6bf0940580dfaeb393ec0786abc8f7bbb7b4", + "created_at": "2026-10-14T01:20:30Z", + "state": "open", + "user": "bbMisk", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1473" + }, + { + "number": 1325, + "title": "Research: classify P112 sparse-lift equality and sharp all-active cost 65", + "head": "ba2d1cae64738891dd530b3526fb8ae3b25541aa", + "created_at": "2026-10-13T22:41:28Z", + "state": "closed", + "user": "mightyOil", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1325" + }, + { + "number": 1417, + "title": "Scoped obstruction: sharp P112 endpoint dimension and complete linear-lift cost", + "head": "c755bf393bea26d2275e1516b0560ca92de7a52e", + "created_at": "2026-10-14T00:32:37Z", + "state": "closed", + "user": "aliromman", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1417" + }, + { + "number": 1633, + "title": "Scoped theorem: sharp excess-rank budgets for exact overcomplete E8 decoders", + "head": "652264fa1f70820139b2730363a0056b7fadc689", + "created_at": "2026-10-14T04:29:32Z", + "state": "open", + "user": "bbMisk", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1633" + }, + { + "number": 1656, + "title": "Bounded decoder experiment: 296 pair-total replacements fail the cost screen", + "head": "9fca8c97464eac1a76045ab1a9b97507af656b4b", + "created_at": "2026-10-14T05:28:25Z", + "state": "open", + "user": "antunishdPursuit", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1656" + }, + { + "number": 1191, + "title": "Research: one-sided E8 mask rigidity on 1,373 punctured units (no new kappa)", + "head": "640b43bb13d3d476a2d83b74ef0d33f14d1b5711", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1191", + "user": "mightyOil", + "created_at": "2026-10-13T19:54:49Z", + "state": "closed" + } + ], + "discussions_read": [ + 1163, + 1166, + 1167 + ], + "coverage_limit": "Focused PR title/body search and relevant proof definitions; discussion pages read, not an exhaustive crawl of every discussion reply. No priority claim.", + "conclusion": "PR1197 disjointness is added-reader coefficient support, not source row support; our two readers can overlap on {p,q}. PR1327 is a different two-sided parity-lift family whose 76 floor requires both factors off-root-code. PR1191 addresses masked exactness, while our identity is all-pairs. Free-rectangle and selected-supplier endpoint works are distinct. Added evidence is the exact 72/77 specialized support-cell certificate and independent census, not a general decoder impossibility." } } diff --git a/research/p112-masked-walsh/README.md b/research/p112-masked-walsh/README.md index 3f06d674fc..2b01d09b1c 100644 --- a/research/p112-masked-walsh/README.md +++ b/research/p112-masked-walsh/README.md @@ -146,15 +146,52 @@ masked-Walsh form and limits modified readers to two coordinate columns. It does not close the general two-total or mixed-beta problem. No worldwide priority is claimed for the support-cell method. +Concurrent work checked again on October 14: Philipp / @mightyOil's +[PR1197](https://github.com/CrocSwap/integer-mult-bounds/pull/1197) +excludes two-total savings when added-reader **coefficient** supports are +disjoint, among other cases. Here the two coefficient columns can both use +`{p,q}`; the disjoint row supports of Z and W do not satisfy that hypothesis. +This package gives a quantitative result for an explicit subfamily of the +overlapping-reader case it leaves open. @thakrarsagar's +[PR1327](https://github.com/CrocSwap/integer-mult-bounds/pull/1327) +studies two-sided parity lifts; its strengthened floor requires off-root-code +columns on both factors, whereas all our reader columns remain in col(X). +These are adjacent obstructions, not dependencies of our proof. +[PR1191](https://github.com/CrocSwap/integer-mult-bounds/pull/1191)'s one-sided +mask rigidity reduces masked exactness to all-pairs exactness in its class; +our identity already holds on all pairs. The free-rectangle mechanisms of +[PR1375](https://github.com/CrocSwap/integer-mult-bounds/pull/1375), +[PR1460](https://github.com/CrocSwap/integer-mult-bounds/pull/1460) and +[PR1473](https://github.com/CrocSwap/integer-mult-bounds/pull/1473) change a +different factorization. The added evidence here is the all-pair/all-cut +72/77 certificate, discrete histogram and independent direct-pairing replay; +no general decoder impossibility or priority over those works is claimed. +Their exact heads and other inspected contributions are in OVERLAP.json. + +## Open next questions + +Can compatibility among the four minimizing coefficient choices sharpen the +continuous 72/77 bounds? A bounded first step is to evaluate the full cost on +compatible residual/reader support cells for one pair and a minimizing cut. +The blocker is tracking reader-ratio and residual-value constraints together; +the current independent-minimum certificate does not assert attainability. +This would refine the obstruction, not produce a cheaper supplier. + +Changing the source masks or allowing dense readers could escape this family. +A useful first step is to specify one such class outside the pinned concurrent +obstructions and derive its optimistic complete cost before a new search. +No claim about that broader class follows from this package. + Exact base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. At that base the selected conditional result is #799 with #589/#555, κ=`1661634653669567/10^18`. The selected certificate, X4 construction note and maintainer review were read; no historical or pending headline was used as the accepted frontier. [SOURCES.json](SOURCES.json) pins consumed source bytes and predecessor heads. -At the pre-submission refresh, main was `ce7ad1b6ab09452c3478723a2e96ed5ff212dc08` +At the final pre-submission refresh, main was `5e554ff58d01921747d27177045c0061f31e1ad1` and selected #1094 at κ=`0.001672660197076918`. The pinned P112 geometry and both consumed predecessor heads were unchanged. [OVERLAP.json](OVERLAP.json) -records the newer P104, bit-puncture, routing and single-lift work inspected. +records the October 13 and October 14 overlap checks, including the newer +two-total, parity-lift and free-rectangle work. The selected frontier and `upstream/` are unchanged. Inherited all-size, compiler, physical/hosting, precision/tape and analytic assumptions remain.