diff --git a/research/p112-diagonal-rank-boundary/README.md b/research/p112-diagonal-rank-boundary/README.md new file mode 100644 index 0000000000..777f2d9d1e --- /dev/null +++ b/research/p112-diagonal-rank-boundary/README.md @@ -0,0 +1,202 @@ +# 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 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. 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 +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()