[unpaidmoon]

Change and mathematical scope

Scoped written proof with finite corroboration. No new κ. The selected record stays 363005817/100000000000. The inherited gap 28 <= f(8) <= 32 is unchanged. This does not decide whether a universal length-28 word exists.

Fork note: this draft is opened against unpaidmoon's stale main. The branch is one commit on canonical e54523517d0f03e58352e647c403a5af3e525a57. Review git diff e54523517d0f03e58352e647c403a5af3e525a57...762f0ffaf66a8f954bf251c88dc6725e585f9745.

In the restored binary singleton model, a closed length-28 word with multiplicities (4,4,4,4,4,4,2,2) and an 8-step all-ones arc normalizes to the arc 0,1,2,3,4,5,6,7. The two multiplicity-2 sources a < b each turn off once in the complement. If b turns off before a, quadrant (0,1) is empty and the three nonempty body slices are pairwise difference bases of F_2^6. The nine arc prefixes force three flags whose pairwise sums are direct and have size at most 16, so those flags miss the obligation. The complement must add further body states. The same reduction does not apply when a turns off first.

The abstract size budget still admits triples such as (8,8,8), so this is not an exclusion of case II. No supplier, readout schedule, or multiplication theorem is changed.

Task and overlap

Base commit e54523517d0f03e58352e647c403a5af3e525a57. Card connector-alphabet-change, priority revision 8. Scope status: changed. The card asks for one new priced connector operation. The alphabet stays the published singleton alphabet. The result is the turn-off split requested by discussion CrocSwap#1166 comment 19537798, which is item 2 of the handoff-first list for this session.

The concrete object is one normalized 8-step all-ones arc and the 28 label pairs for its two multiplicity-2 sources. Distances 10, 12, and 14, and every length-30 profile, stay outside the argument.

Nearest work:

• Prove an eight-source singleton floor of 28 calls (no new κ) CrocSwap/integer-mult-bounds#5234 supplies 28 <= f(8) <= 32 and the multiplicity shape. Cited, not replayed.
• Prove length-28 double sojourns use at least four sources. CrocSwap/integer-mult-bounds#6966 supplies the rank-at-least-4 filter. Cited, not replayed. The three-pass witnesses show that filter leaves both turn-off orders nonempty for every label pair.
• Record the length-28 flat-step budget forcing a rank-7 arc (no κ) CrocSwap/integer-mult-bounds#7088 is the pending flat-step budget. Its constants are not used.
• Record length-30 sojourn obstructions for eight singleton sources CrocSwap/integer-mult-bounds#6943, Record that rank 3 blocks a universal length-30 singleton word CrocSwap/integer-mult-bounds#7015, and Record that a rank-4 length-30 sojourn needs at least 17 layer-0 points (no κ) CrocSwap/integer-mult-bounds#7093 are length-30 statements.
• Fork branch cursor/length28-allones-placement-09de at 25ce041f09c0924b382b2360b5c470ad598ac978 (draft Record the length-28 all-ones placement split for the two double sources (no κ) #293) counts rank-feasible segment matrices on this same normal form. It does not split turn-off order or prove the flag bound. This package does not recount those matrices.

Validation

CPython 3.12.3, standard library, from the repository root:

python3 -W error -I -B research/length28-allones-case-two/verify.py
python3 -W error -I -O -B research/length28-allones-case-two/verify.py
python3 -B scripts/research_package.py --package research/length28-allones-case-two

Observed marker:

PASS_LENGTH28_ALLONES_CASE_TWO permutations=40320 flags=28 max_forced_sum=16 case_i=28 case_ii=28 min_rank=4 witness_coverage_max=111 gray_distance=16

PASS_REGISTERED_RESEARCH_PACKAGE research/length28-allones-case-two outcome=completed also passed. The package checker is a metadata and replay check, not mathematical acceptance.

The proof is the counting argument in research/length28-allones-case-two/README.md. The verifier exhausts the 40320 relabelings, the 28 flag rows, the 28 positive compositions of 9, and the lexicographically first rank-feasible three-pass witness in each turn-off case. It does not search the remaining complement orderings. The length-32 Gray word is a positive control: one all-ones pair, at circular distance 16, with coverage 256. Deleting a complement step, relabeling that step, a constant word, and one changed Gray label are rejected.

Not run: make frontier7000-verify, Lean, Docker, a solver search, and any replay of f(7) = 24.

Credit

Ross Richardson, CrocSwap#943, for the singleton model and prefix criterion. Douglas Colkitt, CrocSwap#1185, for the length-32 Gray upper construction. conorholds, CrocSwap#3058, for f(7) = 24, cited by CrocSwap#5234 and not replayed. Nick Petalas, CrocSwap#5234, for the length-28 floor, the multiplicity shape, and the handoff. The rank floor is unpaidmoon's merged CrocSwap#6966. The parallel matrix census is unpaidmoon's fork branch cursor/length28-allones-placement-09de.

Prepared by unpaidmoon with substantial Cursor Grok assistance. New work is Apache-2.0. Independent human and proof-kernel review are unclaimed.

Open next questions

Linked from research/length28-allones-case-two/README.md and TASK.json:

1. Can a case-II complement enlarge the three slices until all three pairwise sums equal F_2^6? Smallest step: for labels (6,7), test only walks that meet a feasible size triple. Blocker: an unpruned listing is too large, and a partial search is not an exclusion.
2. Does case I contain a universal word? Smallest step: write the two-sumset union that replaces each cross condition. Blocker: that union is weaker, and no universal length-28 word is known.
3. Do distances 10, 12, and 14 have an analogous split? Smallest step: for distance 10, record that one source appears three times on the short arc and the other seven appear once. Blocker: the permutation normalization stops applying.

Workflow feedback (optional)

The handoff's fixed prefix 0..7 is the right normal form, and separating the two turn-off orders is a smaller proof than another conflict-bounded SAT run. A rank-matrix census of the same interval landed on the fork while this proof was being written; the sumset obligation is the part that census does not contain.