[aliromman]

Change and mathematical scope

Scoped combinatorial proof: the high-weight excess cap improves from 15 to the sharp value 11 for simple restored universal length-twelve singleton-prefix walks on F2^5. The proof also excludes every weight-four (8,4) split. This closes Open next question 1 of PR #4907, whose finite checks already measured both facts.

Complete proof, exact receipt, standalone verifier, and source pins.

The new quotient argument forces a repeated minority projection. The cycle then needs at least five neighbor incidences, while a translation partition permits only four. Small difference-support bounds settle the remaining (6,6) and (7,5) cases. Explicit words attain eleven at weights four and five.

This adds one six-file package. It changes no engine, supplier, paid profile or selected frontier. The complete kappa calculation does not improve: selected kappa remains 60403/20000000. The result does not extend to other dimensions or lengths, low-weight functionals, partial prefixes, nonsimple walks, nonuniversal sets or point sets without a cycle.

Task and overlap

Canonical main base: b91956876e5b4122fd89179f1b57557ff8378f15, priority revision 7; unchanged at submission refresh. Task census-pruning-audit, changed scope to the explicit proof handoff in PR #4907. This is a small pruning-model theorem, not a new seven-label exclusion.

The consumed documents are retained at that base: PR #4907's proof and PR #4894's matching-balance proof. Their original PR heads are faf51ea356b9b5d5ce00c141124e4fc3fcefce73 and 2e95d12a8f1557a90102314a773c74420bcbd4fe. No predecessor executable is imported.

Canonical claim. The final refresh covered 333 open PRs and 4,085 Discussion records with complete remote pagination. It searched 65 local records, including the relevant f7 notes, against 6,636 tracked note paths. Omitted notes, arbitrary diffs and unpublished work remain limits; no competing proof was found in that coverage.

Validation

CPython 3.12.13, macOS, standard library only; direct checks also passed on 3.14.7. From the repository root, use Python 3.12 for the registered runner:

python3.12 -B scripts/research_package.py --package research/f7-five-label-sharp-cap
python3.12 -I -O -W error -B research/f7-five-label-sharp-cap/verify.py
python3.12 -B scripts/check_research_commit.py --package research/f7-five-label-sharp-cap

Expected markers: PASS_REGISTERED_RESEARCH_PACKAGE, PASS_F7_FIVE_LABEL_SHARP_CAP, and PASS_RESEARCH_COMMIT_BYTES.

• All 23,816 subsets of sizes five, six and seven in F2^4 check the support lemmas.
• All 127,400 invariant-majority (8,4) set pairs are checked. All 13,664 universal sets fail an independent literal cube-graph Hamiltonian search; it does not use the quotient proof.
• Both sharp witnesses, 12 semantic rejection controls and two typed receipt mutations pass. Eight actual code mutations fail with receipt comparison disabled.
• Normal and optimized registered replay, committed bytes and export integrity pass. The Git-free optimized export passes with an empty PATH and read-only files; all seven exported files stay unchanged. Separate proof and receipt corruptions fail.
• All linked source files match their exact GitHub objects. The optional full-history preflight could not run in this shallow checkout. A direct check confirmed that all four provenance pins resolve at the stated base, which is an ancestor of the publication commit, with matching Git blob IDs and SHA-256 values.

These tests corroborate the written proof. No independent human or proof-kernel acceptance, engine integration, seven-label census, selected cold replay, Lean or Docker run is claimed. Hosted CI was not used as evidence for the local result.

Credit

Mihir Srivastava (@mihir-s-05) supplied PR #4907: the cap-15 proof, quotient setup, measured sharp cap and open question. Nick Petalas (@petalas) supplied PR #4894: matching balance and the four-label proof. Both source notices were checked. The package preserves the earlier attribution to unpaidmoon, Nicholas Stone, James Reed and Ross Richardson, with links to their contributions. Prior measurements and witnesses are not claimed as new.

Prepared for Ali Romman with substantial OpenAI Codex assistance for proof, code, verification and publication. Apache-2.0; predecessor sources remain unchanged.

Open next questions

Can this complete-walk bound support a useful partial-prefix prune? First prove a remaining-edge completion bound that retains every universal completion, then measure it in a maintained engine. Neither that contract nor a runtime gain is supplied here.