Exclude 48 flagless span-six dirty-auxiliary pools (no new κ)

research/flagless-kernel-obstruction/PROOF.md

@@ -0,0 +1,131 @@
+# A coordinate-kernel obstruction for flagless span-six words
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Model and inherited premises
+
+Use the formal abelian model of unpaidmoon's PR4119, with four scalar
+roles, eight nonzero rank-one rational 3-by-3 frames A_j and binary
+rank-one idempotents N_j. A paid call is
+
+    D_N([A]) = I + ([A]-1) N.
+
+The endpoint is diag([C_0],...,[C_3]); three specified C_i are invertible.
+The fourth role is arbitrarily dirty and may have any diagonal monomial
+endpoint. Equality is in the full group algebra of the additive rational
+matrix group. No clean allocation or extra free address map is allowed.
+
+The rational frame span has dimension six. We take the following reductions
+from PR4119, sections 2, 3 and 5, as cited mathematical premises.
+
+1. Cube-relation rank at most one is already excluded.
+2. Otherwise the relation lattice has a saturated cube basis r,s, independent
+   modulo two. For fixed independent off-diagonal patterns B,C,
+   off(N_j) = (r_j mod 2)B + (s_j mod 2)C.
+3. If S indexes noncoordinate projectors and T the coordinate projectors,
+   r and s vanish on T. Thus all relations are on S, the generated group
+   splits as H_S direct-sum Z^T, and dim_Q span{A_j:j in S}=|S|-2.
+
+We also cite waynenilsen's PR1882 theorem: two invertible rational 3-by-3
+data targets need at least six calls, with any finite dirty auxiliary
+workspace and arbitrary diagonal monomial auxiliary endpoints. It imposes
+no lower-triangularity requirement on the two data targets. The present
+proof does not replay or independently establish that theorem.
+
+## New obstruction
+
+Suppose the occurring noncoordinate pool has a nonzero common right-kernel
+vector v and a nonzero common left-kernel vector w. Put
+
+    U = supp(v) union supp(w).
+
+If |U|>=2, no such eight-call endpoint exists, provided |S|>=3.
+Only existence of these vectors is needed; their kernels need not be
+exactly one-dimensional. This hypothesis uses the original coordinates.
+
+First apply the group homomorphism setting every T generator to zero.
+Each coordinate factor becomes I. The surviving S word is still diagonal,
+with endpoint diag([C_i^S]); the decomposition gives
+C_i=C_i^S+C_i^T. Every S factor fixes v on the right and w^T on the left.
+Therefore the diagonal endpoint does too. In the full group algebra,
+
+    C_i^S = 0 for every i in U.                         (1)
+
+For example, if v_i=1, the i-th coordinate of Dv=v is [C_i^S]=1.
+Distinct rational matrices are distinct formal group elements, so C_i^S=0.
+The left-kernel argument is identical. Coordinate calls in the original
+word need not preserve either kernel. Removing them uses the group split,
+not an invariant-subspace claim about the interleaved full word.
+
+Let s=|S| and t=|T|, so s+t=8 and s>=3. Every C_i^S belongs to the
+frame span on S. A basis can be selected from its rank-one paid frames,
+so rank subadditivity gives
+
+    rank(C_i^S) <= s-2.                                (2)
+
+Let t_i count coordinate calls with projector E_ii. Project instead onto
+Z^T, setting every S generator to zero. The coordinate factors commute
+and each contributes to exactly one coordinate, hence
+
+    rank(C_i^T) <= t_i,    sum_i t_i=t.                 (3)
+
+At least one of the three data coordinates lies in U. If at least two do,
+(1) and invertibility force t>=6, contradicting s>=3. Thus exactly one data
+coordinate lies in U. Call it a. Equations (1) and (3) force t_a>=3.
+For the other two data coordinates, (2)-(3) give
+
+    3 <= (s-2)+t_i.
+
+Since t>=3, s<=5. Summing the last two inequalities and reserving the
+three calls at a gives
+
+    6 <= 2(s-2)+(t-3) = s+1.
+
+Consequently s=5, t=3, t_a=3, and neither other data coordinate has a
+T contribution. Both corresponding C_i^S are invertible. But the S word
+then realizes two invertible targets in five calls, with the other two
+arbitrarily dirty roles ending diagonally. This contradicts PR1882's
+six-call theorem. The obstruction follows.
+
+## Application to the exceptional pools
+
+PR4119 leaves 72 flagless noncoordinate pools with three projectors and
+two realized off-diagonal patterns. woklerx's earlier PR1846 already
+classifies these into coordinate-permutation/transpose orbits of sizes
+24 and 48. Those classification and orbit-size results retain their
+credit. The new contribution excludes the 48-pool orbit as a possible
+eight-call realization. The finite corroboration retains the original
+four coordinate axes throughout.
+
+The 48 newly excluded pools are exactly the disjoint coordinate-permutation
+orbits of the following triple and its transpose:
+
+    X = 1100/0000/0000/0000, packed 0x0003,
+    Y = 0100/0100/0000/0000, packed 0x0022,
+    Z = 0000/1011/1011/0000, packed 0x0dd0.
+
+Row strings list column 0 first; packed bit 4i+j is entry (i,j).
+For this triple v=e_2+e_3 and w=e_3. Thus |U|=2. Transpose exchanges
+the left and right kernels. Each coordinate-permutation orbit has 24
+pools, their intersection is empty, and every pool meets the obstruction.
+This is a finite certificate attached to the universal scoped argument.
+
+The remaining 24 pools form the coordinate-permutation orbit of
+(0x0003,0x0022,0x0550), the representative in PR4119. Their left and
+right kernels have the same single-coordinate support. The new hypothesis
+fails there. Their eight-call feasibility, and span five, remain open here.
+
+## Evidence boundary
+
+The executable checks the new coordinate orbits, kernel supports, formal
+kernel identities and all finite rank-budget allocations. Its formal-word
+checks use independent integer exponents, without reducing address frames
+modulo two. They corroborate the fixed-vector argument and do not enumerate
+rational frame relations or settle arbitrary endpoint feasibility.
+
+The universal exclusion depends on the cited relation-support reduction
+and two-target theorem. Their scientific suites are unrun. This result is
+neither independent acceptance of those premises nor a proof-kernel theorem.
+Native legality, frames, physical costs, precision/tape, stock, compiler,
+recursive supplier admission and the full multiplication theorem are outside
+scope. No new kappa or selected-frontier change follows.

research/flagless-kernel-obstruction/README.md

@@ -0,0 +1,121 @@
+# Excluding 48 flagless span-six dirty-auxiliary pools
+
+Scoped mathematical proof with finite exact corroboration. This contribution
+was produced by Nick Petalas. No new kappa or selected-frontier change.
+
+In the four-register abelian bit model, eight nonzero rank-one calls at
+rational frame span six cannot realize three invertible 3-by-3 targets when
+their noncoordinate projectors belong to any of 48 specified flagless pools.
+The fourth role is arbitrarily dirty and may end at any diagonal monomial.
+These are 48 of the 72 exceptional pools left by unpaidmoon's
+[PR4119](https://github.com/CrocSwap/integer-mult-bounds/pull/4119).
+The other 24 pools, and span five, remain open here.
+The scalar catalogue and its 24/48 orbit split were already established
+by woklerx's [PR1846](https://github.com/CrocSwap/integer-mult-bounds/pull/1846).
+The new result rules out realization of its 48-pool orbit.
+
+The new step keeps the target coordinate-diagonal. A common left or right
+kernel supported on two coordinates forces the noncoordinate subword to
+contribute zero on both. One invertible data target then consumes three
+coordinate calls. The resulting five-call subword would have to realize two
+invertible targets, contradicting waynenilsen's six-call theorem with dirty
+auxiliaries. [PROOF.md](PROOF.md) gives the quantified argument and names
+its inherited mathematical premises.
+
+The excluded pools are the disjoint coordinate-permutation orbits of
+`(0x0003,0x0022,0x0dd0)` and its transpose. Bit `4i+j` is entry `(i,j)`.
+The first pool has common right kernel `e_2+e_3` and common left kernel
+`e_3`. Each orbit contains 24 pools. The remaining orbit has representative
+`(0x0003,0x0022,0x0550)` and both kernels supported on the same coordinate.
+No arbitrary change of basis is used to preserve a coordinate target.
+
+## Evidence and reproduction
+
+Use CPython 3.12 and the standard library, from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/flagless-kernel-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/flagless-kernel-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/flagless-kernel-obstruction
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/flagless-kernel-obstruction --check-source-history
+```
+
+Any CPython 3.12 installation can replace the displayed interpreter.
+The direct checker emits `PASS_FLAGLESS_KERNEL_OBSTRUCTION` in a generated
+JSON receipt bound to the six package-file hashes. It writes only to stdout,
+imports no predecessor code, and works in a Git-free package export.
+Correctness checks use explicit exceptions and remain active under `-O`.
+
+The finite evidence includes the three disjoint coordinate orbits and their
+kernel supports, independent literal binary matrix products, 1,920 formal
+words through length three and 7,632 coefficient matrices, 3,888 diagonal
+label assignments, and 96 critical eight-call rank allocations. Every
+critical allocation has five noncoordinate calls and would require the
+cited two-target theorem's impossible endpoint. The nine-call budget
+control survives this relaxation; it is not a nine-call construction in
+the excluded pools. Named controls preserve the remaining coordinate-kernel
+orbit and distinguish coordinate interleaving from subword kernel invariance.
+
+The written proof supplies the universal rational-frame exclusion. The
+finite word checks corroborate its kernel identity, rather than enumerate
+all rational frame relations or certify every possible endpoint.
+
+## Scope and provenance
+
+Canonical base is `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority
+revision 7. The `bit-new-register-model` card is refined to this explicit
+four-register handoff. Its current source-binding orientation command,
+`scripts/research_selected_baseline.py`, passes. This authenticates selected
+metadata only; it is not a selected cold replay.
+
+[SOURCES.json](SOURCES.json) pins the predecessor statements, catalogue and
+selected record as historical provenance. No predecessor implementation or
+scientific receipt is imported. The relation-support reduction from PR4119
+and the two-target theorem from PR1882 remain cited proof dependencies.
+Their scientific suites were not replayed as this contribution.
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146123)
+follows live PR, Discussion, recent-account, main-tree and merged-term checks.
+The cached entry scan reports 341 open PRs and 4,446 Discussion records with
+complete remote text pagination, but only 162 of 6,996 local notes. Sparse
+notes, arbitrary unsearched diffs and unpublished work limit novelty coverage.
+Search absence is not a novelty certificate.
+
+This is a partial formal-register obstruction, not a native supplier or a
+complete multiplication theorem. Physical legality, caller/frame/access costs,
+dirty restoration in an actual implementation, stock, precision/tape,
+compiler and outer admission remain unpriced. Independent human and formal
+proof-kernel review are unclaimed. No Lean, Docker, predecessor scientific
+suite or selected operator replay was run.
+
+## Open next questions
+
+- Can the remaining 24 coordinate-kernel pools realize the eight-call
+  endpoint? Start with the literal representative and retain both cube
+  relations and target coordinate projectors. The support union has size
+  one, so the new rank budget does not decide this branch.
+- Can one changed register mechanism occur in a literal native caller with
+  a favorable complete bill? First specify independent targets, arbitrary
+  dirty inputs and every frame/access/restoration charge. No such caller
+  or physical invoice is supplied here.
+
+## Credit and implementation limits
+
+Credit woklerx/PR1846 for the exceptional scalar catalogue and orbit split;
+unpaidmoon/PR4119 for the relation-support
+reduction and open question; JoyboyBrian/PR5075 for the surviving-branch
+handoff; waynenilsen/PR1882 for the dirty-auxiliary two-target theorem; and
+Ali Romman/PR468 for the formal alphabet and low-span method. The retained
+lineage includes eumemic/PR288 and huxint/PR203. Classical kernel and rank
+arguments are not claimed as new techniques. The new obstruction and its
+48-pool application were produced by Nick Petalas. Apache-2.0.
+
+The code has no recursion, solver, subprocess or network access. Its matrix
+domain is fixed at four binary coordinates; formal words have at most three
+letters and eight monomials. Coordinate budgets stop at nine calls, and the
+largest allocation loop has at most 7^4 candidates. Functions stay below
+60 lines. Power of Ten rule 3 has a managed-runtime deviation: Python exact
+integers, dictionaries and standard iterators allocate dynamically within
+these fixed domains. No fixed-pool memory implementation is claimed.
+Warning-strict normal and optimized replay supplies interpreter diagnostics;
+no unavailable external static analyzer or proof kernel is claimed.

research/flagless-kernel-obstruction/SOURCES.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/auxiliary-span-six-cyclic-line/README.md",
+      "usage": "provenance",
+      "git_blob": "15cb91a38710642fd801b5cb42df705de1ae1790",
+      "sha256": "8be8cb05e213eaf50f29c75e8aa71894a6f836357765fb42a1070178e8543454"
+    },
+    {
+      "path": "research/auxiliary-span-six-flag/README.md",
+      "usage": "provenance",
+      "git_blob": "fcb3305be469805d6f6a15eb2c8ca6676af16730",
+      "sha256": "babb6e44c8ac7640a0cde329b7f6582e72adc2c9307de0d4b5bd2b2510489e1d"
+    },
+    {
+      "path": "research/bit-dirty-auxiliary-registers/README.md",
+      "usage": "provenance",
+      "git_blob": "273bb963ee40869145cf8309db4f8dddebcfe43d",
+      "sha256": "da984fddaa09bfa7b1a3e11505e737283cee36e7972b2081f9de28ec420607cd"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    },
+    {
+      "path": "research/bit-four-role-two-patterns/README.md",
+      "usage": "provenance",
+      "git_blob": "e79087d9cd8f4473e6e48fa4e521902b7809f3a4",
+      "sha256": "e4ee830e783b20bfb0886ae8c91133a6138157ed5dcaac90ce16ddc616c8d49f"
+    }
+  ],
+  "predecessor_references": [
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4119",
+      "head": "ea20dfd71c24072888755e2d03d61278bd25f2db",
+      "credit": "unpaidmoon",
+      "usage": "Exceptional-pool handoff, saturated cube relations and coordinate-call separation; cited premises, no scientific replay."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5075",
+      "head": "c7b3403cf154ccb92286b911055db5d38dfd8bd6",
+      "credit": "JoyboyBrian",
+      "usage": "Explicit surviving flagless-branch handoff; cyclic-line theorem is separate."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1882",
+      "credit": "waynenilsen",
+      "usage": "Two-invertible-target six-call theorem with dirty auxiliaries; cited mathematical premise.",
+      "head": "a9c146e2919c82065e157b3e9bc050f38ac816db"
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/468",
+      "head": "07a78bf335b0b5039a1fecd7cd74a0fe1d1605ea",
+      "credit": "Ali Romman",
+      "usage": "Formal abelian alphabet and low-span reasoning, with retained eumemic and huxint lineage."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1846",
+      "head": "ebd6bf651e1728a94d98c54208f74a529eddb43f",
+      "credit": "woklerx",
+      "usage": "Existing scalar catalogue and 24/48 orbit split. The new contribution excludes eight-call realization of the 48-pool orbit; it does not claim the classification."
+    }
+  ]
+}