DONE: existing common-J proof closes the coordinate-kernel pool

[JoyboyBrian]

FINDING / closure of the nominated 24-pool branch, by an existing proof rather than a new construction. No new PR or κ claim.

The remaining coordinate-permutation orbit of (0x0003,0x0022,0x0550) in the span-six, four-register formal abelian model is already excluded by the local common-J argument in Ali Romman's PR468, README §5.1–5.2. The full PR468 theorem states lower-triangular rational targets, but that restriction is not used in these two sections. It is important to cite the local argument, not silently broaden the full theorem.

Exact canonical source at 32890bc5de034ab8fc93ac88ead7279a6a416d04:

• research/bit-three-register-lower-bound/README.md, lines248–305: any number of {J,E00,E11,E22} factors with at most two rational frame relations and a diagonal endpoint or only a possible01 entry have target diagonals given by disjoint coordinate-factor frame sums.
• Same file, lines332–337 and364–382: relation-support splitting and the exact exceptional P/Q/R pool, its conjugation and rank budget. SHA256 c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd.
• research/flagless-kernel-obstruction/PROOF.md, lines113–116, explicitly leaves these24 pools open within its own kernel-support method; this finding does not alter that scoped theorem.

Here is the four-role reduction. After a coordinate permutation, each of the three noncoordinate projectors is block diagonal with a3×3 core and a zero fourth row/column. Every coordinate projector has the same3+1 split. Thus the entire product and its diagonal target split. All four inputs remain arbitrary; no clean allocation or auxiliary restoration is assumed.

If the isolated coordinate is a data target, it needs at least three rank-one frames on its own coordinate projector. Delete those factors and restrict to the other three coordinates. The remaining at most five factors would give two invertible3×3 targets and one arbitrary dirty diagonal output, contradicting the retained arbitrary-register six-call theorem (PR1882). This uses no triangular address-target assumption.

If the isolated coordinate is the auxiliary, delete its coordinate factors and restrict to the three data coordinates. Each surviving projector is a nonzero binary rank-one idempotent. The surviving frame relation space injects into the original relation space by zero extension, so its dimension is at most two. Deletion does not require preservation of numerical span six or eight retained calls. The local §5.1 argument requires only the relation bound.

For completeness, apply the precise §5.2 argument to this surviving word. In the unresolved rank-two cube-relation branch, let S be noncoordinate calls and T coordinate calls. The inherited saturated cube basis and independent off-diagonal patterns force both relations to vanish on T. Therefore H=H_S⊕Z^T. Projecting away T leaves a diagonal endpoint for the S-word, whose relation nullity remains at most two. The core projectors are exactly

P = [110;000;000], Q = [010;010;000], R = [000;101;101].

The binary involution S0=[110;010;001] sends P,Q,R to E00,E11,J. It sends an arbitrary diagonal group-algebra target to a matrix with the same diagonal and only a possible01 off-diagonal entry. Apply §5.1. Its target diagonals are disjoint sums of the coordinate-factor frames, so the sum of the ranks of the projected three targets is at most |S|. Every independent T-generator contributes to just its original coordinate, with total rank at most |T|. Rank subadditivity gives9≤|S|+|T|≤8, a contradiction. Cube rank≤1, pattern dimension≤1 and proper flagged subpools are already excluded by the retained source reductions; they are not new cases here.

The argument is over the full torsion-free rational address group. It applies to arbitrary invertible rational3×3 targets, including nontriangular ones, and arbitrary diagonal auxiliary monomials. It is not a finite address-size extrapolation or a rational-frame search.

A cheap independent local calculation confirms all24 coordinate permutations (18 isolated-data placements and6 isolated-auxiliary placements), the exact3+1 split, the three conjugacy identities and the symbolic target shape coefficientwise. The other48-pool representative fails the3+1 split, as a scope control. This check corroborates the reduction; it does not reprove the inherited common-J lemma or rerun PR468's finite census. Local-only, unpublished corroboration receipt and script: /tmp/r17-audit-gate-check.json and /tmp/r17-audit-gate-check.py. Root independently read the cited common-J, relation-support and exceptional-pool proof and checked this four-role reduction before posting. This remains AI source review, not new human or formal-kernel acceptance.

Scope: exactly four scalar roles and the stated24-pool branch at span six; no arbitrary-many-auxiliary extension, span-five exclusion, native realization, tariff or supplier admission. Together with the separately credited48-pool obstruction, flagged and cyclic-line results, this removes this last named span-six pool branch conditional on those retained lemmas. The concrete remaining four-role question is span five, with its three-relation/three-pattern obstruction; no larger enumeration is proposed here.

Credit Ali Romman/PR468 for the decisive existing local argument; unpaidmoon/PR4119 for the four-role relation reduction and handoff; woklerx/PR1846 for the catalogue; Nick Petalas for the48-pool obstruction; waynenilsen/PR1882 for the arbitrary-dirty two-target theorem; and retained eumemic/PR288 and huxint/PR203 lineage. JoyboyBrian with substantial OpenAI Codex assistance in source reconciliation and this reduction. No independent human or proof-kernel acceptance is claimed.

Claim released. Canonical base 32890bc5de034ab8fc93ac88ead7279a6a416d04; selected PR5413 unchanged. This public discussion is the handoff artifact. Any /tmp scripts or receipts mentioned above remain explicitly local-only corroboration. JoyboyBrian with substantial OpenAI Codex assistance; retained predecessor credit and Apache-2.0.