Mister-Meeseeks · Oct 28, 2026 · Oct 27, 2026
diff --git a/research/four-subset-side-spectrum/PROOF.md b/research/four-subset-side-spectrum/PROOF.md
@@ -0,0 +1,142 @@
+# Exact spectrum and full side rank for the four-subset decoder
+
+This is a scoped proof over Q, also valid over every characteristic-zero
+field. It takes the definition of K from Cinna Davis's
+[PR #2225](https://github.com/CrocSwap/integer-mult-bounds/pull/2225).
+The predecessor's fitting, dyadic-coefficient and physical-support claims
+are cited background. They are not reverified here.
+
+Let n >= 5 be odd, let V be the set of four-subsets of [n], and put
+
+    K(S,T) = binomial(|S intersection T|/2, 2).
+
+The new conclusion is that I-K is invertible for every such n. Thus the
+exact side response cannot factor through fewer than binomial(n,4) scalar
+linear intermediates. This only excludes a factorization with no direct
+source-to-output bypass. It is not a lower bound on arbitrary side circuits,
+their work, native calls, or their paid rank profile.
+
+## 1. Incidence decomposition
+
+For j=1,2 let W_j have rows indexed by four-subsets and columns by
+j-subsets, with entry one for containment and zero otherwise. Since
+
+    binomial(t/2,2) = (1/4) binomial(t,2) - (1/8) binomial(t,1),
+
+the definition gives
+
+    8K = 2 W_2 W_2^T - W_1 W_1^T.                         (1)
+
+Let B be the n-by-binomial(n,2) vertex/pair incidence matrix. Directly
+counting four-subsets containing a prescribed union gives
+
+    W_2^T W_2 = a I + (n-4) B^T B + J,
+    a = (n-4)(n-5)/2,                                   (2)
+    B B^T = (n-2) I + J,
+    W_2 B^T = 3 W_1.                                    (3)
+
+Here each J is the all-ones matrix of its displayed size. For (2), the
+three entries, according to pair intersection size 2,1,0, are
+binomial(n-2,2), n-3, 1. This proves (2) without invoking a spectrum theorem.
+
+Assume n >= 7. Pair-coordinate space is the orthogonal direct sum
+
+    E0 = constants,                       dimension 1,
+    E1 = B^T {u : sum(u)=0},              dimension n-1,
+    E2 = ker B,                          dimension binomial(n,2)-n.
+
+The formula for B B^T shows that B has row rank n. The three eigenvalues
+of W_2^T W_2 in (2) are respectively
+
+    6 binomial(n-2,2), 3 binomial(n-3,2), binomial(n-4,2).
+
+They are positive for n >= 7. Hence W_2 has full column rank and maps
+these subspaces injectively into port space. The orthogonal complement
+of its image has dimension binomial(n,4)-binomial(n,2).
+
+On W_2 E0 the eigenvalue of W_1 W_1^T is 4 binomial(n-1,3), by its
+constant row sum. On W_2 E2 it is zero, by (3). To check the remaining
+space directly, counting vertex/pair incidences gives
+
+    W_1^T W_2 = binomial(n-3,2) B + (n-3) J.
+
+For sum(u)=0 use B B^T u=(n-2)u and W_1 u=W_2 B^T u/3.
+It follows that W_1 W_1^T acts on W_2 E1 with eigenvalue
+binomial(n-2,3). Both terms of (1) vanish on the remaining port space.
+
+## 2. The spectrum
+
+Substitution into (1) gives the following eigenvalues of K, with their
+multiplicities. Coincident eigenvalues have additive multiplicities.
+
+| Eigenvalue | Multiplicity |
+| --- | ---: |
+| (n-2)(n-3)(10-n)/12 | 1 |
+| (n-3)(n-4)(20-n)/48 | n-1 |
+| (n-4)(n-5)/8 | binomial(n,2)-n |
+| 0 | binomial(n,4)-binomial(n,2) |
+
+For odd n >= 7 the first three are nonzero, so rank(K)=binomial(n,2).
+This rank statement concerns rational linear intermediates; it supplies
+no implementation of a smaller dyadic feature basis.
+
+For n=5, distinct four-subsets intersect in three points. Thus
+K=(5/8)I+(3/8)J. Its eigenvalues are 5/2 once and 5/8 four times.
+Its rank is five. The n>=7 incidence multiplicities do not apply here.
+
+## 3. No eigenvalue is one
+
+For the first eigenvalue, n=7 and n=9 give 5 and 7/2; every odd n>=11
+gives a negative value. For the second, each odd n in [7,15] has numerator
+at least 4*3*5=60>48. At n=17 and n=19 its numerators are 546 and 240.
+Every odd n>=21 gives a negative value. For the third, n=7 gives 3/4;
+every odd n>=9 gives at least 5/2. The zero eigenvalue and the two n=5
+eigenvalues also differ from one.
+
+Therefore I-K is invertible for every allowed n. For the first requested
+side-map instance n=9, the exact spectra are
+
+    K:     (7/2)^1, (55/8)^8, (5/2)^27, 0^90;
+    I-K:   (-5/2)^1, (-47/8)^8, (-3/2)^27, 1^90.
+
+In particular, rank(K)=36 and rank(I-K)=126, and
+
+    det(I-K) = 5 * 3^27 * 47^8 / 2^52.
+
+The source incidence expansion has 45 features. Its feature count is not
+asserted to be its rational rank.
+
+## 4. The exact compression obstruction
+
+If all source dependence reaches the output through h scalar linear
+intermediates, the side map has a factorization I-K=D A, with A having h
+rows and D having h columns. Therefore
+
+    binomial(n,4) = rank(I-K) <= h.
+
+This bound is sharp in that declared algebraic model: A=I and D=I-K use
+exactly binomial(n,4) intermediates. No physical cost is assigned to this
+attaining factorization. A direct identity contribution and a separate
+compressed -K correction fall outside the no-bypass hypothesis and remain
+available to a future side circuit. Dirty helpers, restoration, actual
+frames, chronology, native orientation and a complete invoice still need
+separate constructions and proofs.
+
+## 5. Evidence and scope
+
+The standalone verifier builds the complete integer matrix 8K directly
+from intersections at n=5,7,9. Fraction-free elimination checks every
+predicted eigenspace dimension and the full determinant of 8K-8I. It also
+counts literal pair-incidence Gram entries at n=7,9 and checks the scalar
+formulas on a bounded larger domain. The proof above, not that finite
+domain, supplies the every-n quantifier. Mutations and an actual rank-four
+compression control test the new conclusions. Nothing imports or replays
+the predecessor's verifier. The output receipt is generated from results
+and package hashes; no receipt is handwritten.
+
+The new result was produced by Nick Petalas. The kernel definition,
+decoder motivation and open side-map obligation are by Cinna Davis, with
+the subset/compiler ancestry retained in PR #2225. Incidence decompositions
+and the rank inequality for a product are classical. No new general
+spectral method, supplier, kappa, selected-frontier update, formal-kernel
+acceptance or independent human review is claimed.
diff --git a/research/four-subset-side-spectrum/README.md b/research/four-subset-side-spectrum/README.md
@@ -0,0 +1,100 @@
+# Full side rank for the four-subset decoder
+
+For every odd n >= 5, the complementary four-subset kernel
+K(S,T)=binomial(|S intersection T|/2,2) has invertible side map I-K over Q.
+At n=9 its ranks are rank(K)=36 and rank(I-K)=126. The
+[proof](PROOF.md) gives the complete spectrum for every n and a sharp
+algebraic consequence: implementing the whole side response through scalar
+linear intermediates, with no direct source-to-output bypass, needs at least
+binomial(n,4) intermediates. This is a scoped proof, not a physical tariff or
+a new kappa.
+
+This takes a partial step on Cinna Davis / 1337isnot1337's
+[PR #2225](https://github.com/CrocSwap/integer-mult-bounds/pull/2225), which
+leaves the side map open. It derives a new side-map obstruction from that
+kernel's definition. It does not audit the predecessor's fitting theorem,
+feature supports or numbers. A direct identity contribution plus a compressed
+-K correction remains outside this obstruction and may still help a circuit.
+
+Ali Romman's merged [PR #5458](https://github.com/CrocSwap/integer-mult-bounds/pull/5458)
+studies the cube restriction of the same kernel and separate binary endpoint
+hulls. Here the port set is the entire constant-weight shell, with 126 ports
+at n=9, and the conclusion is its full side-map spectrum. Full-rank
+compensation in other geometries is also prior work, including Dominik
+Scholz's [PR #606](https://github.com/CrocSwap/integer-mult-bounds/pull/606)
+on E8 squared. This package claims the four-subset result, not the general
+idea of a compensation-rank obstruction.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/four-subset-side-spectrum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/four-subset-side-spectrum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/four-subset-side-spectrum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/four-subset-side-spectrum --check-source-history
+```
+
+Another CPython 3.12 path can be substituted. The direct success marker is
+`PASS_FOUR_SUBSET_SIDE_SPECTRUM`. The registered launcher must print
+`PASS_REGISTERED_RESEARCH_PACKAGE`; the publication check must print
+`PASS_RESEARCH_COMMIT_BYTES`.
+
+The read-only verifier reconstructs all 17,126 matrix entries at n=5,7,9
+directly from intersections. Exact fraction-free elimination checks all ten
+eigenspace dimensions, the three full side ranks and their complete
+determinants. Literal incidence counting checks 1,737 pair-Gram entries.
+The bounded formula check covers 499 odd n through 1001; it is not the proof
+of the unbounded statement. Three malformed spectra are rejected, and an
+actual smaller compression has the expected deficient rank. A generated
+stdout receipt records results, interpreter version and all six package-file
+hashes. No receipt or replay output is written into the checkout.
+
+## Scope and implementation limits
+
+The result is over characteristic zero. It covers k=4, not every even k.
+It proves no bound on circuits with retained source access, general dirty
+workspace, native queries or paid recursive work. The rank-36 kernel at n=9
+does not supply a 36-feature dyadic circuit. Its predecessor's 45-feature
+incidence expansion remains credited and unchanged. Physical side construction,
+restoration, both native orientations, hosting, precision and the complete
+supplier invoice remain open. The selected frontier and its five framework
+assumptions are unchanged. No selected cold replay, Lean, Docker, independent
+human review or formal proof-kernel review is claimed.
+
+The verifier uses no external runtime inputs. `SOURCES.json` pins the source
+definition and task/selected-record provenance through ancestor Git blobs.
+The bounded checker uses dynamic Python allocation, a managed-runtime
+deviation from Power of Ten's fixed-allocation rule. Its largest dense matrix
+is 126 by 126, its incidence list has 36 pairs, and every loop has a finite
+bound from the explicit replay domain. Elimination checks every exact division;
+exceptions propagate. Warning-strict normal and optimized execution retain
+all acceptance checks. There is no recursive or generated executable code.
+
+## Open next questions
+
+- Can a legal direct identity route plus a compressed -K correction implement
+  the n=9 side map cheaply? Begin with explicit input/output frames and charge
+  arbitrary dirty restoration. This theorem does not exclude that route.
+- For another even k, when is one an eigenvalue of the complementary-subset
+  kernel? Derive its incidence action before inferring any physical invoice.
+
+## Credit and coordination
+
+This contribution was produced by Nick Petalas. Cinna Davis supplies the
+kernel definition, dyadic fitting construction, support theorem and open
+side-map question in PR #2225. The source retains the Zhihao Chen subset and
+compiler ancestry. Incidence decomposition and rank bounds for products are
+classical; the contribution is this exact spectrum and its scoped side-map
+consequence.
+
+Base: `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228386)
+records the scope. The initial P104-oriented selection changed to this
+specific decoder-side obligation. Main, merged PRs, open PRs, this account's
+recent contributions and active claims were searched. The cached open snapshot
+covered 393 PRs and complete Discussion pagination; sparse local note coverage
+was incomplete. The relevant source was materialized and main was searched
+through Git. No matching side-spectrum result was found in that coverage;
+unpublished work remains outside it.
diff --git a/research/four-subset-side-spectrum/SOURCES.json b/research/four-subset-side-spectrum/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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/even-subset-dyadic-kernels/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "5f760220be590e9b891e8867d5c366a601bc019d",
+      "sha256": "ddc0d91dff486a4593c6f200191f12774406ea84f52bde8bf75d1a473b5e6d52"
+    }
+  ]
+}
diff --git a/research/four-subset-side-spectrum/TASK.json b/research/four-subset-side-spectrum/TASK.json
@@ -0,0 +1,93 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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": "changed",
+  "actual_scope": "Prove the exact characteristic-zero spectrum of the complementary four-subset kernel and invertibility of I-K for every odd n>=5; derive its sharp no-bypass linear-intermediate floor.",
+  "scope_change_reason": "The initial P104-oriented selection encountered a distinct explicit side-map obligation in Cinna Davis PR2225. This is a scoped algebraic decoder-side result, not a priced supplier or a coframe search.",
+  "bottleneck_link": "PR2225 leaves I-K unimplemented. Its full rank rules out compressing the entire side response through fewer linear intermediates without a direct source bypass; it does not rule out a complete side circuit.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved and exactly checked side-map rank obstruction; do not extend to other k or synthesize a physical caller.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-n proof; verify.py checks complete n=5,7,9 eigenspaces and determinants plus literal incidence counts and controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a legal direct identity route and a compressed -K correction implement the n=9 side map cheaply?",
+      "why_it_matters": "That route escapes the no-bypass compression obstruction.",
+      "first_step": "Specify the physical entry/exit frames and emit one arbitrary-input side circuit with dirty restoration.",
+      "blocked_by": "No physical side word or complete invoice is supplied."
+    },
+    {
+      "question": "For other even k, when is one an eigenvalue of the complementary-subset kernel?",
+      "why_it_matters": "The side rank can then change.",
+      "first_step": "Derive the incidence action for one changed k.",
+      "blocked_by": "Only k=4 is proved here."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228386",
+    "source": "PR #2225",
+    "source_author": "1337isnot1337",
+    "open_pr_records": 393,
+    "discussion_records": 5631,
+    "local_note_records": 68,
+    "local_head_note_records": 8136,
+    "sparse_local_coverage_complete": false,
+    "playbook": "Autonomous local run",
+    "preserved_state": "Clean detached HEAD at 19fdb086ea96af9a9f87936a2b888e10af4ed810; no earlier branch name."
+  }
+}
diff --git a/research/four-subset-side-spectrum/VERIFY.json b/research/four-subset-side-spectrum/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": 60,
+      "checks": "Complete exact n=5,7,9 eigenspaces and side determinants; literal incidence Gram counts; finite scalar formula checks and four controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same complete check under optimized Python; explicit acceptance checks remain enabled."
+    }
+  ]
+}