From 65704df0ff4e7cad336694d39ff3492df48e0c04 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 13:18:37 +0000 Subject: [PATCH] feat(research): obstruct joint dyadic Gram normalization --- .../p104-joint-spectral-obstruction/PROOF.md | 166 ++++++++++ .../p104-joint-spectral-obstruction/README.md | 91 ++++++ .../SOURCES.json | 24 ++ .../p104-joint-spectral-obstruction/TASK.json | 109 +++++++ .../VERIFY.json | 36 +++ .../p104-joint-spectral-obstruction/verify.py | 283 ++++++++++++++++++ 6 files changed, 709 insertions(+) create mode 100644 research/p104-joint-spectral-obstruction/PROOF.md create mode 100644 research/p104-joint-spectral-obstruction/README.md create mode 100644 research/p104-joint-spectral-obstruction/SOURCES.json create mode 100644 research/p104-joint-spectral-obstruction/TASK.json create mode 100644 research/p104-joint-spectral-obstruction/VERIFY.json create mode 100644 research/p104-joint-spectral-obstruction/verify.py diff --git a/research/p104-joint-spectral-obstruction/PROOF.md b/research/p104-joint-spectral-obstruction/PROOF.md new file mode 100644 index 0000000000..c485b0bb9e --- /dev/null +++ b/research/p104-joint-spectral-obstruction/PROOF.md @@ -0,0 +1,166 @@ +# A persistent joint code cannot spectrally normalize the Gram pair + +This contribution was produced by Nick Petalas. It is a scoped written proof +with finite exact corroboration. It gives no new kappa or physical call tariff. + +## Contract and cited premises + +Let R = Z[i,1/2]. Chris R / Clear1nsight's +[PR #3979](https://github.com/CrocSwap/integer-mult-bounds/pull/3979), at +`a8a1d744811cd7d1f9c43ec7ccbae85ef9695b61`, supplies the P104 Gram matrix A, +of size n = 104, and the premises + +``` +A² = 13A, rank(A modulo 13, i -> 5) = r = 8. +``` + +The exact cited text is pinned in SOURCES.json at the canonical base. These +premises, the original code and its invoice are not rechecked here. The new +argument begins with the complete two-stage operator. The predecessor excludes +bank-separate codes for the same spectral target. Its proof explicitly leaves +general bank mixing outside that obstruction. + +Put B = A tensor I_n and C = I_n tensor A. On the two banks define + +``` +F = upper(-C) lower(B) = [ I-CB -C ]. + [ B I ] +``` + +Let P be the coordinate rank-r projector, P_r = P tensor I_n and +P_c = I_n tensor P. The proposed spectral endpoint is + +``` +T = upper(-alpha P_c) lower(beta P_r), alpha,beta in R, +alpha beta = 169. +``` + +The allowed code is one arbitrary Q in GL_(2n²+h)(R), for any finite h >= 0. +It may mix both data banks and all scratch coordinates. The same code is used +at entry and exit. Scratch has arbitrary initial data and must return exactly, +so the endpoints compared are F direct-sum I_h and T direct-sum I_h. Different +entry and exit codes, interleaved new operations, and a changed scratch return +are outside this contract. + +## Complete-pair invariant + +Reduce through the ring map R -> F_13 given by i -> 5 and 1/2 -> 7. An +R-invertible code stays invertible after reduction. Bars are omitted in this +section. Now A² = 0 and rank A = r. Hence B² = C² = 0, BC = CB, and + +``` +rank B = rank C = nr, D = BC = A tensor A, rank D = r². +N = F-I = [ -D -C ], N² = [ -D 0 ], N³ = 0. + [ B 0 ] [ 0 -D ] +``` + +To compute the first rank without an inequality, N(x,y) = 0 implies Bx = 0. +Then Dx = CBx = 0, so also Cy = 0. The converse holds. Thus +ker N = ker B direct-sum ker C, and + +``` +rank N = 2nr, rank N² = 2r², rank N³ = 0. +``` + +These identities hold over every field for a square-zero A. In particular, +r <= n/2. The nilpotent Jordan multiplicities are + +``` +size 3: 2r²; size 2: 2r(n-2r); size 1: 2(n-r)². +``` + +For the cited P104 premises, the new complete-pair invariants are + +``` +dimension 21632; ranks 1664, 128, 0; +Jordan multiplicities 128 blocks of size 3, + 1408 blocks of size 2, + 18432 blocks of size 1. +``` + +The Jordan facts used here are standard nilpotent linear algebra. Their +application to this complete Gram pair and the following stable obstruction +are the new step. + +## Joint codes and restored scratch still fail + +Since alpha beta reduces to zero in a field, at least one coefficient reduces +to zero. Therefore T-I reduces to a single off-diagonal square-zero block, +or to zero. Its rank is nr if exactly one coefficient survives, and zero if +both vanish. In particular its rank is at most nr, strictly below 2nr when +r > 0. + +Conjugacy preserves rank after subtracting the identity. Adding I_h adds +only zero blocks to that difference. Consequently + +``` +Q (F direct-sum I_h) Q^-1 != T direct-sum I_h +``` + +for every code and finite restored scratch allowed by the contract. This +removes the bank-separate restriction from this particular free-normalization +exclusion. It does not exclude arbitrary joint programs or every decoder. + +## The correction rank and its precise sharpness + +Write E = Q(F direct-sum I_h)Q^-1 - (T direct-sum I_h). The rank inequality +rank(X-Y) >= rank X - rank Y, applied after subtracting the identity, gives + +``` +rank_F13 E >= nr = 832, +rank_F13 E >= 2nr = 1664 if both coefficients vanish modulo 13. +``` + +The second case includes alpha = beta = 13. A nonzero minor over F_13 comes +from a nonzero minor over Q(i). Thus the same lower bounds hold for the +characteristic-zero rank of any R-valued E. Rank is an endpoint matrix rank, +not a number of native children or a complete paid invoice. + +The bounds are exact in the modular relaxation, even without scratch. In +Jordan coordinates N has 2r(n-r) nontrivial chains. This is at least nr. +Select one arrow in each of nr different chains, and let M retain just these +arrows. Then M² = 0, rank M = nr, and rank(N-M) = 2nr-nr = nr. Distinct +Jordan arrows have distinct row and column indices, so the last equality +follows by counting the remaining arrows. + +Every square-zero matrix of this dimension and rank nr is similar over the +field to M. Hence this construction attains the lower bound for every modular +target with exactly one surviving coefficient. When neither survives, the +target is the identity and rank N = 2nr attains the other bound. The verifier +enumerates all 21632 Jordan coordinates and an explicit permutation matching +the 832 projector arrows to the selected arrows. Existence of the Jordan +basis follows from the written argument, not a reconstruction of the original +P104 matrix. + +This is sharpness over F_13. No exact dyadic rank-832 correction or lift of +the entire corrected endpoint is constructed or claimed. + +## Finite corroboration and boundaries + +The verifier multiplies the literal two shears for each tensor pair of a +size-two nilpotent block or a size-one zero block. Exact elimination checks +their ranks and cubes in five prime fields. It enumerates the direct-sum +components and all Jordan coordinates for n = 104, r = 8. Small stable +fixtures mix data and restored scratch and cover every coefficient residue +pair whose product is zero. They are finite checks of the new formulas, +not independent verification of the predecessor's Gram premises. + +An exact rational control uses A = [[13,1],[0,0]] and +S = [[1,1/13],[0,1]]. Here SAS^-1 = diag(13,0). The two-axis code built from +S tensor S does perform the spectral normalization. Its forbidden denominator +shows why the coefficient-ring hypothesis matters. A separate scratch control +can move the nontrivial endpoint entirely into an unreturned scratch bank. +That is why an identity return on the whole scratch space is required. + +No selected native, caller, compiler, precision, stock, tape or analytic replay +is needed for this algebraic side result, and none is claimed. Independent +human and formal proof-kernel review are unclaimed. + +## Open next questions + +Can an exact R-valued correction attain rank 832 for this spectral target? +Start with n = 2, r = 1 and the displayed integral A; require one common +R-invertible code and an exact endpoint. A modular witness alone cannot +answer this lifting question. A useful physical implementation must then price +access, native maps and complete restoration. A different producer/consumer +boundary must state which common-code hypothesis it changes. diff --git a/research/p104-joint-spectral-obstruction/README.md b/research/p104-joint-spectral-obstruction/README.md new file mode 100644 index 0000000000..4bb5bad2cc --- /dev/null +++ b/research/p104-joint-spectral-obstruction/README.md @@ -0,0 +1,91 @@ +# Joint bank mixing does not remove the dyadic Gram spectral obstruction + +This contribution was produced by Nick Petalas. It is a scoped written proof +with finite exact corroboration. No new kappa is claimed. + +Chris R / Clear1nsight's [PR #3979](https://github.com/CrocSwap/integer-mult-bounds/pull/3979) +leaves joint bank mixing outside its exclusion of a free spectral split of the +P104 Gram pair. The new result closes that particular escape when one persistent +Gaussian-dyadic invertible code is used at both endpoints. The code can mix both +banks and any finite number of arbitrary scratch coordinates, provided all +scratch returns identically. + +For the complete pair F = upper(-I tensor A) lower(A tensor I), reduction modulo +13 gives ranks 1664, 128 and zero for F-I, its square and its cube. Its nilpotent +Jordan blocks have sizes 3, 2 and 1 with multiplicities 128, 1408 and 18432. +A spectral-projector pair with coefficients alpha beta = 169 has rank at most +832 after subtracting the identity. Similarity and identity scratch preserve +the discrepancy. + +Every exact Gaussian-dyadic endpoint correction consequently has matrix rank +at least 832, or at least 1664 when both coefficients vanish modulo 13, including +alpha = beta = 13. Both bounds are attained in the modular relaxation. An exact +dyadic attaining correction is not supplied. Matrix rank is not a native-call +tariff or a complete recursive invoice. + +[PROOF.md](PROOF.md) gives the general n,r statement, the kernel calculation, +the stable obstruction and the exact modular sharpness argument. The predecessor +premises n = 104, A² = 13A and rank(A modulo 13) = 8 are cited and source-bound. +Its original code, counts and proofs are not replayed or audited here. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-joint-spectral-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/p104-joint-spectral-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-joint-spectral-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-joint-spectral-obstruction --check-source-history --check-modes +``` + +Another CPython 3.12 executable may replace the local path. Direct output is a +generated JSON receipt bound to package and premise-file hashes, followed by +`PASS_P104_JOINT_SPECTRAL_OBSTRUCTION modular_repair=832 balanced=1664 no_new_kappa`. +The launcher also checks metadata and exact source pins. + +The finite checks cover 20 literal atomic tensor pairs over five prime fields, +80 small direct-sum assemblies, all 9216 canonical P104 components and all 21632 +Jordan coordinates. An explicit coordinate permutation matches the 832 projector +arrows to the attaining modular repair. Seventy-five stable fixtures cover every +zero-product coefficient residue pair with zero, one and three restored scratch +coordinates. Controls retain a rational normalization using 1/13, an omitted +stage, unreturned scratch and invalid square-zero source parameters. + +The program reads one pinned premise file. It builds no dense matrix larger +than 32 by 32; the full canonical witness uses bounded coordinate dictionaries. +Python allocates managed objects during the finite run. These explicit size +bounds replace a fixed-allocation implementation. Every function is below +60 lines, and the registered commands enable warnings as errors and exercise +normal and optimized execution. No external static analyzer is required. + +## Limits + +One common code at entry and exit, the Gaussian-dyadic coefficient ring and +identity return of the entire scratch space are essential. New interleaved +operations, distinct endpoint codes, other spectral targets and odd-denominator +codes are not excluded. No physical producer/consumer implementation or paid +rank conversion follows from this endpoint invariant. + +No selected native, caller, compiler, precision, storage, tape or analytic replay +was run. Independent human and formal proof-kernel review are unclaimed. The +selected frontier and frozen predecessors are unchanged. + +## Open next questions + +Can an exact Gaussian-dyadic correction attain rank 832? Start with the displayed +n = 2, r = 1 integral matrix in the proof and require the same dyadic-invertible +code at both endpoints. A modular solution alone does not establish a lift. +Only after an exact endpoint exists should its native access and complete paid +restoration costs be priced. [TASK.json](TASK.json) records the question and +blocker explicitly. + +## Predecessor credit + +Chris R / Clear1nsight owns PR3979's tensor code, original bank-separate +obstruction, scalar words and invoice. PR3961 supplies the preceding code +mismatch; PR3882, PR3940, PR3943 and PR3954 retain the caller lineage. ToikY's +literal-word audit and the native, geometry and compiler authors credited by +PR3979 retain their contributions. No predecessor construction credit is claimed. +Nilpotent Jordan classification and rank inequalities are classical. New work +is under Apache-2.0. diff --git a/research/p104-joint-spectral-obstruction/SOURCES.json b/research/p104-joint-spectral-obstruction/SOURCES.json new file mode 100644 index 0000000000..758e238442 --- /dev/null +++ b/research/p104-joint-spectral-obstruction/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-tensor-code/PROOF.md", + "usage": "input", + "git_blob": "b570c8bdf5acec263c63562ddb5e384ff3616c3f", + "sha256": "259ba7b0926dd6db4e7c45ff7ccb10659dee06aef0a573547236c994ad304756" + } + ] +} diff --git a/research/p104-joint-spectral-obstruction/TASK.json b/research/p104-joint-spectral-obstruction/TASK.json new file mode 100644 index 0000000000..92ffc32ac6 --- /dev/null +++ b/research/p104-joint-spectral-obstruction/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Extend the PR3979 free spectral-normalization exclusion to a common arbitrary joint-bank Gaussian-dyadic code with any finite identically restored scratch. Prove exact complete-pair modular ranks and the sharp modular correction-rank bounds 832 and 1664.", + "scope_change_reason": "The current decoder card permits a target-specific changed-code obstruction. PR3979 leaves joint bank mixing outside its bank-separate obstruction. This result addresses that precise missing hypothesis instead of searching a new itinerary or auditing the predecessor.", + "bottleneck_link": "A free spectral split would discard the nontrivial dyadic coupling in a changed P104 producer/consumer interface. The new stable obstruction forces a nonzero correction even with unrestricted persistent bank mixing. Matrix rank does not price the native or complete recursive bill.", + "budget_minutes": 60, + "stop_rule": "Stop and package the first verified joint-code obstruction; do not expand to physical synthesis or further mechanisms.", + "outcome": "completed", + "evidence": "PROOF.md gives the quantified argument. verify.py generates a hash-bound stdout receipt: 20 atomic block cases, 80 small assemblies, all 9216 P104 canonical components, 21632 Jordan coordinates and 75 stable coefficient fixtures. Predecessor Gram identities are cited premises, not replayed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an exact Gaussian-dyadic correction attain characteristic-zero rank 832 for the spectral-projector target?", + "why_it_matters": "The modular rank floor is sharp over F13 but does not construct a dyadic corrected endpoint or a favorable paid bill.", + "first_step": "Solve the exact n=2, r=1 example A=[[13,1],[0,0]] with one common dyadic-invertible code and a rank-two correction, before attempting the P104 instance.", + "blocked_by": "Lifting the modular endpoint and pricing access, native calls and restoration." + } + ], + "predecessor": { + "pr": 3979, + "author": "Clear1nsight / Chris R", + "head": "a8a1d744811cd7d1f9c43ec7ccbae85ef9695b61", + "premises": "A^2=13A; n=104; rank(A mod13)=8; original code and invoice not replayed." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267739", + "overlap": { + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "priority_revision": 8, + "checked_utc": "2026-10-29T13:06:00Z", + "sources": [ + "Live open PR list and full overlap corpus", + "Latest handoff comments and local reservations", + "Main READMEs for bank-mixing, spectral normalization, Gram/Jordan and rank terms", + "Merged PR searches; this account had no recent PR mentioning PR3979" + ], + "limitations": "Read-only bounded overlap evidence, not proof of novelty. Earlier colliding code-weight and variable-target sources were abandoned before any public claim or computation.", + "submission_checked_utc": "2026-10-29T13:16:31Z", + "canonical_main_unchanged": true, + "remote_coverage": { + "open_prs": 317, + "discussions": 5863, + "open_fetched_at": "2026-10-29T13:05:54.416586+00:00", + "discussions_fetched_at": "2026-10-29T13:07:07.751181+00:00", + "local_head_notes": 8567, + "complete_pagination": true + } + }, + "environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "requirements": "standard library only" + } +} diff --git a/research/p104-joint-spectral-obstruction/VERIFY.json b/research/p104-joint-spectral-obstruction/VERIFY.json new file mode 100644 index 0000000000..c77a86289c --- /dev/null +++ b/research/p104-joint-spectral-obstruction/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-tensor-code/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal shear/block products; modular rank and nilpotent powers; complete canonical P104 component and Jordan enumeration; explicit rank-optimal modular repair permutation; stable mixing and every zero-product coefficient residue pair; invalid parameter, omitted stage, unreturned scratch and rational escape controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all new finite checks and source binding with interpreter assertions disabled." + } + ] +} diff --git a/research/p104-joint-spectral-obstruction/verify.py b/research/p104-joint-spectral-obstruction/verify.py new file mode 100644 index 0000000000..307a6c9a8a --- /dev/null +++ b/research/p104-joint-spectral-obstruction/verify.py @@ -0,0 +1,283 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the joint-bank spectral obstruction.""" + +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def eye(n): + require(0 <= n <= 32, "dense matrix capacity") + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def multiply(a, b, prime=13): + require(len(a[0]) == len(b), "matrix product shape") + out = [[sum(x * y for x, y in zip(row, col)) + for col in zip(*b)] for row in a] + return out if prime is None else [[x % prime for x in row] for row in out] + + +def subtract(a, b, prime=13): + require(len(a) == len(b) and len(a[0]) == len(b[0]), "difference shape") + out = [[x - y for x, y in zip(u, v)] for u, v in zip(a, b)] + return out if prime is None else [[x % prime for x in row] for row in out] + + +def kron(a, b): + return [[x * y for x in ar for y in br] for ar in a for br in b] + + +def diagonal(a, b): + return ([row + [0] * len(b) for row in a] + + [[0] * len(a) + row for row in b]) + + +def rank(a, prime): + require(1 <= len(a) <= 32 and 1 <= len(a[0]) <= 32, "rank capacity") + work = [[x % prime for x in row] for row in a] + pivot = 0 + for col in range(len(work[0])): + hit = next((i for i in range(pivot, len(work)) if work[i][col]), None) + if hit is None: + continue + work[pivot], work[hit] = work[hit], work[pivot] + inverse = pow(work[pivot][col], -1, prime) + work[pivot] = [x * inverse % prime for x in work[pivot]] + for i in range(len(work)): + if i != pivot: + factor = work[i][col] + work[i] = [(x - factor * y) % prime + for x, y in zip(work[i], work[pivot])] + pivot += 1 + if pivot == len(work): + break + return pivot + + +def gram_pair(a, prime=13): + """Literal upper(-I tensor A) times lower(A tensor I).""" + n = len(a) + b, c = kron(a, eye(n)), kron(eye(n), a) + size = n * n + upper, lower = eye(2 * size), eye(2 * size) + for i, j in product(range(size), repeat=2): + upper[i][size + j] = -c[i][j] + lower[size + i][j] = b[i][j] + return multiply(upper, lower, prime), b, c + + +def rectangular_pair(a, b, prime): + left, right = kron(a, eye(len(b))), kron(eye(len(a)), b) + size = len(a) * len(b) + upper, lower = eye(2 * size), eye(2 * size) + for i, j in product(range(size), repeat=2): + upper[i][size + j] = -right[i][j] + lower[size + i][j] = left[i][j] + actual = subtract(multiply(upper, lower, prime), eye(2 * size), prime) + joint = multiply(right, left, prime) + formula = ([[-x for x in u] + [-x for x in v] + for u, v in zip(joint, right)] + + [row + [0] * size for row in left]) + require(actual == [[x % prime for x in row] for row in formula], + "literal product and block formula disagree") + return actual + + +def local_blocks(): + blocks = {1: [[0]], 2: [[0, 1], [0, 0]]} + result = {} + for prime, p, q in product((2, 3, 5, 13, 17), (1, 2), (1, 2)): + nilpotent = rectangular_pair(blocks[p], blocks[q], prime) + square = multiply(nilpotent, nilpotent, prime) + cube = multiply(square, nilpotent, prime) + ranks = (rank(nilpotent, prime), rank(square, prime), rank(cube, prime)) + expected = (int(p == 2) * q + int(q == 2) * p, + 2 * int(p == q == 2), 0) + require(ranks == expected, "atomic tensor ranks") + result[f"{prime}:{p}x{q}"] = [2 * p * q, *ranks] + return result + + +def assemble(n, r, atoms): + require(0 <= 2 * r <= n <= 104, "square-zero source parameters") + parts = [2] * r + [1] * (n - 2 * r) + counts = Counter() + totals = [0, 0, 0, 0] + for p, q in product(parts, repeat=2): + data = atoms[f"13:{p}x{q}"] + counts[f"{p}x{q}"] += 1 + totals = [x + y for x, y in zip(totals, data)] + dimension, first, second, third = totals + require(totals == [2 * n * n, 2 * n * r, 2 * r * r, 0], "assembled ranks") + jordan = {"3": second, "2": first - 2 * second, + "1": dimension - 2 * first + second} + require(all(x >= 0 for x in jordan.values()), "Jordan multiplicities") + return {"n": n, "r": r, "components": dict(sorted(counts.items())), + "dimension": dimension, "ranks": [first, second, third], + "jordan_blocks": jordan} + + +def matching_rank(mapping): + require(len(set(mapping.values())) == len(mapping), "distinct arrow images") + return len(mapping) + + +def optimal_modular_repair(data): + """Enumerate Jordan arrows, and match an actual projector's arrows to them.""" + original, chosen = {}, {} + cursor = 0 + target_rank = data["n"] * data["r"] + for size in (3, 2, 1): + for _ in range(data["jordan_blocks"][str(size)]): + for offset in range(1, size): + original[cursor + offset] = cursor + offset - 1 + if size >= 2 and len(chosen) < target_rank: + chosen[cursor + 1] = cursor + cursor += size + require(cursor == data["dimension"], "complete Jordan coordinates") + require(len(chosen) == target_rank, "enough disjoint Jordan chains") + require(all(dest not in chosen for dest in chosen.values()), "square-zero target") + correction = {col: row for col, row in original.items() if col not in chosen} + require(matching_rank(original) == data["ranks"][0], "Jordan source rank") + require(matching_rank(correction) == target_rank, "attaining repair rank") + n, r = data["n"], data["r"] + target = {n * n + i * n + j: i * n + j + for i, j in product(range(n), range(r))} + permutation = {} + for (col, row), (new_col, new_row) in zip(target.items(), chosen.items()): + permutation[col], permutation[row] = new_col, new_row + remaining = sorted(set(range(cursor)) - set(permutation.values())) + old_remaining = sorted(set(range(cursor)) - set(permutation)) + permutation.update(zip(old_remaining, remaining)) + require(len(set(permutation.values())) == cursor, "full coordinate permutation") + require({permutation[c]: permutation[v] for c, v in target.items()} == chosen, + "projector conjugacy witness") + return {"asymmetric_minimum_modular_rank": matching_rank(correction), + "balanced_minimum_modular_rank": matching_rank(original), + "enumerated_coordinates": cursor, "projector_arrows": len(target)} + + +def stable_fixtures(): + source, _, _ = gram_pair([[0, 1], [0, 0]]) + cases = 0 + for scratch in (0, 1, 3): + extended = diagonal(source, eye(scratch)) + size = len(extended) + code, inverse = eye(size), eye(size) + for i in range(size - 1): + step, back = eye(size), eye(size) + step[i][i + 1], back[i][i + 1] = 1, -1 + code = multiply(step, code) + inverse = multiply(inverse, back) + require(multiply(code, inverse) == eye(size), "joint mixing inverse") + mixed = multiply(multiply(code, extended), inverse) + require(rank(subtract(mixed, eye(size)), 13) == 4, "restored scratch invariant") + for alpha, beta in product(range(13), repeat=2): + if alpha * beta % 13: + continue + p = [[1, 0], [0, 0]] + left, right = kron(p, eye(2)), kron(eye(2), p) + target = eye(8) + for i, j in product(range(4), repeat=2): + target[i][4 + j] = -alpha * right[i][j] + target[4 + i][j] = beta * left[i][j] + target = diagonal(target, eye(scratch)) + trank = rank(subtract(target, eye(size)), 13) + require(trank == (2 if alpha or beta else 0), "projector target rank") + require(rank(subtract(mixed, target), 13) >= 4 - trank, + "stable correction lower bound") + cases += 1 + return cases + + +def rational_escape(): + source, _, _ = gram_pair([[13, 1], [0, 0]], None) + t = [[1, Q(1, 13)], [0, 1]] + inverse = [[1, Q(-1, 13)], [0, 1]] + code = diagonal(kron(t, t), kron(t, t)) + back = diagonal(kron(inverse, inverse), kron(inverse, inverse)) + target, _, _ = gram_pair([[13, 0], [0, 0]], None) + require(multiply(code, back, None) == eye(8), "rational code inverse") + require(multiply(multiply(code, source, None), back, None) == target, + "odd-denominator escape must remain possible") + require(any(isinstance(x, Q) and x.denominator % 13 == 0 + for row in code for x in row), "escape leaves dyadic ring") + + +def return_controls(): + source, b, _ = gram_pair([[0, 1], [0, 0]]) + lower = eye(8) + for i, j in product(range(4), repeat=2): + lower[4 + i][j] = b[i][j] + require(rank(subtract(lower, eye(8)), 13) == 2, "omitted stage changes invariant") + extended = diagonal(source, eye(8)) + swap = [[int((i + 8) % 16 == j) for j in range(16)] for i in range(16)] + moved = multiply(multiply(swap, extended), swap) + require(moved == diagonal(eye(8), source), "discarded scratch escape") + require(moved != eye(16), "scratch return must be checked") + + +def source_binding(): + path = HERE / "SOURCES.json" + require(path.stat().st_size <= 16384, "source manifest capacity") + manifest = json.loads(path.read_text(encoding="utf-8")) + require(len(manifest["files"]) == 3, "source inventory capacity") + bound = {} + for item in manifest["files"]: + if item["usage"] == "input": + require(item["path"] == "research/p104-tensor-code/PROOF.md", + "declared premise path") + path = ROOT / item["path"] + require(not path.is_symlink() and path.stat().st_size <= 16 * 1024 * 1024, + "bounded regular source") + digest = sha256(path.read_bytes()).hexdigest() + require(digest == item["sha256"], "cited premise source changed") + bound[item["path"]] = digest + require(len(bound) == 1, "one cited premise source") + return bound + + +def main(): + bound = source_binding() + atoms = local_blocks() + small = [assemble(n, r, atoms) for n in range(1, 17) + for r in range(n // 2 + 1)] + actual = assemble(104, 8, atoms) + repair = optimal_modular_repair(actual) + rational_escape() + return_controls() + invalid = 0 + for n, r in ((1, 1), (104, 53), (105, 1), (2, -1)): + try: + assemble(n, r, atoms) + except ValueError: + invalid += 1 + require(invalid == 4, "invalid parameter controls") + report = {"schema": "p104-joint-spectral-obstruction/1", + "claim_type": "scoped proof with finite exact corroboration", + "p104": actual, "repair": repair, "local_block_cases": len(atoms), + "small_assemblies": len(small), "stable_cases": stable_fixtures(), + "controls": ["invalid_square_zero_parameters", "odd_denominator_escape", + "omitted_stage", "unreturned_scratch_escape"], + "cited_premise_hashes": bound, + "scope": "The predecessor Gram identities are premises, not replayed results. Sharpness is over F13, not an exact dyadic repair.", + "package_hashes": {name: sha256((HERE / name).read_bytes()).hexdigest() + for name in ("verify.py", "PROOF.md", "SOURCES.json", "TASK.json", "VERIFY.json", "README.md")}} + print(json.dumps(report, sort_keys=True)) + print("PASS_P104_JOINT_SPECTRAL_OBSTRUCTION modular_repair=832 balanced=1664 no_new_kappa") + + +if __name__ == "__main__": + main()