From 0f4419bc55adf4fe9b2469f98f7e8f95a21b6b6d Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Tue, 27 Oct 2026 13:38:46 +0000
Subject: [PATCH] feat(research): prove sharp shared-block spectral envelopes

---
 .../shared-block-spectral-envelope/PROOF.md   | 152 ++++++++++
 .../shared-block-spectral-envelope/README.md  | 118 ++++++++
 .../SOURCES.json                              |  30 ++
 .../shared-block-spectral-envelope/TASK.json  |  89 ++++++
 .../VERIFY.json                               |  34 +++
 .../shared-block-spectral-envelope/verify.py  | 265 ++++++++++++++++++
 6 files changed, 688 insertions(+)
 create mode 100644 research/shared-block-spectral-envelope/PROOF.md
 create mode 100644 research/shared-block-spectral-envelope/README.md
 create mode 100644 research/shared-block-spectral-envelope/SOURCES.json
 create mode 100644 research/shared-block-spectral-envelope/TASK.json
 create mode 100644 research/shared-block-spectral-envelope/VERIFY.json
 create mode 100644 research/shared-block-spectral-envelope/verify.py

diff --git a/research/shared-block-spectral-envelope/PROOF.md b/research/shared-block-spectral-envelope/PROOF.md
new file mode 100644
index 0000000000..aa761529de
--- /dev/null
+++ b/research/shared-block-spectral-envelope/PROOF.md
@@ -0,0 +1,152 @@
+# Sharp spectral envelope for a shared support block
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let F be any field of characteristic two, let r >= 1, and let D in M_r(F)
+be idempotent of rank k. For a matrix X, let z(X) be the algebraic multiplicity
+of zero in its characteristic polynomial, equivalently dim ker(X^r).
+Consider every ordered pair A,B in M_r(F) satisfying A+B=D. Then
+
+```text
+max [z(A)+z(B)] = r        if k=r;
+                   2r-1   if 0<k<r and k is odd;
+                   2r     if 0<=k<r and k is even.
+```
+
+The maximum exists and can always be attained by binary matrices after putting
+D into its coordinate basis. Thus the formula is independent of the particular
+characteristic-two field. In the original basis, conjugate both witnesses by
+the same change of basis that carries diag(I_k,0) to D.
+
+There is also a rigidity statement. If r >= 3 is odd, k=r-1, and the maximum
+2r is attained, both A and B have exactly one nilpotent Jordan block of size r.
+In particular, A^(r-1) and B^(r-1) are nonzero. The high zero multiplicity
+cannot in this case be attained by replacing either summand with only short
+nilpotent chains.
+
+This is a local matrix theorem. It imposes no chronological support history,
+external response conditions or physical realization on A,B.
+
+## Upper bounds
+
+Every r-by-r matrix has z <= r. This proves the 2r bound when k is even.
+If k is odd, tr(A)+tr(B)=tr(D)=1 in F. Two nilpotent matrices have trace zero,
+so at least one summand has z <= r-1. Consequently z(A)+z(B) <= 2r-1.
+
+When k=r, an invertible idempotent is I, so B=I+A. The zero primary subspace
+of B is the one primary subspace of A. The zero and one primary subspaces of A
+have direct sum inside F^r, since t and t+1 are relatively prime. Their
+dimensions are z(A) and z(B), respectively. Therefore z(A)+z(B) <= r.
+These arguments apply over F itself; algebraic closure is not required.
+
+## An explicit even-rank construction
+
+First take even k and dimension n=k+1, so n is odd. Let J_n be the all-ones
+matrix, let U be its strictly upper triangular part, and let L be its strictly
+lower triangular part. In characteristic two,
+
+```text
+U+L = I_n+J_n = D_0,
+J_n^2 = n J_n = J_n,
+D_0^2 = D_0.
+```
+
+Both U and L are nilpotent. The kernel of D_0 is the all-ones line, and its
+image is the coordinate-sum-zero subspace. Thus rank(D_0)=n-1=k.
+For a literal coordinate endpoint, use the ordered basis
+
+```text
+e_1+e_n, ..., e_(n-1)+e_n, (1,...,1).
+```
+
+It is a basis: if a linear combination vanishes, its first n-1 coordinates
+force all coefficients on the first n-1 vectors to equal the last coefficient.
+The last coordinate then forces that coefficient to vanish, because n is odd.
+The first n-1 vectors are fixed by D_0 and the last is killed. If S has these
+basis columns, then
+
+```text
+S^-1 D_0 S = diag(I_k,0),
+A_0=S^-1 U S, B_0=S^-1 L S,
+z(A_0)=z(B_0)=k+1.
+```
+
+For any r>k, append r-k-1 zero coordinates to both matrices. This attains 2r
+for every proper even rank, including k=0.
+
+For odd 0<k<r, use the even-rank k-1 construction in dimension k. Add one
+scalar coordinate with A=0, B=1, and then r-k-1 zero coordinates. Move the
+core's zero coordinate after the added one coordinate. The endpoint is
+exactly diag(I_k,0). Now A is nilpotent and B has precisely one nonzero
+eigenvalue, so z(A)+z(B)=r+(r-1). Finally, for k=r take A=0 and B=I.
+All entries and basis maps used here lie in F2 and remain valid after scalar
+extension to F.
+
+This explicit construction uses the classical method of splitting a zero-diagonal
+matrix into two strict triangular parts. General trace-zero/nilpotent-sum
+classification is not claimed as new. For context see Simion Breaz and Grigore
+Calugareanu, [Sums of nilpotent matrices](https://math.ubbcluj.ro/~calu/su-ni.pdf),
+Proposition 3, and the classical prescribed-diagonal theorem credited there.
+The displayed special construction and the upper bounds make this proof
+self-contained; no result from that paper is needed for verification.
+
+## Forced full-length chains at corank one
+
+Suppose r is odd, k=r-1 and z(A)+z(B)=2r. Both matrices are nilpotent. Put
+E=I+D; since D is idempotent of rank r-1, E has rank one. If
+v is in ker(A) intersect ker(E), then Dv=v and
+
+```text
+Bv = (D+A)v = v.
+```
+
+Nilpotence of B forces v=0. Hence E is injective on ker(A), giving
+dim ker(A) <= rank(E)=1. A nilpotent matrix on a positive-dimensional space
+has nonzero kernel, so dim ker(A)=1. Its nilpotent Jordan form has one block,
+of size r. Interchange A and B for the other conclusion. This also proves
+that the explicit corank-one construction has the necessary chain lengths.
+
+## Consequence for larger support blocks
+
+JoyboyBrian's [PR #5507](https://github.com/CrocSwap/integer-mult-bounds/pull/5507),
+head `1691a6024b60bdf28d7a2eed13cb32d78e2ea5b4`, proves a complete two-owner
+four-support funding obstruction. Its Section 3 studies exactly
+A+B=diag(t), with k the number of Q flags. For r<=3 it bounds the sum by
+2r-k except for the genuine r=3,k=2 exception. The global proof compensates
+that exception through native chains and disjoint support classes.
+
+The new envelope identifies the precise loss from using 2r-k in larger
+local blocks. At a proper even rank the possible excess is k; at a proper
+odd rank it is k-1. This excess is unbounded as support size grows. In
+particular, r=5,k=4 has maximum 10, whereas 2r-k is 6. A binary coordinate
+witness, whose rows are encoded with bit j as column j, is
+
+```text
+A = (11,25,13,21,10),
+B = (10,27, 9,29,10).
+```
+
+It satisfies A+B=diag(1,1,1,1,0), A^5=B^5=0 and A^4,B^4 != 0.
+The theorem supplies both the local ceiling and a necessary full-length-chain
+condition in this corank-one family. It neither refutes #5507's four-support
+theorem nor generalizes its global compensation. A larger caller still needs
+its exact chronology, support ownership, native-chain restrictions and complete
+paid/target invoice. No new controller or multiplication saving follows.
+
+## Evidence boundary
+
+The written proof carries all dimensions and all characteristic-two fields.
+The standalone checker constructs every (r,k) with 1<=r<=33, 0<=k<=r.
+Its small census enumerates every binary A through dimension four with D
+fixed to each coordinate rank, so every ordered pair B=A+D is covered.
+For each enumerated A, it compares dim ker(A^r), computed by binary matrix
+powers and elimination, with the order at zero of a separate Leibniz
+characteristic polynomial. It also checks every corank-one extremizer in
+that census for the forced full chain. The finite checks are corroboration,
+not a formal proof of the quantified theorem.
+
+No predecessor verifier is imported or replayed. No native implementation,
+rounded execution, supplier admission or complete multiplication theorem is
+asserted. Independent human and formal proof-kernel review are unclaimed.
diff --git a/research/shared-block-spectral-envelope/README.md b/research/shared-block-spectral-envelope/README.md
new file mode 100644
index 0000000000..76bc329270
--- /dev/null
+++ b/research/shared-block-spectral-envelope/README.md
@@ -0,0 +1,118 @@
+# Sharp spectral envelopes for shared BIT blocks
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped algebraic proof with exact finite corroboration.** For every
+characteristic-two field, idempotent D of rank k in dimension r, and matrices
+A+B=D, the sharp maximum of the total algebraic zero multiplicity is
+
+```text
+r       when k=r;
+2r-1    when 0<k<r is odd;
+2r      when 0<=k<r is even.
+```
+
+Explicit binary witnesses attain every case. When r>=3 is odd and k=r-1,
+every maximizer consists of two single full-length nilpotent Jordan blocks.
+The [proof](PROOF.md) gives the construction, upper bounds and rigidity argument.
+
+JoyboyBrian's [PR #5507](https://github.com/CrocSwap/integer-mult-bounds/pull/5507)
+handles shared blocks of size at most three in its complete four-support BIT
+obstruction. Its triple exception is genuine. This new local law shows that
+larger blocks can exceed the ordinary 2r-k bound by an unbounded amount.
+Already at r=5,k=4 the exact maximum is 10 rather than 6, with a literal
+coordinate witness in PROOF.md. The forced chain length is an additional
+constraint for anyone trying to realize these local extremes.
+
+The new contribution is this source-scoped spectral envelope and its chain
+consequence. General nilpotent-sum theory and zero-diagonal splitting are
+classical and credited in PROOF.md. This is not a larger-support global funding
+theorem, a physical word, a complete invoice or a new kappa.
+
+## Reproduce
+
+Use CPython 3.12 and its standard library. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/shared-block-spectral-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/shared-block-spectral-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shared-block-spectral-envelope
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shared-block-spectral-envelope --check-source-history
+```
+
+Any CPython 3.12 path can replace the displayed local interpreter. The direct
+marker is `PASS_SHARED_BLOCK_SPECTRAL_ENVELOPE`. The registered commands run
+normally and under optimization, with admission checks enabled in both modes.
+
+The complete finite evidence is 594 constructed (r,k) witnesses through r=33,
+329,780 binary ordered matrix pairs through r=4, 66,066 independent
+characteristic-polynomial comparisons, and ten domain/witness rejection
+controls. The JSON stdout includes every census maximum and maximizer count.
+Use `--receipt /absolute/external/new.json` for a generated receipt binding
+all package files by SHA256. It refuses an existing receipt or a path inside
+the package. Ordinary replay is read-only and creates no artifacts.
+
+## Scope and predecessor credit
+
+Base `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+The `bit-helper-contract` card changes to this local spectral side result,
+rather than another G20 word search. The current baseline command passed
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it is metadata orientation, not a
+scientific replay. Live PRs, handoff claims, local reservations and main's
+formula/object terms were checked before claiming and are refreshed before
+publication. Cached search is a lead, not a novelty certificate; unpublished
+work and exhaustive older Discussion coverage remain outside that search.
+
+Credit JoyboyBrian #5507 for the larger-support boundary, the genuine triple
+exception and its global compensation; Ali Romman #5456 for the early-helper
+support model; and the retained #5452/#5388/#589/#555 BIT, native, owner and
+compiler lineage. Their results are cited at their stated scopes. No
+predecessor scientific replay or audit is the deliverable. The classical
+trace, primary decomposition, Jordan and triangular-splitting methods retain
+their mathematical attribution. No claim of general linear-algebra priority
+is made. Exact provenance hashes are in [SOURCES.json](SOURCES.json).
+
+## Limitations and unrun obligations
+
+Only characteristic two is covered. The binary census is complete only through
+dimension four; higher dimensions and other fields rely on the written proof.
+Local attaining matrices are not chronological native controllers. Higher-support
+global compensation, independent-symbol constraints, native chains, helper
+ownership, physical coefficient realization, dirty restoration, tape, precision,
+compiler and supplier/outer accounting remain unproved. No selected frontier
+record changes. Independent human and formal proof-kernel review are unclaimed.
+No Lean, Docker, heavy selected replay or predecessor replay is needed or run.
+Every registered check runs locally; hosted CI is reported separately in the PR.
+
+## Open next questions
+
+- Can a larger-support caller compensate the exact local surplus using its
+  native chain and ownership constraints? Start with one declared support size
+  and its chronological block decomposition. The missing completed word and
+  full target/paid invoice block a supplier claim.
+- With a fixed upper bound on native nilpotent chain length, what is the sharp
+  local envelope? Start at r=5,k=4 with chains of length at most four, which
+  the proved corank-one rigidity already excludes from attaining 10. This
+  package does not determine the next-best value or a global caller budget.
+
+Structured questions and their blockers are in [TASK.json](TASK.json).
+
+## Implementation bounds
+
+The new code is confined to verify.py, with no external runtime inputs or
+predecessor imports. All loops are bounded by r<=33, the binary r<=4 census,
+its at most 4! permutations, or the at most sixteen receipt files. Functions
+are below sixty physical lines. Admission uses explicit exceptions and remains
+active under optimization. Normal replay writes only stdout; optional external
+receipts use exclusive creation and scoped file closure.
+
+Power of Ten rules 3 and 9 have managed-runtime deviations. Python integers,
+tuples, lists and iterator objects allocate during computation; their capacities
+are bounded by the fixed dimensions, at most 65,536 entries per census array,
+and receipt files of at most 1 MiB each. Python's ordinary builtin iterator and
+argument-parser dispatch are retained; callable targets are explicit and no
+plugins or dynamic code are loaded. A fixed-memory native implementation would
+be needed to remove those deviations. Warning-strict normal and optimized
+execution, independent algebraic oracles and rejecting controls are the local
+verification. Repository-wide diagnostic configuration is unchanged by this
+isolated standard-library package.
diff --git a/research/shared-block-spectral-envelope/SOURCES.json b/research/shared-block-spectral-envelope/SOURCES.json
new file mode 100644
index 0000000000..95044543ed
--- /dev/null
+++ b/research/shared-block-spectral-envelope/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-multigraph-funding-obstruction/README.md",
+      "usage": "provenance",
+      "git_blob": "74f548eca31f49e34b6a678dc9c650ce857dae59",
+      "sha256": "7f7d266deac4153277279fd7bd5631e078d3d0b2970389e3ff61406ec6f25b6c"
+    },
+    {
+      "path": "research/bit-multigraph-funding-obstruction/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "f594891f3fb1c219905e0184df80d81eea916aaf",
+      "sha256": "8f7ce9d378299e4dccc94a3232b623149b5876a4bb9472bdeb6e7095ad6de580"
+    }
+  ]
+}
diff --git a/research/shared-block-spectral-envelope/TASK.json b/research/shared-block-spectral-envelope/TASK.json
new file mode 100644
index 0000000000..5597e54316
--- /dev/null
+++ b/research/shared-block-spectral-envelope/TASK.json
@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "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",
+      "research/g20-helper-split/README.md",
+      "research/g20-conjugation-admission/README.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 full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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",
+        "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": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.",
+    "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": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "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": "changed",
+  "actual_scope": "Sharp all-dimension characteristic-two spectral envelope for A+B=D with D idempotent, explicit attaining binary pairs, and forced full-length nilpotent chains for corank-one even-rank extremizers.",
+  "scope_change_reason": "The current G20 card changes to a local algebraic side result at the larger-support boundary named by JoyboyBrian PR5507. No new word or complete paid invoice is claimed.",
+  "bottleneck_link": "The exact surplus over 2r-k and its forced chain length constrain attempts to extend the early-helper global funding argument to larger supports.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified spectral envelope; do not extend it into controller searches or assert a global funding theorem.",
+  "outcome": "completed",
+  "evidence": "PROOF.md carries the universal proof; verify.py constructs 594 witnesses, exhausts 329780 binary pairs and uses 66066 independent characteristic-polynomial comparisons plus ten rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a larger-support caller compensate the exact local spectral surplus?",
+      "why_it_matters": "Only a source-bound global argument can establish a new complete funding obstruction or construction.",
+      "first_step": "Choose one larger support size and derive the exact chronological blocks and native-chain ledger.",
+      "blocked_by": "No completed changed word, ownership proof or full target/paid invoice is supplied."
+    },
+    {
+      "question": "What is the sharp spectral envelope under a specified bound on native nilpotent chain length?",
+      "why_it_matters": "The unrestricted local maximum can require chains longer than a proposed native call supports.",
+      "first_step": "At r=5,k=4 impose nilpotency indices at most four; the proved rigidity excludes the maximum ten.",
+      "blocked_by": "The next-best constrained value and its global caller consequences are not determined."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217878",
+  "predecessor": {
+    "pr": 5507,
+    "author": "JoyboyBrian",
+    "head": "1691a6024b60bdf28d7a2eed13cb32d78e2ea5b4"
+  }
+}
diff --git a/research/shared-block-spectral-envelope/VERIFY.json b/research/shared-block-spectral-envelope/VERIFY.json
new file mode 100644
index 0000000000..984d4bd24a
--- /dev/null
+++ b/research/shared-block-spectral-envelope/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete binary census, independent characteristic-polynomial oracle, all-size construction samples and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same complete checks with optimization and explicit admission checks active."
+    }
+  ]
+}
diff --git a/research/shared-block-spectral-envelope/verify.py b/research/shared-block-spectral-envelope/verify.py
new file mode 100644
index 0000000000..c2e311222e
--- /dev/null
+++ b/research/shared-block-spectral-envelope/verify.py
@@ -0,0 +1,265 @@
+#!/usr/bin/env python3
+"""Exact corroboration of the written shared-block spectral theorem."""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import itertools
+import json
+from pathlib import Path
+
+MAX_DIMENSION = 33
+CENSUS_DIMENSION = 4
+
+
+def need(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def domain(r: int, k: int) -> None:
+    need(type(r) is int and type(k) is int, "dimensions must be integers")
+    need(1 <= r <= MAX_DIMENSION and 0 <= k <= r, "dimension outside replay domain")
+
+
+def envelope(r: int, k: int) -> int:
+    domain(r, k)
+    if k == r:
+        return r
+    return 2 * r - (k % 2)
+
+
+def identity(r: int) -> tuple[int, ...]:
+    return tuple(1 << i for i in range(r))
+
+
+def diagonal(r: int, k: int) -> tuple[int, ...]:
+    return tuple((1 << i) if i < k else 0 for i in range(r))
+
+
+def add(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]:
+    need(len(a) == len(b), "matrix shape mismatch")
+    return tuple(x ^ y for x, y in zip(a, b))
+
+
+def multiply(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]:
+    n = len(a)
+    need(len(b) == n, "matrix shape mismatch")
+    rows = [0] * n
+    for i in range(n):
+        for j in range(n):
+            if (a[i] >> j) & 1:
+                rows[i] ^= b[j]
+    return tuple(rows)
+
+
+def power(a: tuple[int, ...], exponent: int) -> tuple[int, ...]:
+    need(0 <= exponent <= MAX_DIMENSION, "power outside replay domain")
+    result = identity(len(a))
+    base = a
+    for bit in range(exponent.bit_length()):
+        if (exponent >> bit) & 1:
+            result = multiply(result, base)
+        base = multiply(base, base)
+    return result
+
+
+def rank(a: tuple[int, ...]) -> int:
+    n = len(a)
+    rows = list(a)
+    pivot = 0
+    for col in range(n):
+        chosen = next((i for i in range(pivot, n) if (rows[i] >> col) & 1), None)
+        if chosen is None:
+            continue
+        rows[pivot], rows[chosen] = rows[chosen], rows[pivot]
+        for i in range(pivot + 1, n):
+            if (rows[i] >> col) & 1:
+                rows[i] ^= rows[pivot]
+        pivot += 1
+    return pivot
+
+
+def inverse(a: tuple[int, ...]) -> tuple[int, ...]:
+    n = len(a)
+    rows = [a[i] | (1 << (n + i)) for i in range(n)]
+    for col in range(n):
+        chosen = next((i for i in range(col, n) if (rows[i] >> col) & 1), None)
+        need(chosen is not None, "singular basis")
+        rows[col], rows[chosen] = rows[chosen], rows[col]
+        for i in range(n):
+            if i != col and (rows[i] >> col) & 1:
+                rows[i] ^= rows[col]
+    return tuple(row >> n for row in rows)
+
+
+def zero_multiplicity(a: tuple[int, ...]) -> int:
+    return len(a) - rank(power(a, len(a)))
+
+
+def characteristic(a: tuple[int, ...]) -> int:
+    """Leibniz determinant in F2[t], independent of elimination/powers."""
+    n = len(a)
+    need(n <= CENSUS_DIMENSION, "characteristic oracle exceeds its bound")
+    result = 0
+    for perm in itertools.permutations(range(n)):
+        term = 1
+        for i, j in enumerate(perm):
+            coefficient = (a[i] >> j) & 1
+            if i == j:
+                term = (term << 1) ^ (term if coefficient else 0)
+            elif coefficient == 0:
+                term = 0
+        result ^= term
+    need(result.bit_length() == n + 1, "characteristic polynomial must be monic")
+    return result
+
+
+def polynomial_order(polynomial: int) -> int:
+    need(polynomial > 0, "zero polynomial has no finite order")
+    return (polynomial & -polynomial).bit_length() - 1
+
+
+def even_core(k: int) -> tuple[tuple[int, ...], tuple[int, ...]]:
+    """Conjugate the strict triangular halves of I+J_(k+1)."""
+    need(k >= 0 and k % 2 == 0 and k + 1 <= MAX_DIMENSION, "bad even core")
+    n = k + 1
+    upper = tuple(sum(1 << j for j in range(i + 1, n)) for i in range(n))
+    lower = tuple((1 << i) - 1 for i in range(n))
+    # Columns are e_i+e_(n-1), followed by the all-ones kernel vector.
+    basis = tuple(((1 << i) if i < k else (1 << k) - 1) | (1 << k)
+                  for i in range(n))
+    back = inverse(basis)
+    a = multiply(multiply(back, upper), basis)
+    b = multiply(multiply(back, lower), basis)
+    need(add(a, b) == diagonal(n, k), "core does not have the coordinate endpoint")
+    return a, b
+
+
+def witness(r: int, k: int) -> tuple[tuple[int, ...], tuple[int, ...]]:
+    domain(r, k)
+    if k == r:
+        return (0,) * r, identity(r)
+    if k % 2 == 0:
+        a, b = even_core(k)
+        return a + (0,) * (r - len(a)), b + (0,) * (r - len(b))
+    # Put one eigenvalue-one block next to a rank-(k-1) even core.
+    a, b = even_core(k - 1)
+    a = a + (0,) * (r - len(a))
+    b = b + (0,) * (r - len(b))
+    # The core's zero coordinate is k-1; place the one block at k,
+    # then swap those two coordinates to obtain diag(I_k,0).
+    b = tuple(row ^ ((1 << k) if i == k else 0) for i, row in enumerate(b))
+    swap = list(identity(r))
+    swap[k - 1], swap[k] = swap[k], swap[k - 1]
+    return multiply(multiply(tuple(swap), a), tuple(swap)), \
+        multiply(multiply(tuple(swap), b), tuple(swap))
+
+
+def check_witness(r: int, k: int, a: tuple[int, ...], b: tuple[int, ...]) -> None:
+    domain(r, k)
+    need(len(a) == r and len(b) == r, "witness size mismatch")
+    need(all(type(row) is int and 0 <= row < (1 << r) for row in a + b),
+         "invalid binary row")
+    need(add(a, b) == diagonal(r, k), "wrong endpoint")
+    need(zero_multiplicity(a) + zero_multiplicity(b) == envelope(r, k),
+         "witness misses sharp envelope")
+    if k == r - 1 and k > 0 and k % 2 == 0:
+        for matrix in (a, b):
+            need(rank(matrix) == r - 1, "corank-one extremizer has extra Jordan blocks")
+            need(power(matrix, r) == (0,) * r, "extremizer not nilpotent")
+            need(power(matrix, r - 1) != (0,) * r, "nilpotent chain is too short")
+
+
+def census() -> list[dict[str, object]]:
+    summaries = []
+    for r in range(1, CENSUS_DIMENSION + 1):
+        size = 1 << (r * r)
+        mask = (1 << r) - 1
+        z_values = [0] * size
+        for code in range(size):
+            a = tuple((code >> (i * r)) & mask for i in range(r))
+            z_values[code] = zero_multiplicity(a)
+            need(z_values[code] == polynomial_order(characteristic(a)),
+                 "power and characteristic oracles disagree")
+        for k in range(r + 1):
+            d_code = sum(1 << (i * r + i) for i in range(k))
+            scores = [z_values[code] + z_values[code ^ d_code] for code in range(size)]
+            maximum = max(scores)
+            need(maximum == envelope(r, k), "complete census disagrees with theorem")
+            # Check the forced regular chains for every binary corank-one maximizer.
+            if k == r - 1 and k > 0 and k % 2 == 0:
+                for code in range(size):
+                    if scores[code] == maximum:
+                        a = tuple((code >> (i * r)) & mask for i in range(r))
+                        b = tuple((code ^ d_code) >> (i * r) & mask for i in range(r))
+                        check_witness(r, k, a, b)
+            summaries.append({"r": r, "k": k, "matrices": size,
+                              "maximum": maximum, "maximizers": scores.count(maximum)})
+    return summaries
+
+
+def rejection_controls() -> int:
+    bad = [(0, 0), (34, 0), (3, -1), (3, 4), (True, 1), (3, False)]
+    count = 0
+    for r, k in bad:
+        try:
+            envelope(r, k)
+        except ValueError:
+            count += 1
+    need(count == len(bad), "invalid domain accepted")
+    a, b = witness(5, 4)
+    mutants = [((a[0] ^ 1,) + a[1:], b), ((0,) * 5, diagonal(5, 4)),
+               (a[:-1], b), (a, (True,) + b[1:])]
+    for x, y in mutants:
+        try:
+            check_witness(5, 4, x, y)
+        except ValueError:
+            count += 1
+    need(count == len(bad) + len(mutants), "bad witness accepted")
+    return count
+
+
+def report() -> dict[str, object]:
+    constructed = 0
+    for r in range(1, MAX_DIMENSION + 1):
+        for k in range(r + 1):
+            check_witness(r, k, *witness(r, k))
+            constructed += 1
+    rows = census()
+    a, b = witness(5, 4)
+    return {"status": "PASS_SHARED_BLOCK_SPECTRAL_ENVELOPE",
+            "claim_type": "scoped algebraic proof with finite corroboration",
+            "constructed_cases": constructed,
+            "complete_binary_matrix_pairs": sum(row["matrices"] for row in rows),
+            "independent_characteristic_checks": sum(1 << (r * r) for r in range(1, 5)),
+            "rejection_controls": rejection_controls(),
+            "five_coordinate_witness_rows": {"A": a, "B": b},
+            "census": rows}
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--receipt", type=Path, help="write a new external hash-bound receipt")
+    args = parser.parse_args()
+    if args.receipt is not None:
+        need(not args.receipt.exists(), "receipt already exists")
+        need(Path(__file__).resolve().parent not in args.receipt.resolve().parents,
+             "receipt must be outside the package")
+    result = report()
+    if args.receipt is not None:
+        package = Path(__file__).resolve().parent
+        files = sorted(path for path in package.iterdir() if path.is_file())
+        need(len(files) <= 16, "package inventory exceeds receipt bound")
+        need(all(path.stat().st_size <= 1024 * 1024 for path in files),
+             "package file exceeds receipt byte bound")
+        hashes = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() for path in files}
+        payload = {"result": result, "package_sha256": hashes}
+        with args.receipt.open("x", encoding="utf-8") as stream:
+            stream.write(json.dumps(payload, indent=2, sort_keys=True) + "\n")
+    print(json.dumps(result, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()