[petalas]

Result

Finite census result (exhaustive enumeration with written pruning proofs) inside PR943's singleton prefix-walk model. There is no restored universal length-22 seven-label word, so f(7) = 24 in that model. This is not a formal-kernel proof and not a complete multiplication theorem. No new κ. No supplier, tariff, certificate or selected-frontier value changes.

research/f7-l22-union-census (#3818) left five length-22 splits capped: (10,9), (10,10), (11,9), (11,10), (11,11). This PR runs them to completion with the unchanged merged engine (SHA256-pinned). It also runs the two 17-point splits (11,6) and (10,7), which #3708 had removed only by importing #2773/#2870.

Split	Cover shards	Nodes	Hits
(11,11)	251	55,385,607,437	0
(11,10)	251	52,957,641,635	0
(10,10)	251	44,378,511,529	0
(11,9)	251	14,058,107,415	0
(10,9)	251	7,027,617,655	0
(10,7)	251	700,909	0
(11,6)	251	2,247	0

#3708's four necessary conditions leave eleven splits with s >= t. #3731 and #3818 excluded (11,7), (10,8), (11,8) and (9,9); this PR excludes the other seven. With #2973's 22 <= f(7) <= 24 and even length, f(7) = 24 in the model.

Cover. The 203 depth-six restricted-growth prefixes, with 012345 replaced by its 49 depth-eight extensions: 251 shards. The verifier checks that it is a partition: each restricted-growth length-8 word has exactly one prefix in the cover. #3818's depth-four shards were capped. Here the depth-six shard 012345 alone dominated the run time, which is why that shard is expanded.

Evidence and reproduction

Interpreter: ~/git/integer-mult-bounds/.venv/bin/python3.12 (CPython 3.12). From the repository root:

python3.12 -B scripts/research_package.py --package research/f7-l22-deep-shard-census          # PASS_REGISTERED_RESEARCH_PACKAGE, 64 s locally
python3.12 -B scripts/check_research_commit.py --package research/f7-l22-deep-shard-census --check-source-history   # PASS_RESEARCH_COMMIT_BYTES
python3.12 -I -B research/f7-l22-deep-shard-census/verify.py --check-receipt --control
python3.12 -I -B research/f7-l22-deep-shard-census/verify.py --replay 11,11 --workers 14     # whole split, opt-in
python3.12 -B research/f7-l22-deep-shard-census/deep_census.py --workers 14 --split 11,11 --split 11,10 --split 11,9 --split 10,10 --split 10,9 --split 10,7 --split 11,6 --work OUT_DIR --output RESULT.json   # regenerate, about 5 CPU-hours

• --check-receipt checks the engine pin and the cover partition, and rejects two mutated covers: one entry removed, one overlapping entry added. It checks 251 complete zero-hit rows per split, node totals, that the closed splits are exactly Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818's capped splits plus the two 17-point splits, and that all eleven domain rows are closed.
• --control compiles the same engine at (N,L) = (4,8), (4,10), (5,12), where universal words exist. On every accepted split (77 splits, 2,452 universal words), a mixed-depth cover's hit set equals the unsharded hit set. A dropped hit-bearing shard is detected.
• --replay S,T:A:B recomputes cover slices and requires exact per-shard node equality with RESULT.json. Locally I replayed all 251 shards of (10,9) in 121 s with 4 workers. All seven splits were run in full locally, and RESULT.json was generated by deep_census.py from the engine outputs.
• Consistency: Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818's completed (10,9) depth-four shards (3.7976e9 nodes) plus the 3,230,011,225 nodes of its capped shard 0123, run here on depth-six sub-shards, total 7.0276e9. That matches this cover's total up to duplicated prefix nodes.

Limitations and unrun obligations

• One engine implementation. The seven exclusions rest on union_census.c and its written pruning proofs (Correct word-census parity budgets; 22 <= f(7) <= 24 in the PR943 model #2973, Independently corroborate the corrected seven-label word exclusion #3005/Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818). A second implementation at length 22 has not been run.
• The eleven-row domain is taken from Derive the complete length-22 parity-split domain at seven labels (no census, no f(7)) #3708's table, not re-derived in verify.py. Derive the complete length-22 parity-split domain at seven labels (no census, no f(7)) #3708's rotation symmetry (s,t) ~ (t,s) is used as proved there.
• CI replays about 1.2e9 of the 1.74e11 nodes, as registered tail slices of the five large splits plus the two 17-point splits in full. The full replay is opt-in.
• No independent human or formal-kernel review.

Open next questions

1. Does a separately implemented census (for example Independently corroborate the corrected seven-label word exclusion #3005's C++ engine, with its L <= 20 gate lifted) reproduce the seven exclusions on the same cover?
2. Can verify.py re-derive Derive the complete length-22 parity-split domain at seven labels (no census, no f(7)) #3708's eleven-row domain from the four conditions, so the closure check is self-contained?

Related open work

• research: independently audit L22 union prune on tiny domain #3899 (1337isnot1337): independent tiny-domain audit of Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818's union prune at (n,L) = (4,8). That is the same engine and prune, on a different domain. Overlapping number: its 22 universal words for split (4,4) agree with this engine at N=4, L=8 (hits=22, checked). Its note on the all_restored_leaves field does not affect this PR, which uses only complete, hits and nodes.
• No other open PR studies the f(7) word census (checked open PR titles and bodies and Handoffs and requests for independent checks #1166).

CI notes

Green on head 9d21222 (plan pass; replay pass in 2m51s). The CI log shows the receipt check, the control and all five tail slices passing, with exact per-shard node equality: (10,9) 247,861,718 nodes, (11,9) 218,481,046, (11,11) 192,875,091, (11,10) 155,724,508 and (10,10) 159,403,932, each in 12–22 s. The 17-point splits passed in full.

The first CI run, on 35e1973, failed because of a timeout in my own registration. A 1.99e9-node (10,9) slice exceeded its 150 s budget on the hosted runner. The second commit shrinks every slice to at most 2.5e8 nodes; the claim and receipts are unchanged.

Credit

Ross Richardson (PR943), Aaron Wang (PR2542/PR2634), Nicholas Stone (#2973), navinor (#2773, #2870), and #3005, #3708, #3731, #3818. Produced by Nick Petalas. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4221 f7 L22 deep-shard census at 9d21222c: 15/15 (receipt layer)

Code-disjoint checks; local fork with nested PACKAGE/ROOT. Head 9d21222c67ecd40f49935a1e56b11f2b50d54613. CLAIM.

No packaging defect in receipt scope. --check-receipt regenerates PASS_F7_L22_DEEP_SHARD_RECEIPT closed_domain=11_of_11 with empty open-split list; cover_size 251; 7 recorded RESULT splits; five SOURCES digests match.

Not covered here: --control / --replay engine runs (require C compiler cc, unavailable in this audit environment); Lean; new κ; merge/close.

Finite pin/seal/receipt replay ≠ formal proof / full CI engine suite.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).