From 97473c6585920cbb07a24994f670c773f61d6492 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 15:02:38 +0100 Subject: [PATCH 1/2] feat(research): prove sharp P112 diagonal completion boundary --- .../p112-diagonal-rank-boundary/README.md | 203 ++++++++++++++++ .../p112-diagonal-rank-boundary/SOURCES.json | 42 ++++ .../p112-diagonal-rank-boundary/TASK.json | 78 ++++++ .../p112-diagonal-rank-boundary/VERIFY.json | 32 +++ .../p112-diagonal-rank-boundary/verify.py | 230 ++++++++++++++++++ 5 files changed, 585 insertions(+) create mode 100644 research/p112-diagonal-rank-boundary/README.md create mode 100644 research/p112-diagonal-rank-boundary/SOURCES.json create mode 100644 research/p112-diagonal-rank-boundary/TASK.json create mode 100644 research/p112-diagonal-rank-boundary/VERIFY.json create mode 100644 research/p112-diagonal-rank-boundary/verify.py diff --git a/research/p112-diagonal-rank-boundary/README.md b/research/p112-diagonal-rank-boundary/README.md new file mode 100644 index 0000000000..be80f7b480 --- /dev/null +++ b/research/p112-diagonal-rank-boundary/README.md @@ -0,0 +1,203 @@ +# The sharp rank boundary for P112 diagonal completions + +This package was produced by Nick Petalas. Apache-2.0. + +**Scoped mathematical proof with exact finite corroboration.** For the P112 +Gram matrix G and an arbitrary complex diagonal matrix Delta, write s for the +number of nonzero diagonal corrections. For every integer q with 8<=q<=58, + +```text +rank_C(G+Delta)<=q if and only if s<=q-8. +In that range, rank_C(G+Delta)=8+s. +``` + +The upper endpoint 58 is sharp. A constant diagonal correction on 53 positions +has rank 59, rather than the additive prediction 61. This answers Open next +question 1 of Arham-Tahir64's [PR #1313](https://github.com/CrocSwap/integer-mult-bounds/pull/1313), +which gives the sufficient range through 20 and leaves its sharpness open. +The new result is the sharp completion boundary. The root-code distance, +hyperplane classification and original completion argument are credited +premises. No COPY improvement, physical supplier or new kappa is claimed. + +## Model and inherited geometric premises + +Let X contain the 112 doubled E8 root-line representatives after removing +the eight lines e_(2j)+/-e_(2j+1), j=0,1,2,3. Each row of X has squared norm +eight. Set G=XX^T. With conventional norm-two roots R=X/2, the target +2RR^T is G/2. Scaling Delta by the same factor transfers every rank statement +between these conventions. All ranks are over C and transposes are ordinary. + +This is the mask that fixes every off-diagonal entry and frees diagonals. +The genuine odd-only decoder mask fixes diagonals and frees certain +off-diagonal entries. Our witness is not an odd-only completion. + +We use two predecessor premises without auditing them: + +1. Every nonzero complex root-code vector Xa has support at least 53 on + P112. This is the distance statement in woklerx's + [PR #1447](../p112-sparse-completion-rank/README.md). +2. Every real root-spanned hyperplane of E8 is one of the eight types in + themilkman216's [PR #968, premise F6](../complex-frame-pair-decoders/PROOF.md). + Only E7 has more than 42 root lines. It has 63 and its normal is a root. + The classification remains a cited premise, as in the predecessors. + +One additional finite fact used below is that the intersection of two +distinct root-normal E7 hyperplanes contains at most 36 E8 root lines. +The verifier enumerates every unordered pair of distinct normals: 3,780 +intersections have 30 lines and 3,360 have 36. These are exact integer zero +tests, independent of any predecessor executable. + +It follows that a root-spanned subspace of dimension at most six contains +at most 42 E8 root lines. Otherwise extend its root basis to a basis of R^8. +Omitting two different added basis roots gives two distinct root-spanned +hyperplanes containing the original subspace. Both contain more than 42 +lines, so both are E7. Their intersection has at most 36 lines, a +contradiction. The bound 42 is sufficient here; no sharp rank-six count is +claimed. It also bounds any subset of P112 of root rank at most six. + +## Rank stratification and the sharp lower bound + +Let S be the changed diagonal support and J its complement. Put +r=rank(X_J). Choose r independent unchanged rows B in J. Their real Gram +matrix is positive definite, so G[B,B] is invertible over C. Pivoting on +that principal block leaves the unchanged rows in J minus B zero. +On S, the remaining original Gram matrix H has rank 8-r: it is the Gram +matrix of the root vectors projected orthogonally off span(X_B). +The correction Delta_S is invertible. Therefore + +```text +rank(G+Delta) = r + rank(H+Delta_S) + >= r + s - (8-r) = s+2r-8. (1) +``` + +If r=8, H=0 and the rank is exactly 8+s. If r=7, a nonzero normal to X_J +gives a nonzero root-code vector supported on S. Premise 1 gives s>=53, +and (1) gives rank(G+Delta)>=59. If r<=6, the preceding subspace bound +gives |J|<=42, hence s>=70. Rank subadditivity alone then gives +rank(G+Delta)>=s-8>=62. Thus every completion of rank at most 58 has +r=8 and rank exactly 8+s. + +Conversely, if s<=q-8 with q<=58, then s<=50. Premise 1 implies that +X_J spans all eight dimensions, since at most 50 rows were removed. +The r=8 equality gives rank(G+Delta)=8+s<=q. This proves both directions +for arbitrary complex diagonal values. The finite checks below do not +enumerate those values; the written rank argument provides that scope. + +## A rank-59 witness + +Take the live root alpha=(1,1,1,1,1,1,1,1) and c=X alpha. Let S=supp(c) +and let D_S be the diagonal projection onto those coordinates. Exact +enumeration gives |S|=53 and rank(X_J)=7. The new completion is + +```text +K = G - 112 D_S. (2) +``` + +The P112 tight-frame identity is X^T X=112I. Consequently P=G/112 is the +orthogonal projection onto U=col(X). Let V be the coordinate subspace on S. +Since X_J has rank seven, dim(U intersect V)=1. Also dim(U)=8, dim(V)=53, +and dim(U+V)=60. For two orthogonal projections P,D_S, + +```text +ker(P-D_S) = (U intersect V) direct_sum (U^perp intersect V^perp). +``` + +Indeed, if Px=D_S x=y, then y belongs to both images and x-y belongs to +both kernels. The converse is immediate. The two summands have dimensions +one and 112-60=52. Thus K has nullity 53 and rank 59. Its correction has +53 nonzero diagonal entries, so additivity would predict 61. This proves +that the lower-rank range cannot include 59. On the convention G/2, +replace the coefficient -112 by -56. + +The standalone verifier constructs (2) and obtains rank 59 by exact +rational elimination. It also checks Kc=0, the tight-frame identity, +the 53-position support and the rank-seven unchanged rows. It checks all +12,432 off-diagonal entries against G. This is a finite witness and a +scoped universal proof, not a failed search. + +## Reproduction and verification + +From the repository root, CPython 3.12 and standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p112-diagonal-rank-boundary/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/p112-diagonal-rank-boundary/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p112-diagonal-rank-boundary +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p112-diagonal-rank-boundary --check-source-history +``` + +Any CPython 3.12 path may replace the displayed interpreter. Expected status +is `PASS_P112_DIAGONAL_RANK_BOUNDARY`, with first nonadditive rank 59. +Each run prints a generated receipt with SHA256 hashes of all five package +files. Optional `--receipt /absolute/scratch/new.json` saves the receipt +outside the package and refuses to overwrite an existing file. No receipt +is hand-written or committed. + +Eight direct completion fixtures cover diagonal-support sizes 21,31,40,50, +with two distinct support/value patterns at each size. Their ranks are +29,39,48,58 respectively. A separate five-row, three-dimensional fixture +checks (1) on all 32 supports and four nonzero correction values, giving +128 cases. Six controls reject a false rank-58 witness, extending additivity +through 59, the wrong projection scale, an omitted correction, a forbidden +off-diagonal edit and confusion with the odd-only mask. Checks remain +enabled under optimization. The verifier imports no predecessor code. + +## Scope, sources and implementation limits + +The scientific base is canonical main +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority revision 7. +SOURCES.json pins the task, selected record and predecessor proof texts as +historical provenance. There are no live predecessor executable inputs. +The complex-rank-shape-decoder card changes to an algebraic side question +following #1313's explicit handoff. Ordinary completion rank is not a +recursive child rank, so no packing-cap or physical-budget inference is +made. The card's historical positive control raises +`KeyError: 'complex_profile'` under the changed selected schema. The current +selected source-binding orientation passes with +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; this is metadata orientation only. + +Credit Arham-Tahir64 #1313 for the diagonal-mask question and pivot method; +woklerx #1447 for the code-distance premise and #1077 for complex-coefficient +scope; themilkman216 #968 for the root-flat framework; DreamingOfClouds +#717/#595/#446 for the geometric decoder model; Mihir Srivastava #845, +Joel Pulikkan #620, icekylinx and the retained E8/Hamming lineage for their +predecessor contributions. Schur rank inequalities and the difference-of- +projections identity are classical. The new application gives the sharp +diagonal-completion threshold. Predecessor files and credit are unchanged. + +Independent human and formal proof-kernel review are unclaimed. The proof +retains the cited geometric premises. No copied-information optimum, +arbitrary off-diagonal mask, rounded identity, physical source access, +dirty-workspace schedule, native realization, compiler, stock, tape, +precision or analytic transfer is supplied. Lean, Docker and a selected +operator replay were not run. No unknown physical cost is priced as zero. +The first verified improvement ends discovery; no construction expansion +or larger-rank classification follows. + +The engineering-mode autonomous-run playbook uses Build the Lever and +Prove It Works: the exact verifier is the retained evidence artifact. +Functions have fewer than 60 lines, with no recursion or dynamic code +execution. Root lists have at most 120 elements, normal pairs number 7,140, +and elimination matrices have at most 112 rows and columns with integer +inputs bounded in absolute value by 224. Power of Ten rule 3 requires a +managed-runtime deviation: Python allocates integers, fractions and lists +during these finite computations. The fixed dimensions bound live storage; +Hadamard's bound controls the elimination minors. This deviation is +confined to the standalone verifier. A fixed-storage implementation is +a follow-up only if this becomes a persistent service or accepts larger +inputs. Warning-strict ordinary and optimized commands are registered; +no separate static analyzer is configured for this package. + +## Open next questions + +1. Which diagonal corrections attain the first nonadditive rank 59? + Begin with r=7, s=53 and the rank-one Schur complement in (1), retaining + arbitrary complex diagonal values. A complete minimum-support codeword + classification and its parameter equivalences remain needed. +2. Does a specified diagonal-completion factorization change any complete + paid decoder bill? First state whether the caller allows changed diagonals + and price its repair. This rank boundary supplies no copied-information, + physical realization or restoration contract; those obligations block a + supplier or kappa claim. + +Structured questions are in TASK.json. diff --git a/research/p112-diagonal-rank-boundary/SOURCES.json b/research/p112-diagonal-rank-boundary/SOURCES.json new file mode 100644 index 0000000000..5c576c23a9 --- /dev/null +++ b/research/p112-diagonal-rank-boundary/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/complex-diagonal-mask-rigidity/PROOF.md", + "usage": "provenance", + "git_blob": "e93a0057c7d81e5de07537dcb7d98b5f2e32c746", + "sha256": "ee365adaaa5112a1cf3eecf9ad75e6fa523a6cd0e9cc2607668e328dc17ede46" + }, + { + "path": "research/complex-diagonal-mask-rigidity/README.md", + "usage": "provenance", + "git_blob": "f00165b471fc7c54aa05cb921b89219a5c898428", + "sha256": "5304bc31fb65a330e70fc4e54a5d8bf4791410c7469b587f6d6820cc109ffcb5" + }, + { + "path": "research/complex-frame-pair-decoders/PROOF.md", + "usage": "provenance", + "git_blob": "889f3a653ed1bdbb7df61ebe3af4f2103602a1f4", + "sha256": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74" + }, + { + "path": "research/p112-sparse-completion-rank/README.md", + "usage": "provenance", + "git_blob": "1118f0a09c80c4ab54bb048d21a8d3d2cb59d283", + "sha256": "771893ee9c728d8fe84b69ec9883133f9284d5f0319c890ab37d3949f152777a" + } + ] +} diff --git a/research/p112-diagonal-rank-boundary/TASK.json b/research/p112-diagonal-rank-boundary/TASK.json new file mode 100644 index 0000000000..0262d86868 --- /dev/null +++ b/research/p112-diagonal-rank-boundary/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp rank boundary for arbitrary complex diagonal completions of the fixed P112 Gram matrix: additivity through rank 58 and a rank-59 counterexample.", + "scope_change_reason": "Answer Open next question 1 of Arham-Tahir64 PR1313 instead of synthesizing a physical block decoder. This is an algebraic side result, without a paid-profile claim.", + "bottleneck_link": "Bounds the ordinary factorization rank available from freeing only diagonal entries. This does not establish copied-information or recursive costs.", + "budget_minutes": 60, + "stop_rule": "Stop discovery at the first verified original improvement; package the sharp rank-59 boundary without pursuing higher-rank classifications.", + "outcome": "completed", + "evidence": "Written Schur-complement proof using credited geometric premises; exact rational rank-59 witness on 53 changed positions; 7140 root-hyperplane pairs; eight extended-range and 128 Schur-bound fixtures; six controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which complex diagonal corrections attain the first nonadditive rank 59?", + "why_it_matters": "Would classify the first escape from low-rank diagonal rigidity.", + "first_step": "Use r=7, s=53 and the rank-one Schur complement, preserving arbitrary complex diagonal entries.", + "blocked_by": "A complete minimum-support codeword classification and parameter equivalences." + }, + { + "question": "Can an allowed diagonal-completion factorization improve a complete paid decoder bill?", + "why_it_matters": "Ordinary matrix rank alone does not measure copied information or recursive cost.", + "first_step": "Name a caller permitting changed diagonals and price its repair before factor synthesis.", + "blocked_by": "Copied-information, physical source access, frames, restoration and complete supplier contracts." + } + ] +} diff --git a/research/p112-diagonal-rank-boundary/VERIFY.json b/research/p112-diagonal-rank-boundary/VERIFY.json new file mode 100644 index 0000000000..2d244d7c0d --- /dev/null +++ b/research/p112-diagonal-rank-boundary/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": 120, + "checks": "Exact sharp rank-59 diagonal completion, extended-range fixtures, Schur lower bound, finite root-hyperplane intersection premise and six controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact checks with optimization, retaining all guards." + } + ] +} diff --git a/research/p112-diagonal-rank-boundary/verify.py b/research/p112-diagonal-rank-boundary/verify.py new file mode 100644 index 0000000000..78b1fbc3e4 --- /dev/null +++ b/research/p112-diagonal-rank-boundary/verify.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the sharp P112 diagonal-completion boundary. + +SPDX-License-Identifier: Apache-2.0 +""" + +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + need(len(left) == len(right) <= 112, "dot dimensions") + return sum(a * b for a, b in zip(left, right)) + + +def exact_rank(matrix): + """Rational elimination, with a fixed input capacity and no tolerance.""" + need(len(matrix) <= 112, "rank row capacity") + if not matrix: + return 0 + width = len(matrix[0]) + need(width <= 112 and all(len(row) == width for row in matrix), "rank shape") + need(all(type(x) is int and abs(x) <= 224 for row in matrix for x in row), + "bounded integer rank input") + rows = [[Fraction(x) for x in row] for row in matrix] + rank = 0 + for column in range(width): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + scale = rows[rank][column] + rows[rank] = [value / scale for value in rows[rank]] + for i in range(rank + 1, len(rows)): + scale = rows[i][column] + if scale: + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[rank])] + rank += 1 + if rank == len(rows): + break + return rank + + +def geometry(): + lines = set() + for i, j in combinations(range(8), 2): + for a, b in product((-2, 2), repeat=2): + row = [0] * 8 + row[i], row[j] = a, b + value = tuple(row) + lines.add(max(value, tuple(-x for x in value))) + for row in product((-1, 1), repeat=8): + if sum(x < 0 for x in row) % 2 == 0: + lines.add(max(row, tuple(-x for x in row))) + frame = set() + for i in range(0, 8, 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[i + 1] = 2, 2 * sign + frame.add(tuple(row)) + roots = sorted(lines) + live = [row for row in roots if row not in frame] + need(len(roots) == 120 and len(live) == 112, "root and puncture sizes") + need(all(dot(row, row) == 8 for row in roots), "doubled-root normalization") + return roots, live + + +def pair_intersections(roots): + """Finite premise for the new unchanged-row argument, not a flat audit.""" + zeros = [sum(1 << i for i, row in enumerate(roots) if dot(row, alpha) == 0) + for alpha in roots] + histogram = Counter((a & b).bit_count() for a, b in combinations(zeros, 2)) + need(histogram == {30: 3780, 36: 3360}, "distinct root-hyperplane intersections") + return {str(size): count for size, count in sorted(histogram.items())} + + +def changed_diagonal(gram, support, coefficient): + need(type(coefficient) is int and 1 <= abs(coefficient) <= 112, "diagonal coefficient") + need(all(type(i) is int and 0 <= i < len(gram) for i in support), "diagonal support") + return [[value + (coefficient if i == j and i in support else 0) + for j, value in enumerate(row)] for i, row in enumerate(gram)] + + +def validate_diagonal(gram, changed): + need(len(changed) == len(gram), "completion rows") + need(all(len(row) == len(gram) for row in changed), "completion columns") + need(all(changed[i][j] == gram[i][j] + for i in range(len(gram)) for j in range(len(gram)) if i != j), + "off-diagonal entries must be unchanged") + + +def witness(live): + gram = [[dot(a, b) for b in live] for a in live] + covariance = [[sum(row[i] * row[j] for row in live) for j in range(8)] + for i in range(8)] + need(covariance == [[112 * (i == j) for j in range(8)] for i in range(8)], + "tight-frame scale for the projection witness") + alpha = (1,) * 8 + need(alpha in live, "specified live normal") + values = [dot(row, alpha) for row in live] + support = {i for i, value in enumerate(values) if value} + unchanged = [row for i, row in enumerate(live) if i not in support] + need(len(support) == 53 and exact_rank(unchanged) == 7, "witness support and complement") + need(all(dot(row, values) == 112 * value for row, value in zip(gram, values)), + "root-code eigenvector") + changed = changed_diagonal(gram, support, -112) + validate_diagonal(gram, changed) + need(all(dot(row, values) == 0 for row in changed), "new kernel direction") + rank = exact_rank(changed) + need(rank == 59, "sharp rational completion rank") + return gram, support, values, changed, { + "normal": list(alpha), "support": sorted(support), "diagonal_coefficient": -112, + "unchanged_root_rank": 7, "completion_rank": rank, + "additive_prediction": 61, + } + + +def new_range_fixtures(gram, live): + results = [] + for size in (21, 31, 40, 50): + for stride, coefficient in ((1, 1), (17, -3)): + support = {(stride * i) % 112 for i in range(size)} + need(len(support) == size, "fixture distinct positions") + unchanged = [row for i, row in enumerate(live) if i not in support] + rank = exact_rank(changed_diagonal(gram, support, coefficient)) + need(exact_rank(unchanged) == 8 and rank == 8 + size, "extended-range fixture") + results.append({"size": size, "stride": stride, "coefficient": coefficient, + "completion_rank": rank}) + return results + + +def schur_bound_fixtures(): + rows = ((1, 0, 0), (0, 1, 0), (0, 0, 1), (1, 1, 0), (0, 1, 1)) + gram = [[dot(a, b) for b in rows] for a in rows] + count = 0 + for mask in range(32): + support = {i for i in range(5) if mask >> i & 1} + unchanged_rank = exact_rank([row for i, row in enumerate(rows) if i not in support]) + for coefficient in (-3, -1, 1, 2): + rank = exact_rank(changed_diagonal(gram, support, coefficient)) + need(rank >= len(support) + 2 * unchanged_rank - 3, "Schur rank lower bound") + if unchanged_rank == 3: + need(rank == 3 + len(support), "full unchanged-rank equality") + count += 1 + return count + + +def rejection_controls(gram, support, values, changed): + rejected = [] + try: + need(exact_rank(changed) == 58, "false rank-58 witness") + except ValueError: + rejected.append("false boundary rank") + try: + need(exact_rank(changed) == 8 + len(support), "false rank-59 additivity") + except ValueError: + rejected.append("invalid extension through rank 59") + wrong = changed_diagonal(gram, support, -111) + need(any(dot(row, values) for row in wrong) and exact_rank(wrong) == 60, + "changed scale must lose the claimed kernel") + rejected.append("wrong projection scale") + missing = changed_diagonal(gram, support - {min(support)}, -112) + need(exact_rank(missing) == 60, "missing diagonal must lose sharp rank") + rejected.append("omitted correction") + off_diagonal = [row[:] for row in changed] + off_diagonal[0][1] += 1 + try: + validate_diagonal(gram, off_diagonal) + except ValueError: + rejected.append("forbidden off-diagonal edit") + need(any(changed[i][i] != gram[i][i] for i in range(112)), + "witness cannot satisfy the distinct odd-only mask") + rejected.append("confusion with the odd-only mask") + need(len(rejected) == 6, "all six controls must execute") + return rejected + + +def run(): + roots, live = geometry() + intersections = pair_intersections(roots) + gram, support, values, changed, sharp = witness(live) + return { + "status": "PASS_P112_DIAGONAL_RANK_BOUNDARY", + "claim_type": "scoped proof with exact finite corroboration", + "additive_rank_range": [8, 58], "first_nonadditive_rank": 59, + "witness": sharp, "root_hyperplane_pair_intersections": intersections, + "extended_range_fixtures": new_range_fixtures(gram, live), + "schur_bound_fixtures": schur_bound_fixtures(), + "controls": rejection_controls(gram, support, values, changed), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a new receipt outside the package") + args = parser.parse_args() + if args.receipt: + destination = args.receipt.resolve() + need(HERE not in destination.parents, "receipt must be outside the package") + need(not destination.exists(), "receipt must be new") + result = run() + hashes = {} + for name in PACKAGE_FILES: + path = HERE / name + need(path.stat().st_size <= 131072, "package file capacity") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + receipt = {"result": result, "package_sha256": hashes} + payload = json.dumps(receipt, sort_keys=True, indent=2) + "\n" + if args.receipt: + with args.receipt.open("x", encoding="utf-8") as stream: + need(stream.write(payload) == len(payload), "complete receipt write") + print(payload, end="") + + +if __name__ == "__main__": + main() From 1c8bf3f3dadd1f6fd14892630eb76e984a74738a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 15:04:42 +0100 Subject: [PATCH 2/2] docs(research): keep diagonal boundary note focused on the result --- research/p112-diagonal-rank-boundary/README.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/research/p112-diagonal-rank-boundary/README.md b/research/p112-diagonal-rank-boundary/README.md index be80f7b480..777f2d9d1e 100644 --- a/research/p112-diagonal-rank-boundary/README.md +++ b/research/p112-diagonal-rank-boundary/README.md @@ -174,12 +174,11 @@ operator replay were not run. No unknown physical cost is priced as zero. The first verified improvement ends discovery; no construction expansion or larger-rank classification follows. -The engineering-mode autonomous-run playbook uses Build the Lever and -Prove It Works: the exact verifier is the retained evidence artifact. -Functions have fewer than 60 lines, with no recursion or dynamic code +The exact verifier is the retained evidence artifact. Functions have +fewer than 60 lines, with no recursion or dynamic code execution. Root lists have at most 120 elements, normal pairs number 7,140, and elimination matrices have at most 112 rows and columns with integer -inputs bounded in absolute value by 224. Power of Ten rule 3 requires a +inputs bounded in absolute value by 224. Fixed allocation requires a managed-runtime deviation: Python allocates integers, fractions and lists during these finite computations. The fixed dimensions bound live storage; Hadamard's bound controls the elimination minors. This deviation is