[unpaidmoon]

Change and mathematical scope

On the g=3, d=2 paired-star full-call contract, the next distinct F₂-nullity-7 affine class of two thin maps, after the class settled by PR #7028, has rank(Zg)+rank(Zh) at least 8 over every field of characteristic 2, including F₈ = F₂[x]/(x³+x+1).

The class is resolutions (0, 0, 3), permutation index 8, and gaps 2 and 5. Chronological order, rightmost factor first, is calls 0, 3, 1, 2, 4, 5. It is not the settled class. That class is permutation index 4, calls 1, 2, 0, 3, 4, 5. Permutation index 5 has the same reduced basis as permutation 4, so it is the same affine space and is not a second class. The free support here puts rows {2, 5} on columns {2, 5}, with rows 3 and 4 on separate columns. The column partition of PR #7028 does not describe this support.

The bound is a case analysis of the seven-parameter shape in research/paired-star-f8-perm8-nullity7/PROOF.md: a disjoint column split of Zh, a 4×4 minor of Zg when c₆ = 0, and a four-vector reduction when c₆ = 1. It is attained by two F₂ points, of ranks (4, 4) and (6, 2).

This is a proof for one affine class. It is not an exhaustive census of every F₈ class, and it is not unrestricted nonexistence of a rank-6 or rank-7 two-map word. The F₈ point set of this class is finite, of size 8⁷ = 2,097,152. Both enumerators report minimum 8, exactly two points at 8, and none below. Checksum 3440682239519878741. PR #7028 records checksum 6631801623909619557 for the settled class. The enumeration corroborates the proof on F₈; the proof is what covers every characteristic-2 field for this same shape.

No κ change. The selected frontier stays κ = 781451/250000000.

Task and overlap

Base commit: 17469fff78c22941280f04d39dc5a1faee09c840 (canonical CrocSwap main). This fork PR is based on the pin branch of that commit so the diff is only this package.

Task card: joint-query-controller, scope refined. The card asks whether a changed caller or query demand removes real work. This package answers the next small-nullity F₈ question left by PR #7028, on the same two-map full-call contract.

Nearest overlap:

• PR Exclude the 31-leaf target with a chronological connector rank bound #5747 is the contract and the commuting rank-8 control.
• Upstream PR Record that two F2 thin maps on the three-leaf paired star need total rank 8 #6940 settles two thin maps over F₂.
• Upstream PR Record a partial F4 census of two thin maps on the three-leaf paired star #7006 is the partial F₄ census. It leaves F₈ open.
• Upstream PR Prove one F8 nullity-7 paired-star class has rank sum at least 8. #7028 settles one nullity-7 class, resolutions (0, 0, 3), permutation 4, gaps 2 and 5, and asks for the next small-nullity class. This package takes that class. It does not rerun the settled argument.
• Open Record a partial F4 census of two thin maps on the three-leaf paired star #7006's nullity-32 Schur-complement question is a different field and a different class.
• Merged Record that three full calls miss the paired-star endpoint. #6956 changes the full-call count. Open Record that three F2 thin maps meet total rank 6 on the three-leaf paired star #7011 uses three thin maps over F₂. This package keeps exactly two thin maps and two full calls per stage.

Overlap was checked against open upstream PRs #7005–#7038, discussion #1166, discussion #5593, and fork cursor/* paired-star branches. No open item settles this second nullity-7 class over F₈.

Validation

python3 -B research/paired-star-f8-perm8-nullity7/verify.py

Python 3.12 and gcc, no OpenMP. The command checks the field, the Zh block formula on every F₈ point, the c₆ = 1 row reduction on every tuple of the other six coefficients, the load-bearing constant ones, the diagonal commuting-control identity, and the lex derivation of the shape. It then compiles search.c and requires the two enumerators to agree.

Recorded F₈ census: 2,097,152 points, minimum rank sum 8, exactly two points at 8, none below. Checksum 3440682239519878741. Histogram of sums 0 through 16:

0,0,0,0,0,0,0,0,2,0,1194,3306,42661,192405,414638,545106,897840

Registered package command: PASS_REGISTERED_RESEARCH_PACKAGE research/paired-star-f8-perm8-nullity7 outcome=negative-result.

Evidence class: a scoped proof for one affine space, plus an exhaustive finite census of that space over F₈. The census is not a heuristic search. It does not speak for the classes after permutation 8.

No native caller, Lean proof, Docker replay, or selected-frontier replay was run. The source-history preflight was not required: every provenance pin is on the base commit.

Credit

The contract and the rank floor are PR #5747. The F₂ two-map census is research/paired-star-two-thin-rank (upstream PR #6940). The partial F₄ census is upstream PR #7006. The lex-first nullity-7 class is upstream PR #7028, fork commit b1d471c158d3b71e79464752219f52e1eff2d95d.

Prepared by unpaidmoon with substantial Cursor Grok assistance. Independent human review and a proof-assistant proof are unclaimed.

Open next questions

research/paired-star-f8-perm8-nullity7/README.md and TASK.json.

The smallest useful follow-up is the next distinct nullity-7 class after permutation 8 on this same contract. The row split used here does not transfer. A nullity-8 class has 8⁸ points, so the same direct enumeration does not fit this replay.

Workflow feedback (optional)

PR #7028 named the next small-nullity class as the extension to try, and its column partition does not apply. Keeping the replay on one named word made a different rank split visible.

#1200