Prove H6 commuting dyadic repairs need rank 816 (no new κ)

research/h6-commuting-repair/PROOF.md

@@ -0,0 +1,133 @@
+# Commuting dyadic repairs of the H6 complement
+
+This scoped proof was produced by Nick Petalas. Its H6 spectral premises
+and the unrestricted rank-560 comparison are cited from Ross Richardson's
+[PR3655](https://github.com/CrocSwap/integer-mult-bounds/pull/3655),
+head `7bf23e128e58a33c019268f57129629f603547f7`. They are not audited here.
+
+## Statement and inherited premises
+
+Put D=Z[1/2]. Let K be the symmetric dyadic H6 matrix on N=30960 ports
+from the cited source, and put C=I-K. Its cited characteristic polynomial is
+
+```text
+char_K(x) = x^30144 (x-39)^224 (x-45)^560
+            (x^2+186x-6075)^16.
+```
+
+For every B in M_N(D) satisfying BK=KB and C+B in GL_N(D),
+
+```text
+ker_Q B is contained in ker_Q K,
+rank_Q B >= 816.
+```
+
+The minimum is exactly 816. B=K attains it because C+B=I and the cited
+symmetry and characteristic polynomial give rank K=816. In particular,
+every polynomial correction B=f(K) with dyadic coefficients obeys this
+lower bound. The attaining correction cancels the kernel response. It
+does not supply an encoder or a useful physical source operation.
+
+The cited unrestricted minimum is 560. Consequently every rank-560 dyadic
+repair must fail to commute with K. The new cost of this commutation
+restriction is exactly 256 rational rank units. These units are correction
+matrix ranks, not Gaussian child ranks or paid native calls.
+
+## An invariant-kernel lemma
+
+Let C,B be finite square matrices over D with BC=CB and R=C+B in GL(D).
+Let M=ker_D B. This submodule is saturated: if nonzero d in D and dx is
+in M, then dBx=0 in a torsion-free module, so Bx=0. Because D is a PID,
+M is free and is a direct summand of D^N. Its rank is dim_Q ker_Q B.
+This also follows by clearing a denominator from any rational kernel
+vector to obtain a vector in M.
+
+B commutes with R. It therefore commutes with R inverse, which has dyadic
+entries. Both R and R inverse preserve M, so R restricts to a dyadic
+automorphism of M. On M, R=C. It follows that C restricted to M is an
+automorphism, and its determinant is a unit of D.
+
+In a D basis extending a basis of M, C is block upper triangular. Thus
+the characteristic polynomial of C restricted to M is a monic divisor
+of char_C in D[z]. Its constant coefficient is a dyadic unit. This is the
+obstruction: an invariant kernel of a commuting correction cannot retain
+a characteristic factor with a nonunit constant coefficient.
+
+The argument holds for every finite N. It permits arbitrary mixing inside
+repeated eigenspaces. It does not assume that B is symmetric, diagonal,
+normal, diagonalizable, or a polynomial in C.
+
+## Apply the lemma to H6
+
+Substitution z=1-x gives the cited C characteristic factors
+
+```text
+char_C(z) = (z-1)^30144 (z+38)^224 (z+44)^560
+            (z^2-188z-5888)^16.
+```
+
+The quadratic is irreducible over Q. Its discriminant is
+58896=144*409, and 20^2<409<21^2. Unique factorization in Q[z] implies
+that the characteristic polynomial of C restricted to M has the form
+
+```text
+(z-1)^a (z+38)^b (z+44)^c (z^2-188z-5888)^d,
+0<=a<=30144, 0<=b<=224, 0<=c<=560, 0<=d<=16.
+```
+
+Its determinant, up to sign, has absolute factors
+
+```text
+38^b 44^c 5888^d,
+38=2*19, 44=4*11, 5888=256*23.
+```
+
+The 19-, 11- and 23-adic valuations are respectively b,c,d. A dyadic
+unit has all three valuations zero, so b=c=d=0. Thus dim_Q ker B=a<=30144
+and rank B>=30960-30144=816.
+
+Furthermore C is diagonalizable over the reals because K is symmetric.
+Its restriction to an invariant subspace has the same property. The only
+remaining eigenvalue on M is 1, so C acts as the identity on M and K acts
+as zero. This gives the stronger kernel containment in the statement.
+
+Together with B=K, this proves the exact minimum. No H6 matrix entries,
+Smith factors, predecessor counts or source programs need to be replayed
+to deduce this new consequence of the cited characteristic polynomial.
+
+## The hypotheses matter
+
+For C=diag(3,5), the dyadic correction
+
+```text
+B = [[2,4],[-4,-8]],  rank B=1,
+C+B = [[5,4],[-4,-3]],  det(C+B)=1
+```
+
+does not commute with C. Every commuting dyadic repair of this C has
+rank two, by the lemma. Thus an unrestricted low-rank repair can genuinely
+escape the conclusion. This example is a control for the new hypothesis,
+not a replacement for the H6 predecessor's rank-560 certificate.
+
+The ring hypothesis also matters. The commuting rational correction
+B=diag(-14/5,0) has rank one and det(C+B)=1, but C+B=diag(1/5,5) is not a
+matrix over D. Rational invertibility, or a determinant-one condition
+without the dyadic entry condition, does not establish a dyadic automorphism.
+
+Extra directions change the contract. For the one-dimensional C=[3],
+the two-dimensional matrix [[3,1],[-1,0]] is unimodular. The theorem fixes
+the original dimension and endpoint and makes no claim about such stable
+extensions or their dirty-helper restoration.
+
+## Verification boundary
+
+The standalone checker enumerates an explicitly bounded two-dimensional
+matrix domain and checks new abstract attaining endpoints under dyadic
+conjugation. It also checks the stated characteristic-factor application,
+its irreducibility condition, altered factor certificates and essential
+hypotheses. Its output counts every domain actually executed.
+
+The finite checks corroborate the invariant-kernel proof. They do not
+establish the H6 spectrum, reconstruct its 30960-square matrix, audit the
+rank-560 completion, synthesize a paid circuit or prove a multiplication
+theorem. Independent human and formal proof-kernel review are unclaimed.

research/h6-commuting-repair/README.md

@@ -0,0 +1,113 @@
+# H6 commuting dyadic repairs need rank 816
+
+For the H6 kernel K and its complement C=I-K, every dyadic correction B
+with BK=KB and C+B invertible over Z[1/2] has rational rank at least
+**816**. This is sharp: B=K makes the endpoint the identity. The stronger
+conclusion is ker B contained in ker K. Polynomial corrections are included.
+
+Ross Richardson's [PR3655](https://github.com/CrocSwap/integer-mult-bounds/pull/3655)
+gives the unrestricted rank-560 dyadic completion. That result and the H6
+spectrum are cited premises, not fresh audits. The new obstruction shows
+that any rank-560 completion must break commutation with K. Restricting
+to commuting corrections costs exactly 256 additional correction rank units.
+Correction matrix rank is not a native Gaussian tariff.
+
+This is a scoped written proof with finite exact corroboration. It supplies
+no physical source word, paid supplier, new kappa or selected-frontier change.
+The rank-816 attainer cancels the useful kernel response and is only an
+algebraic witness to sharpness.
+
+## Why the restriction matters
+
+A commuting correction has an invariant kernel. If C+B is a dyadic
+automorphism, then its restriction to that kernel is C and must also be a
+dyadic automorphism. The nonidentity H6 characteristic factors have odd
+nonunit constant terms. None can remain on that kernel. The cited spectrum
+therefore forces all 816 responsive dimensions to be changed.
+
+[PROOF.md](PROOF.md) gives the all-dimensional invariant-kernel argument and
+the H6 application. It permits arbitrary mixing inside repeated eigenspaces
+and does not assume B is symmetric or diagonalizable. A literal two-by-two
+noncommuting correction demonstrates that the commutation hypothesis is
+essential. Odd denominators and extra directions have separate controls.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/h6-commuting-repair/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/h6-commuting-repair/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/h6-commuting-repair
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/h6-commuting-repair --check-source-history
+```
+
+Another CPython 3.12 executable may replace the local path. The last command
+checks publication bytes after committing. Both registered scientific commands
+print `PASS_H6_COMMUTING_REPAIR rank=816 no_new_kappa`.
+
+The verifier enumerates all 390,625 ordered pairs of two-by-two integer
+matrices with entries in {-2,-1,0,1,2}. Exactly 12,465 pairs commute, and
+6,552 also have a dyadic-unit repaired determinant. Every one satisfies
+the invariant-kernel rank bound; 1,856 attain that bound. It checks 36
+literal dyadic conjugations of attaining abstract matrices, three altered
+factor certificates, four hypothesis controls and ten invalid certificates.
+These finite domains corroborate the proof; they do not establish the H6
+spectral premise by enumeration.
+
+The program needs no Git, network, predecessor executable or source import.
+It emits a generated receipt bound to all six package files and writes no
+files. SOURCES.json pins the historical source statements as provenance.
+The registered metadata check authenticates those pins separately.
+
+## Limits and execution bounds
+
+The same 30,960-dimensional endpoint and the dyadic coefficient ring are
+essential. Noncommuting corrections, rational coefficients with odd
+denominators and stable extensions are outside the theorem. The H6 spectrum,
+symmetry and unrestricted 560-row completion retain their cited status.
+No dense H6 reconstruction, predecessor replay, native circuit, complete
+cost/precision/tape/stock calculation or supplier admission is performed.
+Independent human and formal proof-kernel review are unclaimed.
+
+The checker has no recursion or shared mutable state. Its largest nested
+enumeration has exactly 625 squared iterations. Factor certificates have at
+most eight factors of degree at most two, multiplicity at most 40,000,
+128-bit coefficient numerators/denominators and total dimension at most
+100,000. Matrix helpers consume fixed four-entry internal tuples. Every
+function is shorter than 60 lines; exceptions preserve checks under -O.
+Registered invocations enable warnings as errors.
+
+Power-of-Ten rule 3 has a managed-runtime deviation. Python allocates its
+integers, fractions and collections during the bounded one-shot replay.
+The matrix box contains only 625 tuples, and the other finite domains and
+factor limits above bound live data. This is not a persistent service or
+a fixed-allocation native implementation. No metaprogramming, callback
+dispatch or mutable global registry is used.
+
+## Open next questions
+
+- Construct explicit noncommuting coefficients for the predecessor's named
+  560-row completion. Identify the spectral components they mix, then price
+  legal source frames, scalar work and dirt restoration. Those coefficients
+  and a physical word remain missing.
+- Consider an enlarged dirty-helper interface only after specifying all
+  arbitrary inputs, required outputs and its complete paid/target invoice.
+  A stable extension changes the theorem's endpoint and can leave helper
+  dirt or restoration costs unpaid.
+
+The structured questions and blockers are in [TASK.json](TASK.json).
+The original decoder card is explicitly changed to this algebraic side
+obstruction. Selected-baseline metadata orientation passes; it is not a
+scientific replay of the selected supplier.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Ross Richardson supplies
+PR3655's H6 dyadic repair and its retained spectral premises. Credit Dominik
+Scholz's PR606 geometry/factorization, DreamingOfClouds' H6/Walsh proposal
+and the retained PR1830 spectral, compensation and encoder lineage.
+Saturated kernels over a PID, characteristic polynomials and odd-prime
+valuations are classical. The new result is their invariant-kernel use to
+prove the exact commuting-repair obstruction for this fixed source.
+Apache-2.0.

research/h6-commuting-repair/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/h6-dyadic-source-repair/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c0afff43035b2ec4c8ac3e0991473da4d420419e",
+      "sha256": "c58fe24fcbe26a577cea4e418f62041c5ad0e3cf1e8d7e85b4654674963eff5c"
+    },
+    {
+      "path": "research/h6-dyadic-source-repair/README.md",
+      "usage": "provenance",
+      "git_blob": "f086ace2422585d1faa824652d936a5750e7179b",
+      "sha256": "a9b97857189465b716a7c6e46a0d3a2f266ce8f85edc70a7996fc965a791eb62"
+    }
+  ]
+}

research/h6-commuting-repair/TASK.json

@@ -0,0 +1,83 @@
+{
+  "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": "Exact minimum rank 816 of a commuting dyadic repair of the H6 complement, conditional on its cited spectrum; unrestricted rank 560 remains a cited predecessor result.",
+  "scope_change_reason": "A scoped decoder-side obstruction replaces the card construction search. The new restriction is commutation of the correction with the fixed H6 kernel, including polynomial corrections. This is not a new target in a predecessor call-count model.",
+  "bottleneck_link": "The H6 alternative decoder still needs a paid source completion. A rank-560 realization must mix different spectral components: every commuting repair has rank at least 816. Matrix rank is not a native tariff.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved and locally corroborated obstruction; package it without attempting a larger construction or a paid circuit.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the invariant-kernel lemma and exact H6 bound. verify.py corroborates it with bounded exact matrix domains, hypothesis controls and factor-certificate rejection.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the cited 560-row completion be synthesized by a noncommuting dyadic correction at legal H6 source frames?",
+      "why_it_matters": "The new obstruction rules out every commuting and polynomial correction at rank 560.",
+      "first_step": "Use the predecessor row-support certificate to produce explicit completion coefficients and identify which spectral components they mix.",
+      "blocked_by": "No coefficients, legal frame access, dirt restoration or paid physical word is supplied here."
+    },
+    {
+      "question": "Can a useful enlarged dirty-helper interface preserve a spectral implementation while beating its complete recursive bill?",
+      "why_it_matters": "Stable extensions are outside the fixed-dimensional obstruction, but helper dirt and restoration are additional obligations.",
+      "first_step": "Specify every arbitrary input and required output and give a complete channel, restoration and productive-target invoice before searching.",
+      "blocked_by": "A commuting map on an enlarged space is a different contract; neither native legality nor its complete cost is established."
+    }
+  ],
+  "claim_type": "scoped written proof with finite exact corroboration",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228563"
+}

research/h6-commuting-repair/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": "Finite exact commuting-pair domain, dyadic conjugates, new H6 factor consequence, hypothesis controls and invalid factor certificates."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same mathematical checks under optimized Python; no assertions may disappear."
+    }
+  ]
+}